Class: don't route internal callers through the notModelled forName - #43
Draft
tautschnig wants to merge 1 commit into
Draft
Class: don't route internal callers through the notModelled forName#43tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
Class.forName's body is deliberately CProver.notModelled() +
throw new AssertionError() (its singleton/lookup semantics are
unimplemented) -- but getPrimitiveClass(String), getPrimitiveClass(int)
and getSuperclass() still routed through it. getPrimitiveClass is called
from every boxed-primitive <clinit> (Integer.<clinit> calls
getPrimitiveClass("int")), so ANY program that autoboxes -- e.g. any use
of HashMap<Integer, ...> -- failed verification with forName's spurious
AssertionError before its own assertions were even considered.
Add a private cproverClassWithName factory (a fresh Class with the given
name, exactly what forName's pre-notModelled body used to build) and route
the three internal callers through it. forName itself stays notModelled
for user code. isPrimitive()'s literal-pointer-equality trick is preserved:
the factory receives the same constant string literals.
Verified with JBMC: HashMap/ArrayList put/get/size/enhanced-for probes now
VERIFICATION SUCCESSFUL (previously failed in Integer.<clinit>);
Integer.TYPE.isPrimitive() and getName() prove; a deliberately-false
HashMap property still fails (no vacuity).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
This PR prevents internal java.lang.Class helpers (primitive-class lookup and getSuperclass()) from calling Class.forName(String), which is intentionally CProver.notModelled() + AssertionError in this model library. This avoids spurious verification failures triggered during boxed-primitive <clinit> execution (e.g., Integer.TYPE initialization).
Changes:
- Add a private
cproverClassWithName(String)factory to createClassinstances with a known name without routing throughforName. - Route
getPrimitiveClass(String),getPrimitiveClass(int), andgetSuperclass()through the new factory.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
405
to
+407
| public Class getSuperclass(){ | ||
| // TODO: here we assume no superclass which may not be correct | ||
| return Class.forName(null); | ||
| return cproverClassWithName(null); |
tautschnig
marked this pull request as draft
July 30, 2026 09:06
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.
Class.forName's body is deliberately CProver.notModelled() + throw new AssertionError() (its singleton/lookup semantics are unimplemented) -- but getPrimitiveClass(String), getPrimitiveClass(int) and getSuperclass() still routed through it. getPrimitiveClass is called from every boxed-primitive (Integer. calls getPrimitiveClass("int")), so ANY program that autoboxes -- e.g. any use of HashMap<Integer, ...> -- failed verification with forName's spurious AssertionError before its own assertions were even considered.
Add a private cproverClassWithName factory (a fresh Class with the given name, exactly what forName's pre-notModelled body used to build) and route the three internal callers through it. forName itself stays notModelled for user code. isPrimitive()'s literal-pointer-equality trick is preserved: the factory receives the same constant string literals.
Verified with JBMC: HashMap/ArrayList put/get/size/enhanced-for probes now VERIFICATION SUCCESSFUL (previously failed in Integer.); Integer.TYPE.isPrimitive() and getName() prove; a deliberately-false HashMap property still fails (no vacuity).