SV-COMP: explorer-owned per-testcase stats.json + runs/ layout & analysis (#25)

[nils-loose]

Addresses all five parts of #25 by making the explorer the single owner of per-testcase output and consolidating the harness onto the svcomp CLI. Two commits:

550d304 — explorer-owned stats.json via trace metadata (executor + explorer)

• The executor no longer writes stats_<id>.json. It accumulates missing invocations (each flagged when it caused symbolic context loss) in StatsStorage and ships them with the trace (TraceDTO.missingInvocations / new InvocationDTO).
• The explorer accumulates this per testcase on the Tree and, at testcase completion, writes one consolidated stats.json to the log dir (same hook as timing_data.json): verdict, soundness flags, the missing-invocation superset and the explicit context-loss subset.
• Errors can't ride the trace (in sv-comp every error path halts the JVM before the trace is sent), so they're surfaced from the executor stdout markers the explorer already scans ([SWAT Exception] / internal SWAT AssertionError) and recorded into stats.json.
• Removes the now-dead executor error chain (StatsStorage.errors, recordException, ErrorRecord) and the unused StatsStorage.entrypoint.

d2c6708 — runs/run_<ts>/ layout, stats.json analysis, CLI consolidation (Python harness)

• Run folder structure (part 4): each svcomp test run writes its per-testcase logs and aggregated results under one timestamped runs/run_<ts>/{logs,results} dir (runs-debug/<target>/run_<ts>/logs for debug configs). Old runs are preserved (part 2); a single run timestamp is threaded through command generation + result writing.
• Analysis on stats.json (parts 1, 3): rewrote lib/analysis/context_loss.py to read each testcase's consolidated stats.json instead of scraping explorer.log / stats_*.json. Reports the missing-invocation superset and its authoritative context-loss subset — fixing the old regex inconsistency.
• Scoring summary (part 5): svcomp analyze results prints a Correct/Failed/Unk/Error/Timeout table per category and overall.
• Consolidation: run_locally.sh and ci_run.sh now invoke ./svcomp test run; the 9 dead legacy top-level duplicates are removed (target_execution.py, command_generation.py, analyse_ctx_loss.py, analyze_by_correctness.py, compare_results.py, target_selection.py, witness_validation.py, util.py, dtypes.py). README + .gitignore updated.

Test plan

• Rebuilt the agent jar; ran sv-comp targets via the CLI:
  • clean violation (autostub/Boolean…compare) → correct stats.json, no stats_*.json anywhere.
  • context-loss target (Math.getExponent(double)) → verdict correctly downgraded to UNKNOWN; symbolic_context_loss=true, missing_invocations[0].context_loss=true count=2 (merged across traces), context_loss_methods=["java/lang/Math/getExponent:(D)I"].
• Parallel CLI run produced runs/run_<ts>/{logs,results} with stats.json per testcase; svcomp analyze results rendered the scoring summary + superset/subset.
• Unit-tested the explorer DTO/merge/assembly and the classify() buckets (Correct/Failed/Unk/Error/Timeout, with precedence).

Notes / out of scope

• The full Java unit suite was not run (it has ~1670 known-failing value tests unrelated to this change); relied on grep-for-removed-APIs, clean compiles, and end-to-end smoke runs.
• lib/analysis/{timing,failures,performance}.py still default to the old flat logs/ when called standalone (the active flow passes the run dir explicitly).
• sv-comp.cfg:8 logging.invocations=true is a pre-existing no-op (Config reads logging.statistics) — flagged, not changed.

Closes #25.

🤖 Generated with Claude Code