JBMC: make Object.getClass return the unique Class object of each class by tautschnig · Pull Request #9390 · diffblue/cbmc

tautschnig · 2026-11-03T20:54:10Z

In the JVM, each class has exactly one java.lang.Class object: 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. Code relies on this, e.g., in equals methods and in Enum.compareTo. With the models library's Object.getClass (Class.forName(CProver.classIdentifier(this))), neither holds with the version of the models library that CBMC currently uses, and on the models library's master branch Class.forName is CProver.notModelled(), which cuts off all paths through getClass().

This PR implements getClass in JBMC:

For each class C that can have instances, a synthetic C.getClass() overrides Object.getClass and returns &C@class_model. Virtual method dispatch selects the override of the runtime type, which symbolic execution resolves without involving the string solver.
This is compatible with both kinds of lazy loading: only the method symbols are created up front. Context-insensitive lazy loading converts the overrides of instantiated classes only, symex-driven lazy loading converts the ones symbolic execution reaches.
Class literals are created up front, as they must exist before __CPROVER_initialize is generated. Those that the program does not refer to are initialised on the first call of the corresponding getClass override rather than in __CPROVER_initialize, which would otherwise make every program larger under symex-driven lazy loading (trivial program: 37348 steps before, 53079 if initialised eagerly, 37540 with this PR).
The first commit makes JBMC initialise class literals after all other static symbols, so that static state that cproverInitializeClassLiteral sets up (as a Class.forName model with unique Class objects needs to) is not reset afterwards.
The third commit lets the models library provide the Class object of a class whose class literal the program does not refer to, via a new Class.cproverGetClassObject (Model Class.forName with unique Class objects java-models-library#50). That model returns the object that Class.forName created for the class, if any, so that Class.forName("Foo") == new Foo().getClass() also holds when forName is called first. With models that lack this method, the class literal is initialised as before; with models that have neither this method nor cproverInitializeClassLiteral, __CPROVER_initialize initialises the class literal as on develop. New test: jbmc/get-class-for-name, which uses its own model of java.lang.Class.
The fourth commit binds invokespecial calls of getClass dynamically. Object.getClass is final, so super.getClass() returns the runtime type's Class object; compilers other than javac may emit invokespecial A.getClass, which would otherwise reach A's override. New test: jbmc/get-class-invokespecial (Jasmin), which fails without this commit.
The fifth commit makes the lazy initialisation thread-safe with --java-threading, using the protocol of the thread-safe static initializer wrappers. New test: get-class-for-name/threading.desc.

Objects whose runtime type is java.lang.Object keep using the models library's Object.getClass, which calls Class.forName; with diffblue/java-models-library#50 that returns Object.class (test: get-class-for-name/objectReceiver.desc). Arrays are not covered: JBMC represents all reference arrays by one type (String[].class and Object[].class are the same class literal), so their Class objects cannot be made unique per JVM class without changing JBMC's array representation.

Alternatives I measured before settling on this: a lookup by name in the models library (a list of Class objects compared via String.equals) took 81 s for a program calling getClass on objects of 10 classes, and did not finish within 7 minutes for 20 classes; an if-then-else chain over all classes in JBMC scales linearly but makes every program that calls getClass initialise the class literals of all ~130 loaded classes. With this PR the same benchmark takes 0.33 s for 10 classes and 1.3 s for 40.

All JBMC regression tests (CORE, both lazy-loading modes, java-unit) pass with the models library version used by develop; the sum of per-test times was 1003 s and 1027 s in two runs, against 1003 s on develop. The new tests jbmc/get-class (5 cases), jbmc/get-class-for-name (9 cases), jbmc/get-class-invokespecial and jbmc/class-literals-static-state pass with and without --symex-driven-lazy-loading; with develop, get-class, class-literals-static-state and 2 of the get-class-for-name cases fail. The related models-library change (a Class.forName model that returns unique Class objects, replacing CProver.notModelled()) will be proposed in diffblue/java-models-library separately.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

java_static_lifetime_init initialises static symbols in alphabetical order. For a class literal (Foo@class_model) it emits a call to java.lang.Class.cproverInitializeClassLiteral of the models library. That method may access static fields, which runs static initializers. Static fields, and the flags that record whether a static initializer has run, are zero-initialised in the same alphabetical pass. Thus, for example, java::Test$A@class_model was initialised before java::java.lang.Class's static fields and its clinit_already_run flag: the effects of the class literal's initialisation on static state were undone, and the static initializer of java.lang.Class ran again later. Initialise class literals only once all other static symbols (and any symbols that their initialisation creates) have been initialised. With the current models library nothing changes: its cproverInitializeClassLiteral does not access static fields, and all JBMC regression tests pass. A model of Class.forName that keeps the unique Class object of each class in a static data structure, including the class literals, requires this change. The new regression test uses its own model of java.lang.Class, whose cproverInitializeClassLiteral counts the initialised class literals in a static field of another class. Without this change, that count is 0 when the entry point runs. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

In the JVM, each class has exactly one java.lang.Class object, so that 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. Code relies on this, e.g., in equals methods and in Enum.compareTo. JBMC used the Object.getClass model of the models library, which calls Class.forName with the name of the runtime type. Implementing Class objects that are unique per name in the models library requires a lookup by name, which compares strings using the string solver: with a list of all Class objects, a program that calls getClass on objects of 10 different classes took 81 seconds, and with 20 classes did not finish within 7 minutes. An if-then-else chain over all classes in JBMC itself scales linearly, but makes every program that calls getClass initialise the class literals of all of the about 130 classes that are loaded. Instead, add a synthetic method C.getClass, which overrides Object.getClass and returns the class literal of C, for each class C that can have instances. Virtual method dispatch then selects the override of the runtime type, which symbolic execution resolves without involving the string solver. This is compatible with both kinds of lazy loading, as only the method symbols are created up front: context-insensitive lazy loading only converts the overrides of classes that it finds to be instantiated, and symex-driven lazy loading converts the ones that symbolic execution reaches. Class literals must exist before __CPROVER_initialize is generated, so create one for each class up front. If the program does not refer to a class literal, it is not initialised in __CPROVER_initialize, but on the first call of the class's getClass override, using CProver.classIdentifier for the name (as no new String literals can be created at that point). Initialising the class literals of all classes in __CPROVER_initialize would increase the size of the program expression for a trivial program from 37348 to 53079 steps with symex-driven lazy loading, which does not remove unused globals; with this change, it is 37540 steps. For the benchmark described above, verification now takes 0.33 seconds with 10 classes and 1.3 seconds with 40 classes. All JBMC regression tests pass; the sum of per-test times was 1003 and 1027 seconds in two runs, compared with 1003 seconds without this change. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Copilot

🟡 Changes recommended

Critical defects remain in Object/array Class identity, super.getClass() runtime-type semantics, and Class-object initialization under concurrency or when the literal initializer is absent.

4 open issues

What changed in this PR

This PR implements runtime-class identity in JBMC through synthetic getClass() methods that return canonical class literals, while preserving lazy-loading behavior.

Changes:

Add synthetic getClass() overrides and initialize otherwise-unused class literals on first access.
Initialize class literals after other static state to preserve initializer side effects.
Add regressions for class identity, class names, and static-state preservation.

File	Description
`jbmc/src/java_bytecode/synthetic_methods_map.h`	Add the synthetic `GET_CLASS` method kind.
`jbmc/src/java_bytecode/java_entry_point.cpp`	Defer class-literal initialization until other static state is initialized.
`jbmc/src/java_bytecode/java_bytecode_language.cpp`	Generate `getClass()` overrides and lazy class-literal initialization.
`jbmc/regression/jbmc/pom.xml`	Register both new regression modules.
`jbmc/regression/jbmc/get-class/src/main/java/Test.java`	Exercise class identity, literals, names, and differing runtime types.
`jbmc/regression/jbmc/get-class/sameClass.desc`	Check identity for objects of the same class.
`jbmc/regression/jbmc/get-class/pom.xml`	Configure the class-identity regression module.
`jbmc/regression/jbmc/get-class/noClassLiteral.desc`	Check lazy initialization without an explicit class literal.
`jbmc/regression/jbmc/get-class/mustFail.desc`	Require failure when distinct runtime classes are equated.
`jbmc/regression/jbmc/get-class/differentClass.desc`	Check distinct identities across runtime classes.
`jbmc/regression/jbmc/get-class/classLiteral.desc`	Check identity against explicit class literals.
`jbmc/regression/jbmc/class-literals-static-state/test.desc`	Run the static-state preservation regression.
`jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java`	Assert that class-literal initialization effects persist.
`jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java`	Track initialized literals in shared static state.
`jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java`	Provide a test model with observable initializer side effects.
`jbmc/regression/jbmc/class-literals-static-state/pom.xml`	Configure the static-state regression module.

_{Review effort: Balanced}

tautschnig · 2026-11-04T21:35:13Z

+    if(
+      !symbol.is_type || symbol.mode != ID_java ||
+      !can_cast_type<java_class_typet>(symbol.type) ||
+      symbol.name == "java::java.lang.Object" || is_java_array_tag(symbol.name))


Objects of type java.lang.Object keep using the models' Object.getClass; with diffblue/java-models-library#50 that returns Object.class (test get-class-for-name/objectReceiver.desc). Arrays are not addressed: JBMC uses one class literal for all reference arrays, so this needs a change to the array representation (noted in the PR description).

tautschnig · 2026-11-04T21:35:15Z

+      symbol_table.get_writeable_ref(literal_id)
+        .type.set(ID_C_no_initialization_required, true);


Fixed in 879f7c5: without cproverGetClassObject or cproverInitializeClassLiteral, __CPROVER_initialize initialises the class literal as before.

tautschnig · 2026-11-04T21:35:17Z

+    init.add(code_frontend_assignt{
+      initialized->symbol_expr(), from_integer(1, java_boolean_type())});


Fixed in 4c8c3bd: with --java-threading, getClass uses the protocol of the thread-safe clinit wrappers (test get-class-for-name/threading.desc).

tautschnig · 2026-11-04T21:35:20Z

+  code.add(code_frontend_returnt{typecast_exprt::conditional_cast(
+    address_of_exprt{class_literal}, method_type.return_type())});


Fixed in e922456: invokespecial of getClass is now bound dynamically (test get-class-invokespecial).

codecov · 2026-11-03T21:22:28Z

Codecov Report

❌ Patch coverage is 97.72727% with 5 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.93%. Comparing base (a521901) to head (4c8c3bd).

Files with missing lines	Patch %	Lines
jbmc/src/java_bytecode/java_bytecode_language.cpp	97.51%	5 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9390      +/-   ##
===========================================
+ Coverage    80.91%   80.93%   +0.01%     
===========================================
  Files         1719     1719              
  Lines       190344   190564     +220     
  Branches        73       73              
===========================================
+ Hits        154022   154237     +215     
- Misses       36322    36327       +5

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

peterschrammel

How does this support Class.forName(String)?
Does this work with symex-driven lazy loading?

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 <kiro-agent@users.noreply.github.com>

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 <kiro-agent@users.noreply.github.com>

If the program does not refer to the class literal of a class C, the override of getClass for C initialises C's class literal on its first call. A model of Class.forName that returns unique Class objects cannot find that class literal before then, so a call of Class.forName("C") before the first call of getClass for C creates a second Class object for C: Class.forName("C") == new C().getClass() did not hold. Instead, obtain the Class object of such a class from the method cproverGetClassObject of the model of java.lang.Class, if it exists, on the first call of getClass for C, and store it in a global. The model can then return the Class object that forName created for C, if any. cproverGetClassObject takes the same arguments as cproverInitializeClassLiteral, so that the model can record whether C is an enum etc. With models that do not have cproverGetClassObject, the class literal is initialised as before. If the model of java.lang.Class has neither cproverGetClassObject nor cproverInitializeClassLiteral, the class literal is now initialised by __CPROVER_initialize as before this series, rather than not at all. The new regression test get-class-for-name uses its own model of java.lang.Class with such a cproverGetClassObject method. It also covers programs that first call getClass for a class on only one branch: the model must not add an object that might already be in one of its lists, as symbolic execution would then consider cyclic lists and could not bound the loops over them. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Object.getClass is final, so that super.getClass() returns the Class object of the runtime type of the receiver, just like getClass(). javac compiles super.getClass() to invokespecial java/lang/Object.getClass, but other compilers may name the superclass, e.g. invokespecial A.getClass in a subclass B of A. JBMC binds invokespecial calls statically, so that such a call reached the getClass override of A that JBMC now creates, and returned the Class object of A instead of B. Bind invokespecial calls of getClass:()Ljava/lang/Class; dynamically instead, so that they reach the override of the runtime type. This also applies to javac's form, which thus no longer goes through the model of Object.getClass. The new regression test get-class-invokespecial uses Jasmin to create such an invokespecial instruction; it fails without this change. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

With --java-threading, two threads could both find that the Class object of a class whose class literal the program does not refer to has not been obtained yet, and both call cproverGetClassObject, or one thread could see the Class object before it was initialised. With --java-threading, use the protocol of the thread-safe static initializer wrappers instead: in an atomic section, a thread waits (via an assumption) while another thread obtains the Class object, and claims the task if no thread has done so yet; once done, it records completion in another atomic section. Obtaining the Class object does not call getClass for the same class, so that, unlike for static initializers, recursive initialisation by the same thread need not be handled. Without --java-threading, the code is unchanged. The new test get-class-for-name/threading.desc runs one of the existing cases with --java-threading. In a program in which two threads call getClass for the same class, JBMC did not report a violation of uniqueness either before or after this change, with --unwind 2 taking about 335 seconds in both cases, which is too long for a regression test. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig · 2026-11-04T21:35:27Z

@peterschrammel

Class.forName with unique Class objects is modelled in Model Class.forName with unique Class objects java-models-library#50. 879f7c5 makes getClass and forName return the same object in either call order (test get-class-for-name).
Yes: only the method symbols are created up front, and all new tests run in both modes. With symex-driven lazy loading, a trivial program grows from 37348 to 37617 steps.

tautschnig and others added 2 commits November 3, 2026 16:36

tautschnig requested review from TGWDB, kroening and peterschrammel as code owners November 3, 2026 20:54

Copilot AI balanced review requested due to automatic review settings November 3, 2026 20:54

Copilot started reviewing on behalf of tautschnig November 3, 2026 20:55

View session

Copilot AI reviewed Nov 3, 2026

View reviewed changes

tautschnig mentioned this pull request Nov 3, 2026

Model Class.forName with unique Class objects diffblue/java-models-library#50

Open

peterschrammel reviewed Nov 3, 2026

View reviewed changes

tautschnig mentioned this pull request Nov 4, 2026

Model additions from SV-COMP 26 diffblue/java-models-library#48

Open

tautschnig and others added 3 commits November 4, 2026 18:30

tautschnig force-pushed the kiro/jbmc-get-class branch from 4aa1099 to 4c8c3bd Compare November 4, 2026 18:30

Navigation Menu

Repository navigation

JBMC: make Object.getClass return the unique Class object of each class - #9390

JBMC: make Object.getClass return the unique Class object of each class#9390
tautschnig wants to merge 5 commits into
diffblue:developfrom
tautschnig:kiro/jbmc-get-class

tautschnig commented Nov 3, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

tautschnig Nov 4, 2026

Uh oh!

tautschnig Nov 4, 2026

Uh oh!

tautschnig Nov 4, 2026

Uh oh!

tautschnig Nov 4, 2026

Uh oh!

codecov Bot commented Nov 3, 2026 •

edited

Loading

Uh oh!

peterschrammel left a comment

Uh oh!

tautschnig commented Nov 4, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		symbol_table.get_writeable_ref(literal_id)
		.type.set(ID_C_no_initialization_required, true);

		init.add(code_frontend_assignt{
		initialized->symbol_expr(), from_integer(1, java_boolean_type())});

		code.add(code_frontend_returnt{typecast_exprt::conditional_cast(
		address_of_exprt{class_literal}, method_type.return_type())});

Conversation

tautschnig commented Nov 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

🟡 Changes recommended

Uh oh!

tautschnig Nov 4, 2026

Choose a reason for hiding this comment

Uh oh!

tautschnig Nov 4, 2026

Choose a reason for hiding this comment

Uh oh!

tautschnig Nov 4, 2026

Choose a reason for hiding this comment

Uh oh!

tautschnig Nov 4, 2026

Choose a reason for hiding this comment

Uh oh!

codecov Bot commented Nov 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Nov 4, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented Nov 3, 2026 •

edited

Loading

codecov Bot commented Nov 3, 2026 •

edited

Loading