[tautschnig]

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().

This PR is based on the branch of #43; until #43 is merged, its base is that branch.

[Copilot]

🟡 Changes recommended

Critical issues allow lazy initialization and concurrent registration to return distinct Class objects for the same name, while concurrent updates can also lose registrations.

2 open issues

• Concurrent class registration returns duplicate Class objects · New
• forName returns noncanonical Class objects before lazy registration · New

What changed in this PR

Restores a working Class.forName model so verification can continue through dependent calls, with a shared registry intended to preserve Class identity.

Changes:

• Replaces the unused fixed-size arrays with a linked registry backed by a final array.
• Registers class literals and reuses registered objects in forName.
• Adds null-name rejection and documents unsupported initialization and class-existence checks.

File	Description
src/​main/​java/​java/​lang/​Class.java	Implements the Class registry, restores forName, and registers class literals.

_{Review effort: Balanced}