Model Class.forName with unique Class objects

src/main/java/java/lang/Class.java

@@ -120,12 +120,18 @@ private static Class<?> cproverClassWithName(String className) {
     private boolean cproverIsMemberClass;
     private boolean cproverIsEnum;
 
-    // TODO: these fields are to enforce singleton semantics of
-    // Class objects as returned by Object.getClass() and Class.forName()
-    // The size is currently hard-coded which may lead to incorrect results.
-    // A map could be used here in future.
-    private static String[] cproverClassNames = new String[8];
-    private static Class<?>[] cproverClassInstances = new Class<?>[8];
+    // DIFFBLUE MODEL LIBRARY
+    // The JVM creates exactly one Class object per class, so that, e.g.,
+    // a.getClass() == b.getClass() holds if and only if a and b have the same
+    // runtime type, and a.getClass() == A.class if and only if a has type A.
+    // We keep all Class objects created so far in a linked list: the class
+    // literals, which JBMC creates and initialises via
+    // cproverInitializeClassLiteral, and the ones that forName (and thus
+    // getClass) creates for classes that do not have a class literal.
+    // The head of the list is stored in a final array so that --nondet-static
+    // does not replace it with a nondeterministic value.
+    private static final Class<?>[] cproverClasses = new Class<?>[1];
+    private Class<?> cproverNextClass;
 
     public String toString() {
         return (isInterface() ? "interface " : (isPrimitive() ? "" : "class "))
@@ -179,29 +185,34 @@ public String toGenericString() {
         }
     }
 
-    // TODO: This is a very partial model of the actual behaviour of the Java
-    // forName method. The goal is to correctly model combinations of forName
-    // and getName, but precisely following the JDK behaviour is more involved.
+    /**
+     * @diffblue.limitedSupport
+     * Returns the unique Class object for the given class name, creating it if
+     * necessary. Unlike the JVM, this does not run the static initializer of
+     * the class, and does not throw ClassNotFoundException for names of classes
+     * that do not exist.
+     */
     public static Class<?> forName(String className) {
-        CProver.notModelled();
-        throw new AssertionError();
-        /*
-        String foundName = null;
-        for (int i = 0; i < cproverClassNames.length; ++i) {
-            String currentName = cproverClassNames[i];
-            if (currentName == null) {
-                Class<?> c = new Class();
-                c.name = className;
-                cproverClassNames[i] = className;
-                cproverClassInstances[i] = c;
+        // DIFFBLUE MODEL LIBRARY
+        if (className == null) {
+            throw new NullPointerException();
+        }
+        for (Class<?> c = cproverClasses[0]; c != null; c = c.cproverNextClass) {
+            if (className.equals(c.name)) {
                 return c;
             }
-            if (className.equals(currentName)) {
-                return cproverClassInstances[i];
-            }
         }
-        return CProver.nondetWithoutNullForNotModelled();
-        */
+        Class<?> c = new Class();
+        c.name = className;
+        c.cproverRegister();
+        return c;
+    }
+
+    // DIFFBLUE MODEL LIBRARY
+    // Add this Class object to the list of all Class objects.
+    private void cproverRegister() {
+        cproverNextClass = cproverClasses[0];
+        cproverClasses[0] = this;
     }
 
     public static Class<?> forName(String name, boolean initialize,
@@ -567,6 +578,7 @@ public void cproverInitializeClassLiteral(
         this.cproverIsLocalClass = isLocalClass;
         this.cproverIsMemberClass = isMemberClass;
         this.cproverIsEnum = isEnum;
+        cproverRegister();
     }
 
     /**