Java class literals: init using a library hook when possible

The Java library definition of java.lang.Class, when nondet initialized, can be quite time
consuming due to the enumeration constant dictionary's internal array. Instead, let's give
the library a chance to set Class constants (literals like MyClass.class) itself.

While we're at it we might as well gain the ability to prove some properties of the literals.
We currently supply those class attributes that are easy to come by in the parse tree; with a
little more effort in the parser IsLocalClass and IsMemberClass could be determined.

Author: smowton

jbmc/regression/jbmc/class-literals/ExampleAnnotation.class

@@ -0,0 +1,4 @@
+
+public @interface ExampleAnnotation {
+
+}

jbmc/regression/jbmc/class-literals/ExampleAnnotation.java

@@ -0,0 +1,4 @@
+public enum ExampleEnum {
+
+}
+

jbmc/regression/jbmc/class-literals/ExampleEnum.class

@@ -0,0 +1,4 @@
+
+interface ExampleInterface {
+
+}

jbmc/regression/jbmc/class-literals/ExampleEnum.java

@@ -0,0 +1,25 @@
+
+public class Test {
+
+  public static void main() {
+
+    assert ExampleAnnotation.class.isAnnotation();
+    assert int[].class.isArray();
+    assert ExampleInterface.class.isInterface();
+    assert ExampleEnum.class.isEnum();
+
+    // Note use of '==' not '.equals', as we expect the same exact literal,
+    // which in jbmc always have the same address.
+    // Note int[].class.getName() is not tested yet, as arrays' types are
+    // printed as their raw signature, to be addressed separately.
+    // Note also primitive types (e.g. int.class) are not addresses here, as
+    // they are created through box types' static initializers (e.g. Integer
+    // has a static member TYPE that holds the Class for `int.class`)
+
+    assert ExampleAnnotation.class.getName() == "ExampleAnnotation";
+    assert ExampleInterface.class.getName() == "ExampleInterface";
+    assert ExampleEnum.class.getName() == "ExampleEnum";
+
+  }
+
+}

jbmc/regression/jbmc/class-literals/ExampleInterface.class

@@ -0,0 +1,45 @@
+package java.lang;
+
+public class Class {
+
+  private String name;
+
+  private boolean isAnnotation;
+  private boolean isArray;
+  private boolean isInterface;
+  private boolean isSynthetic;
+  private boolean isLocalClass;
+  private boolean isMemberClass;
+  private boolean isEnum;
+
+  public void cproverInitializeClassLiteral(
+    String name,
+    boolean isAnnotation,
+    boolean isArray,
+    boolean isInterface,
+    boolean isSynthetic,
+    boolean isLocalClass,
+    boolean isMemberClass,
+    boolean isEnum) {
+
+    this.name = name;
+    this.isAnnotation = isAnnotation;
+    this.isArray = isArray;
+    this.isInterface = isInterface;
+    this.isSynthetic = isSynthetic;
+    this.isLocalClass = isLocalClass;
+    this.isMemberClass = isMemberClass;
+    this.isEnum = isEnum;
+
+  }
+
+  public String getName() { return name; }
+
+  public boolean isAnnotation() { return isAnnotation; }
+  public boolean isArray() { return isArray; }
+  public boolean isInterface() { return isInterface; }
+  public boolean isSynthetic() { return isSynthetic; }
+  public boolean isLocalClass() { return isLocalClass; }
+  public boolean isMemberClass() { return isMemberClass; }
+  public boolean isEnum() { return isEnum; }
+}