Make the explorer robust: iterative tree, lock safety, crashes end UNKNOWN by nils-loose · Pull Request #72 · SWAT-project/SWAT

nils-loose · 2026-10-18T22:50:11Z

Changes (symbolic-explorer only)

Tree: Node holds a single element. Tree.add, dfs (same pre-order), Tree.__deepcopy__ and add_to_dot no longer recurse. The constraint-variable walk is iterative and visits each subterm once. (Explorer fails on very large traces (RecursionError building the execution tree) #59)
UNMODELLED_EXCEPTION markers are no longer tree levels. Each marker is a flag on the next node, and dfs drops the SA walk there, as it did at the marker. check_divergence skips markers in the same way. A trace that still does not fit is left out of the tree from that point on, and tree_mismatch is recorded. (Static pre-analysis pruning, with soundness fixes #65 crash)
Database: every lock is taken with with lock (get_violations also leaked the lock). Soundness flags are recorded before the tree insert. A failure while adding a trace records trace_ingest_failed, and the driver then reports UNKNOWN.
Driver: an exception in the exploration ends the run with UNKNOWN (explorer_crash), and run_sv_comp prints DONT-KNOW and exits. (Explorer hangs when the SV-COMP worker thread raises #62) The divergence check runs only when the round sent a new trace; otherwise it records no_trace. tree_mismatch, trace_ingest_failed, no_trace and explorer_crash rule out SAFE.
Tests: tests/test_tree.py, test_database.py and test_driver_robustness.py, plus additions to test_sa_walk and test_divergence. All 95 tests pass.

Measurement (nosa, 300 s, sv-comp cfg, mem15g; base = baseline-results.jsonl)

1115 runs in total: 84 affected (the KB causes plus all 40 base stalls) and 1031 baseline-correct runs.

task	prop	base	new	pts
java-ranger-regression/apachecli_eqchk	NRE	stall	VIOLATION (exp. SAFE)	-16
securibench/Inter14	NRE	stall	SAFE	+2
securibench/Datastructures6	NRE	stall	SAFE	+2
securibench/Inter14, Collections14, Datastructures6	valid-assert	stall	VIOLATION	+1 each
jayhorn-recursive/UnsatAckermann01, UnsatFibonacci01	valid-assert	stall	VIOLATION	+1 each
jbmc-regression/StringBuilderChars03, StringMiscellaneous03	NRE	stall	VIOLATION	+1 each

Points: gained +11, lost -16, net -5. Without apachecli the net is +11. Stalls went from 40 to 0. Among the 1031 regression runs there are 0 flips.

The apachecli_eqchk verdict

Before this change, apachecli_eqchk under no-runtime-exception stalled. Now round 1 runs with the chars '-', '\0' x7 and false.

CLI.execute catches the ParseException (CLI.java:101) and returns commandLine, which is null at that point.
TestCLI.java:18 then calls outSPF.equals(...) on that null and throws a real NullPointerException. This reproduces on a plain JVM with a stub Verifier.

So the task's expected_verdict: true for no-runtime-exception, which upstream sv-benchmarks has as well, is wrong. It is listed in #63.

Fixes #59
Fixes #62

🤖 Generated with Claude Code

… be added Every Database method now holds the lock in a with-block. An exception in add_trace (a RecursionError on a long trace) used to leave it held, and the driver then waited for it until the time limit. get_violations also returned with the lock held for an unknown endpoint. add_trace records the soundness flags before it adds the trace to the tree, so they hold even if that fails. ConstraintService catches a failure, logs it and records a trace_ingest_failed execution error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

- An exception in the exploration ends the run at once with UNKNOWN and an explorer_crash execution error. Before, the worker thread died, the HTTP server kept the process alive and the run hung until the time limit. run_sv_comp prints DONT-KNOW for anything that fails around the driver and exits. - A trace that could not be added ends the search with UNKNOWN: the tree lacks its path. A violation in the same run still counts. - The divergence check only runs when the round sent a trace. Before, it checked the previous round's trace. A round without a trace records no_trace: its branch counts as solved and is never tried again. - tree_mismatch, trace_ingest_failed, no_trace and explorer_crash rule out SAFE. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The walk was recursive and visited shared subterms once per path to them, which is exponential in the depth of a DAG. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…ION off its levels - Node holds one trace element. Tree.add follows and extends a path in a loop, without trace.pop(0). dfs keeps its own stack (the same pre-order), and Tree copies itself without recursing along paths. Traces of a few thousand branches (a StackOverflowError on a symbolic path, deep recursion) used to raise RecursionError. - The executor emits an UNMODELLED_EXCEPTION marker only in the run that throws, so two runs with the same branches had different elements at the same depth, and Tree.add raised "Branch id's dont match" (StringBuilderChars03, StringMiscellaneous03). The marker is no longer a level of the tree. It is kept as a flag on the node after it, and dfs drops the SA walk there, as it did at the marker. check_divergence skips markers in the same way. - A trace that still does not fit (the throwing run goes on in a handler, or another element at the same id) leaves the tree as it is, drops the rest of the trace and records tree_mismatch, which rules out SAFE. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

_extract_variables: one copy (#82 cherry-picks #72's patch). StrategyService.py, Database.py: #82 walks the Database's tree under the lock; visit_tree passes the solved and #74's retired branches, in #72's 'with lock' style. SVCompDriver.py: #82's shallow snapshot of the target node for check_divergence, with #74's solution record and #80's guess flag; the ingest-failure (#72) and stack-overflow (#78) checks read the Database without copying the tree. DTOBuilder.java: #82's FormulaDumper with #71's SymbolRegistry check. DFS.py: #82 logs the per-node line only with an SA graph. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

SVCompDriver.py: - one C1-only option (#82 and #88 both added it), in #88's EXECUTOR_JVM_OPTIONS, with #88's budget-derived heap; - determine_next_step drops a stack-overflow run's violations (#78) before #88's out-of-memory and resource-limit handling, and reads the Database without copying the tree (#82); - a run stopped by the budget is not checked for divergence; #72's no-trace check applies to the others; - every query, first or retry (#74), runs under the budget's interrupt; - #88's cut-short check joins #72's incomplete-search check, and both apply to every SAFE; - the stats keep the pre-check (#73), divergence retries (#74) and resources (#88). DFS.py: the per-node line is at #88's TRACE level, with the CHOICE label. TestcaseStats.py, test_solver_rlimit.py: both sides. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Combining #72, #74, #78, #82 and #88: the driver tests create #88's budget and verdict lock, and #88's tests get the stack-overflow (#78) and copy-free (#82) Database reads and the choice flag (#76). A run reports one verdict (#88), so the incomplete-search subtests reset the flag. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

SVCompDriver.py: one no_trace mechanism. run_testcase decides received_trace once (#89); a run without one is not checked for divergence and, after the output scan, ends UNKNOWN with a single no_trace error, which names the branch #72 used to record it for. A run stopped by the resource budget (#88) is handled before, as in #88. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…property Combining #73 and #89: after round 0 a proof turned the verdict into SAFE, also for a run that never reached main (no trace), which #89 ends UNKNOWN. The proof now applies only when round 0 sent a trace. The no-trace tests get the Database reads, the pre-check and the budget of the other PRs; #72's robustness test no longer expects no_trace for a failed (ERROR) run, which ends UNKNOWN by itself. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Tree.py: #84's loop-state positions are registered at the start of #72's iterative Tree.add; the recursive add_recursive is not brought back. Node/Branch/TraceParser/DataTransferObjects.py, BranchDTO/DTOBuilder.java: both the choice flag (#69/#76) and the loop states (#84). SymbolicTraceHandler.java: addChoiceBranch, checkAndSetLibraryBranch and the loop-state collection side by side. StrategyService.py: the walk on the live tree (#82) reports #84's count of pruned subtrees. SVCompDriver.py: #84's --no-loop-state-matching next to the other state. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…tates to every branch Combining #72, #82 and #84: - #84 pruned a subtree below a repeated loop-head state by returning from the recursive dfs. In #72's iterative walk that return ended the whole walk, so the open branches of every later subtree were never offered, and an exhausted search could report SAFE. It now skips that subtree only (regression test added). - The pruned-subtree count is reset for each walk, as #82 walks the persistent tree instead of a copy. - The choice branches (#69/#76) and library-call branches (#75/#90) take the pending loop-head states too, so a state always goes with the branch right after it, which its position assumes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

nils-loose · 2026-10-20T12:59:36Z

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.

nils-loose and others added 4 commits October 18, 2026 20:45

Extract constraint variables without recursion, each subterm once

58c15ae

The walk was recursive and visited shared subterms once per path to them, which is exponential in the depth of a DAG. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

nils-loose mentioned this pull request Oct 18, 2026

Expected verdicts of PieSegment_true and AlbersProjection_true #63

Open

nils-loose mentioned this pull request Oct 20, 2026

SV-COMP 2027 version #92

Merged

nils-loose closed this Oct 20, 2026

This was referenced Oct 20, 2026

Explorer fails on very large traces (RecursionError building the execution tree) #59

Closed

Explorer hangs when the SV-COMP worker thread raises #62

Closed

Navigation Menu

Repository navigation

Make the explorer robust: iterative tree, lock safety, crashes end UNKNOWN - #72

Make the explorer robust: iterative tree, lock safety, crashes end UNKNOWN#72
nils-loose wants to merge 4 commits into
svcomp27/integrationfrom
fix/explorer-robustness

nils-loose commented Oct 18, 2026

Uh oh!

nils-loose commented Oct 20, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

nils-loose commented Oct 18, 2026

Changes (symbolic-explorer only)

Measurement (nosa, 300 s, sv-comp cfg, mem15g; base = baseline-results.jsonl)

The apachecli_eqchk verdict

Uh oh!

nils-loose commented Oct 20, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant