Move the property pre-check to cfg-extraction; prune under no-runtime-exception (#93)

.github/workflows/gradle.yml

@@ -28,11 +28,27 @@ jobs:
       run: ./gradlew copyNativeLibs
     - name: Build
       run: ./gradlew --no-daemon build -x test
+    # The property pre-check (svcomp/PropertyPreCheck.py) is part of cfg-extraction's static
+    # pre-analysis; SWAT pins the cfg-extraction ref it ships in cfg-extraction.ref.
+    - name: Read pinned cfg-extraction ref
+      id: cfg
+      run: echo "ref=$(tr -d '[:space:]' < cfg-extraction.ref)" >> "${GITHUB_OUTPUT}"
+    - name: Check out cfg-extraction
+      uses: actions/checkout@v7
+      with:
+        repository: SWAT-project/cfg-extraction
+        ref: ${{ steps.cfg.outputs.ref }}
+        path: cfg-extraction
+    - name: Build the property pre-check
+      working-directory: cfg-extraction
+      run: ./gradlew --no-daemon precheckJar
     - name: Upload JARs
       uses: actions/upload-artifact@v7
       with:
         name: release-jars-${{ github.sha }}
-        path: symbolic-executor/lib/symbolic-executor.jar
+        path: |
+          symbolic-executor/lib/symbolic-executor.jar
+          cfg-extraction/build/libs/cfg-extractor-precheck.jar
         if-no-files-found: error
         retention-days: 1
 

CLAUDE.md

@@ -25,6 +25,9 @@ and used in `strategy/DFS.py`.
   `[DFS] SA desync`, stops the walk on that path and records `sa_desync`, which turns SAFE into
   UNKNOWN. When the walk has no node, `SAGraph.resync` finds the next branch by key, with the call
   stack rebuilt from the trace. The extractor computes the same keys; change both together.
+- **Guards that cannot raise:** a phantom guard the extractor marks `cannotRaise` (the property
+  pre-check proves its implicit exception cannot happen, cfg-extraction `RaiseSites`) gets a dead
+  node as its exception side in `SAGraph.load_json_graph`, so that side is never interesting.
 - **Concrete branches count:** they are in the tree too. Filtering to symbolic branches happens
   after `dfs`.
 - **Walker giving up is safe:** when `walk_till_branch` returns `None`, the walker has no
@@ -38,9 +41,24 @@ and used in `strategy/DFS.py`.
 - **`<clinit>` and callbacks are masked:** static initializers are not in the graph, and neither is
   application code that library code calls back (the executor flags those branches `callback`,
   see `ShadowContext.inCallback`), so the walk is frozen inside them.
-- **Asserts are only the first target:** pruning aims at assertion points for now because they
-  are easy to test (SV-COMP's valid-assert). Later targets include shell calls, SQL statement
-  building and uncaught exceptions, so prefer changes that work for any kind of target point.
+- **Targets per property:** pruning aims at the graph's target points for the property being
+  checked (`StaticPreAnalysis.SA_TARGETS`): assertion points (`assertionPointIds`) under
+  valid-assert, and under no-runtime-exception the sites that may raise a RuntimeException plus the
+  `uncaught[T]` nodes of RuntimeException types (`runtimeExceptionPointIds`, from the property
+  pre-check's value analysis, cfg-extraction `RaiseSites`). `SANode.isAssert` marks a target point
+  of either kind. Later targets include shell calls and SQL statement building, so prefer changes
+  that work for any kind of target point.
+  - **No-runtime-exception is opt-in in the harness** (`svcomp test run --sa-no-runtime-exception`;
+    the explorer prunes whenever it gets `--sa-path`). On the 736 tasks (300 s, 2026-10-24) it is
+    sound (no false SAFE) and cuts queries on the solved SAFE tasks by a third, but solves nothing
+    new: the pre-check already proves 426 tasks and the extractor costs 3 to 6 s per task. (Its
+    first run also lost 9 SAFE to desyncs, fixed since: see SWAT helpers below.)
+- **SWAT helpers and `nondetObject` in the walk:** branches taken inside SWAT's own helpers (the
+  reference-comparison rewrite `UtilInstrumented.refEquals`) are flagged like callbacks
+  (`ShadowContext.inSwatHelper`), since how many there are depends on runtime types; the graph has
+  none of them. `Verifier.nondetObject(type, factory)`, which the executor runs as
+  `factory.createObject()`, is expanded and keyed as that call by the extractor. Before these, 73 of
+  978 valid-assert tasks had an SA desync.
 - **Exceptions the graph does not model** (null dereferences, casts, library calls, Errors): the
   extractor gives them pseudo types (`?Exception`, `?Error`) whose escapes SAGraph treats as
   caught by any handler listed for them (`unknown_handlers`), so paths into such handlers stay
@@ -82,7 +100,7 @@ spot a walk that has fallen out of step with the execution.
 
 ```bash
 cd targets/sv-comp && ./scripts/svcomp test run --mode parallel --no-witness --categories valid-assert.prp
-./scripts/svcomp test run --help      # --suite, --limit-nr-tests, --no-sa, --parallel-sa, --sa-rank-distance, --solver-rlimit, --testcase-timeout-s ...
+./scripts/svcomp test run --help      # --suite, --limit-nr-tests, --no-sa, --parallel-sa, --sa-rank-distance, --search-order, --solver-rlimit, --testcase-timeout-s ...
 ```
 
 - **Duration:** a full valid-assert run takes about 40 min with the default 900 s timeout, and
@@ -105,6 +123,24 @@ cd targets/sv-comp && ./scripts/svcomp test run --mode parallel --no-witness --c
   10 s). A branch that runs out is retried later with 5x the limit, after the cheaper queries; a
   lone retry runs unlimited. Off by default. Each query's time and rlimit use are in the
   `[SOLVER]` debug lines of `explorer.log`.
+- **Property pre-check:** before round 0, `svcomp/PropertyPreCheck.py` runs cfg-extraction's
+  `cfg-extractor-precheck.jar` (`de.uzl.its.cfg.staticcheck.ExceptionFreedomCheck`, an ASM pass,
+  about 0.2 s). A proof of no-runtime-exception or valid-assert gives SAFE without exploring
+  (round 0 still runs as a cross-check). The jar comes from `--precheck-jar`, else from next to
+  `symbolic-explorer/` (the SV-COMP archive), else `../cfg-extraction/build/libs/`; without it the
+  check is skipped (`missing_jar`). CI builds it at the cfg-extraction tag in `cfg-extraction.ref`
+  and the archive ships it as `cfg-extraction/cfg-extractor-precheck.jar`. Its soundness gate is
+  `cfg-extraction/scripts/precheck_gate.py` (0 contradictions over sv-benchmarks).
+- **Search order:** `--search-order` picks which open branch is flipped next (`StrategyService`):
+  `dfs` (default), `shallow`, `coverage` (sides no trace took yet, then the shallowest),
+  `coverage-dfs`, `generational`. Plain DFS keeps unrolling input-parsing loops one char per round
+  with ever larger queries; `coverage` found 6 more violations than `dfs` on 978 valid-assert tasks
+  (300 s, no SA) and lost none. The order changes only how fast violations are found, not SAFE.
+- **Int/string queries:** `solver/Int2BvLifting.py` rewrites the executor's bit-vector ints where
+  they meet string lengths, indices and char codes into Integer arithmetic before solving, and
+  solves bit-vector inputs used only as numbers over Integer stand-ins (`lift_inputs`, mapped back
+  to the inputs by `Z3Handler.map_lifted_inputs`). Mixed `int_to_bv`/`ubv_to_int` queries are
+  what makes Z3 slow on string code.
 - **Benchmarks:** `targets/sv-comp/sv-benchmarks/` is a sparse checkout of `java/` from
   SWAT-project/SV-Benchmarks, which mirrors upstream sv-benchmarks with precompiled `.class` files;
   `.last_sv_commit` names the upstream commit. Older suites are kept next to it as

cfg-extraction.ref

@@ -0,0 +1 @@
+v0.1.0

scripts/check-svcomp-package.sh

@@ -27,7 +27,7 @@ top_dirs="$(unzip -Z1 "$ZIP_PATH" | cut -d/ -f1 | sort -u)"
 check_dir="$(mktemp -d "${TMPDIR:-/tmp}/swat-svcomp-check.XXXXXX")"
 unzip -q "$ZIP_PATH" -d "$check_dir"
 tool_dir="${check_dir}/${top_dirs}"
-for f in LICENSE README.md smoketest.sh run-swat.sh libs/python/PYTHON_VERSION; do
+for f in LICENSE README.md smoketest.sh run-swat.sh libs/python/PYTHON_VERSION cfg-extraction/cfg-extractor-precheck.jar; do
   [[ -f "${tool_dir}/${f}" ]] || fail "missing ${f} in archive root ${top_dirs}/"
 done
 [[ -s "${tool_dir}/THIRD-PARTY-LICENSES.md" ]] || fail "missing or empty THIRD-PARTY-LICENSES.md in archive root ${top_dirs}/"
@@ -44,6 +44,9 @@ docker run --rm -v "${tool_dir}:/tool" -w /tool -e UBUNTU_PACKAGES="$UBUNTU_PACK
   echo "version: ${version}"
   [ -n "$version" ] && [ "$(printf "%s\n" "$version" | wc -l)" -eq 1 ] || { echo "error: --version must print one non-empty line" >&2; exit 1; }
   [ "$(./run-swat.sh -v)" = "$version" ] || { echo "error: -v and --version differ" >&2; exit 1; }
+  precheck="$(java -cp cfg-extraction/cfg-extractor-precheck.jar de.uzl.its.cfg.staticcheck.ExceptionFreedomCheck smoketest/common smoketest | tail -n 1)"
+  echo "property pre-check: ${precheck}"
+  case "$precheck" in *"\"tool\": \"cfg-extraction\""*) ;; *) echo "error: the property pre-check did not run" >&2; exit 1;; esac
   ./smoketest.sh > smoketest.out 2>&1 || { cat smoketest.out; exit 1; }
   echo "smoketest stdout: $(wc -c < smoketest.out) bytes"
   [ -f witness/witness.yml ] && [ -f witness/witness.graphml ] || { echo "error: smoketest left no witness/witness.yml + witness.graphml" >&2; exit 1; }

scripts/package-svcomp.sh

@@ -10,6 +10,9 @@ set -euo pipefail
 #
 # - symbolic-executor/lib/symbolic-executor.jar, or symbolic-executor.jar at the
 #   root (actions/upload-artifact drops the directories of a single-file upload)
+# - cfg-extraction/build/libs/cfg-extractor-precheck.jar, or cfg-extractor-precheck.jar
+#   at the root: the property pre-check, built from cfg-extraction at the ref pinned in
+#   cfg-extraction.ref (./gradlew precheckJar)
 #
 # Set SWAT_SVCOMP_PYTHON_DIR to the Python dependency directory produced by
 # scripts/build-svcomp-python-runtime.sh (it includes the witnesscreator
@@ -131,6 +134,12 @@ EXECUTOR_JAR="$(first_artifact_file \
   symbolic-executor/build/libs/symbolic-executor-all.jar)"
 copy_artifact_file "$EXECUTOR_JAR" "$PACKAGE_DIR/symbolic-executor/lib/symbolic-executor.jar"
 
+# The property pre-check from cfg-extraction (svcomp/PropertyPreCheck.py, --precheck-jar).
+PRECHECK_JAR="$(first_artifact_file \
+  cfg-extraction/build/libs/cfg-extractor-precheck.jar \
+  cfg-extractor-precheck.jar)"
+copy_artifact_file "$PRECHECK_JAR" "$PACKAGE_DIR/cfg-extraction/cfg-extractor-precheck.jar"
+
 copy_tree_files symbolic-explorer "$PACKAGE_DIR/symbolic-explorer"
 
 install_z3_runtime_file bin/z3 0755

scripts/svcomp-package/README.md

@@ -9,6 +9,8 @@ Important entry points:
 - `compile-target.sh`: helper used by `run_swat.py` to compile Java benchmark sources.
 - `smoketest.sh`: runs SWAT on the bundled smoke-test target.
 - `sv-comp.cfg`: SWAT configuration for SV-COMP mode.
+- `cfg-extraction/cfg-extractor-precheck.jar`: the static property pre-check (from
+  cfg-extraction), which can prove no-runtime-exception or valid-assert before exploring.
 - `THIRD-PARTY-LICENSES.md`: bundled third-party components and their licenses.
 
 Requirements (SV-COMP 2027 environment, Ubuntu 26.04): `python3` (3.14) and

scripts/svcomp-package/run_swat.py

@@ -111,6 +111,7 @@ def generate_command(args, property_file: str, property_path: str, input_paths:
     base_command = [ sys.executable, "-u", os.path.join(SCRIPT_DIR, 'symbolic-explorer', 'SymbolicExplorer.py'),
                      "-prp", property_file,
                      "--agent", agent_path,
+                     "--precheck-jar", os.path.join(SCRIPT_DIR, 'cfg-extraction', 'cfg-extractor-precheck.jar'),
                      "--config", config_path,
                      "-z3", library_path,
                      "--logdir", LOG_DIR,

scripts/svcomp-package/third_party_licenses.py

@@ -5,7 +5,8 @@
 
 Inputs, all read from the package itself:
 - META-INF/swat-third-party.json inside symbolic-executor/lib/symbolic-executor.jar
-  (written by the thirdPartyList Gradle task: the Java components shaded into the jar);
+  (written by the thirdPartyList Gradle task: the Java components shaded into the jar), and the
+  same file inside cfg-extraction/cfg-extractor-precheck.jar (cfg-extraction's precheckJar task);
 - libs/java-library-path/z3-LICENSE.txt (LICENSE.txt of the bundled Z3 release);
 - every libs/python/*.dist-info (bundled Python packages and the license files they ship).
 
@@ -23,6 +24,7 @@
 
 LICENSE_DIR = Path(__file__).resolve().parent / "licenses"
 JAR = "symbolic-executor/lib/symbolic-executor.jar"
+PRECHECK_JAR = "cfg-extraction/cfg-extractor-precheck.jar"
 JAR_LIST = "META-INF/swat-third-party.json"
 Z3_LICENSE = "libs/java-library-path/z3-LICENSE.txt"
 PYTHON_DIR = "libs/python"
@@ -65,15 +67,15 @@ def spdx_of(name):
     return JAVA_LICENSES.get(key.lower())
 
 
-def java_components(pkg):
-    jar = pkg / JAR
+def java_components(pkg, jar_path=JAR):
+    jar = pkg / jar_path
     if not jar.is_file():
-        fail(f"missing {JAR}")
+        fail(f"missing {jar_path}")
     with zipfile.ZipFile(jar) as zf:
         try:
             entries = json.loads(zf.read(JAR_LIST))
         except KeyError:
-            fail(f"{JAR} has no {JAR_LIST}; build it with the thirdPartyList Gradle task")
+            fail(f"{jar_path} has no {JAR_LIST}; build it with the thirdPartyList (or precheckJar) Gradle task")
     comps = []
     for e in entries:
         coord = f"{e['group']}:{e['name']}"
@@ -167,6 +169,7 @@ def main():
         sys.exit(__doc__)
     pkg = Path(sys.argv[1])
     java = java_components(pkg)
+    precheck = java_components(pkg, PRECHECK_JAR)
     z3_license = pkg / Z3_LICENSE
     if not z3_license.is_file():
         fail(f"native Z3: missing license text {Z3_LICENSE}")
@@ -191,6 +194,10 @@ def main():
         "",
         table(java),
         "",
+        f"## Java (bundled in `{PRECHECK_JAR}`, the property pre-check from cfg-extraction)",
+        "",
+        table(precheck),
+        "",
         "## Native (`libs/java-library-path/`)",
         "",
         table(native),
@@ -204,8 +211,8 @@ def main():
         "### Java",
         "",
     ]
-    for spdx in sorted({i for c in java for i in c["ids"]}):
-        users = ", ".join(c["name"] for c in java if spdx in c["ids"])
+    for spdx in sorted({i for c in java + precheck for i in c["ids"]}):
+        users = ", ".join(dict.fromkeys(c["name"] for c in java + precheck if spdx in c["ids"]))
         out += [f"#### {spdx}", "", f"Used by: {users}", "",
                 block((LICENSE_DIR / f"{spdx}.txt").read_text(encoding="utf-8")), ""]
     out += ["### Native", "", "#### Z3", "", block(z3_license.read_text(encoding="utf-8")), "",
@@ -215,7 +222,7 @@ def main():
             out += [f"#### {c['name']} {c['version']}: {fname}", "", block(text), ""]
     target = pkg / "THIRD-PARTY-LICENSES.md"
     target.write_text("\n".join(out), encoding="utf-8")
-    print(f"Wrote {target}: {len(java)} Java, {len(native)} native, {len(python)} Python components")
+    print(f"Wrote {target}: {len(java) + len(precheck)} Java, {len(native)} native, {len(python)} Python components")
 
 
 if __name__ == "__main__":