From 945cb84253dae4a9d35c2bdbf575e51f8d5b1c94 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Nov 2026 21:18:28 +0000 Subject: [PATCH] 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 getPrimitiveClass and getSuperclass no longer call forName. 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 --- src/main/java/java/lang/Class.java | 62 ++++++++++++++++++------------ 1 file changed, 37 insertions(+), 25 deletions(-) diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index eec4b6f..a120175 100644 --- a/src/main/java/java/lang/Class.java +++ b/src/main/java/java/lang/Class.java @@ -115,12 +115,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 ")) @@ -174,29 +180,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, @@ -562,6 +573,7 @@ public void cproverInitializeClassLiteral( this.cproverIsLocalClass = isLocalClass; this.cproverIsMemberClass = isMemberClass; this.cproverIsEnum = isEnum; + cproverRegister(); } /**