From ab647567341a15c9cfec913576bef5402d1d668d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 29 Jul 2026 00:22:07 +0000 Subject: [PATCH 1/2] Class: create primitive classes without calling forName Class.forName calls CProver.notModelled() and then throws an AssertionError, as its model is incomplete. getPrimitiveClass(String), getPrimitiveClass(int) and getSuperclass() still called forName, and the static initializers of all boxed types call getPrimitiveClass (e.g., Integer. calls getPrimitiveClass(4)). Thus, JBMC reported a failing assertion in forName for any program that uses a boxed type, and did not explore any paths beyond that call. Create the Class objects in getPrimitiveClass directly instead. isPrimitive(), which compares the name with string literals by reference, still works, as the names are the same literals. getSuperclass() now returns null, which matches the existing comment that the model assumes there is no superclass. Returning a new Class object instead would make Enum.getDeclaringClass() return a different object on each call, so that E.A.getDeclaringClass() == E.B.getDeclaringClass() would not hold. With JBMC, assertions about Integer.TYPE.isPrimitive() and getName(), and about HashMap and ArrayList of Integer, now verify, and a false assertion about a HashMap is still reported as failing. Co-authored-by: Kiro --- src/main/java/java/lang/Class.java | 48 +++++++++++++++++------------- 1 file changed, 28 insertions(+), 20 deletions(-) diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index 36d0482..eec4b6f 100644 --- a/src/main/java/java/lang/Class.java +++ b/src/main/java/java/lang/Class.java @@ -95,6 +95,14 @@ public final class Class { private Class() {} + // DIFFBLUE MODEL LIBRARY Creates the Class objects of primitive types. + // These must not be created via forName, which is not modelled. + 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 +399,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 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 +436,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() { From 115d0d23b73bc26546a79d6b255ae4f1b94259da Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 4 Nov 2026 11:30:48 +0000 Subject: [PATCH 2/2] Byte, Short, Float: use the right primitive class for TYPE Byte.TYPE, Short.TYPE and Float.TYPE were initialised with getPrimitiveClass(7), which is the class of double, so that, e.g., Byte.TYPE.getName() returned "double". Use the indices of byte (2), short (3) and float (6) instead, and mark the change from the JDK source, which uses getPrimitiveClass(String), as Integer.java does. Co-authored-by: Kiro --- src/main/java/java/lang/Byte.java | 5 ++++- src/main/java/java/lang/Float.java | 5 ++++- src/main/java/java/lang/Short.java | 5 ++++- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/main/java/java/lang/Byte.java b/src/main/java/java/lang/Byte.java index f11261c..536cef8 100644 --- a/src/main/java/java/lang/Byte.java +++ b/src/main/java/java/lang/Byte.java @@ -62,8 +62,11 @@ public final class Byte extends Number implements Comparable { * The {@code Class} instance representing the primitive type * {@code byte}. */ + // DIFFBLUE MODEL LIBRARY + // We use the int version of getPrimitiveClass instead of + // the original String version @SuppressWarnings("unchecked") - public static final Class TYPE = (Class) Class.getPrimitiveClass(7); + public static final Class TYPE = (Class) Class.getPrimitiveClass(2); /** * Returns a new {@code String} object representing the diff --git a/src/main/java/java/lang/Float.java b/src/main/java/java/lang/Float.java index e18d54f..3f384aa 100644 --- a/src/main/java/java/lang/Float.java +++ b/src/main/java/java/lang/Float.java @@ -137,8 +137,11 @@ public final class Float extends Number implements Comparable { * * @since JDK1.1 */ + // DIFFBLUE MODEL LIBRARY + // We use the int version of getPrimitiveClass instead of + // the original String version @SuppressWarnings("unchecked") - public static final Class TYPE = (Class) Class.getPrimitiveClass(7); + public static final Class TYPE = (Class) Class.getPrimitiveClass(6); /** * Returns a string representation of the {@code float} diff --git a/src/main/java/java/lang/Short.java b/src/main/java/java/lang/Short.java index 1fd1a98..502bac8 100644 --- a/src/main/java/java/lang/Short.java +++ b/src/main/java/java/lang/Short.java @@ -61,8 +61,11 @@ public final class Short extends Number implements Comparable { * The {@code Class} instance representing the primitive type * {@code short}. */ + // DIFFBLUE MODEL LIBRARY + // We use the int version of getPrimitiveClass instead of + // the original String version @SuppressWarnings("unchecked") - public static final Class TYPE = (Class) Class.getPrimitiveClass(7); + public static final Class TYPE = (Class) Class.getPrimitiveClass(3); /** * Returns a new {@code String} object representing the * specified {@code short}. The radix is assumed to be 10.