SVCOMP'23 updates

src/main/java/java/lang/Class.java

@@ -39,6 +39,58 @@
 
 import org.cprover.CProver;
 
+/**
+ * Instances of the class {@code Class} represent classes and
+ * interfaces in a running Java application.  An enum is a kind of
+ * class and an annotation is a kind of interface.  Every array also
+ * belongs to a class that is reflected as a {@code Class} object
+ * that is shared by all arrays with the same element type and number
+ * of dimensions.  The primitive Java types ({@code boolean},
+ * {@code byte}, {@code char}, {@code short},
+ * {@code int}, {@code long}, {@code float}, and
+ * {@code double}), and the keyword {@code void} are also
+ * represented as {@code Class} objects.
+ *
+ * <p> {@code Class} has no public constructor. Instead {@code Class}
+ * objects are constructed automatically by the Java Virtual Machine as classes
+ * are loaded and by calls to the {@code defineClass} method in the class
+ * loader.
+ *
+ * <p> The following example uses a {@code Class} object to print the
+ * class name of an object:
+ *
+ * <blockquote><pre>
+ *     void printClassName(Object obj) {
+ *         System.out.println("The class of " + obj +
+ *                            " is " + obj.getClass().getName());
+ *     }
+ * </pre></blockquote>
+ *
+ * <p> It is also possible to get the {@code Class} object for a named
+ * type (or for void) using a class literal.  See Section 15.8.2 of
+ * <cite>The Java&trade; Language Specification</cite>.
+ * For example:
+ *
+ * <blockquote>
+ *     {@code System.out.println("The name of class Foo is: "+Foo.class.getName());}
+ * </blockquote>
+ *
+ * @param <T> the type of the class modeled by this {@code Class}
+ * object.  For example, the type of {@code String.class} is {@code
+ * Class<String>}.  Use {@code Class<?>} if the class being modeled is
+ * unknown.
+ *
+ * @author  unascribed
+ * @see     java.lang.ClassLoader#defineClass(byte[], int, int)
+ * @since   JDK1.0
+ *
+ * @diffblue.limitedSupport
+ * Generated tests that create an instance of Class will be incorrect:
+ * <ul>
+ *   <li>IllegalAccessError error when attempting to set the java.lang.class via reflection</li>
+ *   <li>When JBMC mocks java.lang.Class, it causes IllegalAccessError</li>
+ * </ul>
+ */
 public final class Class<T> {
 
     private Class() {}
@@ -55,6 +107,13 @@ private Class() {}
     private boolean cproverIsMemberClass;
     private boolean cproverIsEnum;
 
+    // TODO: these fields are to enforce singleton semantics of
+    // Class objects as returned by Object.getClass() and Class.forName()
+    // The size is currently hard-coded which may lead to incorrect results.
+    // A map could be used here in future.
+    private static String[] cproverClassNames = new String[8];
+    private static Class<?>[] cproverClassInstances = new Class<?>[8];
+
     public String toString() {
         return (isInterface() ? "interface " : (isPrimitive() ? "" : "class "))
             + getName();
@@ -111,9 +170,25 @@ public String toGenericString() {
     // forName method. The goal is to correctly model combinations of forName
     // and getName, but precisely following the JDK behaviour is more involved.
     public static Class<?> forName(String className) {
-        Class c=new Class();
-        c.name=className;
-        return c;
+        CProver.notModelled();
+        throw new AssertionError();
+        /*
+        String foundName = null;
+        for (int i = 0; i < cproverClassNames.length; ++i) {
+            String currentName = cproverClassNames[i];
+            if (currentName == null) {
+                Class<?> c = new Class();
+                c.name = className;
+                cproverClassNames[i] = className;
+                cproverClassInstances[i] = c;
+                return c;
+            }
+            if (className.equals(currentName)) {
+                return cproverClassInstances[i];
+            }
+        }
+        return CProver.nondetWithoutNullForNotModelled();
+        */
     }
 
     public static Class<?> forName(String name, boolean initialize,
@@ -205,7 +280,7 @@ ClassLoader getClassLoader0() {
         // DIFFBLUE MODEL LIBRARY The real java.lang.Class stores a
         // `private final ClassLoader classLoader` which is initialised by the
         // jvm rather than by the constructor of this object.
-        // TODO test-gen should understand this method natively.
+        // TODO JBMC should understand this method natively.
         return null;
     }
 
@@ -453,6 +528,7 @@ private static boolean desiredAssertionStatus0(Class<?> clazz) {
     protected void cproverNondetInitialize() {
         CProver.assume(name != null);
         CProver.assume(enumConstantDirectory == null);
+        CProver.assume(classValueMap == null);
     }
 
     // DIFFBLUE MODEL LIBRARY
@@ -607,6 +683,13 @@ public Method getMethod(String name, Class<?>... parameterTypes) throws NoSuchMe
         return new Method(this, name, parameterTypes);
     }
 
+    // DIFFBLUE MODEL LIBRARY
+    // This field is never read in our model. We include them because ClassValue
+    // (in the java library, not our models) references it, so it is needed to
+    // make ClassValue compile.
+    // transient ClassValue.ClassValueMap classValueMap;
+    transient ClassValue.ClassValueMap classValueMap = null;
+
     /**
      * Returns the {@code Class} representing the component type of an
      * array.  If this class does not represent an array class this method
@@ -615,10 +698,12 @@ public Method getMethod(String name, Class<?>... parameterTypes) throws NoSuchMe
      * @return the {@code Class} representing the component type of this
      * class if this class is an array
      * @see     java.lang.reflect.Array
-     * @since 1.1
+     * @since JDK1.1
+     * @diffblue.noSupport
      */
+    // public native Class<?> getComponentType();
     public Class<?> getComponentType() {
         CProver.notModelled();
-        return CProver.nondetWithoutNullForNotModelled();
+        return CProver.nondetWithNullForNotModelled();
     }
 }

src/main/java/java/lang/Double.java

@@ -816,7 +816,7 @@ public static int hashCode(double value) {
      * @diffblue.fullSupport
      *
      * Until the native method doubleToRawLongBits(D) is implemented in
-     * CBMC, this model will allow test generation for checking equality
+     * CBMC, this model will allow JBMC for checking equality
      * between two Doubles.
      */
     public boolean equals(Object obj) {

src/main/java/java/lang/Float.java

@@ -716,7 +716,7 @@ public static int hashCode(float value) {
      * @diffblue.fullSupport
      *
      * Until the native method floatToRawIntBits(F) is implemented in
-     * CBMC, this model will allow test generation for checking equality
+     * CBMC, this model will allow JBMC for checking equality
      * between two Floats.
      */
     public boolean equals(Object obj) {

src/main/java/java/lang/Math.java

@@ -364,12 +364,10 @@ public static double log10(double a) {
      * result of sqrt is equal to the original number, which is not always
      * true. As a result, the solver will return UNSAT in many cases.
      * For instance, {@code Math.sqrt(2.0)} will cause the solver to be UNSAT.
-     * Reported in: TG-5598
      *
      * Also, there are precision issues on very small numbers. For instance,
      * for values between 0 and {@code 0x0.0000000000001p-900}, the sqrt method
      * is likely to not be equal to the result of the real Math.sqrt method.
-     * Reported in: TG-5602
      */
     public static double sqrt(double a) {
         // return StrictMath.sqrt(a); // default impl. delegates to StrictMath

src/main/java/java/lang/String.java

@@ -2996,8 +2996,7 @@ public String replaceAll(String regex, String replacement)
     {
         // return Pattern.compile(regex).matcher(this).replaceAll(replacement);
         // DIFFBLUE MODELS LIBRARY: we assume the expression is just a string literal
-        CProver.assume(
-            regex.indexOf('[') == -1 &&
+        if (regex.indexOf('[') == -1 &&
             regex.indexOf(']') == -1 &&
             regex.indexOf('.') == -1 &&
             regex.indexOf('\\') == -1 &&
@@ -3010,8 +3009,12 @@ public String replaceAll(String regex, String replacement)
             regex.indexOf('}') == -1 &&
             regex.indexOf('|') == -1 &&
             regex.indexOf('(') == -1 &&
-            regex.indexOf(')') == -1);
-        return replace(regex, replacement);
+            regex.indexOf(')') == -1) {
+            return replace(regex, replacement);
+        } else {
+            CProver.notModelled();
+            return CProver.nondetWithNullForNotModelled();
+        }
     }
 
     /**
@@ -4330,7 +4333,7 @@ public static String valueOf(float f) {
      */
     public static String valueOf(double d) {
         // string solver only knows how to convert floats to string
-        return CProverString.toString(d);
+        return CProverString.toString((float)d);
         // return Double.toString(d);
     }
 

src/main/java/java/lang/StringBuffer.java

@@ -333,7 +333,7 @@ public synchronized void setCharAt(int index, char ch) {
 
     /**
      * @diffblue.limitedSupport
-     * This method can be slow to generate tests due to TG-2866 and is
+     * This method can be slow to generate tests due to an issue and is
      * also limited by which {@code toString()} methods have been modelled.
      */
     @Override

src/main/java/java/lang/StringBuilder.java

@@ -156,7 +156,7 @@ public StringBuilder(CharSequence seq) {
 
     /**
      * @diffblue.limitedSupport
-     * This method can be slow to generate tests due to TG-2866 and is
+     * This method can be slow to generate tests due to an issue and is
      * also limited by which {@code toString()} methods have been modelled.
      */
     @Override