From 485f4497cd4e2821b67200f4fc776a1a3925f2b9 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 that JBMC reports a failing assertion in forName for every call of getClass(), and does not check any assertion after such a call, e.g., after a call of Object.toString(), Enum.compareTo, or an equals() method that compares getClass() results. 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 two linked lists instead, whose heads are stored in final arrays so that --nondet-static leaves them alone: cproverInitializeClassLiteral, which JBMC calls to initialise each class literal, adds the literal to the first list, and forName adds a new Class object to the second list only if none with that name exists in either list 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. For classes whose class literal the program does not refer to, JBMC (with diffblue/cbmc#9390) does not create a class literal, but calls the new method cproverGetClassObject on the first call of getClass() for the class. It returns the Class object that forName created for the class, if any, so that Class.forName("Foo") == new Foo().getClass() holds also if forName is called first, and a new one in the second list otherwise. Objects are only ever added at the head of a list, and only once: as symbolic execution generally does not resolve the name comparisons, moving objects between lists or adding an object to a list a second time would make JBMC consider cyclic lists, so that it could not bound the loops over them. There are no locks: JBMC's model of monitors requires the monitor count to be zero, and atomic sections cannot be used either, as JBMC's static initialization code uses atomic sections, which cannot be nested. 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 | 133 +++++++++++++++++++++++------ 1 file changed, 109 insertions(+), 24 deletions(-) diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index eec4b6f..7b072ae 100644 --- a/src/main/java/java/lang/Class.java +++ b/src/main/java/java/lang/Class.java @@ -115,12 +115,30 @@ 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 two linked lists: + // - cproverClassLiterals: the class literals, which JBMC initialises via + // cproverInitializeClassLiteral; + // - cproverOtherClasses: the Class objects that forName creates for names + // that are not in cproverClassLiterals, and those that + // cproverGetClassObject creates. + // JBMC only creates class literals of classes that the program refers to + // by a class literal. For other classes, getClass calls + // cproverGetClassObject on its first call for that class, which returns + // the Class object that forName created for the class, if any. + // Objects are only ever added at the head of a list, and each object only + // once: the name comparisons are generally not resolved during symbolic + // execution, and adding an object that may already be in a list would let + // JBMC consider cyclic lists, so that it could not bound the loops over + // the lists. + // The heads of the lists are stored in final arrays so that + // --nondet-static does not replace them with nondeterministic values. + private static final Class[] cproverClassLiterals = new Class[1]; + private static final Class[] cproverOtherClasses = new Class[1]; + private Class cproverNextClass; public String toString() { return (isInterface() ? "interface " : (isPrimitive() ? "" : "class ")) @@ -174,29 +192,51 @@ 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 = cproverClassLiterals[0]; c != null; + c = c.cproverNextClass) { + if (className.equals(c.name)) { return c; } - if (className.equals(currentName)) { - return cproverClassInstances[i]; + } + Class c = cproverFindOtherClass(className); + if (c == null) { + c = cproverNewOtherClass(); + c.name = className; + } + return c; + } + + // DIFFBLUE MODEL LIBRARY + // Find the Class object with the given name in cproverOtherClasses. + private static Class cproverFindOtherClass(String className) { + for (Class c = cproverOtherClasses[0]; c != null; + c = c.cproverNextClass) { + if (className.equals(c.name)) { + return c; } } - return CProver.nondetWithoutNullForNotModelled(); - */ + return null; + } + + // DIFFBLUE MODEL LIBRARY + // Create a Class object and add it to cproverOtherClasses. + private static Class cproverNewOtherClass() { + Class c = new Class(); + c.cproverNextClass = cproverOtherClasses[0]; + cproverOtherClasses[0] = c; + return c; } public static Class forName(String name, boolean initialize, @@ -554,6 +594,51 @@ public void cproverInitializeClassLiteral( boolean isLocalClass, boolean isMemberClass, boolean isEnum) { + cproverSetClassInfo( + name, isAnnotation, isArray, isInterface, isSynthetic, + isLocalClass, isMemberClass, isEnum); + cproverNextClass = cproverClassLiterals[0]; + cproverClassLiterals[0] = this; + } + + // DIFFBLUE MODEL LIBRARY + // JBMC calls this method on the first call of getClass on an object of a + // class whose class literal the program does not refer to, and returns + // the result from all calls of getClass for objects of that class. It + // takes the same arguments as cproverInitializeClassLiteral. To ensure + // that there is only one Class object for each class, this returns the + // object that forName created for the class, if any. + @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 = cproverFindOtherClass(name); + if (c == null) { + c = cproverNewOtherClass(); + } + c.cproverSetClassInfo( + name, isAnnotation, isArray, isInterface, isSynthetic, + isLocalClass, isMemberClass, isEnum); + return c; + } + + // DIFFBLUE MODEL LIBRARY + @org.cprover.MustNotThrow + private void cproverSetClassInfo( + String name, + boolean isAnnotation, + boolean isArray, + boolean isInterface, + boolean isSynthetic, + boolean isLocalClass, + boolean isMemberClass, + boolean isEnum) { this.name = name; this.cproverIsAnnotation = isAnnotation; this.cproverIsArray = isArray;