|
| 1 | +--- |
| 2 | +name: svcomp-run |
| 3 | +description: Run the SWAT SV-COMP benchmark harness — parallel scoring runs and single-testcase debug runs — and debug one testcase's verdict via single mode. Use when running/scoring sv-benchmarks locally, reproducing or debugging a single testcase, or interpreting points/verdicts/soundness downgrades. Covers setup, the ./svcomp CLI, config files, log locations, and the per-testcase wall-clock cap. |
| 4 | +--- |
| 5 | + |
| 6 | +# Running & debugging the SV-COMP harness |
| 7 | + |
| 8 | +The custom local harness is in `targets/sv-comp/scripts/`. Per testcase it compiles the target, runs |
| 9 | +SWAT (Java agent + Python explorer over HTTP), scores the verdict, and optionally validates witnesses. |
| 10 | +Drive everything through the `./svcomp` wrapper (it selects the venv Python) **from |
| 11 | +`targets/sv-comp/scripts/`**. This is the *local/custom* runner; the real competition infra uses a |
| 12 | +separate wrapper (`scripts/svcomp-package/run_swat.py`) — don't confuse the two. |
| 13 | + |
| 14 | +## One-time setup |
| 15 | + |
| 16 | +From the repo root, build the agent + native libs (rebuild the jar after ANY executor change — the |
| 17 | +harness runs the jar, not the classes): |
| 18 | +```bash |
| 19 | +./gradlew copyNativeLibs # z3 -> libs/java-library-path |
| 20 | +./gradlew :symbolic-executor:copyJar # -> symbolic-executor/lib/symbolic-executor.jar |
| 21 | +./gradlew :targets:sv-comp:WitnessCreator:shadowJar # only if validating violation witnesses |
| 22 | +``` |
| 23 | +Then in `targets/sv-comp/scripts/`: |
| 24 | +```bash |
| 25 | +python3 -m venv .venv && .venv/bin/pip install -r requirements.txt |
| 26 | +./svcomp setup checkout-benchmarks # SSH clone of SV-Benchmarks (sparse java/) -> ../sv-benchmarks |
| 27 | +./svcomp setup checkout-validator # wit4java, only for witness validation |
| 28 | +``` |
| 29 | + |
| 30 | +## Run — parallel (scoring) |
| 31 | +```bash |
| 32 | +./svcomp test run --mode parallel --workers 50 |
| 33 | +./svcomp test run --categories valid-assert.prp --workers 30 # one property only |
| 34 | +``` |
| 35 | +- Uses `../sv-comp.cfg` (quiet: WARN, no console). Prints per-category points and |
| 36 | + `TOTAL POINTS (ALL CATEGORIES): N`, and saves `results/results_<category>_<timestamp>.json`. |
| 37 | +- `./svcomp analyze results` summarizes the latest results file (context losses / failures). |
| 38 | +- `./svcomp test list [--stats]` enumerates testcases; `./svcomp test validate-ports` checks ports. |
| 39 | + |
| 40 | +## Run — single (one testcase, debug) |
| 41 | +```bash |
| 42 | +./svcomp test run --mode single \ |
| 43 | + --target "autostub/String_public_java_lang_String_java_lang_String_toLowerCase" [--no-witness] |
| 44 | +``` |
| 45 | +- `--target` is the testcase identifier `<group>/<Name>` (matched by suffix against the testcase path). |
| 46 | +- Single mode forces `../swat-debug.cfg` (INFO, console on, shadow-stack + symbolic-execution logging on). |
| 47 | +- `--no-witness` skips witness gen/validation (avoids wit4java); fine when you only care about the verdict. |
| 48 | + |
| 49 | +## Debugging a testcase (single mode) |
| 50 | +1. Run it single-mode; watch the console. SWAT's own lines are prefixed `[SWAT] -->`. |
| 51 | +2. Per-testcase logs land in `logs-debug/<group>/<Name>_<property>/` (`verdict.log`, symbolic-execution |
| 52 | + and shadow-stack logs). Parallel mode instead writes to `logs/`. |
| 53 | +3. The exact forked command is logged, e.g. |
| 54 | + `java -Xmx32g -Dconfig.path=…/swat-debug.cfg -Dexplorer.port=<port> -javaagent:…/symbolic-executor.jar |
| 55 | + -Djava.library.path=… -cp <common>:<z3>:<testcase> -ea Main`. Copy it to run SWAT directly (attach a |
| 56 | + debugger, change flags, add `-Dsolver.mode=PRINT` to dump the TraceDTO without the explorer). |
| 57 | +4. Markers to grep: |
| 58 | + - `[VERDICT <prop>] == TRUE | FALSE | DONT-KNOW` — explorer verdict (safe / violation / unknown). |
| 59 | + - `Context loss recorded!` / `Found symbolic context loss`, `Found ... precision loss` — soundness |
| 60 | + downgrades (a would-be SAFE becomes UNKNOWN). |
| 61 | + - `Invocation of method X in class Y ... cases context loss` (`InvocationHandler.java`) — an unmodeled |
| 62 | + method hit with symbolic input. |
| 63 | + - `Points: P, Case: <expected> -> <got>` — the scored outcome. |
| 64 | + |
| 65 | +## Reading the result |
| 66 | +`Case: <expected_verdict> -> <swat_verdict>`; expected comes from the testcase `.yml` |
| 67 | +(`expected_verdict: true` = no violation → TRUE; `false` = violation reachable → FALSE): |
| 68 | +- match → `Points: 1` (a violation also needs a validated witness for the point unless `--no-witness`); |
| 69 | +- mismatch or unknown → `Points: 0`. |
| 70 | +- A `… -> unknown` caused by context/precision loss is **sound** — SWAT declined rather than answered |
| 71 | + wrong; not a bug. Example: the flagship `…toLowerCase` case scores `violation -> unknown` because no-arg |
| 72 | + `toLowerCase` is locale-dependent and unmodeled, so its result is concretized + context-loss-flagged. |
| 73 | + |
| 74 | +## Per-testcase wall-clock cap (outside the actual run) |
| 75 | +Each testcase's SWAT process is wrapped in `lib/execution.py:run_command_with_timeout` — launched in its |
| 76 | +own session (`start_new_session=True`); on `TimeoutExpired` it `os.killpg(…, SIGKILL)`s the whole tree |
| 77 | +(JVM + Z3) and records `ExecutionStatus.TIMEOUT` → 0 points, never a wrong verdict. This is entirely |
| 78 | +outside the run (SWAT is given no limit; the harness kills it). Default is **900s**; set a shorter |
| 79 | +per-testcase cap here (e.g. 120s), or expose it as a `--timeout` option on `swat test`. Do **not** edit |
| 80 | +`scripts/svcomp-package/run_swat.py` — that is the separate wrapper the competition infra uses. |
| 81 | + |
| 82 | +## Key files |
| 83 | +- `svcomp.py` + `commands/{setup,test,analyze,util}.py` — the click CLI. |
| 84 | +- `lib/execution.py` — `target_execution` (one task), `run_parallel`, `run_single_target`, |
| 85 | + `run_command_with_timeout` (the wall-clock cap), scoring + `save_results`. |
| 86 | +- `lib/command_gen.py` — builds the per-testcase `java … -javaagent … Main` command. |
| 87 | +- `lib/selection.py` — `extract_testcases` (parses the `.yml`s). |
| 88 | +- Configs: `../sv-comp.cfg` (parallel), `../swat-debug.cfg` (single/debug) — differ only in logging. |
| 89 | +- `../sv-benchmarks/java/<group>/<Name>/` — testcase: `Main.java` + `<Name>.yml` (holds `expected_verdict`). |
| 90 | + |
| 91 | +## Gotchas |
| 92 | +- Always run from `targets/sv-comp/scripts/` via `./svcomp` (not `svcomp.py` directly — the wrapper sets |
| 93 | + the venv Python). The older standalone `target_execution.py` (invoked by `run_locally.sh`) is a separate |
| 94 | + path with its own shorter timeout — prefer the `swat test` CLI. |
| 95 | +- Witness validation (wit4java) resolves `python3` via PATH and needs extra venv packages |
| 96 | + (`setuptools`, `pyyaml`, `javalang`, `networkx`); prefix with `PATH="$PWD/.venv/bin:$PATH"` or use |
| 97 | + `--no-witness`. |
| 98 | +- `solver.mode=HTTP`: the explorer runs as a per-testcase HTTP server on an allocated port; parallel runs |
| 99 | + use many ports at once. |
| 100 | +- Rebuild `:symbolic-executor:copyJar` after executor changes, or you'll score the old jar. |
0 commit comments