From b6ac7e569064f1934c6096bac959e74419cfd6a7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 29 Jul 2026 00:22:07 +0000 Subject: [PATCH] Class: don't route internal callers through the notModelled forName 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 -- 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). Co-authored-by: Kiro --- src/main/java/java/lang/Class.java | 53 +++++++++++++++++++----------- 1 file changed, 33 insertions(+), 20 deletions(-) diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index 36d0482..592b8f0 100644 --- a/src/main/java/java/lang/Class.java +++ b/src/main/java/java/lang/Class.java @@ -95,6 +95,19 @@ public final class Class { private Class() {} + // DIFFBLUE MODEL LIBRARY Internal factory for Class objects whose name + // is known to the model (primitive classes, the getSuperclass stub). + // Deliberately NOT forName: forName is notModelled() (its + // singleton/lookup semantics are unimplemented), and routing internal + // callers through it made EVERY boxed-primitive -- i.e. any + // autoboxing -- fail with forName's AssertionError (e.g. + // Integer. calls getPrimitiveClass("int")). + private static Class cproverClassWithName(String className) { + Class c = new Class<>(); + c.name = className; + return c; + } + private transient String name; // TODO: these boolean fields model the internal encoding of classes @@ -391,33 +404,33 @@ private String resolveName(String name) { public Class getSuperclass(){ // TODO: here we assume no superclass which may not be correct - return Class.forName(null); + return cproverClassWithName(null); } public static Class getPrimitiveClass(String s){ if("boolean".equals(s)) - return Class.forName("boolean"); + return cproverClassWithName("boolean"); if("char".equals(s)) - return Class.forName("char"); + return cproverClassWithName("char"); if("byte".equals(s)) - return Class.forName("byte"); + return cproverClassWithName("byte"); if("short".equals(s)) - return Class.forName("short"); + return cproverClassWithName("short"); if("int".equals(s)) - return Class.forName("int"); + return cproverClassWithName("int"); if("long".equals(s)) - return Class.forName("long"); + return cproverClassWithName("long"); if("float".equals(s)) - return Class.forName("float"); + return cproverClassWithName("float"); if("double".equals(s)) - return Class.forName("double"); + return cproverClassWithName("double"); if("void".equals(s)) - return Class.forName("void"); + return cproverClassWithName("void"); // TODO: we should throw an exception but this does not seem to work well // at the moment, so we will assume it does not happen instead. // throw new IllegalArgumentException("Not primitive type : " + s); CProver.assume(false); - return Class.forName(""); + return cproverClassWithName(""); } // This version is nicer for the symbolic execution as it knows how to @@ -428,22 +441,22 @@ public static Class getPrimitiveClass(String s){ // takes 8 seconds while the int version takes 3 seconds. static Class getPrimitiveClass(int i){ if(i==0) - return Class.forName("boolean"); + return cproverClassWithName("boolean"); if(i==1) - return Class.forName("char"); + return cproverClassWithName("char"); if(i==2) - return Class.forName("byte"); + return cproverClassWithName("byte"); if(i==3) - return Class.forName("short"); + return cproverClassWithName("short"); if(i==4) - return Class.forName("int"); + return cproverClassWithName("int"); if(i==5) - return Class.forName("long"); + return cproverClassWithName("long"); if(i==6) - return Class.forName("float"); + return cproverClassWithName("float"); if(i==7) - return Class.forName("double"); - return Class.forName("void"); + return cproverClassWithName("double"); + return cproverClassWithName("void"); } Map enumConstantDirectory() {