Model Class.forName with unique Class objects

Commit 75beb6b made Class.forName call CProver.notModelled(), as it does
not run static initializers. Object.getClass() is implemented as
Class.forName(CProver.classIdentifier(this)), so every path through
getClass() was cut off: for example, assertions after a call to
Object.toString(), Enum.compareTo, or an equals() method that compares
getClass() results were reported as SUCCESS without being checked.

The model before that commit, which kept Class objects in two static
arrays of size 8, had problems as well:
- With more than 8 classes, forName returned a nondeterministic object.
- Class literals (Foo.class) were not in the arrays, so
  Class.forName("Foo") == Foo.class was false.
- With JBMC's --nondet-static, the non-final static arrays are
  initialised nondeterministically, which made the search for a class
  name compare it with nondeterministic strings: JBMC's nondet-static
  regression test did not terminate within 15 minutes with that model,
  and finishes within a second when the arrays are final.

Keep all Class objects in a linked list instead, whose head is stored in
a final array so that --nondet-static leaves it alone.
cproverInitializeClassLiteral, which JBMC calls to initialise each class
literal, adds the literal to the list, and forName adds a new Class
object only if none with that name exists yet. Thus there is one Class
object per class name, as in the JVM. forName now throws
NullPointerException for a null name, as the JVM does. It still does
not run static initializers, and does not throw ClassNotFoundException
for names of classes that do not exist; its documentation now says so.

Each lookup compares the name with those of all Class objects created
so far using String.equals, which is expensive for JBMC's string solver
when there are many of them: a program that calls getClass() on objects
of 10 different classes took 81 seconds. JBMC therefore implements
getClass() for all classes except java.lang.Object itself without going
through forName (diffblue/cbmc#9390), so that this lookup is only used
for explicit calls of Class.forName and for getClass() on objects of
type java.lang.Object. For class literals to be added to the list, JBMC
must initialise class literals after the static fields of
java.lang.Class, which diffblue/cbmc#9390 also does; with older versions
of JBMC, Class.forName("Foo") == Foo.class remains false.

This builds on #43, which makes the models' internal uses of forName
(getPrimitiveClass, getSuperclass) use a separate factory instead.

With these models (and #49 for building with JDK 25), 3 of JBMC's
regression tests fail, compared with 113 with the current master branch:
two depend on the numbering of dynamic objects in traces, and one fails
JBMC's trace validation also without this change. This holds both with
and without diffblue/cbmc#9390. With #43 and #49, but without this
change, 3 tests fail as well, but two of them because getClass() on an
object of type java.lang.Object reaches CProver.notModelled().

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

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();
     }
 
     /**