Repository navigation
Make the models compile with JDK 25 - #49
Open
tautschnig wants to merge 1 commit into
Open
tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
Building the models with JDK 25 (the default JDK on Ubuntu 26.04, and thus on GitHub's ubuntu-latest runners) fails with three errors: - Object.java: "flexible constructors is not supported in -source 8". java.lang.Object has no superclass, so javac 25 treats every statement in its constructor as part of a constructor prologue (JEP 513). Initialise cproverMonitorCount in its declaration instead. - Class.java: ClassLoader.checkClassLoaderPermission no longer exists. As the call was already passing null for the caller class, it did not check anything; comment it out like the original call. - URLEncoder.java: package sun.security.action does not exist. Read the file.encoding property with System.getProperty: doPrivileged has no effect without a security manager. With these changes the models build with JDK 11, 17 and 25. With JDK 17, the bytecode of Class differs only in the removed call and constant-pool indices, and that of Object only in the constructor no longer storing 0 to cproverMonitorCount, which is the default value of the field. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
🟢 Approval recommended
No active review issues are recorded for the JDK 25 compatibility changes.
No open issues 🎉
What changed in this PR
Updates the Java models for JDK 25 compilation, addressing compatibility issues that affect JBMC builds in CBMC’s CodeQL workflow.
Changes:
- Moves
cproverMonitorCountinitialization from theObjectconstructor to its field declaration. - Comments out the call to the removed
ClassLoader.checkClassLoaderPermissionmethod. - Replaces the internal privileged property lookup with
System.getProperty("file.encoding").
| File | Description |
|---|---|
src/main/java/java/net/URLEncoder.java |
Removes internal security imports and reads the encoding property directly. |
src/main/java/java/lang/Object.java |
Moves field initialization to avoid JDK 25 constructor compilation restrictions. |
src/main/java/java/lang/Class.java |
Disables a permission-check call unavailable in JDK 25. |
Review effort: Balanced
tautschnig
added a commit
that referenced
this pull request
Nov 4, 2026
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>
tautschnig
added a commit
that referenced
this pull request
Nov 4, 2026
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Building the models with JDK 25 (the default JDK on Ubuntu 26.04, and
thus on GitHub's ubuntu-latest runners) fails with three errors:
java.lang.Object has no superclass, so javac 25 treats every
statement in its constructor as part of a constructor prologue
(JEP 513). Initialise cproverMonitorCount in its declaration instead.
As the call was already passing null for the caller class, it did
not check anything; comment it out like the original call.
file.encoding property with System.getProperty: doPrivileged has no
effect without a security manager.
With these changes the models build with JDK 11, 17 and 25. With
JDK 17, the bytecode of Class differs only in the removed call and
constant-pool indices, and that of Object only in the constructor no
longer storing 0 to cproverMonitorCount, which is the default value of
the field.
CBMC's CodeQL workflow builds JBMC, including these models, on
ubuntu-latest, which is moving to Ubuntu 26.04 and thus JDK 25; it currently fails because of the first two of these errors (the version of the models that CBMC uses predates URLEncoder.java).