From 506c20bc3e730e9727f2d4b304b15386fde04ddd Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:43:14 +0000 Subject: [PATCH 1/3] Return a concrete result from Objects.equals with a null operand Objects.equals(null, x) is true iff x is null, whatever x's content, so the model no longer returns a PlaceHolder (which recorded a missing invocation and, for symbolic x, a context loss). The reference-semantic-change check moves out: reference comparisons no longer go through Objects.equals. Co-Authored-By: Claude Opus 5.5 --- .../invoke/java/util/ObjectsInvocation.java | 23 +++---------------- 1 file changed, 3 insertions(+), 20 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java index 2f6cf86a..68d77efa 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java @@ -7,15 +7,10 @@ import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.PlaceHolder; import de.uzl.its.swat.symbolic.value.Value; -import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue; +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.BooleanValue; import de.uzl.its.swat.symbolic.value.reference.ObjectValue; -import de.uzl.its.swat.symbolic.value.reference.lang.CharacterObjectValue; -import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; -import de.uzl.its.swat.thread.ThreadHandler; import org.objectweb.asm.Type; -import static java.lang.Thread.currentThread; - public class ObjectsInvocation { public static Value invokeStaticMethod( @@ -35,21 +30,9 @@ public class ObjectsInvocation { ObjectValue a = args[0].asObjectValue(); ObjectValue b = args[1].asObjectValue(); - // Check for user-de-interned strings with different addresses. - // This detects when refEquals (which calls Objects.equals) compares strings - // that were explicitly created with new String() in user code. - // In such cases, reference equality semantics may differ from what the user intended. - if (a instanceof StringValue s1 && b instanceof StringValue s2) { - if ((s1.isUserDeInterned() || s2.isUserDeInterned()) - && s1.getAddress() != s2.getAddress()) { - // Record that reference equality semantics may have changed - ThreadHandler.getSymbolicTraceHandler(currentThread().getId()) - .recordReferenceSemanticChange(); - } - } - if(a.getAddress() == ObjectValue.ADDRESS_NULL || b.getAddress() == ObjectValue.ADDRESS_NULL) { - return PlaceHolder.instance; + // A null operand: equal iff both are null, independent of any symbolic content. + return new BooleanValue(a.context, a.getAddress() == b.getAddress()); } return a.invokeMethod("equals", null, new Value[]{b} ); } From 0152059dc31e0c4d5ff752b7e59276feff113995 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:43:14 +0000 Subject: [PATCH 2/3] Reproduce Java reference identity in the IF_ACMP rewrite The NoCache transformer de-interns string literals, intern() results and the boxing caches, and the IF_ACMP rewrite compensated by comparing every String and box by value. That made new String(s) == s true and new Integer(5) == new Integer(5) true, and it called the uninstrumented Util helper with symbolic arguments, a context loss on every such comparison. The copies SWAT creates now register themselves in RefIdentity (a weak identity set). refEquals compares two canonical instances (literal copies, interned or pooled strings, valueOf copies and cached boxes) by value, through the modelled equals/unboxing calls, with the cache range for boxes; everything else is plain identity. RefIdentity is an ignored invocation, and ignored invocations no longer scan their arguments for symbolic values. Pooled strings from uninstrumented code are flagged as a reference semantic change when they are symbolic, since their pooling may depend on the value. Co-Authored-By: Claude Opus 5.5 --- .../de/uzl/its/swat/common/RefIdentity.java | 123 ++++++++++++++++++ .../java/de/uzl/its/swat/common/Util.java | 19 --- .../uzl/its/swat/common/UtilInstrumented.java | 66 +++++++++- .../nocache/NoCacheMethodAdapter.java | 23 +++- .../symbolic/invoke/InvocationHandler.java | 15 ++- .../invoke/RefIdentityInvocation.java | 27 ++++ .../symbolic/invoke/StaticInvocation.java | 2 + .../uzl/its/swat/common/RefEqualsSpec.groovy | 110 ++++++++++++++++ 8 files changed, 352 insertions(+), 33 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/common/RefIdentity.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/RefIdentityInvocation.java create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/common/RefEqualsSpec.groovy diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/RefIdentity.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/RefIdentity.java new file mode 100644 index 00000000..d51af9a0 --- /dev/null +++ b/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. + * + *

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. + * + *

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 queue = new ReferenceQueue<>(); + private static final HashSet 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 { + private final int hash; + + Key(Object referent, ReferenceQueue 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(); + } + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java index 2247fb86..98cf9a46 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java @@ -42,10 +42,6 @@ public class Util { private static final HashMap shouldInstrumentCache = new HashMap<>(); - // Maintain a set of class names that have been de-interned - private static final Set 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()); - } - } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java index e288bec7..8282618f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java +++ b/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}). + * + *

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; } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java index aba06b80..b301652e 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java +++ b/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", "", "(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", "", "(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", "", "(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", "", "(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", "", "(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", "", "(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", "", "(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 diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java index d89f7cc2..e7d8208e 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java +++ b/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); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/RefIdentityInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/RefIdentityInvocation.java new file mode 100644 index 00000000..750ea751 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/RefIdentityInvocation.java @@ -0,0 +1,27 @@ +package de.uzl.its.swat.symbolic.invoke; + +import de.uzl.its.swat.common.exceptions.NotImplementedException; +import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; +import de.uzl.its.swat.symbolic.value.PlaceHolder; +import de.uzl.its.swat.symbolic.value.Value; + +/** + * Symbolic side of {@link de.uzl.its.swat.common.RefIdentity}. Its results are concrete facts about + * where objects were created; only {@code valueDependentIdentity} affects the symbolic state. + */ +public final class RefIdentityInvocation { + + public static Value invokeStaticMethod( + String name, Value[] args, SymbolicTraceHandler symbolicTraceHandler) throws NotImplementedException { + if (name.equals("valueDependentIdentity")) { + for (Value arg : args) { + if (arg.isSymbolic()) { + // A reference comparison decided by symbolic values that SWAT does not encode. + symbolicTraceHandler.recordReferenceSemanticChange(); + break; + } + } + } + return PlaceHolder.instance; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java index 21b2849f..d1a9878d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java @@ -53,6 +53,8 @@ public final class StaticInvocation { name, args, desc, symbolicStateHandler); case "java/lang/Double" -> DoubleInvocation.invokeStaticMethod( name, args, desc, symbolicStateHandler); + case "de/uzl/its/swat/common/RefIdentity" -> RefIdentityInvocation.invokeStaticMethod( + name, args, symbolicStateHandler); case "java/util/Objects" -> ObjectsInvocation.invokeStaticMethod( name, args, desc, symbolicStateHandler); default -> PlaceHolder.instance; diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/RefEqualsSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/RefEqualsSpec.groovy new file mode 100644 index 00000000..331432a4 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/RefEqualsSpec.groovy @@ -0,0 +1,110 @@ +package de.uzl.its.swat.common + +import spock.lang.Specification + +/** + * Concrete semantics of the IF_ACMP replacement: on objects de-interned the way the NoCache + * transformer does it, refEquals must give the answer the original program's {@code ==} gives. + */ +class RefEqualsSpec extends Specification { + + /** What the NoCache transformer emits for a string literal. */ + private static String literal(String s) { + String copy = new String(s) + RefIdentity.markDeInterned(copy) + return copy + } + + /** What the NoCache transformer emits for Integer.valueOf. */ + private static Integer boxed(int v) { + Integer copy = new Integer(v) + RefIdentity.markDeInterned(copy) + return copy + } + + def "two de-interned copies of one literal are the same instance"() { + expect: + UtilInstrumented.refEquals(literal("test"), literal("test")) + !UtilInstrumented.refEquals(literal("test"), literal("other")) + } + + def "a string built with new String is never a literal"() { + given: + String s1 = new String(literal("test")) + + expect: + !UtilInstrumented.refEquals(s1, literal("test")) + UtilInstrumented.refEquals(s1, s1) + } + + def "new String of an input differs from the input"() { + given: + String input = new String("fixed".toCharArray()) + String s1 = new String(input) + + expect: + !UtilInstrumented.refEquals(s1, input) + UtilInstrumented.refEquals(input, input) + } + + def "a pooled string from uninstrumented code equals a literal of its value"() { + expect: + UtilInstrumented.refEquals(Boolean.toString(true), literal("true")) + !UtilInstrumented.refEquals(Boolean.toString(false), literal("true")) + } + + def "intern returns the instance a literal of the same value stands for"() { + given: + String built = new StringBuilder("te").append("st").toString() + + expect: + UtilInstrumented.refEquals(UtilInstrumented.intern(built), literal("test")) + !UtilInstrumented.refEquals(built, literal("test")) + } + + def "boxes share an instance only inside the cache range"() { + expect: + UtilInstrumented.refEquals(boxed(v), boxed(v)) == shared + + where: + v || shared + 0 || true + 127 || true + -128 || true + 128 || false + -129 || false + 1000 || false + } + + def "a box is identical to itself outside the cache range"() { + given: + Integer b = boxed(1000) + + expect: + UtilInstrumented.refEquals(b, b) + } + + def "boxes created with new are distinct"() { + expect: + !UtilInstrumented.refEquals(new Integer(5), new Integer(5)) + !UtilInstrumented.refEquals(new Integer(5), boxed(5)) + UtilInstrumented.refEquals(Integer.valueOf(5), boxed(5)) + } + + def "boxes of different types or with null"() { + expect: + !UtilInstrumented.refEquals(boxed(5), Long.valueOf(5)) + !UtilInstrumented.refEquals(boxed(5), null) + UtilInstrumented.refEquals(null, null) + !UtilInstrumented.refEquals(literal("a"), null) + } + + def "other objects compare by identity"() { + given: + Object o = new Object() + + expect: + UtilInstrumented.refEquals(o, o) + !UtilInstrumented.refEquals(o, new Object()) + } +} From 6d511291a56bfba739eb2196cbdb733688fb0d18 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:43:14 +0000 Subject: [PATCH 3/3] Downgrade SAFE on a reference semantic change The flag means a reference comparison depended on symbolic values that SWAT does not encode, so the search may have missed a side of it; a SAFE verdict is as unreliable as a VIOLATION. Co-Authored-By: Claude Opus 5.5 --- symbolic-explorer/driver/SVCompDriver.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..ccc4cd07 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -464,8 +464,8 @@ def run(self): logger.warning(f'[SVCOMP] Found uncaught exceptions during symbolic execution') verdict = Verdict.UNKNOWN - if (verdict == Verdict.VIOLATION) and Database.instance().get_tree(ENDPOINT_ID).reference_semantic_change: - logger.warning(f'[SVCOMP] Found reference semantic change (user-de-interned strings compared via Objects.equals) - downgrading VIOLATION to UNKNOWN') + if (verdict in (Verdict.SAFE, Verdict.VIOLATION)) and Database.instance().get_tree(ENDPOINT_ID).reference_semantic_change: + logger.warning(f'[SVCOMP] Found reference semantic change (reference comparison decided by symbolic values SWAT does not encode) - downgrading {verdict.name} to UNKNOWN') verdict = Verdict.UNKNOWN if verdict == Verdict.NO_SYMBOLIC_VARS: