Repository navigation
Write witnesses from the trace via witnesscreator - #58
Merged
Merged
Conversation
The svcomp26 archive bundled a venv built on Ubuntu 24.04 whose interpreter points at /usr/bin/python3.12; on Ubuntu 26.04 (Python 3.14) the explorer dies with "No module named 'encodings'". Instead of a venv, ship the pinned Python dependencies as plain packages in libs/python/ and run with the system python3 plus PYTHONPATH. libs/ is already in the BenchExec tool-info REQUIRED_PATHS, so no benchexec change is needed. - scripts/build-svcomp-python-runtime.sh: resolves wheels for the target CPython (default 3.14) with pip --target/--python-version, so it runs on any build host (CI stays on ubuntu-24.04). - requirements.txt: bump to versions with cp314 wheels (pydantic_core 2.27.0 has none), matching symbolic-explorer/requirements.txt; drop unused boto. - run-swat.sh: accept --version as well as -v; check the interpreter matches libs/python/PYTHON_VERSION; cap stdout below SV-COMP's 2 MB limit (head + verdict lines + tail, full log kept in out.log). - run_swat.py: launch SymbolicExplorer with sys.executable. - scripts/check-svcomp-package.sh + CI step: verify archive layout and run --version and smoketest.sh in docker.io/ubuntu:26.04 with only the fm-tools required_ubuntu_packages installed. Refs #48 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
SV-COMP 2027 requires Java violation witnesses in the YAML format (version 2.3); WitnessCreator writes them from the executor's witness markers. This supplies what the markers were missing: - [WITNESS] markers now carry the index of the nondet call on its source line (per class, bytecode order = evaluation order), the JVM type descriptor of the value and the class' SourceFile attribute, so WitnessCreator can place the function_return waypoint at the closing parenthesis of the right call, render a typed Java literal and find the file of non-public or inner classes. - A new [WITNESS_TARGET] marker with the uncaught throwable and its stack trace is emitted by Witness.recordTarget, which the surrounding try/catch of main now calls instead of printStackTrace (the trace is still printed). WitnessCreator derives the target waypoint from the innermost frame inside the task sources. - Negative zero is recorded as -0.0 (BigDecimal has no sign for zero). - Harness (lib/witness.py) and competition wrapper (run_swat.py) pass both markers, the task's input paths and the property file to WitnessCreator (--input/--property/--out); sources are no longer copied around. Optional WitnessLint via SWAT_WITNESSLINT. - The package smoketest requires witness.yml with a target waypoint. Requires WitnessCreator >= the YAML-capable release (feat/yaml-witness-2.3); the CI pin WITNESS_CREATOR_VERSION/SHA256 must be bumped with it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The SV-COMP violation witness is built from two things the executor knows: the values returned by Verifier.nondet*() calls (with where each call is) and the throwable that escaped main (with where it was thrown). Until now both were printed as base64 [WITNESS]/[WITNESS_TARGET] markers to stdout and scraped by the driver. They now travel in the TraceDTO: - TraceDTO.nondetReturns: one NondetReturnDTO per nondet call with the Verifier function, the Java type, the value in its witness string form (integers decimal, char as code point, float/double via Java's Float/Double.toString plus the exact IEEE bits, boolean, raw String), the class, its SourceFile attribute, the line and the call index on that line (bytecode = evaluation order; computed by the SV-COMP adapters as before). - TraceDTO.violation: the throwable class and its stack frames innermost first, without JDK/SWAT frames, capped at 32; recorded by Witness.recordTarget from the surrounding try/catch of main (which still prints the stack trace the explorer derives the verdict from). Witness is now a static recorder (one JVM per execution); DTOBuilder attaches its data to every trace. The instrumentation records only the supported Verifier types, so an unsupported nondet (e.g. nondetObject) no longer breaks at the recording call. Tests: WitnessSpec (L0, value rendering and frame filtering) runs with the suite; SvcompWitnessAgentSpec forks a JVM with the agent in solver.mode=PRINT on a small SV-COMP target and checks the trace. It needs the built jar and runs via the new agentTest Gradle task (excluded from test). .gitignore no longer hides the executor's witness packages. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
In SV-COMP mode the explorer now writes witness.yml (format 2.3) and witness.graphml itself, from the trace of the round that produced the VIOLATION verdict, using the witnesscreator package (github.com/SWAT-project/WitnessCreator, pinned in requirements.txt). No stdout parsing for witnesses anymore. - ConstraintRequest carries nondetReturns and violation; the Database keeps the witness data of the latest trace per endpoint. The driver clears it before every round, so only a trace of the violating execution can provide it. - New arguments: --witness-dir (default: witness, relative to the working directory), --witness-input (the task's input files as given to the verifier), --witness-property, --witness-base-dir and --producer-version. - svcomp/WitnessWriter.py maps the trace data onto the witnesscreator API (Task, NondetReturn/Location, Violation/Frame, write_witnesses) and catches everything: the witness is written after the verdict line and can neither break nor delay it. Its time is recorded as witness generation time. - Verdict downgrades are unchanged; a witness is only written for a final VIOLATION. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The competition wrapper no longer runs WitnessCreator: run_swat.py passes the task's input paths, the property file and the version to the explorer (--witness-*), removes a stale witness/ directory before the run and prints witness/witness.yml after a violation verdict. BenchExec collects it via the **/witness.* result-files pattern. The witnesscreator package is pinned to the v1.0.0 tag in the package requirements and installed into libs/python by build-svcomp-python-runtime.sh (built from source as the one pure-Python requirement; SWAT_SVCOMP_WITNESSCREATOR points it at a local checkout or wheel for builds against an unreleased version). The WitnessCreator download, its templates and the WitnessCreator archive directory are gone from the workflow and package-svcomp.sh; the archive check imports witnesscreator and requires the smoketest to leave witness.yml and witness.graphml; the smoketest requires a target waypoint. The benchexec tool-info keeps listing WitnessCreator in REQUIRED_PATHS, which is fine as missing paths are ignored. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The harness passes the task's input directories and property file to the explorer (--witness-*), which writes witness.yml and witness.graphml to the testcase's logs/witness/. lib/witness.py only validates them now: the YAML witness must have exactly one target waypoint (WitnessLint does not check that) and is linted when SWAT_WITNESSLINT names a WitnessLint command (--expectViolationWitness --expectedWitnessVersion 2); the GraphML witness is validated with wit4java as before. Generation time comes from the explorer's timing data. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- NondetReturnDTO.method carries the calling method as name + descriptor (e.g. main([Ljava/lang/String;)V), passed through to witnesscreator's Location.method so the GraphML assumption scope stays java::L<class>;.<method> as before. - A target that ends the JVM with System.exit never reached the instrumented end of main, so its trace was lost: the explorer logged "Target did not explore branch ... as expected" and had to find the violation on another path. The Transformer's shutdown hook now calls Intrinsics.terminateOnShutdown, which sends (HTTP) or prints (PRINT) the traces of thread contexts still active at shutdown; executions that terminated normally have removed their context already. Trace encoding takes the thread id explicitly since the hook runs on another thread. Runtime.halt paths (SWAT errors, Verifier.assume) are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Merged
This was referenced Oct 20, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #57, supersedes #54. The witness data now travels in the executor→explorer trace and the explorer writes the SV-COMP violation witnesses itself with the new Python
witnesscreatorpackage (SWAT-project/WitnessCreator#2). The stdout[WITNESS]/[WITNESS_TARGET]markers, their scraping and the WitnessCreator jar are gone.Depends on #52 (branch is based on it; Ubuntu 26.04 packaging with
libs/python/) and on the WitnessCreatorv1.0.0tag, which bothrequirements.txtpin (witnesscreator @ git+https://github.com/SWAT-project/WitnessCreator@v1.0.0). Until the tag exists, build the archive withSWAT_SVCOMP_WITNESSCREATOR=/path/to/WitnessCreator scripts/build-svcomp-python-runtime.sh …and run the explorer withPYTHONPATH=/path/to/WitnessCreator/src.Changes
TraceDTO.nondetReturns(perVerifier.nondet*()call: function, type, value in the witness string form —Float/Double.toStringplus exact IEEE bits for floats, code point for chars, raw String —, class, calling method, SourceFile, line, call index on the line) andTraceDTO.violation(throwable + frames innermost first, JDK/SWAT frames dropped, cap 32), recorded by the staticWitnessrecorder from the SV-COMP adapters (Emit YAML violation witnesses (format 2.3) #54's call-index logic) and from main's surrounding try/catch, which still prints the stack trace the verdict is derived from. A shutdown hook sends the trace of a still-active execution when the target callsSystem.exit, which used to lose the round. Unsupported nondet types (nondetObject, Support Verifier.nondetObject #53) are not recorded instead of breaking the recording call.VIOLATION(downgrades unchanged)svcomp/WitnessWriter.pycallswitnesscreator.write_witnessesand writeswitness.yml(2.3) +witness.graphmlto--witness-dir(defaultwitness/, relative to cwd). New args--witness-input/--witness-property/--witness-base-dir/--producer-version. Everything is caught and logged; the verdict line is printed first.run_swat.pypasses the task's input paths and property file as given by BenchExec and removes a stalewitness/first (BenchExec collects**/witness.*);witnesscreatoris vendored intolibs/python/bybuild-svcomp-python-runtime.sh; WitnessCreator download/templates/dir removed from the workflow andpackage-svcomp.sh;check-svcomp-package.shimportswitnesscreatorand requires the witness files after the smoketest, which requires a target waypoint. The benchexec tool-info can keepWitnessCreatorinREQUIRED_PATHS.targetwaypoint, WitnessLint viaSWAT_WITNESSLINT, wit4java for GraphML).WitnessSpec(L0, runs withtest),SvcompWitnessAgentSpec(L2, forked agent insolver.mode=PRINT, newagentTesttask)../gradlew :symbolic-executor:test :symbolic-executor:agentTest: 8734 tests, 0 failures.Testing
Local harness, the 40-task campaign of #54 / WitnessCreator#1 (real
witnesscreator1.0.0 fromfeat/python-v1, WitnessLint 2.3, wit4java), vs. the stdout-marker baseline:witness.ymlon violation verdictstargetCharacter_*with chars0→ "Spurious")Every
Verifiertype is covered by the sample (incl.-0.0/NaN handling and two nondet calls on one line); char values are the code points of the inputs of the violating run.Crash cases (constructed tasks):
System.exiton a non-violating path now sends the trace (previously "Target did not explore branch" + luck); a StackOverflowError at the violation is sent as well (not a RuntimeException, so no violation/witness; the ~11k-branch trace stalls the explorer's tree insertion — pre-existing).System.exitinside afinallywhile anAssertionErroris in flight still yields SAFE (pre-existing, the exception never reaches main's handler; not in sv-benchmarks).Package:
scripts/check-svcomp-package.shpasses inubuntu:26.04(Python 3.14.4, witnesscreator 1.0.0 built from the local checkout). BenchExec in the local 2027 competition image (6 tasks × valid-assert / no-runtime-exception, 120 s, upstream tool-info): 6 correct (3 true, 3 false), 0 incorrect, 6 unknown (2 OOM from #51, 2 timeouts, 2 unknown) — same as #52; eachfalserun has exactlywitness/witness.yml+witness.graphmlamong its result files, with the input files as given (/sv-benchmarks/java/...).🤖 Generated with Claude Code