[nils-loose]

What and why

SWAT keeps unrolling loops whose state repeats exactly. In float_unboundedloop the loop is guarded by nondetBoolean() and its state is concrete (for example x stays at 9.5 from iteration 10 on). So the path space is infinite, and no run ever reached a verdict.

This adds loop-head state matching, sound by construction:

• Executor (loopStateMatching=true, set in sv-comp.cfg):
  • The instrumentation finds the targets of backward jumps with an empty operand stack (ASM Analyzer). It probes them with a LOOP_HEAD instruction that carries the locals defined there.
  • LoopStateMatcher hashes the state at the head: the head, its locals, the set of initialized application classes (new ClassInits registry, called from every <clinit>), their static fields, and the reachable heap, encoded as a graph.
  • There is no hash in any of these cases:
    • another application frame is on the stack, or the target runs more than one thread;
    • any shadow value is symbolic;
    • the heap holds anything other than application objects, application enum constants, arrays and plain Objects.
  • A run stops reporting states for good once it calls untracked code. The only exceptions are the Verifier, Math/StrictMath, and the static helpers of Double/Float/Integer/Long (not getInteger/getLong). It also stops on an invokedynamic, or on an access to a static field of an untracked class. Every reported state therefore has a prefix that leaves JDK-held state (System properties, the interrupt flag, the statics of classes in excluded packages) at its initial value.
  • An array with a symbolic length counts as symbolic (ObjectArrayValue, AbstractArrayValue).
  • Each run spends at most 1 s on hashing, and stops hashing once a state repeats on its own path.
  • Hashes reach the explorer with the next branch (BranchDTO.loopStates).
• Explorer:
  • Each state gets a position (branches before it, their outcomes as a binary number, states before it). The tree keeps the smallest position of every state.
  • dfs() does not offer a branch, or anything below it, that follows a state already reached at a smaller position.
  • --no-loop-state-matching turns this off.

Soundness. Order executions by (branch count, branch outcomes, number of states passed), and take a smallest violating execution. If it were cut off, it would pass a state S that some executed path reached at a smaller position. That path's prefix up to S, followed by the violating execution after S, is again an execution: the state is equal, and later inputs are fresh. That execution violates the property too and is smaller, which is a contradiction. The same argument holds for the events that downgrade SAFE (context loss etc.). Two conditions carry this argument:

• the hash covers everything the rest of the run can read;
• the state is the same on every execution with the same branch prefix, because no live value is symbolic.

Related tools:

• JPF/SPF match states, but SPF keeps symbolic values outside the hash, so its matching is unsound for symbolic runs.
• JDart and JBMC do no state matching: JDart bounds by depth, JBMC unwinds loops.

Review

An independent review found 4 wrong-SAFE counterexamples in the first version:

• new Object[n] kept a symbolic length that isSymbolic() ignored;
• a System property;
• the thread interrupt flag;
• a static field of a class in an excluded package (com/google).

All four are fixed by the two rules above. They are now VIOLATION tasks in swat-benchmarks/java/loop-state/:

• five come out VIOLATION;
• the unbounded Object[] variant times out, as it does without matching.

The rest of the reviewer's programs give no SAFE either.

The isSymbolic change also affects context-loss detection: an unmodelled call that receives an array with a symbolic length now counts as symbolic. Over all 482 baseline-correct SAFE runs and all 728 expected-VIOLATION runs, it changed no verdict. I did not check #77's container check, which is not on this branch. Once both are merged, that check also sees such arrays as symbolic.

Measured

Competition config (nosa, 300 s, 15 GB, sv-comp.cfg), compared with baseline-results.jsonl.

The final commit is re-measured on 1262 runs: the 52 gained runs, all 728 expected-VIOLATION runs and all 482 baseline-correct SAFE runs. Result: the same +104, 0 lost, 0 wrong. CPU on runs that finish on both sides is 0.96× the baseline.

The first version was measured on 1381 runs:

• all 728 expected-VIOLATION runs;
• all 1047 baseline-correct runs;
• all 60 float_unboundedloop runs;
• the TCAS and algorithms timeouts;
• 8 MinePump timeouts;
• 89 more runs whose KB record names unbounded-path-space, cpu-timeout-path-explosion, no-loop-state-matching or property-irrelevant-branches-explored.

+104 points, 52 runs gained, 0 lost, 0 new wrong verdicts. All gains are float_unboundedloop SAFE runs: timeout → SAFE.

task (float_unboundedloop)	runs	baseline	branch	CPU s (va / nre)
Batch-Conveyor-Counter	2	timeout	SAFE	7 / 7
Bounded-Proportional-Update	2	timeout	SAFE	56 / 56
Bounded-Reset-Linear-Growth	2	timeout	SAFE	19 / 19
Clamped-Triangular-Drift	2	timeout	SAFE	23 / 23
Cyclic-Preset-Inner-ABC	2	timeout	SAFE	8 / 8
Fixed-Block-Accumulator	2	timeout	SAFE	9 / 9
Inner-Retry-Until-OK	2	timeout	SAFE	6 / 6
Leak-and-Refill	2	timeout	SAFE	9 / 9
Mixed-Phase-AddHalve-with-Slack-Box	2	timeout	SAFE	11 / 11
Nested-Drain-Then-Step	2	timeout	SAFE	6 / 6
Nested-MinStep-Regulator	2	timeout	SAFE	4 / 4
Nested-PingPong-with-Caps	2	timeout	SAFE	4 / 4
Nested-Saturation-Then-Reset	2	timeout	SAFE	9 / 10
Nested-Windowed-Add-Remove	2	timeout	SAFE	43 / 44
Producer-Consumer-Level	2	timeout	SAFE	293 / 292
Ramp-and-Hold	2	timeout	SAFE	36 / 35
Safe-Accumulator-with-Bounded-Noise	2	timeout	SAFE	91 / 90
Saturating-Integrator	2	timeout	SAFE	65 / 65
Slew-Rate-Limiter	2	timeout	SAFE	8 / 8
Switched-Linear-Plant	2	timeout	SAFE	214 / 214
Two-Band-Piecewise-Linear-Oscillator	2	timeout	SAFE	11 / 11
Two-Level-Nested-Scheduler	2	timeout	SAFE	86 / 87
Two-State-FP-Oscillator	2	timeout	SAFE	6 / 6
Two-Var-Nested-Handshake	2	timeout	SAFE	23 / 23
Two-Variable_Averaging_Filter	2	timeout	SAFE	19 / 19
Unbounded-Outer-Inner-Safety-Gate	2	timeout	SAFE	6 / 6

• CPU: on the 1096 runs that finish on both sides, total CPU is 0.97× the baseline, i.e. no measurable overhead.
• Where pruning fires: only in float_unboundedloop (52 runs).

Tests

• LoopHeadsTest (Spock): finds heads and their locals; skips a head with values on the stack; finds no heads without backward jumps.
• tests/test_loop_state_matching.py: positions, pruning on one path and across paths, tie order, the off switch.
• swat-benchmarks/java/loop-state/: the reviewer's counterexamples as VIOLATION tasks.
• Executor default suite: 8733 tests, 0 failures. Explorer unit tests pass.

Known limits

• No help for MinePump, TCAS or algorithms:
  • MinePump's loop is not in the entry method, and caller frames are not hashed.
  • TCAS has no loops.
  • The algorithms tasks keep symbolic data on the heap.
  • Supporting caller frames would need call-site snapshots of the callers' locals.
• Not hashed:
  • Strings and boxed values.
  • Library objects.
  • JDK-held global state. Instead, a run stops reporting states at its first call into untracked code. Programs that call the library before or inside their loop get no matching.
• Still timeouts in the family: 4 float_unboundedloop runs whose state takes too long to repeat (Two-Counter-Lexicographic-Small, Hysteresis-On-Off-with-Deadband NRE, Adjustable-Inner-Count-Halving), plus Adjustable-Inner-Count-Halving's expected violation (valid-assert), which also times out on the baseline.

🤖 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.