[nils-loose]

What changed

SWAT de-interns string literals and the boxing caches (Integer.valueOf etc.) so that the shadow heap keeps them apart. To make this work, the IF_ACMP rewrite compared every String and box by value (Objects.equals). That got Java's == wrong: new String(s) == s and new Integer(5) == new Integer(5) came out true. The rewrite also called the uninstrumented Util.shouldUseValueEquality with symbolic arguments, so every such comparison caused a context loss.

• Identity-preserving refEquals (UtilInstrumented, new RefIdentity):
  • The NoCache transformer now registers each copy it creates (literal, valueOf result, intern() result) in a weak identity set.
  • Two canonical instances (literal copies, interned or pooled strings, valueOf copies and cached boxes) compare by value. The comparison goes through the modelled equals / unboxing calls, so the symbolic state still sees the dependence on the values. For boxes it includes the cache range (-128..127; 0..127 for Character).
  • Every other comparison is plain identity and concrete. This covers new String(..), new Integer(..), nondet strings and all other objects.
• String.intern() is no longer dropped. It is replaced with UtilInstrumented.intern, which returns a registered copy, or the string itself when that string is (or becomes) the pooled instance.
• No helper context loss. RefIdentity is an ignored invocation. Ignored invocations also no longer scan their arguments for symbolic values, which removes the object-graph walk on every comparison.
• Objects.equals with a null operand returns a concrete result instead of a PlaceHolder.
• reference_semantic_change now means "a reference comparison was decided by symbolic values that SWAT does not encode". It is set only for a symbolic pooled string that comes from uninstrumented code. The driver now downgrades SAFE on this flag as well, not only VIOLATION.
• Util.shouldUseValueEquality is removed, and so is the userDeInterned check in ObjectsInvocation. The userDeInterned field in StringValue is left in place and is now unused. StringValue / StringBuilderValue / StringInvocation are not touched.

Measurement

• Configuration: --sv-comp, 300 s CPU, --mem15g, no SA, compared with baseline-results.jsonl.
• 1360 runs:
  • every run of jbmc-regression, jpf-regression, algorithms, objects, jdart-regression, juliet-java, java-ranger-regression, jayhorn-recursive, securibench and autostub;
  • argv-tasks: every expected-VIOLATION run and every baseline-correct run;
  • 60 random baseline-correct runs from the other families.

task	prop	expected	base	new	points
jbmc-regression/StringCompare01	valid-assert	SAFE	unknown	safe	+2
jbmc-regression/StringCompare05	valid-assert	VIOLATION	unknown	violation	+1
jbmc-regression/StringCompare05	no-runtime-exception	SAFE	unknown	safe	+2
jpf-regression/ExDarko_false	no-runtime-exception	SAFE	unknown	safe	+2

• Result: +7 gained, 0 lost, net +7. No new wrong verdict.
• Other flips: the remaining case changes are all 0-point. They are oom, stall, timeout or unknown on both sides, in algorithms/jayhorn-recursive, and are the known noise.
• CPU: the summed CPU of runs that finished on both sides went from 7834 s to 7442 s (median per-run ratio 0.97).
• StringCompare05 caveat (helper fix alone gives a false SAFE): this no longer applies, because the comparison itself is now exact. The SAFE downgrade still ships as a safety net.

Tests

• New RefEqualsSpec (15 cases) covers the concrete semantics: literals, new String, nondet-like strings, pooled JDK strings, intern, box cache range, new Integer, mixed types and null.
• The full executor suite passes (8745 tests, 0 failures).

Known limits

• The pool check interns a fresh probe copy. If a program later calls intern() on a string whose value was probed, it gets the probe instead of its own string.
• The box cache range is fixed at the JDK default. SWAT does not set AutoBoxCacheMax.
• objects05-08 and RedBlackTree-Mem* still fail for their primary causes (ObjectFactory descriptor, timeouts). Their helper context loss is gone.

🤖 Generated with Claude Code

[nils-loose]

Included in dev through #92 (merge commit 534c182), together with the fixes for interactions between PRs. This PR stays as the record of the change and its measured flips.