Java reference-equality semantics for de-interned strings and boxes

symbolic-executor/src/main/java/de/uzl/its/swat/common/RefIdentity.java

@@ -0,0 +1,123 @@
+package de.uzl.its.swat.common;
+
+import java.lang.ref.ReferenceQueue;
+import java.lang.ref.WeakReference;
+import java.util.HashSet;
+
+/**
+ * Bookkeeping that lets {@link UtilInstrumented#refEquals} reproduce Java's reference identity
+ * although the NoCache transformer de-interns string literals and the boxing caches.
+ *
+ * <p>Every object that SWAT creates in place of a shared instance (a string literal, a {@code
+ * valueOf} result, an {@code intern()} result) is registered here. Two such objects are one
+ * instance in the original program exactly when their values are equal (and, for boxes, the value
+ * is in the cache range). Objects that are not registered keep their own identity.
+ *
+ * <p>This class is not instrumented and its methods are ignored invocations: their results only
+ * depend on where an object was created, which the control flow already determines, so the
+ * symbolic state receives them as concrete values.
+ */
+@SuppressWarnings("unused")
+public final class RefIdentity {
+
+    private static final ReferenceQueue<Object> queue = new ReferenceQueue<>();
+    private static final HashSet<Key> deInterned = new HashSet<>();
+
+    private RefIdentity() {}
+
+    /** Registers {@code copy} as standing for the shared instance of its value. */
+    public static void markDeInterned(Object copy) {
+        if (copy == null) return;
+        synchronized (deInterned) {
+            expunge();
+            deInterned.add(new Key(copy, queue));
+        }
+    }
+
+    public static boolean isDeInterned(Object o) {
+        if (o == null) return false;
+        synchronized (deInterned) {
+            return deInterned.contains(new Key(o, null));
+        }
+    }
+
+    /**
+     * Whether {@code s} is, in the original program, the canonical (interned) instance of its value:
+     * a de-interned copy, or a pooled string that reached the program without passing the NoCache
+     * transformer (e.g. a literal returned by the JDK). The pool lookup interns a fresh copy rather
+     * than {@code s}, so it never turns {@code s} itself into the pooled instance.
+     */
+    public static boolean isCanonicalString(String s) {
+        return isDeInterned(s) || isPooledOnly(s);
+    }
+
+    /** Whether {@code s} is an unregistered string that is the pooled instance of its value. */
+    public static boolean isPooledOnly(String s) {
+        return !isDeInterned(s) && new String(s).intern() == s;
+    }
+
+    /**
+     * Whether {@code o} is, in the original program, a cached box: a de-interned {@code valueOf}
+     * copy (cached if its value is in the cache range, which the caller checks), or the cached
+     * instance itself.
+     */
+    public static boolean isCanonicalBox(Object o) {
+        if (isDeInterned(o)) return true;
+        if (o instanceof Integer i) return i == Integer.valueOf(i.intValue());
+        if (o instanceof Long l) return l == Long.valueOf(l.longValue());
+        if (o instanceof Short s) return s == Short.valueOf(s.shortValue());
+        if (o instanceof Byte b) return b == Byte.valueOf(b.byteValue());
+        if (o instanceof Character c) return c == Character.valueOf(c.charValue());
+        if (o instanceof Boolean b) return b == Boolean.valueOf(b.booleanValue());
+        return false;
+    }
+
+    /**
+     * {@code s.intern() == s} with the JVM's own side effect: an unregistered string whose value is
+     * not pooled yet becomes the pooled instance. A registered copy never does, its value is pooled.
+     */
+    public static boolean internsToItself(String s) {
+        return !isDeInterned(s) && s.intern() == s;
+    }
+
+    /** Plain reference identity, kept out of the symbolic state's view of {@code IF_ACMP}. */
+    public static boolean same(Object a, Object b) {
+        return a == b;
+    }
+
+    /**
+     * Marks a reference comparison whose outcome depends on the values of {@code a} and {@code b}
+     * in a way SWAT does not encode. The symbolic state records a reference semantic change when an
+     * argument is symbolic.
+     */
+    public static void valueDependentIdentity(Object a, Object b) {}
+
+    private static void expunge() {
+        Object k;
+        while ((k = queue.poll()) != null) {
+            deInterned.remove(k);
+        }
+    }
+
+    private static final class Key extends WeakReference<Object> {
+        private final int hash;
+
+        Key(Object referent, ReferenceQueue<Object> q) {
+            super(referent, q);
+            this.hash = System.identityHashCode(referent);
+        }
+
+        @Override
+        public int hashCode() {
+            return hash;
+        }
+
+        @Override
+        public boolean equals(Object other) {
+            if (this == other) return true;
+            if (!(other instanceof Key k)) return false;
+            Object referent = get();
+            return referent != null && referent == k.get();
+        }
+    }
+}

symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java

@@ -42,10 +42,6 @@ public class Util {
 
     private static final HashMap<String, Boolean> shouldInstrumentCache = new HashMap<>();
 
-    // Maintain a set of class names that have been de-interned
-    private static final Set<String> deInternedClasses = new HashSet<>(Arrays.asList(
-            String.class.getName(), Boolean.class.getName(), Byte.class.getName(), Short.class.getName(),
-            Character.class.getName(), Integer.class.getName(), Long.class.getName()));
 
     /**
      * Just a method for validating the engine!
@@ -419,19 +415,4 @@ public static boolean isSymbolicMethod(String cname, String name) {
         return Pattern.matches(symbolicMethodPattern, name);
     }
 
-    static boolean shouldUseValueEquality(Object a, Object b) {
-        // If either is null, Objects.equals handles it correctly anyway
-        if (a == null || b == null) {
-            return true;
-        }
-
-        // Check if either object's class has been de-interned
-        return isDeInternedClass(a.getClass()) || isDeInternedClass(b.getClass());
-    }
-
-    private static boolean isDeInternedClass(Class<?> clazz) {
-        // Check the exact class and optionally superclasses if inheritance matters
-        return deInternedClasses.contains(clazz.getName());
-    }
-
 }

symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java

@@ -5,7 +5,6 @@
 
 import java.lang.reflect.InvocationTargetException;
 import java.lang.reflect.Method;
-import java.util.Objects;
 
 @SuppressWarnings("unused")
 public class UtilInstrumented {
@@ -24,14 +23,69 @@ public static void liftClass(Object param, String paramCnameDot, String methodNa
         }
     }
     /**
-     * Conditionally uses Objects.equals() for de-interned classes,
-     * otherwise uses reference equality.
+     * Replaces {@code IF_ACMPEQ}/{@code IF_ACMPNE}: Java reference identity, computed on objects of
+     * which SWAT de-interned the literals and boxing caches (see {@link RefIdentity}).
+     *
+     * <p>Two canonical instances (literals, interned strings, cached boxes) are identical exactly
+     * when their values are equal, and that comparison goes through the modelled {@code equals}
+     * and unboxing calls so the symbolic state sees its dependence on the values. Every other
+     * comparison is plain identity and concrete. The comparisons themselves must not be
+     * {@code IF_ACMP}s here: the symbolic state encodes those on strings as value equality.
      */
     @SuppressWarnings("unused")
     public static boolean refEquals(Object a, Object b) {
-        if (Util.shouldUseValueEquality(a, b)) {
-            return Objects.equals(a, b);
+        if (a instanceof String sa && b instanceof String sb) {
+            if (RefIdentity.isCanonicalString(sa) && RefIdentity.isCanonicalString(sb)) {
+                if (RefIdentity.isPooledOnly(sa) || RefIdentity.isPooledOnly(sb)) {
+                    // Whether a string from uninstrumented code is pooled may depend on its value.
+                    RefIdentity.valueDependentIdentity(sa, sb);
+                }
+                return sa.equals(sb);
+            }
+            return RefIdentity.same(a, b);
         }
-        return a == b;
+        if (RefIdentity.same(a, b)) {
+            return true;
+        }
+        if (RefIdentity.isCanonicalBox(a) && RefIdentity.isCanonicalBox(b)) {
+            // Distinct cached boxes: the same instance iff the values are equal and in the cache range.
+            if (a instanceof Integer x && b instanceof Integer y) {
+                int v = x.intValue();
+                return v == y.intValue() && v >= -128 && v <= 127;
+            }
+            if (a instanceof Long x && b instanceof Long y) {
+                long v = x.longValue();
+                return v == y.longValue() && v >= -128 && v <= 127;
+            }
+            if (a instanceof Short x && b instanceof Short y) {
+                short v = x.shortValue();
+                return v == y.shortValue() && v >= -128 && v <= 127;
+            }
+            if (a instanceof Character x && b instanceof Character y) {
+                char v = x.charValue();
+                return v == y.charValue() && v <= 127;
+            }
+            if (a instanceof Byte x && b instanceof Byte y) {
+                return x.byteValue() == y.byteValue();
+            }
+            if (a instanceof Boolean x && b instanceof Boolean y) {
+                return x.booleanValue() == y.booleanValue();
+            }
+        }
+        return RefIdentity.same(a, b);
+    }
+
+    /**
+     * Replaces {@code String.intern()}: a de-interned copy standing for the pooled instance, or
+     * {@code s} itself when {@code s} is (or, by this call, becomes) the pooled instance.
+     */
+    @SuppressWarnings("unused")
+    public static String intern(String s) {
+        if (RefIdentity.internsToItself(s)) {
+            return s;
+        }
+        String copy = new String(s);
+        RefIdentity.markDeInterned(copy);
+        return copy;
     }
 }

symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java

@@ -23,6 +23,7 @@ public void visitLdcInsn(Object value) {
             mv.visitLdcInsn(value);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/String", "<init>",
                     "(Ljava/lang/String;)V", false);
+            markDeInterned();
             //NoCacheTransformer.getPrintBox()
             //        .addMsg("Replacing LDC with new String");
         } else {
@@ -33,14 +34,16 @@ public void visitLdcInsn(Object value) {
     // Intercept method calls to disable interning and caching.
     @Override
     public void visitMethodInsn(int opcode, String owner, String name, String descriptor, boolean isInterface) {
-        // Skip String.intern() calls.
+        // Replace String.intern() with a de-interned copy that stands for the pooled instance.
         if (opcode == Opcodes.INVOKEVIRTUAL &&
                 owner.equals("java/lang/String") &&
                 name.equals("intern") &&
                 descriptor.equals("()Ljava/lang/String;") &&
                 Config.instance().isUseStringInterning()) {
+            mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/common/UtilInstrumented", "intern",
+                    "(Ljava/lang/String;)Ljava/lang/String;", false);
             NoCacheTransformer.getPrintBox()
-                    .addMsg("Removing String.intern() call");
+                    .addMsg("Replacing String.intern() with UtilInstrumented.intern");
             return;
         }
         // Replace Integer.valueOf(int) with new Integer(int)
@@ -54,6 +57,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Integer", "<init>", "(I)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Integer.valueOf with new Integer");
             return;
@@ -69,6 +73,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.LLOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Long", "<init>", "(J)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Long.valueOf with new Long");
             return;
@@ -84,6 +89,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Short", "<init>", "(S)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Short.valueOf with new Short");
             return;
@@ -99,6 +105,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Byte", "<init>", "(B)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Byte.valueOf with new Byte");
             return;
@@ -114,6 +121,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Character", "<init>", "(C)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Character.valueOf with new Character");
             return;
@@ -129,6 +137,7 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
             mv.visitInsn(Opcodes.DUP);
             mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
             mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Boolean", "<init>", "(Z)V", false);
+            markDeInterned();
             NoCacheTransformer.getPrintBox()
                     .addMsg("Replacing Boolean.valueOf with new Boolean");
             return;
@@ -137,6 +146,16 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri
         mv.visitMethodInsn(opcode, owner, name, descriptor, isInterface);
     }
 
+    /**
+     * Registers the copy on top of the stack as standing for a shared instance, so that
+     * {@code UtilInstrumented.refEquals} can reproduce the identity of the original program.
+     */
+    private void markDeInterned() {
+        mv.visitInsn(Opcodes.DUP);
+        mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/common/RefIdentity", "markDeInterned",
+                "(Ljava/lang/Object;)V", false);
+    }
+
     /*
     // Instrument object reference comparisons (IF_ACMPEQ and IF_ACMPNE) to print a warning.
     @Override

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java

@@ -28,6 +28,7 @@ public class InvocationHandler {
                             "java/io/PrintStream/println",
                             "de/uzl/its/swat/instrument/Intrinsics",
                             "de/uzl/its/swat/common/UtilInstrumented",
+                            "de/uzl/its/swat/common/RefIdentity",
                             "de/uzl/its/swat/witness/Witness",
                             "de/uzl/its/swat/instrument/svcomp/Verifier",
                             "java/io/PrintStream",
@@ -67,8 +68,12 @@ private static boolean hasSymbolicElement(Value<?, ?> v) throws NotImplementedEx
         Type[] types = Type.getArgumentTypes(desc);
         logger.trace("Invoking method {} in class {} with arguments {}", name, owner, arguments);
 
-        // We do that first to include the pointer in instance invocation cases
-        boolean containsSymbolicArgument = arguments.stream().anyMatch(v -> {
+        boolean ignored = IGNORED_INVOCATIONS.contains(owner + "/" + name)
+                || IGNORED_INVOCATIONS.contains(owner);
+
+        // We do that first to include the pointer in instance invocation cases. Ignored
+        // invocations are never recorded, so their arguments need no (possibly deep) scan.
+        boolean containsSymbolicArgument = !ignored && arguments.stream().anyMatch(v -> {
             try {
                 return v.isSymbolic() || hasSymbolicElement(v);
             } catch (NotImplementedException e) {
@@ -78,7 +83,7 @@ private static boolean hasSymbolicElement(Value<?, ?> v) throws NotImplementedEx
         });
 
         if (isInstance) {
-            containsSymbolicArgument = containsSymbolicArgument || instance.isSymbolic();
+            containsSymbolicArgument = containsSymbolicArgument || (!ignored && instance.isSymbolic());
             retValue = instance.invokeMethod(name, types, arguments.toArray(new Value[0]));
         } else {
             retValue =
@@ -91,9 +96,7 @@ private static boolean hasSymbolicElement(Value<?, ?> v) throws NotImplementedEx
         }
 
         // When the method is not implemented and its not on the ignore list, we record it
-        if (retValue instanceof PlaceHolder &&
-                !(IGNORED_INVOCATIONS.contains(owner + "/" + name)
-                || IGNORED_INVOCATIONS.contains(owner))) {
+        if (retValue instanceof PlaceHolder && !ignored) {
 
             if(isInstance) arguments.add(0, instance);