JBMC: make Object.getClass return the unique Class object of each class

jbmc/regression/jbmc/class-literals-static-state/pom.xml

@@ -0,0 +1,37 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.class-literals-static-state</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <dependencies>
+        <dependency>
+            <groupId>org.cprover.util</groupId>
+            <artifactId>cprover-api</artifactId>
+        </dependency>
+    </dependencies>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>

jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java

@@ -0,0 +1,13 @@
+public class Test {
+  static class A {}
+
+  static class B {}
+
+  public static void main() {
+    Class<?> a = A.class;
+    Class<?> b = B.class;
+    assert a != b;
+    // at least the class literals of A and B have been initialised
+    assert org.cprover.regression.ClassLiteralCounter.count[0] >= 2;
+  }
+}

jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java

@@ -0,0 +1,25 @@
+package java.lang;
+
+public class Class<T> {
+
+  private String name;
+
+  @org.cprover.MustNotThrow
+  public void cproverInitializeClassLiteral(
+    String name,
+    boolean isAnnotation,
+    boolean isArray,
+    boolean isInterface,
+    boolean isSynthetic,
+    boolean isLocalClass,
+    boolean isMemberClass,
+    boolean isEnum) {
+    this.name = name;
+    // a static field of another class, which must not be reset afterwards
+    org.cprover.regression.ClassLiteralCounter.count[0]++;
+  }
+
+  public String getName() { return name; }
+
+  public boolean desiredAssertionStatus() { return true; }
+}

jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java

@@ -0,0 +1,6 @@
+package org.cprover.regression;
+
+public class ClassLiteralCounter {
+  // Number of class literals that have been initialised
+  public static final int[] count = new int[1];
+}

jbmc/regression/jbmc/class-literals-static-state/test.desc

@@ -0,0 +1,14 @@
+CORE
+Test
+--function Test.main -cp target/classes
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+JBMC initialises class literals by calling cproverInitializeClassLiteral of the
+model of java.lang.Class. Its effects on static fields must persist: class
+literals must thus only be initialised once all other static symbols
+(including the static fields of java.lang.Class and the flag recording whether
+its static initializer has run) have been initialised.

jbmc/regression/jbmc/get-class-for-name/classLiteral.desc

@@ -0,0 +1,14 @@
+CORE
+Test
+--function Test.classLiteral -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Object.getClass must return the same java.lang.Class object as
+Class.forName, also for classes whose class literal the program does not
+refer to, irrespective of which of the two is called first. JBMC obtains the
+Class object of such a class from cproverGetClassObject of the model of
+java.lang.Class on the first call of getClass for that class.

jbmc/regression/jbmc/get-class-for-name/enumFlag.desc

@@ -0,0 +1,14 @@
+CORE
+Test
+--function Test.enumFlag -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Object.getClass must return the same java.lang.Class object as
+Class.forName, also for classes whose class literal the program does not
+refer to, irrespective of which of the two is called first. JBMC obtains the
+Class object of such a class from cproverGetClassObject of the model of
+java.lang.Class on the first call of getClass for that class.

jbmc/regression/jbmc/get-class-for-name/firstCallOnBranch.desc

@@ -0,0 +1,14 @@
+CORE
+Test
+--function Test.firstCallOnBranch -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Object.getClass must return the same java.lang.Class object as
+Class.forName, also for classes whose class literal the program does not
+refer to, irrespective of which of the two is called first. JBMC obtains the
+Class object of such a class from cproverGetClassObject of the model of
+java.lang.Class on the first call of getClass for that class.

jbmc/regression/jbmc/get-class-for-name/forNameThenGetClass.desc

@@ -0,0 +1,14 @@
+CORE
+Test
+--function Test.forNameThenGetClass -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Object.getClass must return the same java.lang.Class object as
+Class.forName, also for classes whose class literal the program does not
+refer to, irrespective of which of the two is called first. JBMC obtains the
+Class object of such a class from cproverGetClassObject of the model of
+java.lang.Class on the first call of getClass for that class.

jbmc/regression/jbmc/get-class-for-name/getClassThenForName.desc

@@ -0,0 +1,14 @@
+CORE
+Test
+--function Test.getClassThenForName -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Object.getClass must return the same java.lang.Class object as
+Class.forName, also for classes whose class literal the program does not
+refer to, irrespective of which of the two is called first. JBMC obtains the
+Class object of such a class from cproverGetClassObject of the model of
+java.lang.Class on the first call of getClass for that class.

jbmc/regression/jbmc/get-class-for-name/mustFail.desc

@@ -0,0 +1,11 @@
+CORE
+Test
+--function Test.mustFail -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=10$
+^SIGNAL=0$
+^\[java::Test\.mustFail:\(\)V\.assertion\.1\] line 54 .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The Class objects of different classes must be distinct.

jbmc/regression/jbmc/get-class-for-name/objectReceiver.desc

@@ -0,0 +1,12 @@
+CORE
+Test
+--function Test.objectReceiver -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Objects whose runtime type is java.lang.Object use the model of
+Object.getClass, which calls Class.forName; their Class object must be the
+class literal of java.lang.Object, and differ from those of other classes.

jbmc/regression/jbmc/get-class-for-name/pom.xml

@@ -0,0 +1,37 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.get-class-for-name</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <dependencies>
+        <dependency>
+            <groupId>org.cprover.util</groupId>
+            <artifactId>cprover-api</artifactId>
+        </dependency>
+    </dependencies>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>

jbmc/regression/jbmc/get-class-for-name/src/main/java/Test.java

@@ -0,0 +1,56 @@
+public class Test {
+  static class A {}
+  static class B {}
+  static class C {}
+  enum E { X }
+
+  public static void forNameThenGetClass() {
+    Class<?> c = Class.forName("Test$A");
+    assert new A().getClass() == c;
+    assert Class.forName("Test$A") == c;
+  }
+
+  public static void getClassThenForName() {
+    Class<?> c = new A().getClass();
+    assert Class.forName("Test$A") == c;
+  }
+
+  public static void classLiteral() {
+    assert Class.forName("Test$C") == C.class;
+    assert new C().getClass() == C.class;
+  }
+
+  public static void twoClasses() {
+    Class<?> a = Class.forName("Test$A");
+    Class<?> b = Class.forName("Test$B");
+    assert new B().getClass() == b;
+    assert new A().getClass() == a;
+    assert a != b;
+  }
+
+  public static void firstCallOnBranch(boolean nondet) {
+    if (nondet)
+      new A().getClass();
+    Class<?> c = new A().getClass();
+    assert Class.forName("Test$A") == c;
+  }
+
+  public static void enumFlag() {
+    Class<?> c = Class.forName("Test$E");
+    assert E.X.getClass() == c;
+    assert c.isEnum();
+  }
+
+  public static void objectReceiver() {
+    Object o = new Object();
+    assert o.getClass() == Object.class;
+    assert new Object().getClass() == o.getClass();
+    Object a = new A();
+    assert a.getClass() != o.getClass();
+  }
+
+  public static void mustFail() {
+    Class<?> c = Class.forName("Test$A");
+    assert new B().getClass() == c;
+  }
+}

jbmc/regression/jbmc/get-class-for-name/src/main/java/java/lang/Class.java

@@ -0,0 +1,74 @@
+package java.lang;
+
+// A minimal model of java.lang.Class with unique Class objects per name, which
+// provides cproverGetClassObject for JBMC's implementation of getClass.
+public class Class<T> {
+  private String name;
+  private boolean cproverIsEnum;
+  private Class<?> cproverNextClass;
+
+  // Class literals that JBMC initialises in __CPROVER_initialize
+  private static final Class<?>[] literals = new Class<?>[1];
+  // Class objects created by forName or cproverGetClassObject
+  private static final Class<?>[] others = new Class<?>[1];
+
+  public String getName() { return name; }
+  public boolean isEnum() { return cproverIsEnum; }
+  public boolean desiredAssertionStatus() { return true; }
+
+  private static Class<?> findOther(String name) {
+    for (Class<?> c = others[0]; c != null; c = c.cproverNextClass)
+      if (name.equals(c.name))
+        return c;
+    return null;
+  }
+
+  private static Class<?> newOther(String name) {
+    Class<?> c = new Class<>();
+    c.name = name;
+    c.cproverNextClass = others[0];
+    others[0] = c;
+    return c;
+  }
+
+  public static Class<?> forName(String name) {
+    for (Class<?> c = literals[0]; c != null; c = c.cproverNextClass)
+      if (name.equals(c.name))
+        return c;
+    Class<?> c = findOther(name);
+    return c != null ? c : newOther(name);
+  }
+
+  @org.cprover.MustNotThrow
+  public void cproverInitializeClassLiteral(
+    String name,
+    boolean isAnnotation,
+    boolean isArray,
+    boolean isInterface,
+    boolean isSynthetic,
+    boolean isLocalClass,
+    boolean isMemberClass,
+    boolean isEnum) {
+    this.name = name;
+    this.cproverIsEnum = isEnum;
+    cproverNextClass = literals[0];
+    literals[0] = this;
+  }
+
+  @org.cprover.MustNotThrow
+  private static Class<?> cproverGetClassObject(
+    String name,
+    boolean isAnnotation,
+    boolean isArray,
+    boolean isInterface,
+    boolean isSynthetic,
+    boolean isLocalClass,
+    boolean isMemberClass,
+    boolean isEnum) {
+    Class<?> c = findOther(name);
+    if (c == null)
+      c = newOther(name);
+    c.cproverIsEnum = isEnum;
+    return c;
+  }
+}

jbmc/regression/jbmc/get-class-for-name/threading.desc

@@ -0,0 +1,11 @@
+CORE
+Test
+--function Test.forNameThenGetClass --java-threading -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+With --java-threading, getClass obtains the Class object using the same
+protocol as the thread-safe static initializer wrappers.

jbmc/regression/jbmc/get-class-for-name/twoClasses.desc

@@ -0,0 +1,14 @@
+CORE
+Test
+--function Test.twoClasses -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Object.getClass must return the same java.lang.Class object as
+Class.forName, also for classes whose class literal the program does not
+refer to, irrespective of which of the two is called first. JBMC obtains the
+Class object of such a class from cproverGetClassObject of the model of
+java.lang.Class on the first call of getClass for that class.