diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 2ca2d812..a85369b6 100644 --- a/.github/workflows/gradle.yml +++ b/.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 diff --git a/CLAUDE.md b/CLAUDE.md index a9da5d96..38b98d6a 100644 --- a/CLAUDE.md +++ b/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`. - **`` 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 diff --git a/cfg-extraction.ref b/cfg-extraction.ref new file mode 100644 index 00000000..b82608c0 --- /dev/null +++ b/cfg-extraction.ref @@ -0,0 +1 @@ +v0.1.0 diff --git a/scripts/check-svcomp-package.sh b/scripts/check-svcomp-package.sh index b20e1668..2aec8f42 100755 --- a/scripts/check-svcomp-package.sh +++ b/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; } diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh index e3fdaa64..00c5c9fd 100755 --- a/scripts/package-svcomp.sh +++ b/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 diff --git a/scripts/svcomp-package/README.md b/scripts/svcomp-package/README.md index 1708ae16..32161344 100644 --- a/scripts/svcomp-package/README.md +++ b/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 diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py index 052d9a88..12909aad 100755 --- a/scripts/svcomp-package/run_swat.py +++ b/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, diff --git a/scripts/svcomp-package/third_party_licenses.py b/scripts/svcomp-package/third_party_licenses.py index 91627252..2cc23eb7 100755 --- a/scripts/svcomp-package/third_party_licenses.py +++ b/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__": diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/AbsValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/AbsValue.java deleted file mode 100644 index 5fb9b97f..00000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/AbsValue.java +++ /dev/null @@ -1,226 +0,0 @@ -package de.uzl.its.swat.staticcheck; - -import java.util.Objects; -import org.objectweb.asm.tree.analysis.Value; - -/** - * Abstract value of a local variable or operand stack slot for {@link ExceptionFreedomCheck}. - * - *

Every fact is an over-approximation of the concrete values the slot can hold: {@code BOTTOM} - * holds none (not reached yet), {@code NULL} only null, {@code NONNULL} only references, {@code REF} - * references or null, {@code PRIM} a primitive and {@code UNKNOWN} anything. The optional facts - * narrow this further and are dropped (set to null) whenever two values with different facts meet. - */ -final class AbsValue implements Value { - - enum Kind { - BOTTOM, - PRIM, - NULL, - NONNULL, - REF, - UNKNOWN - } - - final Kind kind; - final int size; - /** PRIM: the int or long value, if it is a known constant. */ - final Long constant; - /** NONNULL array: its length, if it is a known constant. */ - final Integer length; - /** - * NONNULL array: its length equals the number of constants of this enum class. PRIM: the value - * is that number. - */ - final String lengthOf; - /** PRIM: the value is the ordinal of a constant of this enum class (0 <= v < its constant count). */ - final String ordinalOf; - /** NONNULL: the runtime class of the object (internal name, or descriptor for arrays). */ - final String exactType; - /** NULL/NONNULL/REF: a type every non-null value is an instance of. */ - final String staticType; - /** The receiver of the current instance method, unchanged since method entry. */ - final boolean isThis; - /** The slot may hold the receiver of the current instance method (a may-alias fact, kept by joins). */ - final boolean mayBeThis; - /** - * The exception caught by the handler with this index in the method's try-catch list (-1: not a - * caught exception, or not known to be one). - */ - final int caughtBy; - - static final AbsValue UNKNOWN1 = new AbsValue(Kind.UNKNOWN, 1, null, null, null, null, null, null, false); - static final AbsValue PRIM1 = prim(1); - static final AbsValue PRIM2 = prim(2); - static final AbsValue NULL = new AbsValue(Kind.NULL, 1, null, null, null, null, null, null, false); - - AbsValue(Kind kind, int size, Long constant, Integer length, String lengthOf, String ordinalOf, - String exactType, String staticType, boolean isThis) { - this(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, isThis, -1); - } - - AbsValue(Kind kind, int size, Long constant, Integer length, String lengthOf, String ordinalOf, - String exactType, String staticType, boolean isThis, int caughtBy) { - this(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, isThis, caughtBy, isThis); - } - - private AbsValue(Kind kind, int size, Long constant, Integer length, String lengthOf, String ordinalOf, - String exactType, String staticType, boolean isThis, int caughtBy, boolean mayBeThis) { - this.mayBeThis = mayBeThis || isThis; - this.kind = kind; - this.size = size; - this.constant = constant; - this.length = length; - this.lengthOf = lengthOf; - this.ordinalOf = ordinalOf; - this.exactType = exactType; - this.staticType = staticType; - this.isThis = isThis; - this.caughtBy = caughtBy; - } - - static AbsValue prim(int size) { - return new AbsValue(Kind.PRIM, size, null, null, null, null, null, null, false); - } - - static AbsValue constant(int size, long value) { - return new AbsValue(Kind.PRIM, size, value, null, null, null, null, null, false); - } - - static AbsValue bottom(int size) { - return new AbsValue(Kind.BOTTOM, size, null, null, null, null, null, null, false); - } - - static AbsValue ref(String staticType) { - return new AbsValue(Kind.REF, 1, null, null, null, null, null, staticType, false); - } - - static AbsValue nonNull(String staticType) { - return new AbsValue(Kind.NONNULL, 1, null, null, null, null, null, staticType, false); - } - - /** A non-null object whose runtime class is known (a fresh allocation, a String literal, ...). */ - static AbsValue exact(String type) { - return new AbsValue(Kind.NONNULL, 1, null, null, null, null, type, type, false); - } - - static AbsValue array(String type, Integer length, String lengthOf) { - return new AbsValue(Kind.NONNULL, 1, null, length, lengthOf, null, type, type, false); - } - - AbsValue withThis() { - return new AbsValue(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, true); - } - - static AbsValue caught(String type, int handler) { - return new AbsValue(Kind.NONNULL, 1, null, null, null, null, null, type, false, handler); - } - - /** The same value without the facts that only hold where it was computed (receiver, handler). */ - AbsValue escaped() { - if (!mayBeThis && caughtBy < 0) return this; - return new AbsValue(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, false, -1); - } - - AbsValue withOrdinalOf(String enumType) { - return new AbsValue(kind, size, constant, length, lengthOf, enumType, exactType, staticType, isThis, caughtBy, mayBeThis); - } - - AbsValue withLengthOf(String enumType) { - return new AbsValue(kind, size, constant, length, enumType, ordinalOf, exactType, staticType, isThis, caughtBy, mayBeThis); - } - - boolean isBottom() { - return kind == Kind.BOTTOM; - } - - boolean isNull() { - return kind == Kind.NULL; - } - - /** No concrete value of this slot can be null (BOTTOM holds no value at all). */ - boolean isNonNull() { - return kind == Kind.NONNULL || kind == Kind.BOTTOM; - } - - boolean isReference() { - return kind == Kind.NULL || kind == Kind.NONNULL || kind == Kind.REF; - } - - @Override - public int getSize() { - return size; - } - - /** The least upper bound of two values. */ - static AbsValue join(AbsValue a, AbsValue b) { - AbsValue j = joinFacts(a, b); - if ((a.mayBeThis || b.mayBeThis) && !j.mayBeThis) { - j = new AbsValue(j.kind, j.size, j.constant, j.length, j.lengthOf, j.ordinalOf, j.exactType, j.staticType, - j.isThis, j.caughtBy, true); - } - return j; - } - - private static AbsValue joinFacts(AbsValue a, AbsValue b) { - if (a.equals(b)) return a; - if (a.isBottom()) return b; - if (b.isBottom()) return a; - if (a.size != b.size) return UNKNOWN1; - if (a.kind == Kind.PRIM && b.kind == Kind.PRIM) { - return new AbsValue(Kind.PRIM, a.size, same(a.constant, b.constant), null, - same(a.lengthOf, b.lengthOf), same(a.ordinalOf, b.ordinalOf), null, null, false); - } - if (a.isReference() && b.isReference()) { - boolean thisRef = a.isThis && b.isThis; - if (a.kind == Kind.NULL || b.kind == Kind.NULL) { - AbsValue other = a.kind == Kind.NULL ? b : a; - return new AbsValue(other.kind == Kind.NULL ? Kind.NULL : Kind.REF, 1, null, null, null, null, - null, other.staticType, false); - } - if (a.kind == Kind.NONNULL && b.kind == Kind.NONNULL) { - return new AbsValue(Kind.NONNULL, 1, null, same(a.length, b.length), same(a.lengthOf, b.lengthOf), - null, same(a.exactType, b.exactType), same(a.staticType, b.staticType), thisRef, - a.caughtBy == b.caughtBy ? a.caughtBy : -1); - } - return new AbsValue(Kind.REF, 1, null, null, null, null, null, same(a.staticType, b.staticType), false); - } - return a.size == 1 ? UNKNOWN1 : new AbsValue(Kind.UNKNOWN, a.size, null, null, null, null, null, null, false); - } - - private static T same(T a, T b) { - return Objects.equals(a, b) ? a : null; - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (!(o instanceof AbsValue)) return false; - AbsValue v = (AbsValue) o; - return kind == v.kind && size == v.size && isThis == v.isThis && mayBeThis == v.mayBeThis && caughtBy == v.caughtBy - && Objects.equals(constant, v.constant) - && Objects.equals(length, v.length) && Objects.equals(lengthOf, v.lengthOf) - && Objects.equals(ordinalOf, v.ordinalOf) && Objects.equals(exactType, v.exactType) - && Objects.equals(staticType, v.staticType); - } - - @Override - public int hashCode() { - return Objects.hash(kind, size, constant, length, lengthOf, ordinalOf, exactType, staticType, isThis, mayBeThis, caughtBy); - } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder(kind.name()); - if (constant != null) sb.append('=').append(constant); - if (length != null) sb.append(" len=").append(length); - if (lengthOf != null) sb.append(" lenOf=").append(lengthOf); - if (ordinalOf != null) sb.append(" ordOf=").append(ordinalOf); - if (exactType != null) sb.append(" exact=").append(exactType); - else if (staticType != null) sb.append(" type=").append(staticType); - if (isThis) sb.append(" this"); - else if (mayBeThis) sb.append(" maybe-this"); - if (caughtBy >= 0) sb.append(" caught#").append(caughtBy); - return sb.toString(); - } -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/ExceptionFreedomCheck.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/ExceptionFreedomCheck.java deleted file mode 100644 index bf750356..00000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/ExceptionFreedomCheck.java +++ /dev/null @@ -1,920 +0,0 @@ -package de.uzl.its.swat.staticcheck; - -import java.nio.file.Path; -import java.util.*; -import org.objectweb.asm.ConstantDynamic; -import org.objectweb.asm.Handle; -import org.objectweb.asm.Opcodes; -import org.objectweb.asm.Type; -import org.objectweb.asm.tree.*; -import org.objectweb.asm.tree.analysis.Analyzer; -import org.objectweb.asm.tree.analysis.AnalyzerException; -import org.objectweb.asm.tree.analysis.Frame; - -/** - * A conservative static check that a program can never end with an uncaught RuntimeException, - * the SV-COMP no-runtime-exception property. If it succeeds, the property holds on every - * execution; if it fails, nothing is known. - * - *

The program is every class on its classpath, entered through {@code Main.main}. The check - * proves that no RuntimeException can escape {@code main} or a static initializer that may run: - * - *

- * - *

Errors (AssertionError, StackOverflowError, OutOfMemoryError, linkage errors, ...) are not - * RuntimeExceptions and are not considered. Enum classes are assumed to be compiled from Java - * source, so the ordinal of a constant is below the number of constants. - */ -public final class ExceptionFreedomCheck implements FactInterpreter.Facts, Opcodes { - - static final String MAIN_CLASS = "Main"; - static final String MAIN_DESC = "([Ljava/lang/String;)V"; - private static final int MAX_ROUNDS = 100; - - /** - * The outcome: whether the program is proven free of uncaught RuntimeExceptions, whether it is - * proven to never create an AssertionError (so no assert can fail), and why not. - */ - public static final class Result { - public final boolean exceptionFree; - public final String reason; - public final boolean assertionFree; - public final String assertionReason; - - Result(boolean exceptionFree, String reason, boolean assertionFree, String assertionReason) { - this.exceptionFree = exceptionFree; - this.reason = reason; - this.assertionFree = assertionFree; - this.assertionReason = assertionReason; - } - - static Result neither(String reason) { - return new Result(false, reason, false, reason); - } - } - - private final Program program; - private final Map fieldFacts = new HashMap<>(); - private final Map parameterFacts = new HashMap<>(); - private final Map returnFacts = new HashMap<>(); - private final Set initializedBeforeRead = new HashSet<>(); - private final Map[]> frames = new HashMap<>(); - private final Map targetCache = new IdentityHashMap<>(); - private final Set unknownTargets = Collections.newSetFromMap(new IdentityHashMap<>()); - private Program.Method entry; - private boolean changed; - - ExceptionFreedomCheck(Program program) { - this.program = program; - } - - public static Result check(List classpath) { - try { - return new ExceptionFreedomCheck(new Program(classpath)).run(); - } catch (Exception | StackOverflowError e) { - return Result.neither("analysis failed: " + e); - } - } - - Result run() throws AnalyzerException { - if (program.unsupportedClasspath() != null) return Result.neither(program.unsupportedClasspath()); - entry = program.method(MAIN_CLASS, "main", MAIN_DESC); - if (entry == null || !entry.isStatic() || !entry.hasCode()) return Result.neither("no Main.main"); - - computeInitializedBeforeRead(); - for (ClassNode c : program.appClasses()) { - for (FieldNode f : c.fields) { - String key = c.name + "." + f.name + ":" + f.desc; - Type t = Type.getType(f.desc); - if (t.getSort() != Type.OBJECT && t.getSort() != Type.ARRAY) { - fieldFacts.put(key, AbsValue.prim(t.getSize())); - continue; - } - // The JVM only applies a ConstantValue attribute to static fields. - if (f.value instanceof String && (f.access & ACC_STATIC) != 0) fieldFacts.put(key, AbsValue.exact("java/lang/String")); - else if (!initializedBeforeRead.contains(key)) fieldFacts.put(key, AbsValue.NULL); - } - } - - // Facts: least fixpoint, from "no value" upwards. - int round = 0; - do { - if (++round > MAX_ROUNDS) return Result.neither("facts did not converge"); - changed = false; - for (Program.Method m : program.methods()) { - if (!m.hasCode()) continue; - Frame[] f = new Analyzer<>(new FactInterpreter(this, m)).analyze(m.owner.name, m.node); - frames.put(m.key, f); - collectFacts(m, f); - } - } while (changed); - - // May-throw: least fixpoint over the call graph. - Map mayThrow = new LinkedHashMap<>(); - boolean grew; - do { - grew = false; - for (Program.Method m : program.methods()) { - if (!m.hasCode() || mayThrow.containsKey(m.key)) continue; - String reason = escapingException(m, mayThrow); - if (reason != null) { - mayThrow.put(m.key, reason); - grew = true; - } - } - } while (grew); - - List roots = new ArrayList<>(); - roots.add(entry); - roots.addAll(initializers(MAIN_CLASS)); - for (ClassNode c : program.appClasses()) { - // The finalizer thread may run it on any unreachable object, even one whose constructor - // threw before it assigned its fields. - Program.Method fin = program.method(c.name, "finalize", "()V"); - if (fin != null && !fin.isStatic()) return Result.neither("finalizer " + fin.key); - } - Set reachable = new LinkedHashSet<>(); - String open = openWorldCall(roots, reachable); - if (open != null) return Result.neither(open); - String assertion = assertionCreation(reachable); - boolean assertionFree = assertion == null; - if (assertionFree) assertion = "no AssertionError is created in code reachable from Main.main or a static initializer"; - // Main.main and every static initializer that may run (an exception escaping one surfaces - // as an ExceptionInInitializerError, but is still counted). - List mustNotThrow = new ArrayList<>(); - mustNotThrow.add(entry); - for (Program.Method m : reachable) if (m.node.name.equals("")) mustNotThrow.add(m); - for (Program.Method r : mustNotThrow) { - if (mayThrow.containsKey(r.key)) return new Result(false, explain(r.key, mayThrow), assertionFree, assertion); - } - return new Result(true, "no instruction reachable from Main.main or a static initializer can throw an uncaught RuntimeException", - assertionFree, assertion); - } - - /** - * Where reachable code may create an AssertionError (null if nowhere). With a closed world, - * only application code creates objects of application classes or of AssertionError: the - * modelled library methods create none, and no assert of the JDK is enabled. - */ - private String assertionCreation(Set reachable) { - for (Program.Method m : reachable) { - Frame[] f = frames.get(m.key); - AbstractInsnNode[] insns = m.node.instructions.toArray(); - for (int i = 0; i < insns.length; i++) { - if (f[i] == null) continue; - String type = null; - if (insns[i].getOpcode() == NEW) type = ((TypeInsnNode) insns[i]).desc; - else if (insns[i].getOpcode() == INVOKESPECIAL && ((MethodInsnNode) insns[i]).name.equals("")) - type = ((MethodInsnNode) insns[i]).owner; - if (type != null && program.isAssignable(type, "java/lang/AssertionError")) - return m.key + ": line " + line(insns[i]) + ": creates " + type; - } - } - return null; - } - - /** - * The analysis assumes a closed world: application code only runs when application code calls - * it, with arguments the facts account for. A reachable call that may run unknown code (an - * unmodelled library method, which could call back into the application) breaks that even if a - * handler catches what it throws, so it fails the check. Returns why, or null, and collects the - * reachable methods, including the static initializers of every class reachable code may - * initialize (new, getstatic, putstatic, invokestatic). Classes are initialized in no other way: - * reflection and method handles are not modelled. - */ - private String openWorldCall(List roots, Set reachable) { - Deque work = new ArrayDeque<>(roots); - while (!work.isEmpty()) { - Program.Method m = work.poll(); - if (!reachable.add(m)) continue; - Frame[] f = frames.get(m.key); - if (f == null) return "reachable method without code: " + m.key; - AbstractInsnNode[] insns = m.node.instructions.toArray(); - for (int i = 0; i < insns.length; i++) { - if (f[i] == null) continue; - if (insns[i] instanceof InvokeDynamicInsnNode && !isStringConcat((InvokeDynamicInsnNode) insns[i])) - return m.key + ": line " + line(insns[i]) + ": invokedynamic"; - if (insns[i] instanceof LdcInsnNode && (((LdcInsnNode) insns[i]).cst instanceof Handle - || ((LdcInsnNode) insns[i]).cst instanceof ConstantDynamic)) - return m.key + ": line " + line(insns[i]) + ": ldc of a method handle or dynamic constant"; - int op = insns[i].getOpcode(); - if (op == NEW) work.addAll(initializers(((TypeInsnNode) insns[i]).desc)); - else if (op == GETSTATIC || op == PUTSTATIC) work.addAll(initializers(((FieldInsnNode) insns[i]).owner)); - else if (op == INVOKESTATIC) work.addAll(initializers(((MethodInsnNode) insns[i]).owner)); - if (!(insns[i] instanceof MethodInsnNode)) continue; - MethodInsnNode mi = (MethodInsnNode) insns[i]; - String reason = openWorldReason(mi, f[i]); - if (reason != null) return m.key + ": line " + line(mi) + ": " + reason; - Program.Targets t = mi.owner.startsWith(Program.VERIFIER_PACKAGE) ? null : targets(mi); - if (t != null) work.addAll(t.methods); - } - } - return null; - } - - /** - * The static initializers that may run when a class is initialized: its own and those of its - * application supertypes (a superset of what the JVM initializes, see JVMS 5.5). - */ - private List initializers(String className) { - List out = new ArrayList<>(); - if (!program.isApp(className)) return out; - for (String t : program.appSupertypes(className)) { - Program.Method clinit = program.method(t, "", "()V"); - if (clinit != null) out.add(clinit); - } - return out; - } - - /** Follows the may-throw reasons from a root down to the instruction that may throw. */ - private static String explain(String key, Map mayThrow) { - StringBuilder sb = new StringBuilder(); - Set seen = new HashSet<>(); - String k = key; - while (k != null && seen.add(k)) { - String reason = mayThrow.get(k); - if (sb.length() > 0) sb.append(" <- "); - sb.append(k).append(": ").append(reason); - k = null; - int i = reason.indexOf("call to "); - if (i >= 0) { - String callee = reason.substring(i + "call to ".length()); - if (mayThrow.containsKey(callee)) k = callee; - } - } - return sb.toString(); - } - - // --------------------------------------------------------------------------------------------- - // Facts - - private void joinInto(Map map, String key, AbsValue v) { - v = v.escaped(); - AbsValue old = map.get(key); - AbsValue joined = old == null ? v : AbsValue.join(old, v); - if (!joined.equals(old)) { - map.put(key, joined); - changed = true; - } - } - - private void collectFacts(Program.Method m, Frame[] f) { - AbstractInsnNode[] insns = m.node.instructions.toArray(); - for (int i = 0; i < insns.length; i++) { - Frame fr = f[i]; - if (fr == null) continue; - AbstractInsnNode insn = insns[i]; - int op = insn.getOpcode(); - if (op == PUTFIELD || op == PUTSTATIC) { - FieldInsnNode fi = (FieldInsnNode) insn; - String key = fieldKey(fi); - if (key != null && isReferenceDesc(fi.desc)) joinInto(fieldFacts, key, top(fr, 0)); - } else if (op == ARETURN) { - joinInto(returnFacts, m.key, top(fr, 0)); - } else if (op >= IRETURN && op <= DRETURN) { - joinInto(returnFacts, m.key, top(fr, 0)); - } else if (insn instanceof MethodInsnNode) { - MethodInsnNode mi = (MethodInsnNode) insn; - Program.Targets t = targets(mi); - if (t == null) continue; - Type[] args = Type.getArgumentTypes(mi.desc); - for (Program.Method target : t.methods) { - AbsValue[] params = parameterFacts.computeIfAbsent(target.key, k -> new AbsValue[args.length]); - for (int a = 0; a < args.length; a++) { - AbsValue v = top(fr, args.length - 1 - a).escaped(); - AbsValue joined = params[a] == null ? v : AbsValue.join(params[a], v); - if (!joined.equals(params[a])) { - params[a] = joined; - changed = true; - } - } - } - } - } - } - - private static boolean isReferenceDesc(String desc) { - return desc.startsWith("L") || desc.startsWith("["); - } - - private static AbsValue top(Frame f, int depth) { - return f.getStack(f.getStackSize() - 1 - depth); - } - - /** The key of the application field a field instruction accesses, or null for a library field. */ - private String fieldKey(FieldInsnNode fi) { - String[] decl = new String[1]; - FieldNode f = program.resolveField(fi.owner, fi.name, fi.desc, decl); - return f == null ? null : decl[0] + "." + f.name + ":" + f.desc; - } - - @Override - public AbsValue field(FieldInsnNode insn) { - if (insn.getOpcode() == GETSTATIC && insn.owner.equals("java/lang/System") - && (insn.name.equals("out") || insn.name.equals("err")) && insn.desc.equals("Ljava/io/PrintStream;")) { - // Non-null, and exactly a PrintStream: System.setOut/setErr are not modelled, so no - // program that passes the check can replace them. - return AbsValue.exact("java/io/PrintStream"); - } - String key = fieldKey(insn); - if (key == null) return FactInterpreter.ofType(Type.getType(insn.desc)); - AbsValue v = fieldFacts.get(key); - if (v == null) return AbsValue.bottom(Type.getType(insn.desc).getSize()); - return v; - } - - @Override - public AbsValue parameter(Program.Method method, int index, Type type) { - AbsValue[] params = parameterFacts.get(method.key); - if (method == entry) { - // The launcher passes a non-null array; the program may call main itself as well. - AbsValue launcher = AbsValue.array(MAIN_DESC.substring(1, MAIN_DESC.indexOf(')')), null, null); - return params == null || params[index] == null ? launcher : AbsValue.join(launcher, params[index]); - } - if (params == null || params[index] == null) return AbsValue.bottom(type.getSize()); - return params[index]; - } - - @Override - public AbsValue callResult(MethodInsnNode insn, List args) { - Type ret = Type.getReturnType(insn.desc); - if (ret.getSort() == Type.VOID) return null; - if (insn.owner.startsWith(Program.VERIFIER_PACKAGE)) { - if (insn.name.equals("nondetString")) return AbsValue.exact("java/lang/String"); - return FactInterpreter.ofType(ret); - } - if (insn.getOpcode() == INVOKESTATIC && insn.name.equals("values") && program.isEnum(insn.owner) - && insn.desc.equals("()[L" + insn.owner + ";")) { - return AbsValue.array("[L" + insn.owner + ";", null, insn.owner); - } - if (insn.name.equals("ordinal") && insn.desc.equals("()I") && insn.getOpcode() != INVOKESTATIC) { - return program.isEnum(insn.owner) ? AbsValue.PRIM1.withOrdinalOf(insn.owner) : AbsValue.PRIM1; - } - Program.Targets t = targets(insn); - if (t == null) return FactInterpreter.ofType(ret); - AbsValue result = null; - for (Program.Method m : t.methods) { - AbsValue r = returnFacts.get(m.key); - if (r == null) r = AbsValue.bottom(ret.getSize()); - result = result == null ? r : AbsValue.join(result, r); - } - for (String lib : t.libraryMethods) { - AbsValue r = libraryResult(lib, ret, args); - result = result == null ? r : AbsValue.join(result, r); - } - return result == null ? FactInterpreter.ofType(ret) : result; - } - - private static AbsValue libraryResult(String lib, Type ret, List args) { - String[] parts = splitMethod(lib); - JdkModel.Entry e = JdkModel.lookup(parts[0], parts[1], parts[2]); - if (e == null) return FactInterpreter.ofType(ret); - switch (e.returns) { - case NONNULL_EXACT: - return AbsValue.exact(ret.getInternalName()); - case RECEIVER: - return args.get(0).escaped(); - case CLONE: { - AbsValue r = args.get(0); - return new AbsValue(AbsValue.Kind.NONNULL, 1, null, r.length, r.lengthOf, null, r.exactType, - r.exactType != null ? r.exactType : r.staticType, false); - } - default: - return FactInterpreter.ofType(ret); - } - } - - /** owner, name and descriptor of "owner.name(desc)". */ - static String[] splitMethod(String key) { - int paren = key.indexOf('('); - int dot = key.lastIndexOf('.', paren); - return new String[] {key.substring(0, dot), key.substring(dot + 1, paren), key.substring(paren)}; - } - - /** The possible targets of a call, or null if they cannot be determined. Not for Verifier calls. */ - private Program.Targets targets(MethodInsnNode mi) { - if (unknownTargets.contains(mi)) return null; - Program.Targets cached = targetCache.get(mi); - if (cached != null) return cached; - Program.Targets t = computeTargets(mi); - if (t == null) unknownTargets.add(mi); - else targetCache.put(mi, t); - return t; - } - - private Program.Targets computeTargets(MethodInsnNode mi) { - if (mi.owner.startsWith(Program.VERIFIER_PACKAGE)) return new Program.Targets(); - int op = mi.getOpcode(); - if ((op == INVOKEVIRTUAL || op == INVOKEINTERFACE) && program.isApp(mi.owner)) { - return program.virtualTargets(mi.owner, mi.name, mi.desc); - } - Program.Targets t = new Program.Targets(); - if (op == INVOKEVIRTUAL || op == INVOKEINTERFACE) { - t.libraryMethods.add(mi.owner + "." + mi.name + mi.desc); - return t; - } - if (op == INVOKESPECIAL && mi.name.equals("")) { - Program.Method m = program.method(mi.owner, mi.name, mi.desc); - if (m != null) t.methods.add(m); - else if (program.isApp(mi.owner)) return null; - else t.libraryMethods.add(mi.owner + "." + mi.name + mi.desc); - return t; - } - String[] lib = new String[1]; - Program.Method m = program.resolveInChain(mi.owner, mi.name, mi.desc, lib); - if (m != null) { - if (!m.hasCode()) return null; - t.methods.add(m); - } else if (lib[0] != null) { - t.libraryMethods.add(lib[0] + "." + mi.name + mi.desc); - } else { - return null; - } - return t; - } - - // --------------------------------------------------------------------------------------------- - // Fields initialized before any read - - /** - * Finds the reference fields that hold a value from their first assignment on, before any code - * that could read them runs. Such a field never shows its default null, so its fact is the join - * of the values stored into it only. - * - *

A static field qualifies if its class initializer assigns it in its straight-line prefix - * (no jumps and no exception handlers), and nothing that prefix may execute (the methods it calls - * and the static initializers of the classes it, its callees or the superclasses touch, all - * transitively) reads a field of that name. An instance field qualifies if every constructor of - * its class assigns it on the receiver in such a prefix, which neither lets the receiver escape - * nor may execute a read of the field. An object is only reachable through the receiver of its - * constructor until it escapes, so no read can come from elsewhere; a constructor that throws - * before the assignment leaves no reference to its object behind. - */ - private void computeInitializedBeforeRead() throws AnalyzerException { - for (ClassNode c : program.appClasses()) { - for (FieldNode f : c.fields) { - if (!isReferenceDesc(f.desc)) continue; - String key = c.name + "." + f.name + ":" + f.desc; - boolean isStatic = (f.access & ACC_STATIC) != 0; - if (isStatic ? staticFieldInitializedFirst(c, f) : instanceFieldInitializedFirst(c, f)) { - initializedBeforeRead.add(key); - } - } - } - } - - /** The instructions every execution of the method runs first, in order, up to the first jump. */ - private static List straightLinePrefix(MethodNode m) { - List out = new ArrayList<>(); - for (AbstractInsnNode insn = m.instructions.getFirst(); insn != null; insn = insn.getNext()) { - if (insn.getOpcode() < 0) continue; // labels, line numbers, frames - int op = insn.getOpcode(); - if (insn instanceof JumpInsnNode || insn instanceof TableSwitchInsnNode || insn instanceof LookupSwitchInsnNode - || op == ATHROW || op == RET || (op >= IRETURN && op <= RETURN)) break; - out.add(insn); - } - return out; - } - - private static boolean coveredByHandler(MethodNode m, AbstractInsnNode insn) { - int idx = m.instructions.indexOf(insn); - for (TryCatchBlockNode tcb : m.tryCatchBlocks) { - if (m.instructions.indexOf(tcb.start) <= idx && idx < m.instructions.indexOf(tcb.end)) return true; - } - return false; - } - - private boolean staticFieldInitializedFirst(ClassNode c, FieldNode f) { - Program.Method clinit = program.method(c.name, "", "()V"); - if (clinit == null) return false; - List before = new ArrayList<>(); - for (AbstractInsnNode insn : straightLinePrefix(clinit.node)) { - if (coveredByHandler(clinit.node, insn)) return false; - if (insn.getOpcode() == PUTSTATIC && assigns((FieldInsnNode) insn, c, f)) { - // The supertypes are initialized before the class; the class itself is being - // initialized already, so touching it again does not rerun its initializer. - Set supertypes = new HashSet<>(program.appSupertypes(c.name)); - supertypes.remove(c.name); - return !mayRead(before, supertypes, Set.of(c.name), f.name, f.desc, true); - } - before.add(insn); - } - return false; - } - - private boolean instanceFieldInitializedFirst(ClassNode c, FieldNode f) throws AnalyzerException { - boolean any = false; - for (MethodNode mn : c.methods) { - if (!mn.name.equals("")) continue; - any = true; - Program.Method ctor = program.method(c.name, mn.name, mn.desc); - Frame[] fr = new Analyzer<>(new FactInterpreter(UNKNOWN_FACTS, ctor)).analyze(c.name, mn); - List before = new ArrayList<>(); - boolean assigned = false; - for (AbstractInsnNode insn : straightLinePrefix(mn)) { - if (coveredByHandler(mn, insn)) return false; - Frame frame = fr[mn.instructions.indexOf(insn)]; - if (frame == null) return false; - if (insn.getOpcode() == PUTFIELD && assigns((FieldInsnNode) insn, c, f) && top(frame, 1).isThis - && !top(frame, 0).mayBeThis) { - assigned = true; - break; - } - if (letsReceiverEscape(insn, frame, new HashSet<>())) return false; - before.add(insn); - } - if (!assigned || mayRead(before, Set.of(), Set.of(), f.name, f.desc, false)) return false; - } - return any; - } - - private boolean assigns(FieldInsnNode fi, ClassNode c, FieldNode f) { - String[] decl = new String[1]; - FieldNode target = program.resolveField(fi.owner, fi.name, fi.desc, decl); - return target == f && c.name.equals(decl[0]); - } - - /** - * Whether the instruction hands the receiver (this) to code that could keep it: as an argument - * or receiver of a call, or as a value stored into a field or an array. The superclass or - * delegated constructor may take it if its own code does not let it escape either. - */ - private boolean letsReceiverEscape(AbstractInsnNode insn, Frame frame, Set checking) { - int op = insn.getOpcode(); - if (op == PUTFIELD || op == PUTSTATIC || op == AASTORE || op == ARETURN || op == ATHROW) { - return top(frame, 0).mayBeThis; - } - if (insn instanceof InvokeDynamicInsnNode) { - int n = Type.getArgumentTypes(((InvokeDynamicInsnNode) insn).desc).length; - for (int i = 0; i < n; i++) if (top(frame, i).mayBeThis) return true; - return false; - } - if (!(insn instanceof MethodInsnNode)) return false; - MethodInsnNode mi = (MethodInsnNode) insn; - int n = Type.getArgumentTypes(mi.desc).length; - for (int i = 0; i < n; i++) if (top(frame, i).mayBeThis) return true; - if (op == INVOKESTATIC || !top(frame, n).mayBeThis) return false; - if (op != INVOKESPECIAL || !mi.name.equals("") || !top(frame, n).isThis) return true; - if (mi.owner.equals("java/lang/Object") && mi.desc.equals("()V")) return false; - if (mi.owner.equals("java/lang/Enum") && mi.desc.equals("(Ljava/lang/String;I)V")) return false; - Program.Method ctor = program.method(mi.owner, mi.name, mi.desc); - if (ctor == null || !ctor.hasCode() || !checking.add(ctor.key)) return true; - try { - Frame[] fr = new Analyzer<>(new FactInterpreter(UNKNOWN_FACTS, ctor)).analyze(ctor.owner.name, ctor.node); - AbstractInsnNode[] insns = ctor.node.instructions.toArray(); - for (int i = 0; i < insns.length; i++) { - if (fr[i] != null && letsReceiverEscape(insns[i], fr[i], checking)) return true; - } - return false; - } catch (AnalyzerException e) { - return true; - } - } - - /** - * Whether running the given instructions may read a field with this name and descriptor: - * directly, in a method they may call (transitively), or in a static initializer they may - * trigger (except those of the classes being initialized already). Unknown callees count as - * reads. - */ - private boolean mayRead(List start, Set initializedClasses, Set initializing, - String name, String desc, boolean isStatic) { - Deque work = new ArrayDeque<>(); - Set seen = new HashSet<>(); - Set classes = new HashSet<>(initializing); - Deque pendingClasses = new ArrayDeque<>(initializedClasses); - List insns = new ArrayList<>(start); - while (true) { - for (AbstractInsnNode insn : insns) { - int op = insn.getOpcode(); - if (insn instanceof FieldInsnNode) { - FieldInsnNode fi = (FieldInsnNode) insn; - if ((op == (isStatic ? GETSTATIC : GETFIELD)) && fi.name.equals(name) && fi.desc.equals(desc)) return true; - if (op == GETSTATIC || op == PUTSTATIC) pendingClasses.add(fi.owner); - } else if (op == NEW) { - pendingClasses.add(((TypeInsnNode) insn).desc); - } else if (insn instanceof InvokeDynamicInsnNode) { - if (!isStringConcat((InvokeDynamicInsnNode) insn)) return true; - } else if (insn instanceof MethodInsnNode) { - MethodInsnNode mi = (MethodInsnNode) insn; - if (mi.owner.startsWith(Program.VERIFIER_PACKAGE)) { - if (!isModelledVerifierCall(mi)) return true; - continue; - } - if (op == INVOKESTATIC) pendingClasses.add(mi.owner); - Program.Targets t = targets(mi); - if (t == null) return true; - for (String lib : t.libraryMethods) { - String[] p = splitMethod(lib); - JdkModel.Entry e = JdkModel.lookup(p[0], p[1], p[2]); - // Without values, a library call is only known not to call back if its model - // has no argument condition about callbacks and no override can intervene. - if (e == null || e.condition == JdkModel.Condition.STRING_ARGS) return true; - if (op != INVOKESTATIC && !program.isApp(mi.owner) && !JdkModel.cannotBeOverridden(p[0], p[1], p[2]) - && !e.exactReceiver) return true; - } - for (Program.Method m : t.methods) if (seen.add(m.key)) work.add(m); - } - } - while (!pendingClasses.isEmpty()) { - String cls = pendingClasses.poll(); - if (cls.startsWith("[") || !program.isApp(cls)) continue; - for (String sup : program.appSupertypes(cls)) { - if (!classes.add(sup)) continue; - Program.Method clinit = program.method(sup, "", "()V"); - if (clinit != null && seen.add(clinit.key)) work.add(clinit); - } - } - if (work.isEmpty()) return false; - Program.Method m = work.poll(); - insns = new ArrayList<>(); - if (!m.hasCode()) return true; - for (AbstractInsnNode insn : m.node.instructions) insns.add(insn); - } - } - - /** Facts for analyses that only need the receiver flag: nothing is known about other values. */ - private static final FactInterpreter.Facts UNKNOWN_FACTS = new FactInterpreter.Facts() { - @Override - public AbsValue field(FieldInsnNode insn) { - return FactInterpreter.ofType(Type.getType(insn.desc)); - } - - @Override - public AbsValue parameter(Program.Method method, int index, Type type) { - return FactInterpreter.ofType(type); - } - - @Override - public AbsValue callResult(MethodInsnNode insn, List args) { - return FactInterpreter.ofType(Type.getReturnType(insn.desc)); - } - }; - - // --------------------------------------------------------------------------------------------- - // Checking instructions - - static boolean isStringConcat(InvokeDynamicInsnNode indy) { - if (!indy.bsm.getOwner().equals("java/lang/invoke/StringConcatFactory")) return false; - for (Type t : Type.getArgumentTypes(indy.desc)) { - if (t.getSort() == Type.OBJECT && !t.getInternalName().equals("java/lang/String")) return false; - if (t.getSort() == Type.ARRAY) return false; - } - return true; - } - - private static boolean isModelledVerifierCall(MethodInsnNode mi) { - return mi.owner.equals(Program.VERIFIER_PACKAGE + "Verifier") && mi.getOpcode() == INVOKESTATIC - && (mi.name.equals("assume") || (mi.name.startsWith("nondet") && !mi.name.equals("nondetObject"))); - } - - /** - * Why a RuntimeException may escape the method, or null if none can, given the methods already - * known to let one escape. - */ - private String escapingException(Program.Method m, Map mayThrow) { - Frame[] f = frames.get(m.key); - MethodNode mn = m.node; - AbstractInsnNode[] insns = mn.instructions.toArray(); - int n = insns.length; - List handlers = mn.tryCatchBlocks; - boolean[][] covers = new boolean[handlers.size()][n]; - for (int h = 0; h < handlers.size(); h++) { - TryCatchBlockNode tcb = handlers.get(h); - int s = mn.instructions.indexOf(tcb.start), e = mn.instructions.indexOf(tcb.end); - for (int i = s; i < e; i++) covers[h][i] = true; - } - // An instruction may raise a RuntimeException; handlers that may catch one. Rethrowing a - // caught exception raises one only if its handler may have caught one: iterate. - String[] raises = new String[n]; - boolean[] handlerCatches = new boolean[handlers.size()]; - boolean grew = true; - while (grew) { - grew = false; - for (int i = 0; i < n; i++) { - if (f[i] == null || raises[i] != null) continue; - String r = raises(m, insns[i], f[i], mayThrow, handlerCatches); - if (r == null) continue; - raises[i] = r; - grew = true; - // Over-approximated: every handler that covers it may have caught it. - for (int h = 0; h < handlers.size(); h++) if (covers[h][i]) handlerCatches[h] = true; - } - } - for (int i = 0; i < n; i++) { - if (raises[i] == null) continue; - boolean caught = false; - for (int h = 0; h < handlers.size() && !caught; h++) { - caught = covers[h][i] && catchesEveryRuntimeException(handlers.get(h).type, insns[i]); - } - if (!caught) return "line " + line(insns[i]) + ": " + raises[i]; - } - return null; - } - - private static int line(AbstractInsnNode insn) { - for (AbstractInsnNode p = insn; p != null; p = p.getPrevious()) { - if (p instanceof LineNumberNode) return ((LineNumberNode) p).line; - } - return -1; - } - - private static boolean catchesEveryRuntimeException(String type, AbstractInsnNode insn) { - if (type == null || type.equals("java/lang/Throwable") || type.equals("java/lang/Exception") - || type.equals("java/lang/RuntimeException")) return true; - // Integer division can only throw ArithmeticException. - int op = insn.getOpcode(); - return type.equals("java/lang/ArithmeticException") && (op == IDIV || op == IREM || op == LDIV || op == LREM); - } - - private String raises(Program.Method m, AbstractInsnNode insn, Frame f, Map mayThrow, - boolean[] handlerCatches) { - int op = insn.getOpcode(); - switch (op) { - case IDIV: case IREM: case LDIV: case LREM: { - AbsValue d = top(f, 0); - if (d.isBottom() || (d.constant != null && d.constant != 0)) return null; - return "division by a value that may be zero"; - } - case IALOAD: case LALOAD: case FALOAD: case DALOAD: case BALOAD: case CALOAD: case SALOAD: case AALOAD: - return arrayAccess(top(f, 1), top(f, 0)); - case IASTORE: case LASTORE: case FASTORE: case DASTORE: case BASTORE: case CASTORE: case SASTORE: - return arrayAccess(top(f, 2), top(f, 1)); - case AASTORE: { - String r = arrayAccess(top(f, 2), top(f, 1)); - if (r != null) return r; - AbsValue arr = top(f, 2), v = top(f, 0); - if (v.isNull() || v.isBottom() || arr.isBottom()) return null; - String elem = arr.exactType != null ? arr.exactType.substring(1) : null; - if (elem != null && elem.startsWith("L")) elem = elem.substring(1, elem.length() - 1); - if (elem != null && program.isAssignable(trustedType(v), elem)) return null; - return "array store of a value that may not fit the array"; - } - case ARRAYLENGTH: - return top(f, 0).isNonNull() ? null : "length of an array that may be null"; - case NEWARRAY: case ANEWARRAY: - return nonNegative(top(f, 0)) ? null : "array size may be negative"; - case MULTIANEWARRAY: { - int dims = ((MultiANewArrayInsnNode) insn).dims; - for (int i = 0; i < dims; i++) if (!nonNegative(top(f, i))) return "array size may be negative"; - return null; - } - case GETFIELD: - return top(f, 0).isNonNull() ? null : "field read on a reference that may be null"; - case PUTFIELD: - return top(f, 1).isNonNull() ? null : "field write on a reference that may be null"; - case CHECKCAST: { - AbsValue v = top(f, 0); - if (v.isNull() || v.isBottom() || program.isAssignable(trustedType(v), ((TypeInsnNode) insn).desc)) return null; - return "cast that may fail"; - } - case ATHROW: { - AbsValue v = top(f, 0); - if (v.isBottom()) return null; - if (v.caughtBy >= 0) return handlerCatches[v.caughtBy] ? "rethrow of a caught RuntimeException" : null; - if (v.exactType != null && isNeverRuntimeException(v.exactType)) return null; - return "throw of a value that may be a RuntimeException"; - } - case MONITORENTER: case MONITOREXIT: - return "monitor instruction"; - case INVOKEDYNAMIC: - return isStringConcat((InvokeDynamicInsnNode) insn) ? null : "invokedynamic"; - case INVOKEVIRTUAL: case INVOKESPECIAL: case INVOKESTATIC: case INVOKEINTERFACE: - return call((MethodInsnNode) insn, f, mayThrow); - default: - return null; - } - } - - private String arrayAccess(AbsValue arr, AbsValue idx) { - if (arr.isBottom() || idx.isBottom()) return null; - if (!arr.isNonNull()) return "access to an array that may be null"; - if (arr.length != null && idx.constant != null && idx.constant >= 0 && idx.constant < arr.length) return null; - if (arr.lengthOf != null && arr.lengthOf.equals(idx.ordinalOf)) return null; - return "array index that may be out of bounds"; - } - - private static boolean nonNegative(AbsValue count) { - return count.isBottom() || (count.constant != null && count.constant >= 0) || count.lengthOf != null; - } - - /** A type every non-null value of the slot is an instance of, if one is reliably known. */ - private String trustedType(AbsValue v) { - if (v.exactType != null) return v.exactType; - String t = v.staticType; - if (t == null) return null; - // The verifier does not check interface types, so only class and array types are trusted. - if (t.startsWith("[") || t.equals("java/lang/Object") || JdkModel.isFinalClass(t)) return t; - ClassNode c = program.clazz(t); - if (c != null && program.isApp(t) && (c.access & ACC_INTERFACE) == 0) return t; - return null; - } - - /** The runtime class is a Throwable that is not a RuntimeException. */ - private boolean isNeverRuntimeException(String exactType) { - List chain = program.superChain(exactType); - String root = chain.get(chain.size() - 1); - if (program.isApp(root)) return false; - return root.equals("java/lang/AssertionError") || root.equals("java/lang/Error") - || root.equals("java/lang/Exception") || root.equals("java/lang/Throwable"); - } - - /** - * Why the call may run code the analysis does not know (null if it cannot): an unresolved or - * unmodelled callee, or a library method whose model does not cover this receiver or these - * arguments. - */ - private String openWorldReason(MethodInsnNode mi, Frame f) { - int op = mi.getOpcode(); - if (mi.owner.startsWith(Program.VERIFIER_PACKAGE)) { - return isModelledVerifierCall(mi) ? null : "call to " + mi.owner + "." + mi.name; - } - Type[] args = Type.getArgumentTypes(mi.desc); - AbsValue receiver = op == INVOKESTATIC ? null : top(f, args.length); - if (receiver != null && receiver.isBottom()) return null; - Program.Targets t = targets(mi); - if (t == null) return "unresolved call to " + mi.owner + "." + mi.name + mi.desc; - for (String lib : t.libraryMethods) { - String[] p = splitMethod(lib); - JdkModel.Entry e = JdkModel.lookup(p[0], p[1], p[2]); - if (e == null) return "library call to " + lib; - boolean viaLibraryOwner = !program.isApp(mi.owner) && op != INVOKESTATIC && !(op == INVOKESPECIAL && mi.name.equals("")); - boolean exactOwner = receiver != null && p[0].equals(receiver.exactType); - if (viaLibraryOwner && !JdkModel.cannotBeOverridden(p[0], p[1], p[2]) && !exactOwner) - return "library call that an override may intercept: " + lib; - if (e.exactReceiver && !exactOwner) return "library call on a receiver of unknown class: " + lib; - if (e.condition != JdkModel.Condition.STRING_ARGS) continue; - for (int a = 0; a < args.length; a++) { - if (args[a].getSort() != Type.OBJECT && args[a].getSort() != Type.ARRAY) continue; - AbsValue v = top(f, args.length - 1 - a); - if (!v.isNull() && !v.isBottom() - && (trustedType(v) == null || !JdkModel.SAFE_TO_STRING.contains(trustedType(v)))) - return "library call that may call toString() of the argument: " + lib; - } - } - return null; - } - - private String call(MethodInsnNode mi, Frame f, Map mayThrow) { - String open = openWorldReason(mi, f); - if (open != null) return open; - if (mi.owner.startsWith(Program.VERIFIER_PACKAGE)) return null; - int op = mi.getOpcode(); - Type[] args = Type.getArgumentTypes(mi.desc); - AbsValue receiver = op == INVOKESTATIC ? null : top(f, args.length); - if (receiver != null && !receiver.isNonNull()) return "call on a reference that may be null: " + mi.owner + "." + mi.name; - if (receiver != null && receiver.isBottom()) return null; - Program.Targets t = targets(mi); - for (String lib : t.libraryMethods) { - String[] p = splitMethod(lib); - JdkModel.Entry e = JdkModel.lookup(p[0], p[1], p[2]); - if (e.condition != JdkModel.Condition.NONNULL_ARGS) continue; - for (int a = 0; a < args.length; a++) { - if (args[a].getSort() != Type.OBJECT && args[a].getSort() != Type.ARRAY) continue; - if (!top(f, args.length - 1 - a).isNonNull()) - return "library call with an argument that may be null: " + lib; - } - } - for (Program.Method target : t.methods) { - if (mayThrow.containsKey(target.key)) return "call to " + target.key; - } - return null; - } - - // --------------------------------------------------------------------------------------------- - - /** - * Command line: the classpath entries of the program. Prints one JSON object with the result. - */ - public static void main(String[] args) { - List cp = new ArrayList<>(); - for (String a : args) for (String p : a.split(java.io.File.pathSeparator)) if (!p.isEmpty()) cp.add(Path.of(p)); - Result r = check(cp); - System.out.println("{\"exception_free\": " + r.exceptionFree + ", \"reason\": \"" + escape(r.reason) - + "\", \"assertion_free\": " + r.assertionFree + ", \"assertion_reason\": \"" + escape(r.assertionReason) + "\"}"); - } - - private static String escape(String s) { - StringBuilder sb = new StringBuilder(); - for (char c : s.toCharArray()) { - if (c == '"' || c == '\\') sb.append('\\').append(c); - else if (c < 0x20) sb.append(String.format("\\u%04x", (int) c)); - else sb.append(c); - } - return sb.toString(); - } -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/FactInterpreter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/FactInterpreter.java deleted file mode 100644 index 71fb8bff..00000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/FactInterpreter.java +++ /dev/null @@ -1,277 +0,0 @@ -package de.uzl.its.swat.staticcheck; - -import java.util.List; -import org.objectweb.asm.Handle; -import org.objectweb.asm.Opcodes; -import org.objectweb.asm.Type; -import org.objectweb.asm.tree.*; -import org.objectweb.asm.tree.analysis.AnalyzerException; -import org.objectweb.asm.tree.analysis.Frame; -import org.objectweb.asm.tree.analysis.Interpreter; - -/** - * Computes {@link AbsValue}s for one method, using the facts the check has collected so far for - * fields, parameters and the results of calls. - */ -final class FactInterpreter extends Interpreter implements Opcodes { - - /** Facts about the rest of the program, as far as they are known. */ - interface Facts { - AbsValue field(FieldInsnNode insn); - - /** The value of parameter number {@code index} (not counting the receiver) of the method. */ - AbsValue parameter(Program.Method method, int index, Type type); - - AbsValue callResult(MethodInsnNode insn, List args); - } - - private final Facts facts; - private final Program.Method method; - private final int[] localToParameter; - - FactInterpreter(Facts facts, Program.Method method) { - super(ASM9); - this.facts = facts; - this.method = method; - Type[] params = Type.getArgumentTypes(method.node.desc); - int locals = method.isStatic() ? 0 : 1; - for (Type t : params) locals += t.getSize(); - localToParameter = new int[locals]; - java.util.Arrays.fill(localToParameter, -1); - int local = method.isStatic() ? 0 : 1; - for (int i = 0; i < params.length; i++) { - localToParameter[local] = i; - local += params[i].getSize(); - } - } - - static AbsValue ofType(Type type) { - if (type == null) return AbsValue.UNKNOWN1; - switch (type.getSort()) { - case Type.VOID: - return null; - case Type.LONG: - case Type.DOUBLE: - return AbsValue.PRIM2; - case Type.OBJECT: - case Type.ARRAY: - return AbsValue.ref(type.getInternalName()); - case Type.METHOD: - return AbsValue.UNKNOWN1; - default: - return AbsValue.PRIM1; - } - } - - @Override - public AbsValue newValue(Type type) { - return ofType(type); - } - - @Override - public AbsValue newParameterValue(boolean isInstanceMethod, int local, Type type) { - if (isInstanceMethod && local == 0) return AbsValue.nonNull(type.getInternalName()).withThis(); - int index = local < localToParameter.length ? localToParameter[local] : -1; - if (index < 0) return ofType(type); - return facts.parameter(method, index, type); - } - - @Override - public AbsValue newEmptyValue(int local) { - return AbsValue.UNKNOWN1; - } - - @Override - public AbsValue newExceptionValue(TryCatchBlockNode tryCatch, Frame handlerFrame, Type exceptionType) { - return AbsValue.caught(exceptionType.getInternalName(), method.node.tryCatchBlocks.indexOf(tryCatch)); - } - - @Override - public AbsValue newOperation(AbstractInsnNode insn) throws AnalyzerException { - switch (insn.getOpcode()) { - case ACONST_NULL: - return AbsValue.NULL; - case ICONST_M1: case ICONST_0: case ICONST_1: case ICONST_2: case ICONST_3: case ICONST_4: case ICONST_5: - return AbsValue.constant(1, insn.getOpcode() - ICONST_0); - case LCONST_0: case LCONST_1: - return AbsValue.constant(2, insn.getOpcode() - LCONST_0); - case FCONST_0: case FCONST_1: case FCONST_2: - return AbsValue.PRIM1; - case DCONST_0: case DCONST_1: - return AbsValue.PRIM2; - case BIPUSH: case SIPUSH: - return AbsValue.constant(1, ((IntInsnNode) insn).operand); - case LDC: { - Object c = ((LdcInsnNode) insn).cst; - if (c instanceof Integer) return AbsValue.constant(1, (Integer) c); - if (c instanceof Long) return AbsValue.constant(2, (Long) c); - if (c instanceof Float) return AbsValue.PRIM1; - if (c instanceof Double) return AbsValue.PRIM2; - if (c instanceof String) return AbsValue.exact("java/lang/String"); - if (c instanceof Type) { - int sort = ((Type) c).getSort(); - if (sort == Type.METHOD) return AbsValue.exact("java/lang/invoke/MethodType"); - return AbsValue.exact("java/lang/Class"); - } - if (c instanceof Handle) return AbsValue.nonNull("java/lang/invoke/MethodHandle"); - return AbsValue.UNKNOWN1; - } - case JSR: - return AbsValue.UNKNOWN1; - case GETSTATIC: - return facts.field((FieldInsnNode) insn); - case NEW: - return AbsValue.exact(((TypeInsnNode) insn).desc); - default: - throw new AnalyzerException(insn, "Unexpected opcode"); - } - } - - @Override - public AbsValue copyOperation(AbstractInsnNode insn, AbsValue value) { - return value; - } - - @Override - public AbsValue unaryOperation(AbstractInsnNode insn, AbsValue value) throws AnalyzerException { - switch (insn.getOpcode()) { - case INEG: - return value.constant != null ? AbsValue.constant(1, (int) -value.constant) : AbsValue.PRIM1; - case IINC: - return value.constant != null - ? AbsValue.constant(1, (int) (value.constant + ((IincInsnNode) insn).incr)) : AbsValue.PRIM1; - case L2I: - return value.constant != null ? AbsValue.constant(1, (int) (long) value.constant) : AbsValue.PRIM1; - case I2L: - return value.constant != null ? AbsValue.constant(2, value.constant) : AbsValue.PRIM2; - case I2B: - return value.constant != null ? AbsValue.constant(1, (byte) (long) value.constant) : AbsValue.PRIM1; - case I2C: - return value.constant != null ? AbsValue.constant(1, (char) (long) value.constant) : AbsValue.PRIM1; - case I2S: - return value.constant != null ? AbsValue.constant(1, (short) (long) value.constant) : AbsValue.PRIM1; - case LNEG: - return value.constant != null ? AbsValue.constant(2, -value.constant) : AbsValue.PRIM2; - case FNEG: case I2F: case L2F: case D2F: case F2I: case D2I: - return AbsValue.PRIM1; - case DNEG: case I2D: case L2D: case F2D: case F2L: case D2L: - return AbsValue.PRIM2; - case IFEQ: case IFNE: case IFLT: case IFGE: case IFGT: case IFLE: - case TABLESWITCH: case LOOKUPSWITCH: - case IRETURN: case LRETURN: case FRETURN: case DRETURN: case ARETURN: - case PUTSTATIC: case ATHROW: case MONITORENTER: case MONITOREXIT: case IFNULL: case IFNONNULL: - return null; - case GETFIELD: - return facts.field((FieldInsnNode) insn); - case NEWARRAY: { - String desc = "[" + primitiveDescriptor(((IntInsnNode) insn).operand); - return AbsValue.array(desc, nonNegative(value), value.lengthOf); - } - case ANEWARRAY: { - String elem = ((TypeInsnNode) insn).desc; - String desc = "[" + (elem.startsWith("[") ? elem : "L" + elem + ";"); - return AbsValue.array(desc, nonNegative(value), value.lengthOf); - } - case ARRAYLENGTH: { - AbsValue len = value.length != null ? AbsValue.constant(1, value.length) : AbsValue.PRIM1; - return value.lengthOf != null ? len.withLengthOf(value.lengthOf) : len; - } - case CHECKCAST: - return value; - case INSTANCEOF: - return AbsValue.PRIM1; - default: - throw new AnalyzerException(insn, "Unexpected opcode"); - } - } - - private static Integer nonNegative(AbsValue count) { - if (count.constant == null || count.constant < 0 || count.constant > Integer.MAX_VALUE) return null; - return (int) (long) count.constant; - } - - static String primitiveDescriptor(int operand) { - switch (operand) { - case T_BOOLEAN: return "Z"; - case T_CHAR: return "C"; - case T_BYTE: return "B"; - case T_SHORT: return "S"; - case T_INT: return "I"; - case T_FLOAT: return "F"; - case T_DOUBLE: return "D"; - case T_LONG: return "J"; - default: return "?"; - } - } - - @Override - public AbsValue binaryOperation(AbstractInsnNode insn, AbsValue v1, AbsValue v2) throws AnalyzerException { - int op = insn.getOpcode(); - switch (op) { - case IALOAD: case BALOAD: case CALOAD: case SALOAD: case FALOAD: - return AbsValue.PRIM1; - case LALOAD: case DALOAD: - return AbsValue.PRIM2; - case AALOAD: { - String t = v1.staticType; - if (t != null && t.startsWith("[")) return AbsValue.ref(Type.getType(t.substring(1)).getInternalName()); - return AbsValue.ref(null); - } - case IADD: case ISUB: case IMUL: case ISHL: case ISHR: case IUSHR: case IAND: case IOR: case IXOR: - if (v1.constant != null && v2.constant != null) { - int a = (int) (long) v1.constant, b = (int) (long) v2.constant; - switch (op) { - case IADD: return AbsValue.constant(1, a + b); - case ISUB: return AbsValue.constant(1, a - b); - case IMUL: return AbsValue.constant(1, a * b); - case ISHL: return AbsValue.constant(1, a << b); - case ISHR: return AbsValue.constant(1, a >> b); - case IUSHR: return AbsValue.constant(1, a >>> b); - case IAND: return AbsValue.constant(1, a & b); - case IOR: return AbsValue.constant(1, a | b); - default: return AbsValue.constant(1, a ^ b); - } - } - return AbsValue.PRIM1; - case IDIV: case IREM: case FADD: case FSUB: case FMUL: case FDIV: case FREM: - case LCMP: case FCMPL: case FCMPG: case DCMPL: case DCMPG: - return AbsValue.PRIM1; - case LADD: case LSUB: case LMUL: case LDIV: case LREM: case LSHL: case LSHR: case LUSHR: - case LAND: case LOR: case LXOR: case DADD: case DSUB: case DMUL: case DDIV: case DREM: - return AbsValue.PRIM2; - case IF_ICMPEQ: case IF_ICMPNE: case IF_ICMPLT: case IF_ICMPGE: case IF_ICMPGT: case IF_ICMPLE: - case IF_ACMPEQ: case IF_ACMPNE: case PUTFIELD: - return null; - default: - throw new AnalyzerException(insn, "Unexpected opcode"); - } - } - - @Override - public AbsValue ternaryOperation(AbstractInsnNode insn, AbsValue v1, AbsValue v2, AbsValue v3) { - return null; - } - - @Override - public AbsValue naryOperation(AbstractInsnNode insn, List values) { - int op = insn.getOpcode(); - if (op == MULTIANEWARRAY) { - String desc = ((MultiANewArrayInsnNode) insn).desc; - return AbsValue.array(desc, nonNegative(values.get(0)), values.get(0).lengthOf); - } - if (op == INVOKEDYNAMIC) { - InvokeDynamicInsnNode indy = (InvokeDynamicInsnNode) insn; - if (ExceptionFreedomCheck.isStringConcat(indy)) return AbsValue.exact("java/lang/String"); - return ofType(Type.getReturnType(indy.desc)); - } - return facts.callResult((MethodInsnNode) insn, values); - } - - @Override - public void returnOperation(AbstractInsnNode insn, AbsValue value, AbsValue expected) {} - - @Override - public AbsValue merge(AbsValue a, AbsValue b) { - return AbsValue.join(a, b); - } -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/JdkModel.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/JdkModel.java deleted file mode 100644 index 79f64a51..00000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/JdkModel.java +++ /dev/null @@ -1,281 +0,0 @@ -package de.uzl.its.swat.staticcheck; - -import java.util.*; - -/** - * The library (JDK) methods {@link ExceptionFreedomCheck} lets a program call. - * - *

Every method listed here throws no RuntimeException for any arguments that meet its - * condition, and never calls back into application code: it calls no method of an argument or - * receiver that an application class could override. A call to any other library method fails the - * check. Entries are matched by owner, name and descriptor as written in the call instruction. - */ -final class JdkModel { - - enum Condition { - NONE, - /** Every reference argument is non-null. */ - NONNULL_ARGS, - /** - * Every reference argument is null or of a final library type whose toString() is one of the - * listed safe methods (the method converts its argument with String.valueOf). - */ - STRING_ARGS - } - - enum Returns { - /** Nothing known beyond the declared return type. */ - DECLARED, - /** A non-null object of exactly the declared return type. */ - NONNULL_EXACT, - /** The receiver (StringBuilder.append). */ - RECEIVER, - /** A copy of the receiver array (same runtime type and length). */ - CLONE - } - - static final class Entry { - final Condition condition; - final Returns returns; - /** The receiver must be exactly of the owner class: subclasses could override the method. */ - final boolean exactReceiver; - - Entry(Condition condition, Returns returns, boolean exactReceiver) { - this.condition = condition; - this.returns = returns; - this.exactReceiver = exactReceiver; - } - } - - /** Final classes: no subclass can override their methods. */ - private static final Set FINAL_CLASSES = Set.of( - "java/lang/String", "java/lang/StringBuilder", "java/lang/StringBuffer", "java/lang/Integer", - "java/lang/Long", "java/lang/Short", "java/lang/Byte", "java/lang/Character", "java/lang/Boolean", - "java/lang/Double", "java/lang/Float", "java/lang/Math", "java/lang/StrictMath", "java/lang/System", - "java/lang/Class"); - - /** Library types whose toString() neither throws nor calls application code. */ - static final Set SAFE_TO_STRING = Set.of( - "java/lang/String", "java/lang/Integer", "java/lang/Long", "java/lang/Short", "java/lang/Byte", - "java/lang/Character", "java/lang/Boolean", "java/lang/Double", "java/lang/Float", - "java/lang/StringBuilder", "java/lang/StringBuffer"); - - /** Math/StrictMath methods that never throw, for every overload. */ - private static final Set MATH = Set.of( - "abs", "max", "min", "sqrt", "cbrt", "pow", "exp", "expm1", "log", "log10", "log1p", "sin", "cos", - "tan", "asin", "acos", "atan", "atan2", "sinh", "cosh", "tanh", "hypot", "ceil", "floor", "rint", - "round", "signum", "toRadians", "toDegrees", "ulp", "copySign", "getExponent", "nextUp", "nextDown", - "nextAfter", "scalb", "IEEEremainder", "random", "fma"); - - private static final Map ENTRIES = new HashMap<>(); - - /** Methods declared by java/lang/Object and java/lang/Enum, the library superclasses we know. */ - private static final Map> DECLARED = new HashMap<>(); - - /** Known library supertypes, for assignability. */ - private static final Map> SUPERTYPES = new HashMap<>(); - - private static void add(String owner, Condition c, Returns r, String... methods) { - for (String m : methods) ENTRIES.put(owner + "." + m, new Entry(c, r, false)); - } - - private static void addExact(String owner, Condition c, Returns r, String... methods) { - for (String m : methods) ENTRIES.put(owner + "." + m, new Entry(c, r, true)); - } - - static { - Condition none = Condition.NONE, nonNull = Condition.NONNULL_ARGS, str = Condition.STRING_ARGS; - Returns decl = Returns.DECLARED, fresh = Returns.NONNULL_EXACT, self = Returns.RECEIVER; - - DECLARED.put("java/lang/Object", Set.of("()V", "getClass()Ljava/lang/Class;", "hashCode()I", - "equals(Ljava/lang/Object;)Z", "clone()Ljava/lang/Object;", "toString()Ljava/lang/String;", - "notify()V", "notifyAll()V", "wait()V", "wait(J)V", "wait(JI)V", "finalize()V")); - DECLARED.put("java/lang/Enum", Set.of("(Ljava/lang/String;I)V", "name()Ljava/lang/String;", - "ordinal()I", "toString()Ljava/lang/String;", "equals(Ljava/lang/Object;)Z", "hashCode()I", - "clone()Ljava/lang/Object;", "compareTo(Ljava/lang/Enum;)I", "getDeclaringClass()Ljava/lang/Class;", - "finalize()V", "describeConstable()Ljava/util/Optional;")); - - SUPERTYPES.put("java/lang/String", List.of("java/lang/Object", "java/io/Serializable", - "java/lang/Comparable", "java/lang/CharSequence")); - SUPERTYPES.put("java/lang/Enum", List.of("java/lang/Object", "java/io/Serializable", "java/lang/Comparable")); - for (String n : List.of("Integer", "Long", "Short", "Byte", "Double", "Float")) - SUPERTYPES.put("java/lang/" + n, List.of("java/lang/Number", "java/lang/Comparable")); - SUPERTYPES.put("java/lang/Number", List.of("java/lang/Object", "java/io/Serializable")); - SUPERTYPES.put("java/lang/Character", List.of("java/lang/Object", "java/io/Serializable", "java/lang/Comparable")); - SUPERTYPES.put("java/lang/Boolean", List.of("java/lang/Object", "java/io/Serializable", "java/lang/Comparable")); - SUPERTYPES.put("java/lang/AssertionError", List.of("java/lang/Error")); - SUPERTYPES.put("java/lang/Error", List.of("java/lang/Throwable")); - SUPERTYPES.put("java/lang/Exception", List.of("java/lang/Throwable")); - SUPERTYPES.put("java/lang/Throwable", List.of("java/lang/Object", "java/io/Serializable")); - - // Object and Enum: the implementations an application class may inherit. The final methods - // are safe for every receiver; the others only as the implementation a class inherits. - add("java/lang/Object", none, decl, "()V", "hashCode()I", "equals(Ljava/lang/Object;)Z"); - add("java/lang/Object", none, Returns.DECLARED, "getClass()Ljava/lang/Class;"); - add("java/lang/Enum", none, decl, "(Ljava/lang/String;I)V", "name()Ljava/lang/String;", "ordinal()I", - "toString()Ljava/lang/String;", "equals(Ljava/lang/Object;)Z", "hashCode()I", - "getDeclaringClass()Ljava/lang/Class;"); - - add("java/lang/Class", none, decl, "desiredAssertionStatus()Z"); - - // Throwables: constructing one is safe as long as the object is exactly the library class (a - // subclass could override fillInStackTrace). Throwing it is checked separately. - addExact("java/lang/AssertionError", none, decl, "()V", "(Z)V", "(C)V", "(I)V", - "(J)V", "(F)V", "(D)V", "(Ljava/lang/String;Ljava/lang/Throwable;)V"); - addExact("java/lang/AssertionError", str, decl, "(Ljava/lang/Object;)V"); - for (String t : List.of("java/lang/Error", "java/lang/Exception", "java/lang/RuntimeException")) - addExact(t, none, decl, "()V", "(Ljava/lang/String;)V"); - - // Boxes and their static helpers (no parsing: that throws NumberFormatException). - for (String[] b : new String[][] {{"Integer", "I"}, {"Long", "J"}, {"Short", "S"}, {"Byte", "B"}}) { - String o = "java/lang/" + b[0], p = b[1]; - add(o, none, fresh, "valueOf(" + p + ")L" + o + ";", "toString(" + p + ")Ljava/lang/String;", - "toString()Ljava/lang/String;"); - add(o, none, decl, "compare(" + p + p + ")I", "hashCode(" + p + ")I", "hashCode()I", - "equals(Ljava/lang/Object;)Z", "intValue()I", "longValue()J", "shortValue()S", "byteValue()B", - "floatValue()F", "doubleValue()D"); - add(o, nonNull, decl, "compareTo(L" + o + ";)I"); - } - for (String o : List.of("java/lang/Integer", "java/lang/Long")) { - String p = o.endsWith("Integer") ? "I" : "J"; - add(o, none, decl, "signum(" + p + ")I", "bitCount(" + p + ")I", "reverse(" + p + ")" + p, - "reverseBytes(" + p + ")" + p, "highestOneBit(" + p + ")" + p, "lowestOneBit(" + p + ")" + p, - "numberOfLeadingZeros(" + p + ")I", "numberOfTrailingZeros(" + p + ")I", - "rotateLeft(" + p + "I)" + p, "rotateRight(" + p + "I)" + p, "sum(" + p + p + ")" + p, - "max(" + p + p + ")" + p, "min(" + p + p + ")" + p, "compareUnsigned(" + p + p + ")I"); - add(o, none, fresh, "toString(" + p + "I)Ljava/lang/String;", "toBinaryString(" + p + ")Ljava/lang/String;", - "toHexString(" + p + ")Ljava/lang/String;", "toOctalString(" + p + ")Ljava/lang/String;"); - } - add("java/lang/Integer", none, decl, "toUnsignedLong(I)J"); - for (String[] b : new String[][] {{"Double", "D", "J"}, {"Float", "F", "I"}}) { - String o = "java/lang/" + b[0], p = b[1], bits = b[2]; - String toBits = p.equals("D") ? "doubleToLongBits" : "floatToIntBits"; - String toRaw = p.equals("D") ? "doubleToRawLongBits" : "floatToRawIntBits"; - String fromBits = p.equals("D") ? "longBitsToDouble" : "intBitsToFloat"; - add(o, none, fresh, "valueOf(" + p + ")L" + o + ";", "toString(" + p + ")Ljava/lang/String;", - "toHexString(" + p + ")Ljava/lang/String;", "toString()Ljava/lang/String;"); - add(o, none, decl, "isNaN(" + p + ")Z", "isInfinite(" + p + ")Z", "isFinite(" + p + ")Z", - "compare(" + p + p + ")I", toBits + "(" + p + ")" + bits, toRaw + "(" + p + ")" + bits, - fromBits + "(" + bits + ")" + p, "hashCode(" + p + ")I", "sum(" + p + p + ")" + p, - "max(" + p + p + ")" + p, "min(" + p + p + ")" + p, "isNaN()Z", "isInfinite()Z", "hashCode()I", - "equals(Ljava/lang/Object;)Z", "intValue()I", "longValue()J", "shortValue()S", "byteValue()B", - "floatValue()F", "doubleValue()D"); - add(o, nonNull, decl, "compareTo(L" + o + ";)I"); - } - add("java/lang/Boolean", none, fresh, "valueOf(Z)Ljava/lang/Boolean;", "toString(Z)Ljava/lang/String;", - "toString()Ljava/lang/String;"); - add("java/lang/Boolean", none, decl, "booleanValue()Z", "compare(ZZ)I", "hashCode(Z)I", "hashCode()I", - "equals(Ljava/lang/Object;)Z", "logicalAnd(ZZ)Z", "logicalOr(ZZ)Z", "logicalXor(ZZ)Z", - "parseBoolean(Ljava/lang/String;)Z"); - add("java/lang/Character", none, fresh, "valueOf(C)Ljava/lang/Character;", "toString(C)Ljava/lang/String;", - "toString()Ljava/lang/String;"); - add("java/lang/Character", none, decl, "charValue()C", "compare(CC)I", "hashCode(C)I", "hashCode()I", - "equals(Ljava/lang/Object;)Z", "digit(CI)I", "digit(II)I", "forDigit(II)C", "getNumericValue(C)I", - "getNumericValue(I)I"); - for (String pred : List.of("isDigit", "isLetter", "isLetterOrDigit", "isWhitespace", "isSpaceChar", - "isUpperCase", "isLowerCase", "isAlphabetic", "isJavaIdentifierStart", "isJavaIdentifierPart", - "isISOControl", "isTitleCase", "isDefined")) { - add("java/lang/Character", none, decl, pred + "(C)Z", pred + "(I)Z"); - } - add("java/lang/Character", none, decl, "toUpperCase(C)C", "toLowerCase(C)C", "toUpperCase(I)I", - "toLowerCase(I)I"); - - // String (final): methods that neither index nor parse. - add("java/lang/String", none, decl, "length()I", "isEmpty()Z", "hashCode()I", "equals(Ljava/lang/Object;)Z", - "equalsIgnoreCase(Ljava/lang/String;)Z", "indexOf(I)I", "indexOf(II)I", "lastIndexOf(I)I", - "lastIndexOf(II)I"); - add("java/lang/String", none, fresh, "toString()Ljava/lang/String;", "intern()Ljava/lang/String;", - "trim()Ljava/lang/String;", - "replace(CC)Ljava/lang/String;", "valueOf(I)Ljava/lang/String;", "valueOf(J)Ljava/lang/String;", - "valueOf(F)Ljava/lang/String;", "valueOf(D)Ljava/lang/String;", "valueOf(Z)Ljava/lang/String;", - "valueOf(C)Ljava/lang/String;", "()V"); - add("java/lang/String", nonNull, decl, "compareTo(Ljava/lang/String;)I", - "compareToIgnoreCase(Ljava/lang/String;)I", "startsWith(Ljava/lang/String;)Z", - "startsWith(Ljava/lang/String;I)Z", "endsWith(Ljava/lang/String;)Z", "indexOf(Ljava/lang/String;)I", - "indexOf(Ljava/lang/String;I)I", "lastIndexOf(Ljava/lang/String;)I", "(Ljava/lang/String;)V", - "([C)V"); - // Not concat, toLowerCase, toUpperCase or new StringBuilder(String): on JDK 8 their size - // computations overflow for huge strings and throw NegativeArraySizeException. - add("java/lang/String", nonNull, fresh, "valueOf([C)Ljava/lang/String;"); - add("java/lang/String", none, Returns.NONNULL_EXACT, "toCharArray()[C"); - add("java/lang/String", str, fresh, "valueOf(Ljava/lang/Object;)Ljava/lang/String;"); - - for (String sb : List.of("java/lang/StringBuilder", "java/lang/StringBuffer")) { - String l = "L" + sb + ";"; - add(sb, none, decl, "()V", "length()I"); - add(sb, none, self, "append(Z)" + l, "append(C)" + l, "append(I)" + l, "append(J)" + l, - "append(F)" + l, "append(D)" + l, "append(Ljava/lang/String;)" + l, "reverse()" + l); - add(sb, str, self, "append(Ljava/lang/Object;)" + l, "append(Ljava/lang/CharSequence;)" + l); - add(sb, nonNull, self, "append([C)" + l); - add(sb, none, fresh, "toString()Ljava/lang/String;"); - } - - // System.out / System.err (exactly java.io.PrintStream, see FactInterpreter). - String ps = "java/io/PrintStream"; - addExact(ps, none, decl, "println()V", "println(Z)V", "println(C)V", "println(I)V", "println(J)V", - "println(F)V", "println(D)V", "println(Ljava/lang/String;)V", "print(Z)V", "print(C)V", "print(I)V", - "print(J)V", "print(F)V", "print(D)V", "print(Ljava/lang/String;)V", "flush()V"); - addExact(ps, str, decl, "println(Ljava/lang/Object;)V", "print(Ljava/lang/Object;)V"); - addExact(ps, nonNull, decl, "println([C)V", "print([C)V"); - - add("java/lang/System", none, decl, "currentTimeMillis()J", "nanoTime()J", - "identityHashCode(Ljava/lang/Object;)I", "exit(I)V"); - add("java/lang/System", none, fresh, "lineSeparator()Ljava/lang/String;"); - } - - /** The model of a library method, or null if calls to it fail the check. */ - static Entry lookup(String owner, String name, String desc) { - if (owner.equals("java/lang/Math") || owner.equals("java/lang/StrictMath")) { - return MATH.contains(name) ? new Entry(Condition.NONE, Returns.DECLARED, false) : null; - } - if (owner.startsWith("[") && name.equals("clone") && desc.equals("()Ljava/lang/Object;")) { - return new Entry(Condition.NONE, Returns.CLONE, false); - } - return ENTRIES.get(owner + "." + name + desc); - } - - /** No class can override this library method: its class is final, or the method is. */ - static boolean cannotBeOverridden(String owner, String name, String desc) { - if (FINAL_CLASSES.contains(owner) || owner.startsWith("[")) return true; - if (owner.equals("java/lang/Object")) return name.equals("getClass") || name.equals(""); - if (owner.equals("java/lang/Enum")) { - return !name.equals("toString"); - } - return name.equals(""); - } - - /** Whether we know every method the class (with its library superclasses) declares. */ - static boolean knowsMethodsOf(String owner) { - return DECLARED.containsKey(owner); - } - - /** Whether the library class or one of its library superclasses declares the method. */ - static boolean declares(String owner, String name, String desc) { - return declaringClass(owner, name, desc) != null; - } - - /** The class among the known library classes that declares the method an instance of owner inherits. */ - static String declaringClass(String owner, String name, String desc) { - for (String c = owner; c != null; c = c.equals("java/lang/Enum") ? "java/lang/Object" : null) { - Set d = DECLARED.get(c); - if (d != null && d.contains(name + desc)) return c; - } - return null; - } - - static List knownSupertypes(String type) { - return SUPERTYPES.getOrDefault(type, List.of("java/lang/Object")); - } - - /** Library interfaces known to declare no default methods (on JDK 8 to 21). */ - private static final Set NO_DEFAULTS = Set.of("java/io/Serializable", "java/lang/Cloneable", - "java/lang/Comparable", "java/lang/Runnable", "java/lang/AutoCloseable", "java/io/Closeable"); - - static boolean hasNoDefaultMethods(String iface) { - return NO_DEFAULTS.contains(iface); - } - - static boolean isFinalClass(String owner) { - return FINAL_CLASSES.contains(owner); - } -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/Program.java b/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/Program.java deleted file mode 100644 index b99e2b8d..00000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/staticcheck/Program.java +++ /dev/null @@ -1,361 +0,0 @@ -package de.uzl.its.swat.staticcheck; - -import java.io.IOException; -import java.io.InputStream; -import java.nio.file.Files; -import java.nio.file.Path; -import java.util.*; -import java.util.jar.JarEntry; -import java.util.jar.JarFile; -import java.util.stream.Stream; -import org.objectweb.asm.ClassReader; -import org.objectweb.asm.Opcodes; -import org.objectweb.asm.tree.ClassNode; -import org.objectweb.asm.tree.FieldNode; -import org.objectweb.asm.tree.MethodNode; - -/** - * The application classes of a program (every class file on its classpath) and the queries the - * check needs on them: hierarchy, method and field resolution, and the possible targets of a call. - * Every class that is not on the classpath is a library (JDK) class. - */ -final class Program { - - /** - * The SV-COMP Verifier package: modelled by the check instead of analysed. Built at run time, - * so that the shadow jar's relocation of org.sosy_lab (java-smt) does not rewrite it. - */ - static final String VERIFIER_PACKAGE = "org/".concat("sosy_lab/sv_benchmarks/"); - - /** A method of an application class. */ - static final class Method { - final ClassNode owner; - final MethodNode node; - final String key; - - Method(ClassNode owner, MethodNode node) { - this.owner = owner; - this.node = node; - this.key = owner.name + "." + node.name + node.desc; - } - - boolean isStatic() { - return (node.access & Opcodes.ACC_STATIC) != 0; - } - - boolean hasCode() { - return (node.access & (Opcodes.ACC_ABSTRACT | Opcodes.ACC_NATIVE)) == 0; - } - - @Override - public String toString() { - return key; - } - } - - /** - * Where a call may go: application methods, plus library methods (owner.name+desc) when the - * receiver can be a library object or inherit a library implementation. - */ - static final class Targets { - final Set methods = new LinkedHashSet<>(); - final Set libraryMethods = new LinkedHashSet<>(); - } - - private final Map classes = new LinkedHashMap<>(); - private final Map methods = new LinkedHashMap<>(); - private final Map> subtypes = new HashMap<>(); - - Program(List classpath) throws IOException { - for (Path entry : classpath) { - if (Files.isDirectory(entry)) { - try (Stream files = Files.walk(entry)) { - for (Path p : (Iterable) files.filter(f -> f.toString().endsWith(".class"))::iterator) { - try (InputStream in = Files.newInputStream(p)) { - add(in); - } - } - } - } else if (entry.toString().endsWith(".jar") && Files.isRegularFile(entry)) { - try (JarFile jar = new JarFile(entry.toFile())) { - for (JarEntry e : Collections.list(jar.entries())) { - if (e.getName().endsWith(".class") && !e.getName().startsWith("META-INF/")) { - try (InputStream in = jar.getInputStream(e)) { - add(in); - } - } - } - } - } - } - for (ClassNode c : classes.values()) { - if (c.superName != null) subtypes.computeIfAbsent(c.superName, k -> new ArrayList<>()).add(c.name); - for (String i : c.interfaces) subtypes.computeIfAbsent(i, k -> new ArrayList<>()).add(c.name); - } - } - - private void add(InputStream in) throws IOException { - ClassNode c = new ClassNode(); - new ClassReader(in).accept(c, ClassReader.SKIP_FRAMES); - // The first definition on the classpath wins, as for the JVM's class loader. - if (classes.containsKey(c.name)) return; - if (unsupported == null) unsupported = unsupportedReason(c.name); - classes.put(c.name, c); - if (c.name.startsWith(VERIFIER_PACKAGE)) return; - for (MethodNode m : c.methods) { - Method method = new Method(c, m); - methods.put(method.key, method); - } - } - - /** - * Why a class on the classpath breaks the assumption that the classpath is the program (null - * if it does not). The JVM does not load such a class the way the analysis models it: it - * refuses java/ packages, serves packages the platform defines from the platform, and the - * analysis models only Verifier and ObjectFactory of the Verifier package, so the static - * initializer of any other class there would run unanalysed. - */ - private static String unsupportedReason(String name) { - int slash = name.lastIndexOf('/'); - String pkg = slash < 0 ? "" : name.substring(0, slash); - if (name.startsWith(VERIFIER_PACKAGE)) { - if (name.equals(VERIFIER_PACKAGE + "Verifier") || name.equals(VERIFIER_PACKAGE + "ObjectFactory")) return null; - return "class " + name + " in the Verifier package"; - } - for (String prefix : PLATFORM_PREFIXES) { - if (name.startsWith(prefix)) return "class " + name + " in a platform package"; - } - if (PLATFORM_PACKAGES.contains(pkg.replace('/', '.'))) return "class " + name + " in a package of the JDK"; - return null; - } - - /** - * Package prefixes of the platform: java/, javax/, jdk/, sun/, and those that exist only in the - * JDK 8 runtime (not as modules of the JDK the check runs on). - */ - private static final List PLATFORM_PREFIXES = List.of("java/", "javax/", "jdk/", "sun/", "com/sun/", - "org/omg/", "org/w3c/", "org/xml/", "org/ietf/", "org/jcp/"); - - /** The packages of the JDK's boot modules (the platform the check runs on). */ - private static final Set PLATFORM_PACKAGES = new HashSet<>(); - - static { - for (Module m : ModuleLayer.boot().modules()) PLATFORM_PACKAGES.addAll(m.getPackages()); - } - - /** Set if a class on the classpath breaks the model of class loading; the check then fails. */ - private String unsupported; - - String unsupportedClasspath() { - return unsupported; - } - - /** An application class (not a library class, and not the modelled Verifier package). */ - boolean isApp(String internalName) { - return classes.containsKey(internalName) && !internalName.startsWith(VERIFIER_PACKAGE); - } - - boolean isOnClasspath(String internalName) { - return classes.containsKey(internalName); - } - - ClassNode clazz(String internalName) { - return classes.get(internalName); - } - - Collection methods() { - return methods.values(); - } - - Method method(String owner, String name, String desc) { - return methods.get(owner + "." + name + desc); - } - - Collection appClasses() { - List out = new ArrayList<>(); - for (ClassNode c : classes.values()) if (isApp(c.name)) out.add(c); - return out; - } - - boolean isEnum(String internalName) { - ClassNode c = classes.get(internalName); - return c != null && isApp(internalName) && (c.access & Opcodes.ACC_ENUM) != 0 - && "java/lang/Enum".equals(c.superName); - } - - /** The class and its application superclasses, ending with the first library class (if any). */ - List superChain(String internalName) { - List chain = new ArrayList<>(); - String c = internalName; - while (c != null) { - chain.add(c); - ClassNode node = classes.get(c); - if (node == null || !isApp(c)) break; - c = node.superName; - } - return chain; - } - - /** All application types that are subtypes of the given type, the type itself included. */ - Set appSubtypes(String type) { - Set out = new LinkedHashSet<>(); - Deque work = new ArrayDeque<>(); - work.add(type); - while (!work.isEmpty()) { - String t = work.poll(); - if (isApp(t) && !out.add(t)) continue; - for (String s : subtypes.getOrDefault(t, List.of())) if (!out.contains(s)) work.add(s); - } - return out; - } - - /** All application supertypes (classes and interfaces) of an application type, itself included. */ - Set appSupertypes(String type) { - Set out = new LinkedHashSet<>(); - Deque work = new ArrayDeque<>(); - work.add(type); - while (!work.isEmpty()) { - String t = work.poll(); - ClassNode c = classes.get(t); - if (c == null || !isApp(t) || !out.add(t)) continue; - if (c.superName != null) work.add(c.superName); - work.addAll(c.interfaces); - } - return out; - } - - /** The field a field instruction refers to: declared in the owner or a superclass/superinterface. */ - FieldNode resolveField(String owner, String name, String desc, String[] declaringClass) { - Deque work = new ArrayDeque<>(); - work.add(owner); - Set seen = new HashSet<>(); - while (!work.isEmpty()) { - String t = work.poll(); - if (!seen.add(t)) continue; - ClassNode c = classes.get(t); - if (c == null || !isApp(t)) continue; - for (FieldNode f : c.fields) { - if (f.name.equals(name) && f.desc.equals(desc)) { - declaringClass[0] = t; - return f; - } - } - work.addAll(c.interfaces); - if (c.superName != null) work.add(c.superName); - } - return null; - } - - /** - * The method a static or special call (or a virtual call on a known runtime class) executes, - * searching the class and its superclasses. Returns the application method, or null with - * libraryOwner[0] set to the first library class of the chain when the search leaves the - * application. - */ - Method resolveInChain(String owner, String name, String desc, String[] libraryOwner) { - for (String c : superChain(owner)) { - if (!isApp(c)) { - libraryOwner[0] = c; - return null; - } - Method m = method(c, name, desc); - if (m != null) return m; - } - return null; - } - - /** All default methods for name+desc in the application interfaces of a class. */ - private List defaults(String clazz, String name, String desc) { - List out = new ArrayList<>(); - for (String t : appSupertypes(clazz)) { - ClassNode c = classes.get(t); - if ((c.access & Opcodes.ACC_INTERFACE) == 0) continue; - Method m = method(t, name, desc); - if (m != null && m.hasCode() && !m.isStatic() && (m.node.access & Opcodes.ACC_PRIVATE) == 0) out.add(m); - } - return out; - } - - /** - * The targets of an invokevirtual/invokeinterface on an application owner type: a superset of - * the methods the JVM may select for each concrete application subtype of the owner (JVMS - * 5.4.6). Rather than following the selection rules exactly (package-private overriding, - * maximally-specific default methods), every non-private instance method with that name and - * descriptor in the superclass chain, and every default method of the application - * superinterfaces, counts. A library implementation counts unless a public or protected - * application method overrides it. Returns null if a library class or library interface whose - * methods are unknown might provide it. - */ - Targets virtualTargets(String owner, String name, String desc) { - Targets t = new Targets(); - Method declared = method(owner, name, desc); - if (declared != null && (declared.node.access & Opcodes.ACC_PRIVATE) != 0) { - // A private method is selected directly (invokevirtual on a nestmate's private method). - if (!declared.hasCode()) return null; - t.methods.add(declared); - return t; - } - for (String sub : appSubtypes(owner)) { - ClassNode c = classes.get(sub); - if ((c.access & (Opcodes.ACC_ABSTRACT | Opcodes.ACC_INTERFACE)) != 0) continue; - boolean overridesLibrary = false; - String lib = null; - for (String k : superChain(sub)) { - if (!isApp(k)) { - lib = k; - break; - } - Method m = method(k, name, desc); - if (m == null || m.isStatic() || (m.node.access & Opcodes.ACC_PRIVATE) != 0) continue; - if ((m.node.access & Opcodes.ACC_NATIVE) != 0) return null; - if (m.hasCode()) t.methods.add(m); - if ((m.node.access & (Opcodes.ACC_PUBLIC | Opcodes.ACC_PROTECTED)) != 0) overridesLibrary = true; - } - t.methods.addAll(defaults(sub, name, desc)); - if (overridesLibrary) continue; - // A default method of a library interface could be selected instead, and we do not know them. - for (String sup : appSupertypes(sub)) { - for (String i : classes.get(sup).interfaces) { - if (!isApp(i) && !JdkModel.hasNoDefaultMethods(i)) return null; - } - } - if (lib == null) continue; - String declaring = JdkModel.declaringClass(lib, name, desc); - if (declaring != null) t.libraryMethods.add(declaring + "." + name + desc); - else if (!JdkModel.knowsMethodsOf(lib)) return null; - } - return t; - } - - /** Whether a value of type {@code from} is always assignable to type {@code to}. */ - boolean isAssignable(String from, String to) { - if (from == null || to == null) return false; - if (from.equals(to) || to.equals("java/lang/Object")) return true; - if (from.startsWith("[")) { - if (to.equals("java/lang/Cloneable") || to.equals("java/io/Serializable")) return true; - if (!to.startsWith("[")) return false; - String fe = from.substring(1), te = to.substring(1); - if (fe.startsWith("[") || te.startsWith("[")) return isAssignable(fe, te); - if (fe.startsWith("L") && te.startsWith("L")) - return isAssignable(fe.substring(1, fe.length() - 1), te.substring(1, te.length() - 1)); - return fe.equals(te); - } - if (to.startsWith("[")) return false; - Deque work = new ArrayDeque<>(); - work.add(from); - Set seen = new HashSet<>(); - while (!work.isEmpty()) { - String t = work.poll(); - if (!seen.add(t)) continue; - if (t.equals(to)) return true; - if (isApp(t)) { - ClassNode c = classes.get(t); - if (c.superName != null) work.add(c.superName); - work.addAll(c.interfaces); - } else { - work.addAll(JdkModel.knownSupertypes(t)); - } - } - return false; - } -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowContext.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowContext.java index 54580208..6710df3b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowContext.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowContext.java @@ -67,15 +67,19 @@ public void putToHeap(int hashCode, Value value) { public void pushFrame(Frame frame) { activeFrame = frame; frameStack.push(frame); - if (!isSwatHelper(frame)) { + if (isSwatHelper(frame)) { + helperFrames++; + } else { pushedSinceBranch.add(frame); } } /** - * A frame of SWAT's own instrumented helpers (e.g. {@code UtilInstrumented.refEquals}). The - * static pre-analysis graph has their branches inline in the caller, so the stack changes the - * trace reports leave their frames out. + * A frame of SWAT's own instrumented helpers (e.g. {@code UtilInstrumented.refEquals}). They + * are not in the static pre-analysis graph: how many branches {@code refEquals} takes depends on + * the runtime types of its arguments. So the stack changes the trace reports leave their frames + * out, and their branches are reported like callbacks ({@link #inSwatHelper}), which the walk + * holds its place for. */ private static boolean isSwatHelper(Frame frame) { return frame.getClassName() != null && frame.getClassName().startsWith("de/uzl/its/swat/"); @@ -91,6 +95,14 @@ private static boolean isSwatHelper(Frame frame) { /** How many frames on the stack are library frames that application code was called back in. */ private int callbackFrames = 0; + /** How many frames on the stack are SWAT helper frames (see {@link #isSwatHelper}). */ + private int helperFrames = 0; + + /** Whether a SWAT helper runs, e.g. a rewritten reference comparison: its branches are not in the graph. */ + public boolean inSwatHelper() { + return helperFrames > 0; + } + /** * Marks the active frame, a library frame, as running application code that the library * called back (a delegation). @@ -131,7 +143,7 @@ public Frame popFrame() { callbackFrames--; } if (isSwatHelper(oldFrame)) { - // not counted on push either + helperFrames--; // not counted in the stack changes on push either } else if (pushedSinceBranch.isEmpty()) { poppedSinceBranch++; } else { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java index 5c0de7a5..9636a01b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java @@ -33,7 +33,9 @@ final class BranchElement extends Element { @lombok.Setter private String key; @lombok.Setter private int pops; @lombok.Setter private java.util.List pushes = java.util.List.of(); - // Recorded in application code that library code called back (see ShadowContext.inCallback). + // Recorded where the static pre-analysis graph has no counterpart: in application code that + // library code called back (see ShadowContext.inCallback), or in a SWAT helper such as the + // reference comparison (see ShadowContext.inSwatHelper). @lombok.Setter private boolean callback; // The loop-head states the execution reached since the previous branch, in order (see // LoopStateMatcher). diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java index 3c36f6b6..5893a523 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java @@ -124,7 +124,8 @@ private static void place(BranchElement branch, long iid, String suffix) throws String key = BranchKeys.keyOf(iid); branch.setKey(key == null ? null : key + suffix); ShadowContext stack = ThreadHandler.getSymbolicVisitor(Thread.currentThread().getId()).getStack(); - branch.setCallback(stack.inCallback()); + // Neither callbacks nor SWAT's helpers are in the static pre-analysis graph: the walk holds its place. + branch.setCallback(stack.inCallback() || stack.inSwatHelper()); ShadowContext.StackDelta delta = stack.takeStackDelta(); branch.setPops(delta.popped()); List pushes = new ArrayList<>(delta.pushed().size()); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/StringArrayValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/StringArrayValue.java index efe5c9ce..2018ca00 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/StringArrayValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/StringArrayValue.java @@ -101,7 +101,8 @@ protected void initArray(String[] array) { StringFormulaManager smgr = context.getFormulaManager().getStringFormulaManager(); // ToDo (Nils): Is this needed or correct? for (int i = 0; i < array.length; i++) { - formula = amgr.store(formula, getIndex(i), smgr.makeString(concrete[i])); + formula = amgr.store(formula, getIndex(i), + StringValue.literal(smgr, context.getFormulaManager().getIntegerFormulaManager(), concrete[i])); } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java index d15dcd98..7448119f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java @@ -45,7 +45,18 @@ public StringValue(SolverContext context, String concrete, int address) { this.smgr = context.getFormulaManager().getStringFormulaManager(); this.imgr = context.getFormulaManager().getIntegerFormulaManager(); this.concrete = concrete; - this.formula = smgr.makeString(concrete); + this.formula = literal(smgr, imgr, concrete); + } + + /** + * A Java string as the solver's string: one char per UTF-16 char. makeString would take a + * surrogate pair for one char (and rejects code points above the third plane). + */ + public static StringFormula literal(StringFormulaManager smgr, IntegerFormulaManager imgr, String s) { + if (s.chars().noneMatch(c -> Character.isSurrogate((char) c))) return smgr.makeString(s); + StringFormula chars = smgr.makeString(""); + for (char c : s.toCharArray()) chars = smgr.concat(chars, smgr.fromCodePoint(imgr.makeNumber(c))); + return chars; } public StringValue(SolverContext context, String concrete, StringFormula formula, int address) { @@ -810,13 +821,15 @@ public static java.util.Locale caseMappingLocale(Value[] args) { throws NotImplementedException, ValueConversionException { if (args.length == 1) { return switch (desc[0].getDescriptor()) { - case "I" -> invokeIndexOf(args[0].asIntValue()); + case "I" -> args[0] instanceof CharValue c + ? invokeIndexOf(c, new IntValue(context, 0)) : invokeIndexOf(args[0].asIntValue()); case "Ljava/lang/String;" -> invokeIndexOf(args[0].asStringValue()); default -> PlaceHolder.instance; }; } else if (args.length == 2) { return switch (desc[0].getDescriptor()) { - case "I" -> invokeIndexOf(args[0].asIntValue(), args[1].asIntValue()); + case "I" -> args[0] instanceof CharValue c + ? invokeIndexOf(c, args[1].asIntValue()) : invokeIndexOf(args[0].asIntValue(), args[1].asIntValue()); case "Ljava/lang/String;" -> invokeIndexOf( args[0].asStringValue(), args[1].asIntValue()); default -> PlaceHolder.instance; @@ -856,13 +869,25 @@ public static java.util.Locale caseMappingLocale(Value[] args) { return new IntValue(context, result, bmgr.ifThenElse(isCodePoint(ch), index.asIntegerFormula(), imgr.makeNumber(-1))); } + /** + * indexOf(int) of a char: a char is a code point in the BMP, so it is searched for as itself, + * without the surrogate pair and range cases of an int (whose div and mod slow Z3 down). + */ + private Value invokeIndexOf(CharValue ch, IntValue fromIndex) { + int result = concrete.indexOf(ch.concrete, fromIndex.concrete); + if (!isSymbolic() && !ch.isSymbolic() && !fromIndex.isSymbolic()) return new IntValue(context, result); + IntValue index = (IntValue) invokeIndexOf( + new StringValue(context, "", smgr.fromCodePoint(ch.asIntegerFormula()), -1), fromIndex); + return new IntValue(context, result, index.formula); + } + /** Whether ch is a code point, i.e. in [0, 0x10FFFF]: the chars indexOf(int)/lastIndexOf(int) can find. */ private BooleanFormula isCodePoint(IntValue ch) { BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); if (!ch.isSymbolic()) return bmgr.makeBoolean(Character.isValidCodePoint(ch.concrete)); - NumeralFormula.IntegerFormula c = ch.asIntegerFormula(); - return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(0)), - imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_CODE_POINT))); + BitvectorFormulaManager bvmgr = context.getFormulaManager().getBitvectorFormulaManager(); + // Unsigned: the negative ints are above every code point. + return bvmgr.lessOrEquals(ch.formula, bvmgr.makeBitvector(32, Character.MAX_CODE_POINT), false); } /** @@ -878,13 +903,23 @@ public StringFormula codePointString(IntValue ch) { for (char c : Character.toChars(ch.concrete)) chars = smgr.concat(chars, smgr.fromCodePoint(imgr.makeNumber(c))); return chars; } - NumeralFormula.IntegerFormula c = ch.asIntegerFormula(); - NumeralFormula.IntegerFormula offset = imgr.subtract(c, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)); - NumeralFormula.IntegerFormula high = imgr.add(imgr.makeNumber(Character.MIN_HIGH_SURROGATE), imgr.divide(offset, imgr.makeNumber(1024))); - NumeralFormula.IntegerFormula low = imgr.add(imgr.makeNumber(Character.MIN_LOW_SURROGATE), imgr.modulo(offset, imgr.makeNumber(1024))); - return bmgr.ifThenElse(imgr.lessThan(c, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)), - smgr.fromCodePoint(c), - smgr.concat(smgr.fromCodePoint(high), smgr.fromCodePoint(low))); + // Over bit-vectors, as ch is one: Integer div and mod of a converted bit-vector slow Z3 down + // badly (a query on s.indexOf(ch) went from minutes to under a second). + BitvectorFormulaManager bvmgr = context.getFormulaManager().getBitvectorFormulaManager(); + BitvectorFormula c = ch.formula; + BitvectorFormula offset = bvmgr.subtract(c, bvmgr.makeBitvector(32, Character.MIN_SUPPLEMENTARY_CODE_POINT)); + BitvectorFormula high = bvmgr.add(bvmgr.makeBitvector(32, Character.MIN_HIGH_SURROGATE), + bvmgr.shiftRight(offset, bvmgr.makeBitvector(32, 10), false)); + BitvectorFormula low = bvmgr.add(bvmgr.makeBitvector(32, Character.MIN_LOW_SURROGATE), + bvmgr.and(offset, bvmgr.makeBitvector(32, 0x3FF))); + return bmgr.ifThenElse(bvmgr.lessThan(c, bvmgr.makeBitvector(32, Character.MIN_SUPPLEMENTARY_CODE_POINT), false), + smgr.fromCodePoint(charCode(bvmgr, c)), + smgr.concat(smgr.fromCodePoint(charCode(bvmgr, high)), smgr.fromCodePoint(charCode(bvmgr, low)))); + } + + /** The low 16 bits of b as an Integer: a char code, where b is known to fit them. */ + private static NumeralFormula.IntegerFormula charCode(BitvectorFormulaManager bvmgr, BitvectorFormula b) { + return bvmgr.toIntegerFormula(bvmgr.extract(b, 15, 0), false); } /** @@ -1250,7 +1285,7 @@ private static String literalRegexArgument(Value[] args) { StringValue replacement = (StringValue) args[1]; String result = concrete.replaceFirst(((StringValue) args[0]).concrete, replacement.concrete); if (!isSymbolic()) return new StringValue(context, result, -1); - return new StringValue(context, result, smgr.replace(formula, smgr.makeString(target), replacement.formula), -1); + return new StringValue(context, result, smgr.replace(formula, literal(smgr, imgr, target), replacement.formula), -1); } /** diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/staticcheck/ExceptionFreedomCheckSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/staticcheck/ExceptionFreedomCheckSpec.groovy deleted file mode 100644 index 038e9251..00000000 --- a/symbolic-executor/src/test/groovy/de/uzl/its/swat/staticcheck/ExceptionFreedomCheckSpec.groovy +++ /dev/null @@ -1,152 +0,0 @@ -package de.uzl.its.swat.staticcheck - -import spock.lang.Specification -import spock.lang.TempDir -import spock.lang.Unroll - -import javax.tools.ToolProvider -import java.nio.file.Files -import java.nio.file.Path - -/** - * Compiles small programs and checks the verdict of the exception-freedom check. The programs - * that may throw an uncaught RuntimeException must never pass; the others document what the - * check is able to prove. - */ -class ExceptionFreedomCheckSpec extends Specification { - - static final String VERIFIER = ''' -package org.sosy_lab.sv_benchmarks; -public final class Verifier { - public static void assume(boolean c) { if (!c) Runtime.getRuntime().halt(1); } - public static boolean nondetBoolean() { return new java.util.Random().nextBoolean(); } - public static int nondetInt() { return new java.util.Random().nextInt(); } - public static long nondetLong() { return new java.util.Random().nextLong(); } - public static double nondetDouble() { return new java.util.Random().nextDouble(); } - public static String nondetString() { return "" + new java.util.Random().nextInt(); } - public static T nondetObject(Class t, ObjectFactory f) { return f.createObject(); } -} -''' - static final String FACTORY = ''' -package org.sosy_lab.sv_benchmarks; -public interface ObjectFactory { T createObject(); } -''' - - @TempDir - Path dir - - ExceptionFreedomCheck.Result check(String main, String release = '8', Map extra = [:]) { - Path src = dir.resolve('src'), out = dir.resolve('classes') - Files.createDirectories(src.resolve('org/sosy_lab/sv_benchmarks')) - Files.createDirectories(out) - Files.writeString(src.resolve('org/sosy_lab/sv_benchmarks/Verifier.java'), VERIFIER) - Files.writeString(src.resolve('org/sosy_lab/sv_benchmarks/ObjectFactory.java'), FACTORY) - Files.writeString(src.resolve('Main.java'), 'import org.sosy_lab.sv_benchmarks.Verifier;\n' + main) - extra.each { path, code -> - Files.createDirectories(src.resolve(path).parent) - Files.writeString(src.resolve(path), code) - } - def files = [] - src.toFile().eachFileRecurse { if (it.name.endsWith('.java')) files << it.path } - int rc = ToolProvider.getSystemJavaCompiler().run(null, null, null, - (['--release', release, '-nowarn', '-d', out.toString()] + files) as String[]) - assert rc == 0 - return ExceptionFreedomCheck.check([out]) - } - - @Unroll - def "may throw: #name"() { - expect: - !check(program, release).exceptionFree - - where: - name | release | program - 'division by input' | '8' | 'public class Main { public static void main(String[] a) { int x = Verifier.nondetInt(); int y = 10 / x; } }' - 'long division by zero constant' | '8' | 'public class Main { public static void main(String[] a) { long x = Verifier.nondetLong(); long y = x / 0L; } }' - 'array index from input' | '8' | 'public class Main { public static void main(String[] a) { int[] arr = new int[3]; arr[Verifier.nondetInt()] = 1; } }' - 'array index past the end' | '8' | 'public class Main { public static void main(String[] a) { int[] arr = new int[3]; int i = 2; i++; arr[i] = 1; } }' - 'array index in a loop' | '8' | 'public class Main { public static void main(String[] a) { int[] arr = new int[3]; for (int i = 0; i < 4; i++) arr[i] = 1; } }' - 'negative array size' | '8' | 'public class Main { public static void main(String[] a) { int[] arr = new int[Verifier.nondetInt()]; } }' - 'field never assigned' | '8' | 'class B { void g() {} } class A { B b; } public class Main { public static void main(String[] a) { new A().b.g(); } }' - 'field assigned on one path' | '8' | 'class B { void g() {} } class A { B b; A(boolean c) { if (c) b = new B(); } } public class Main { public static void main(String[] a) { new A(Verifier.nondetBoolean()).b.g(); } }' - 'field set to null later' | '8' | 'class B { void g() {} } class A { B b = new B(); } public class Main { public static void main(String[] a) { A x = new A(); if (Verifier.nondetBoolean()) x.b = null; x.b.g(); } }' - 'read in overridden method from super constructor' | '8' | 'class B { void g() {} } class P { P() { init(); } void init() {} } class C extends P { B b = new B(); void init() { b.g(); } } public class Main { public static void main(String[] a) { new C(); } }' - 'receiver escapes before assignment' | '8' | 'class B { void g() {} } class Reg { static A last = new A(1); } class A { B b; A(int x) { Reg.last = this; int y = 10 / x; b = new B(); } } public class Main { public static void main(String[] a) { try { new A(Verifier.nondetInt()); } catch (Exception e) {} Reg.last.b.g(); } }' - 'static field read before assignment' | '8' | 'class B { void g() {} } class T { static B peek() { return S.b; } } class S { static B a = T.peek(); static B b = new B(); } public class Main { public static void main(String[] a) { S.a.g(); } }' - 'static field never assigned' | '8' | 'class B { void g() {} } class S { static B b; } public class Main { public static void main(String[] a) { S.b.g(); } }' - 'null argument' | '8' | 'class B { void g() {} } public class Main { static void f(B b) { b.g(); } public static void main(String[] a) { f(Verifier.nondetBoolean() ? new B() : null); } }' - 'null return value' | '8' | 'class B { void g() {} } public class Main { static B make() { return Verifier.nondetBoolean() ? new B() : null; } public static void main(String[] a) { make().g(); } }' - 'interface implementation throws' | '8' | 'interface I { void f(); } class A implements I { public void f() { throw new IllegalStateException(); } } class C implements I { public void f() {} } public class Main { public static void main(String[] a) { I i = Verifier.nondetBoolean() ? new A() : new C(); i.f(); } }' - 'toString callback through valueOf' | '8' | 'class A { public String toString() { throw new IllegalStateException(); } } public class Main { public static void main(String[] a) { String s = String.valueOf(new A()); } }' - 'toString callback in concatenation' | '8' | 'class A { public String toString() { throw new IllegalStateException(); } } public class Main { public static void main(String[] a) { String s = "x" + new A(); } }' - 'toString callback through indy' | '17' | 'class A { public String toString() { throw new IllegalStateException(); } } public class Main { public static void main(String[] a) { String s = "x" + new A(); } }' - 'rethrow of caught exception' | '8' | 'public class Main { public static void main(String[] a) { try { int y = 1 / Verifier.nondetInt(); } catch (ArithmeticException e) { throw e; } } }' - 'finally after a throwing body' | '8' | 'public class Main { static int n; public static void main(String[] a) { try { int y = 1 / Verifier.nondetInt(); } finally { n++; } } }' - 'inner handler rethrows' | '8' | 'public class Main { public static void main(String[] a) { try { try { int y = 1 / Verifier.nondetInt(); } catch (Exception e) { throw new IllegalStateException(); } } catch (ArithmeticException e) {} } }' - 'static initializer throws' | '8' | 'class S { static int x = 10 / Verifier.nondetInt(); } public class Main { public static void main(String[] a) { int y = S.x; } }' - 'array store of wrong type' | '8' | 'public class Main { public static void main(String[] a) { Object[] arr = new String[1]; arr[0] = new Object(); } }' - 'failing cast' | '8' | 'public class Main { public static void main(String[] a) { Object o = Verifier.nondetBoolean() ? (Object) "s" : (Object) new Object(); String s = (String) o; } }' - 'unboxing null' | '8' | 'public class Main { public static void main(String[] a) { Integer i = Verifier.nondetBoolean() ? null : 3; int x = i; } }' - 'callback from a caught library call' | '8' | 'class B { void g() {} } class H { static B b = new B(); } class Cmp implements java.util.Comparator { public int compare(Object x, Object y) { H.b = (B) x; return 0; } } public class Main { public static void main(String[] a) { try { java.util.Arrays.sort(new Object[] {null, null}, new Cmp()); } catch (Exception e) {} H.b.g(); } }' - 'lambda' | '8' | 'public class Main { public static void main(String[] a) { Runnable r = () -> { int y = 1 / Verifier.nondetInt(); }; r.run(); } }' - 'runtime exception subclass thrown' | '8' | 'class E extends RuntimeException {} public class Main { public static void main(String[] a) { if (Verifier.nondetBoolean()) throw new E(); } }' - 'private method of abstract class' | '17' | 'public class Main { static abstract class P { private void m() { int z = Verifier.nondetInt(); int q = 1 / z; } void call() { m(); } } static class Q extends P { void m() {} } public static void main(String[] a) { new Q().call(); } }' - 'nondetObject' | '8' | 'class B { void g() {} } public class Main { public static void main(String[] a) { B b = Verifier.nondetObject(B.class, () -> new B()); b.g(); } }' - 'finalizer' | '8' | 'class B { protected void finalize() {} } public class Main { public static void main(String[] a) { new B(); } }' - 'unmodelled library call' | '8' | 'public class Main { public static void main(String[] a) { String s = Verifier.nondetString(); char c = s.charAt(3); } }' - 'println of an object' | '8' | 'class A { public String toString() { throw new IllegalStateException(); } } public class Main { public static void main(String[] a) { System.out.println(new A()); } }' - 'null string argument' | '8' | 'public class Main { public static void main(String[] a) { String s = Verifier.nondetBoolean() ? null : "x"; boolean b = "abc".startsWith(s); } }' - 'main called with null' | '8' | 'public class Main { public static void main(String[] a) { if (Verifier.nondetBoolean()) { main(null); } else { int n = a.length; } } }' - 'more specific default method' | '8' | 'interface I { default int m() { return 0; } } interface J extends I { default int m() { throw new IllegalStateException(); } } class C implements I, J {} public class Main { public static void main(String[] a) { new C().m(); } }' - 'private method does not implement' | '17' | 'interface I { default void m() { throw new IllegalStateException(); } } class B { private void m() {} } class C extends B implements I {} public class Main { public static void main(String[] a) { I x = new C(); x.m(); } }' - 'receiver escapes through a join' | '8' | 'interface G { String get(); } class G0 implements G { public String get() { return "ok"; } } class Holder { G g; Holder() { this.g = new G0(); } } abstract class Base implements G { Base() { G o = Verifier.nondetBoolean() ? this : Main.H.g; Main.H.g = o; } } class C extends Base { String f; C(int d) { super(); int z = 10 / d; this.f = "x"; } public String get() { return this.f; } } public class Main { static Holder H = new Holder(); public static void main(String[] a) { try { new C(Verifier.nondetInt()); } catch (RuntimeException e) { } String s = H.g.get(); int n = s.length(); } }' - 'concat overflows on JDK 8' | '8' | 'public class Main { public static void main(String[] a) { String s = Verifier.nondetString(); String t = s.concat(s); } }' - 'StringBuilder constructor overflows' | '8' | 'public class Main { public static void main(String[] a) { StringBuilder sb = new StringBuilder(Verifier.nondetString()); } }' - 'library default method' | '8' | 'class It implements java.util.Iterator { public boolean hasNext() { return false; } public Object next() { return null; } } public class Main { public static void main(String[] a) { if (Verifier.nondetInt() == 42) new It().remove(); } }' - 'library default calls back' | '17' | 'class X implements CharSequence { public int length() { throw new IllegalStateException(); } public char charAt(int i) { return 0; } public CharSequence subSequence(int s, int e) { return this; } public String toString() { return ""; } } public class Main { public static void main(String[] a) { if (Verifier.nondetBoolean()) { boolean b = new X().isEmpty(); } } }' - 'library default via app interface' | '8' | 'interface J extends java.util.Iterator {} abstract class Ab implements J { public boolean hasNext() { return false; } } class It extends Ab { public Object next() { return null; } } public class Main { public static void main(String[] a) { J j = new It(); j.remove(); } }' - } - - static final String STEAL = 'static { try { java.lang.reflect.Field f = Class.forName("Main").getDeclaredField("o"); f.setAccessible(true); f.set(null, null); } catch (Exception e) {} }' - - @Unroll - def "classes the JVM loads differently than modelled: #name"() { - when: - def r = check(program, '8', extra) - - then: - !r.exceptionFree - !r.assertionFree - - where: - name | program | extra - 'Verifier package helper' | 'public class Main { static Object o = new Object(); public static void main(String[] a) { int z = org.sosy_lab.sv_benchmarks.Helper.X; System.out.println(o.hashCode() + z); } }' | ['org/sosy_lab/sv_benchmarks/Helper.java': 'package org.sosy_lab.sv_benchmarks; public class Helper { public static int X; ' + STEAL + ' }'] - 'javax class nulls a field' | 'public class Main { static Object o = new Object(); public static void main(String[] a) { int z = javax.mine.Helper.X; System.out.println(o.hashCode() + z); } }' | ['javax/mine/Helper.java': 'package javax.mine; public class Helper { public static int X; ' + STEAL + ' }'] - 'javax class asserts' | 'public class Main { public static void main(String[] a) { int z = javax.mine.Config.LEVEL; System.out.println(z); } }' | ['javax/mine/Config.java': 'package javax.mine; public class Config { public static int LEVEL; static { LEVEL = -1; assert LEVEL >= 0 : "bad level"; } }'] - 'java class field' | 'public class Main { public static void main(String[] a) { int z = java.mine.Config.LEVEL; System.out.println(z); } }' | ['java/mine/Config.java': 'package java.mine; public class Config { public static int LEVEL = 1; }'] - 'java class array' | 'public class Main { public static void main(String[] a) { Object[] arr = new java.mine.Config[1]; System.out.println(arr.length); } }' | ['java/mine/Config.java': 'package java.mine; public class Config { public static int LEVEL = 1; }'] - 'class shadowed by the JDK' | 'import org.xml.sax.helpers.AttributesImpl; public class Main { public static void main(String[] a) { AttributesImpl x = new AttributesImpl(); x.removeAttribute(0); } }' | ['org/xml/sax/helpers/AttributesImpl.java': 'package org.xml.sax.helpers; public class AttributesImpl { public AttributesImpl() {} public void removeAttribute(int index) {} }'] - } - - @Unroll - def "proven exception-free: #name"() { - expect: - check(program, release).exceptionFree - - where: - name | release | program - 'arithmetic and an assert' | '8' | 'public class Main { public static void main(String[] a) { double x = Verifier.nondetDouble(); Verifier.assume(x > 0); double y = Math.sin(x) * x; assert y < 10; } }' - 'division by a constant' | '8' | 'public class Main { public static void main(String[] a) { int x = Verifier.nondetInt(); int d = 4; int y = x / d + x % 3; } }' - 'array with constant indices' | '8' | 'public class Main { public static void main(String[] a) { double[] arr = new double[] {1, 2, 3}; arr[2] = arr[0] + Verifier.nondetDouble(); } }' - 'fields assigned in the constructor' | '8' | 'class B { boolean on; boolean isOn() { return on; } } class A { B b; B c; A() { b = new B(); c = b; } void step() { if (b.isOn()) c.on = false; } } public class Main { public static void main(String[] a) { A x = new A(); while (Verifier.nondetBoolean()) x.step(); } }' - 'enum switch' | '8' | 'enum L { LOW, HIGH } class S { L l = L.LOW; void up() { switch (l) { case LOW: l = L.HIGH; break; default: break; } } } public class Main { public static void main(String[] a) { S s = new S(); if (Verifier.nondetBoolean()) s.up(); assert s.l != L.HIGH; } }' - 'string switch on input' | '8' | 'public class Main { public static void main(String[] a) { String s = Verifier.nondetString(); int r; switch (s) { case "a": r = 1; break; default: r = 0; } } }' - 'recursion' | '8' | 'public class Main { static int f(int n) { return n <= 0 ? 0 : 1 + f(n - 1); } public static void main(String[] a) { int r = f(Verifier.nondetInt()); assert r >= 0; } }' - 'caught division' | '8' | 'public class Main { public static void main(String[] a) { try { int y = 1 / Verifier.nondetInt(); } catch (ArithmeticException e) { assert false; } } }' - 'finally after a safe body' | '8' | 'public class Main { static int n; public static void main(String[] a) { try { n = Verifier.nondetInt(); } finally { n++; } } }' - 'checked exception' | '8' | 'public class Main { public static void main(String[] a) throws Exception { if (Verifier.nondetBoolean()) throw new Exception(); } }' - 'printing' | '8' | 'public class Main { public static void main(String[] a) { int x = Verifier.nondetInt(); System.out.println("x=" + x); } }' - 'static field from initializer' | '8' | 'public class Main { static String s = "abc"; static int[] t = new int[2]; public static void main(String[] a) { t[1] = s.length(); } }' - 'string concatenation with indy' | '17' | 'public class Main { public static void main(String[] a) { int x = Verifier.nondetInt(); String s = "x=" + x + Verifier.nondetString(); assert s.length() > 0; } }' - } -} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/RefEqualsHelperAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/RefEqualsHelperAgentSpec.groovy new file mode 100644 index 00000000..5380594c --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/RefEqualsHelperAgentSpec.groovy @@ -0,0 +1,97 @@ +package de.uzl.its.swat.symbolic + +import com.fasterxml.jackson.databind.ObjectMapper +import spock.lang.Shared +import spock.lang.Specification + +import javax.tools.ToolProvider +import java.nio.file.Files +import java.nio.file.Path +import java.util.concurrent.TimeUnit + +/** + * L2 (forked agent): the branches of SWAT's helper for reference comparisons + * (UtilInstrumented.refEquals) are flagged like callbacks, so the static pre-analysis walk holds + * its place for them; the comparison's own branch is not, and keeps its key. How many branches the + * helper takes depends on the operands' runtime types, so the graph cannot have them. Runs via the + * {@code agentTest} Gradle task (needs the agent jar from {@code copyJar}). + */ +class RefEqualsHelperAgentSpec extends Specification { + + static final Path AGENT_JAR = Path.of("lib", "symbolic-executor.jar").toAbsolutePath() + static final Path NATIVE_LIBS = Path.of("..", "libs", "java-library-path").toAbsolutePath() + static final Path TARGETS = Path.of("src", "test", "resources", "targets").toAbsolutePath() + static final Path SOURCE = TARGETS.resolve("svcomp-refequals/Main.java") + + @Shared Path classes + @Shared Map trace + @Shared String comparisonKey + + def setupSpec() { + assert Files.isRegularFile(AGENT_JAR): "agent jar missing, run copyJar first: ${AGENT_JAR}" + classes = Files.createTempDirectory("swat-refequals-agent-spec") + compile(classes) + trace = parseTrace(run(classes)) + int line = Files.readAllLines(SOURCE).findIndexOf { it.contains("if (a == b)") } + 1 + comparisonKey = "Main.main([Ljava/lang/String;)V|${line}|if|0".toString() + } + + def cleanupSpec() { + classes?.toFile()?.deleteDir() + } + + private List branches() { + return trace.trace.findAll { it.type != "Special" } + } + + def "the helper's branches are flagged, the comparison's own branch is not"() { + when: + def all = branches() + int comparison = all.findIndexOf { it.key == comparisonKey } + def helper = all.subList(0, comparison).findAll { it.key == null } + + then: + comparison >= 0 + !all[comparison].callback + !helper.isEmpty() + helper.every { it.callback } + } + + def "the helper's frames are not reported as stack changes"() { + expect: + branches().every { b -> (b.pushes ?: []).every { it == null || !it.contains("refEquals") } } + } + + private static void compile(Path outDir) { + def sources = [SOURCE, TARGETS.resolve("svcomp/org/sosy_lab/sv_benchmarks/Verifier.java")]*.toString() + def args = ["-source", "1.8", "-target", "1.8", "-g", "-d", outDir.toString()] + sources + def err = new ByteArrayOutputStream() + int rc = ToolProvider.getSystemJavaCompiler().run(null, null, err, args as String[]) + assert rc == 0: "javac failed: ${err}" + } + + private static String run(Path classes) { + def java = Path.of(System.getProperty("java.home"), "bin", "java").toString() + def cmd = [java, + "-javaagent:${AGENT_JAR}".toString(), + "-Djava.library.path=${NATIVE_LIBS}".toString(), + "-Dconfig.path=/nonexistent/swat.cfg", + "-Dinstrumentation.transformer=SV_COMP", + "-Dsolver.mode=PRINT", + "-DexitOnError=false", + "-DlogShadowStateToConsole=false", + "-cp", classes.toString(), "-ea", "Main"] + def proc = new ProcessBuilder(cmd).directory(classes.toFile()).redirectErrorStream(true).start() + def out = proc.inputStream.text + assert proc.waitFor(5, TimeUnit.MINUTES): "target did not finish:\n${out}" + return out + } + + /** The TraceDTO is the single pretty-printed JSON object whose braces start at column 0. */ + private static Map parseTrace(String out) { + int start = out.indexOf("\n{\n") + int end = out.indexOf("\n}\n", start) + assert start >= 0 && end > start: "no trace JSON in output:\n${out}" + return new ObjectMapper().readValue(out.substring(start + 1, end + 2), Map) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy index 105cfea5..dc4d89e4 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy @@ -152,6 +152,27 @@ class StringModelExactnessTest extends Specification { [-3, 0, 2]].combinations() } + @Unroll + def "indexOf of a char (as its own code point) is exact: #sample, #ch, #from"() { + given: + def s = symbolicString("s", "fixed") + def c = new CharValue(context, (char) 'a', bvmgr.makeVariable(16, "ch")) + def f = symbolicInt("from", 0) + def fixed = [fixString(s, sample), bvmgr.equal(c.formula, bvmgr.makeBitvector(16, ch)), fixInt(f, from)] + + when: + def one = (IntValue) call(s, "indexOf", [INT], [c]) + def two = (IntValue) call(s, "indexOf", [INT, INT], [c, f]) + + then: + exactInt(fixed, one, sample.indexOf(ch)) + exactInt(fixed, two, sample.indexOf(ch, from)) + + where: + [sample, ch, from] << [["", "a", "aXa", "97", "a😀b"], [(int) 'a', (int) '9', 0xD83D, 0xDE00, 0xFFFF], + [-3, 0, 2]].combinations() + } + def "indexOf('a') on a concrete char has the Java result concretely"() { expect: ((IntValue) call(new StringValue(context, "xab", -1), "indexOf", [INT], [new IntValue(context, (int) 'a')])).concrete == 1 diff --git a/symbolic-executor/src/test/resources/targets/svcomp-refequals/Main.java b/symbolic-executor/src/test/resources/targets/svcomp-refequals/Main.java new file mode 100644 index 00000000..62ab227d --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/svcomp-refequals/Main.java @@ -0,0 +1,15 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** + * SV-COMP style target for the agent test of reference comparisons: SWAT rewrites a == b into a + * call to UtilInstrumented.refEquals, whose branches the static pre-analysis graph does not have. + */ +public class Main { + public static void main(String[] args) { + Object a = new Object(); + Object b = Verifier.nondetBoolean() ? a : new Object(); + if (a == b) { + assert b != null; + } + } +} diff --git a/symbolic-explorer/SymbolicExplorer.py b/symbolic-explorer/SymbolicExplorer.py index c42cb83d..41a3e74d 100755 --- a/symbolic-explorer/SymbolicExplorer.py +++ b/symbolic-explorer/SymbolicExplorer.py @@ -146,9 +146,12 @@ def init_args(parser: argparse.ArgumentParser): parser.add_argument("--sa-path", help="Path to the static pre-analysis tool for informing branch exploration (optional)") parser.add_argument("--sa-retry-without", action="store_true", help="On a SAFE verdict reached with static pre-analysis, disable it and explore again (guards against false SAFE from incomplete SA)", default=False) parser.add_argument("--sa-no-callback-targets", action="store_true", help="Do not count library calls as possible asserts when application code that library code may call back (overrides of library methods, lambdas) can reach an assert. Unsound: an assert reached only through such a callback can then give a false SAFE", default=False) + parser.add_argument("--prefer-short-strings", action="store_true", default=False, help="Shrink each string input of a solution to the shortest length the query allows") + parser.add_argument("--search-order", choices=["dfs", "shallow", "coverage", "coverage-dfs", "generational"], default="dfs", help="Order in which the open branches are tried: dfs (pre-order of the execution tree), shallow (closest to the root first), coverage (sides no trace took yet first, then shallow), coverage-dfs (the same, then dfs), generational (coverage, then the branches of the traces that covered the most first)") parser.add_argument("--sa-rank-distance", action="store_true", help="Try branches closest to an assert (by static pre-analysis graph distance) first, instead of in plain DFS order", default=False) parser.add_argument("--no-loop-state-matching", action="store_true", help="Flip branches below a loop-head state that was already reached at a smaller position too (the executor reports loop-head states if its config sets loopStateMatching)", default=False) parser.add_argument("--solver-rlimit", type=int, default=0, help="Z3 resource limit (rlimit) for the first query of each branch in sv-comp mode; a branch that runs out is retried later with a growing limit. 0 (default): unlimited") + parser.add_argument("--precheck-jar", default=None, help="cfg-extraction's cfg-extractor-precheck.jar for the property pre-check (default: next to symbolic-explorer in the SV-COMP archive, else ../cfg-extraction/build/libs/)") parser.add_argument("--no-property-precheck", action="store_true", help="Do not run the static property pre-check (sv-comp mode), which can prove no-runtime-exception (no uncaught RuntimeException is possible) or valid-assert (no AssertionError is ever created) for the whole program", default=False) parser.add_argument("--divergence-retries", type=int, default=3, help="How often a branch is re-solved (with the failed solutions excluded) when the run of its solution does not reach it, before it is given up on, which rules out SAFE (sv-comp mode)") parser.add_argument("--approximate-rlimit", type=int, default=250_000_000, help="Z3 resource limit for a query over an approximate Math model in sv-comp mode (about one to one and a half minutes); one that runs out is given up on, which rules out SAFE as the model does anyway. 0: no limit beyond --solver-rlimit") @@ -200,6 +203,7 @@ def init_args(parser: argparse.ArgumentParser): from data.Database import Database Database.instance().optimize_solutions = args.optimize Database.instance().log_smt_formulas = args.log_smt_formulas + Database.instance().prefer_short_strings = args.prefer_short_strings Database.instance().args = args # Store args for access to logdir s = SymbolicExplorer(args) diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py index a7c7eea7..2ff710e3 100755 --- a/symbolic-explorer/data/Database.py +++ b/symbolic-explorer/data/Database.py @@ -46,6 +46,7 @@ def __init__(self): self.witness_data = {} self.optimize_solutions = False # Whether to use Z3 Optimize() to minimize values self.log_smt_formulas = False # Whether to log SMT formulas and models to disk for debugging + self.prefer_short_strings = False # Whether to shrink the string inputs of a model (Z3Handler.shorten_strings) def reset(self): diff --git a/symbolic-explorer/data/StaticAnalysisGraph/SAGraph.py b/symbolic-explorer/data/StaticAnalysisGraph/SAGraph.py index 6938a0c9..ea74968b 100644 --- a/symbolic-explorer/data/StaticAnalysisGraph/SAGraph.py +++ b/symbolic-explorer/data/StaticAnalysisGraph/SAGraph.py @@ -565,9 +565,16 @@ def async_entry_sites(self) -> list[str]: return sites - def load_json_graph(self, path: str): + def load_json_graph(self, path: str, targets: str = "assertionPointIds"): + """ + Loads the extractor's graph. `targets` names the metadata field with the target points of + the property being checked: assertionPointIds (valid-assert) or runtimeExceptionPointIds + (no-runtime-exception). A graph without it cannot be used for that property (KeyError). + """ with open(path, "r") as f: self.json_graph = json.load(f) + if targets not in self.json_graph["metadata"]: + raise KeyError(f"the graph has no {targets}: it was made by an extractor that does not know this property") for json_node in self.json_graph["nodes"]: id = json_node["id"] @@ -579,6 +586,10 @@ def load_json_graph(self, path: str): if isinstance(metadata, str) and metadata.startswith("method: "): self.nodes[id].method = metadata[len("method: "):] self.nodes[id].key = json_node.get("key") + # Phantom guards whose implicit exception the property pre-check proves cannot happen + # (the extractor's cannotRaise, see RaiseSites in cfg-extraction): their exception side + # leads nowhere, below. + cannot_raise = {n["id"] for n in self.json_graph["nodes"] if n.get("cannotRaise") is True} keys: dict[str, SANode] = {} duplicates = set() for n in self.nodes.values(): @@ -628,6 +639,16 @@ def load_json_graph(self, path: str): elif etype == "EXCEPTIONAL_RETURN": source.add_exceptional_return_child(target) + elif etype == "PHANTOM_FALSE_BRANCH" and source.id in cannot_raise: + # The exception side of a guard that cannot raise: a dead end, from which nothing is + # reachable. Should an execution take it after all, the walk ends there with no + # information, which prunes nothing. + dead = SANode(f"dead[{source.id}]") + self.nodes[dead.id] = dead + source.add_fallthrough_child(dead) + dead.prev.append(source) + continue + elif etype in FALLTHROUGH_EDGES: source.add_fallthrough_child(target) @@ -643,13 +664,17 @@ def load_json_graph(self, path: str): n.add_fallthrough_child(n.callees[0]) self.entry_node = self.nodes[self.json_graph["entryNodeId"]] + # Callbacks are only an extra concern for asserts: for runtime exceptions, every library call + # that may call back into the application is a target point itself (see the extractor). graph_index = GraphIndex(keys, self.entry_node.method, - callbacks_reach_assert=bool(self.json_graph["metadata"].get("callbacksReachingAssert"))) + callbacks_reach_assert=targets == "assertionPointIds" + and bool(self.json_graph["metadata"].get("callbacksReachingAssert"))) for n in self.nodes.values(): n.graph_index = graph_index - for assertion_point_id in self.json_graph["metadata"]["assertionPointIds"]: - self.nodes[assertion_point_id].isAssert = True + # isAssert marks a target point of the property, whichever it is (the name is historical). + for target_id in self.json_graph["metadata"][targets]: + self.nodes[target_id].isAssert = True # An incomplete node may hide an assert in the part that was not expanded, so the paths # leading to it have to stay interesting. The extractor already reports these as assertion # points; treating them as such here too means a graph that ever forgets one half still diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index 26e2231f..22df2078 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -621,7 +621,8 @@ def solve_candidates(self, candidates: list[Node]) -> tuple[Node | None, dict, b def retrieve_solution(self): self.adopt_sa_graph() - possible_branches = StrategyService.select_branch(endpoint_id=ENDPOINT_ID, sa_node=self.sa_graph.entry_node, rank_by_distance=self.args.sa_rank_distance) + possible_branches = StrategyService.select_branch(endpoint_id=ENDPOINT_ID, sa_node=self.sa_graph.entry_node, rank_by_distance=self.args.sa_rank_distance, + search_order=getattr(self.args, 'search_order', 'dfs')) logger.info(f'[SYMBOLIC EXPLORATION] Found {len(possible_branches)} possible branches') logger.info(f'[SYMBOLIC EXPLORATION] Possible branch IDs: {[b.id for b in possible_branches]}') candidates = [b for b in possible_branches if StrategyService.is_symbolic_branch(b)] diff --git a/symbolic-explorer/solver/Int2BvLifting.py b/symbolic-explorer/solver/Int2BvLifting.py index ba2a51b5..700c26af 100644 --- a/symbolic-explorer/solver/Int2BvLifting.py +++ b/symbolic-explorer/solver/Int2BvLifting.py @@ -15,24 +15,29 @@ ubv_to_int, + - * and ite of those), - bvadd/bvsub/bvneg/bvmul/ite of liftable terms, as long as the range still fits, - zero/sign extension of liftable terms. -A char code (str.to_code, in [-1, max char]) does not fit 16 bits; it is lifted as -ite(t < 0, t + 2^16, ite(t < 2^16, t, t mod 2^16)), which is exact. +A char code (str.to_code) is in [-1, 0xFFFF]: the chars of a Java string are UTF-16 code units, and +the solver's strings model them char for char (supplementary code points as surrogate pairs). So a +char from charAt, ((_ int_to_bv 16) (str.to_code c)), lifts without a modulo, e.g. to +ite(t <= 2^15 - 1, t, t - 2^16) as a signed value. With [-1, 0x10FFFF] it needed one, and Z3 gave up +on queries that pin a dozen chars. (A string constant holding a supplementary code point as one +char breaks that bound, but charAt on it does not match Java either.) `rewrite(e)` replaces every comparison (=, distinct, bvs*, bvu*) between two liftable bit-vectors that involves int_to_bv by the Integer comparison of their lifts, and ubv_to_int of a liftable term by its lift. Everything else is left as it is. -The ranges of str.len and str.indexof assume that every string has at most 2^31 - 1 chars, as Java -strings do. `rewrite` records the strings whose length it relied on; `lift_query` adds the bound for -each of them to the query, so that the rewritten query is equivalent to the original one under that -bound in every model (and its models are models of the original query). +The ranges of str.len and str.indexof assume that every string has at most 2^31 - 1 chars, and the +range of str.to_code that every char is at most 0xFFFF, as in Java strings. `rewrite` records the +bounds it relied on (`needs`); `lift_query` adds them to the query, so that the rewritten query is +equivalent to the original one under these bounds in every model (and its models are models of the +original query). """ import z3 JAVA_MAX_STRING_LENGTH = 2 ** 31 - 1 -# Upper bound of str.to_code; Z3's char sort is never larger than Unicode. -MAX_CHAR_CODE = 0x10FFFF +# Upper bound of str.to_code for Java strings, whose chars are UTF-16 code units +MAX_CHAR_CODE = 0xFFFF _SIGNED_CMP = {z3.Z3_OP_SLEQ, z3.Z3_OP_SLT, z3.Z3_OP_SGEQ, z3.Z3_OP_SGT} _UNSIGNED_CMP = {z3.Z3_OP_ULEQ, z3.Z3_OP_ULT, z3.Z3_OP_UGEQ, z3.Z3_OP_UGT} @@ -65,15 +70,19 @@ def __init__(self): self._lifted = {} self._ranges = {} self._mentions_int2bv = {} - # Strings whose length bound a rewrite relied on, by expression id + # Bounds (see bound_fact) a rewrite relied on, by expression id self._bounded = {} self._needs = {} + # Integer stand-ins for bit-vector inputs (see lift_inputs): their range, by expression id + self._input_ranges = {} + # The inputs under ubv_to_int in an assertion, by expression id + self._bv2int_inputs = {} # Integer ranges def int_range(self, t): - """(lo, hi) such that lo <= t <= hi in every model (under the string length bound), or None. - Records the strings whose length bound the range relies on in self._needs[t].""" + """(lo, hi) such that lo <= t <= hi in every model (under the bounds of Java strings), or + None. Records the terms whose bound the range relies on in self._needs[t].""" key = t.get_id() if key in self._ranges: return self._ranges[key] @@ -93,15 +102,19 @@ def _int_range(self, t): v = _int_const(t) if v is not None: return (v, v), () + if t.get_id() in self._input_ranges: + return self._input_ranges[t.get_id()], () k = _kind(t) args = t.children() if z3.is_app(t) else [] if k == z3.Z3_OP_SEQ_LENGTH: - return (0, JAVA_MAX_STRING_LENGTH), (args[0],) + return (0, JAVA_MAX_STRING_LENGTH), (z3.Length(args[0]),) if k == z3.Z3_OP_SEQ_INDEX: - return (-1, JAVA_MAX_STRING_LENGTH), (args[0],) + return (-1, JAVA_MAX_STRING_LENGTH), (z3.Length(args[0]),) if k == z3.Z3_OP_STR_TO_CODE: - return (-1, MAX_CHAR_CODE), () + return (-1, MAX_CHAR_CODE), (t,) if k == z3.Z3_OP_BV2INT: + if z3.is_bv_value(args[0]): + return (args[0].as_long(), args[0].as_long()), () return (0, 2 ** args[0].size() - 1), () if k == z3.Z3_OP_SBV2INT: return _view_range(args[0].size(), True), () @@ -133,7 +146,7 @@ def _int_range(self, t): def lift(self, e, signed): """(t, needs): an Integer term with e == int_to_bv(t) and t in the signed/unsigned range of - e's width, and the strings whose length bound that relies on; or None.""" + e's width, and the terms whose bound that relies on; or None.""" key = (e.get_id(), signed) if key not in self._lifted: self._alive.append(e) @@ -192,6 +205,9 @@ def _lift(self, e, signed): if not signed and k == z3.Z3_OP_SIGN_EXT: return None return inner + if k == z3.Z3_OP_CONCAT and len(args) == 2 and z3.is_bv_value(args[0]) and args[0].as_long() == 0: + # A zero extension, as the executor widens a char to an int + return self.lift(args[1], False) return None def _lift_ranged(self, e, signed): @@ -232,7 +248,7 @@ def rewrite(self, e): return result def needs(self, e): - """The strings whose length bound rewrite(e) relies on.""" + """The terms whose bound (see bound_fact) rewrite(e) relies on.""" self.rewrite(e) return self._bounded[e.get_id()] @@ -297,16 +313,31 @@ def _int_const(e): return None +def _normal(e): + """e simplified to a fixpoint (one simplify of ubv_to_int(concat ...) leaves 2^k * ubv_to_int(0)).""" + for _ in range(4): + n = z3.simplify(e) + if n.eq(e): + break + e = n + return e + + def _signed_bv2int_operand(e): """x if e is the signed bv2int ite(bvsle(0, x), ubv_to_int(x), ubv_to_int(x) - 2^w) (in the - forms JavaSMT builds it), else None.""" + forms JavaSMT builds it, or with ubv_to_int(x) expanded, as Z3 does for a concat), else None.""" cond, then, other = e.children() - if _kind(cond) != z3.Z3_OP_SLEQ or _kind(then) != z3.Z3_OP_BV2INT: + if _kind(cond) != z3.Z3_OP_SLEQ: return None zero, x = cond.children() - if not (z3.is_bv_value(zero) and zero.as_long() == 0 and then.arg(0).eq(x)): + if not (z3.is_bv_value(zero) and zero.as_long() == 0): return None m = 2 ** x.size() + if _kind(then) != z3.Z3_OP_BV2INT or not then.arg(0).eq(x): + unsigned = z3.BV2Int(x) + if _normal(then).eq(_normal(unsigned)) and _normal(other).eq(_normal(unsigned - m)): + return x + return None if _kind(other) == z3.Z3_OP_ADD and other.num_args() == 2: a, b = other.children() for u, c in ((a, b), (b, a)): @@ -319,12 +350,106 @@ def _signed_bv2int_operand(e): return None +def bound_fact(t): + """The bound of Java strings that a needed term t obeys: str.len (also for str.indexof) at most + 2^31 - 1, str.to_code at most 0xFFFF.""" + if _kind(t) == z3.Z3_OP_STR_TO_CODE: + return t <= MAX_CHAR_CODE + return t <= JAVA_MAX_STRING_LENGTH + + def lift_query(lifting, exprs): - """The rewritten expressions, plus the length bounds of the strings they rely on.""" + """The rewritten expressions, plus the bounds of Java strings they rely on.""" out = [lifting.rewrite(x) for x in exprs] - strings = {} + terms = {} for x in exprs: - for s in lifting.needs(x): - strings[s.get_id()] = s - out.extend(z3.Length(s) <= JAVA_MAX_STRING_LENGTH for s in strings.values()) + for t in lifting.needs(x): + terms[t.get_id()] = t + # (A char code's index may itself be lifted.) + out.extend(bound_fact(lifting.rewrite(t)) for t in terms.values()) return out + + +def _bv2int_inputs(lifting, exprs): + """The bit-vector variables that occur as ubv_to_int(v) in exprs (cached per expression: the + path constraints recur in every query below them).""" + found = {} + for e in exprs: + key = e.get_id() + if key not in lifting._bv2int_inputs: + lifting._alive.append(e) + lifting._bv2int_inputs[key] = _bv2int_inputs_of(e) + for v in lifting._bv2int_inputs[key]: + found[v.get_id()] = v + return list(found.values()) + + +def _bv2int_inputs_of(expr): + found, seen = {}, set() + stack = [expr] + while stack: + e = stack.pop() + if e.get_id() in seen: + continue + seen.add(e.get_id()) + if _kind(e) == z3.Z3_OP_BV2INT: + v = e.arg(0) + if z3.is_const(v) and v.decl().kind() == z3.Z3_OP_UNINTERPRETED: + found[v.get_id()] = v + if z3.is_app(e): + stack.extend(e.children()) + return list(found.values()) + + +def _remaining_int2bv_args(exprs): + """The ids of the terms t that still occur as int_to_bv(t) in exprs.""" + found, seen = set(), set() + stack = list(exprs) + while stack: + e = stack.pop() + if e.get_id() in seen: + continue + seen.add(e.get_id()) + if _kind(e) == z3.Z3_OP_INT2BV: + found.add(e.arg(0).get_id()) + if z3.is_app(e): + stack.extend(e.children()) + return found + + +def input_stand_in(v): + """The Integer variable that stands in for the bit-vector input v (named so that it is not + taken for an input itself).""" + return z3.Int(f'int!{v.decl().name()}', v.ctx) + + +def lift_inputs(lifting, exprs): + """(out, inputs): lift_query of exprs, with bit-vector inputs that are only used as numbers + solved over the Integers. + + The executor's ints are bit-vectors, but a string index is an Integer: s.charAt(i) reads + (str.at s (ubv_to_int i)), with the signed conversion around it. Z3 decides such mixed queries + badly. Every input v that occurs under ubv_to_int is replaced by int_to_bv(x), for a new + Integer x in [0, 2^w) (exact: that is a bijection), and lifted as above. Where an occurrence + cannot be lifted (bit operations, extracts, ...), int_to_bv(x) would remain; such inputs are + put back as they were. `inputs` maps each lifted x to its v: a model gives v = x.""" + candidates = _bv2int_inputs(lifting, exprs) + if not candidates and not any(lifting.mentions_int2bv(e) for e in exprs): + return list(exprs), {} + while candidates: + stand_ins = {} + for v in candidates: + x = input_stand_in(v) + lifting._alive.append(x) + lifting._input_ranges[x.get_id()] = (0, 2 ** v.size() - 1) + stand_ins[x.get_id()] = (x, v) + subs = [(v, z3.Int2BV(x, v.size())) for x, v in stand_ins.values()] + out = lift_query(lifting, [z3.substitute(e, *subs) for e in exprs]) + remaining = _remaining_int2bv_args(out) + failed = [v for xid, (x, v) in stand_ins.items() if xid in remaining] + if not failed: + out.extend(z3.And(x >= 0, x <= 2 ** v.size() - 1) for x, v in stand_ins.values()) + return out, {x.get_id(): (x, v) for x, v in stand_ins.values()} + failed_ids = {v.get_id() for v in failed} + candidates = [v for v in candidates if v.get_id() not in failed_ids] + return lift_query(lifting, exprs), {} diff --git a/symbolic-explorer/solver/SolverHandler.py b/symbolic-explorer/solver/SolverHandler.py index c8e0cf4a..dab70da0 100755 --- a/symbolic-explorer/solver/SolverHandler.py +++ b/symbolic-explorer/solver/SolverHandler.py @@ -392,21 +392,70 @@ def write_optimizer_to_file(optimizer: Optimize, output_dir: str = "smt_files") return filepath @staticmethod - def lift_int2bv(cache, assertions: list) -> list: - """The assertions with comparisons over int_to_bv of string lengths, indices and char codes - made over the Integers (see Int2BvLifting), which Z3 decides much faster. Equivalent for - Java strings (at most 2^31 - 1 chars); on any error, the assertions as they are.""" - from solver.Int2BvLifting import Int2BvLifting, lift_query + def lift_int2bv(cache, assertions: list) -> Tuple[list, dict]: + """(assertions, inputs): the assertions with comparisons over int_to_bv of string lengths, + indices and char codes made over the Integers, and bit-vector inputs used only as numbers + replaced by Integers (see Int2BvLifting.lift_inputs), which Z3 decides much faster. + Equivalent for Java strings (at most 2^31 - 1 chars); `inputs` maps each Integer stand-in + to its input (see map_lifted_inputs). On any error, the assertions as they are.""" + from solver.Int2BvLifting import Int2BvLifting, lift_inputs try: lifting = getattr(cache, 'int2bv_lifting', None) if lifting is None: lifting = cache.int2bv_lifting = Int2BvLifting() - if not any(lifting.mentions_int2bv(a) for a in assertions): - return assertions - return lift_query(lifting, assertions) + return lift_inputs(lifting, assertions) except Exception as e: logger.warning(f"[SOLVER] int_to_bv lifting failed, solving the query as it is: {e}") - return assertions + return assertions, {} + + @staticmethod + def map_lifted_inputs(model, inputs: dict, encoded: Dict[str, Any]) -> None: + """Adds the values of the bit-vector inputs that the query had replaced by Integer + stand-ins (see lift_int2bv) to the encoded solution: v = x mod 2^w.""" + for x, v in inputs.values(): + value = model.eval(x, model_completion=True) + if not z3.is_int_value(value): + continue + bv = z3.BitVecVal(value.as_long() % 2 ** v.size(), v.size(), v.ctx) + name = str(v.decl().name()) + prefix, _, idx = name.partition('_') + encoded[name] = { + 'encoded_value': Z3Handler.encode_value(prefix, bv), + 'plain_value': bv, + 'index': idx, + } + + @staticmethod + def shorten_strings(solver, model, t_check: float): + """A model of the solver's assertions in which each string input is as short as they allow + (shortest first for the first input, then the next, ...), or `model` where finding one + takes too long. Z3 fills the chars a query leaves open with whatever it likes, often more of + them than needed; in a parser, every extra char is one more step down an error path. + Each check gets a short timeout (twice the first check's time, at least 0.2 s).""" + solver.set("timeout", max(200, int(2000 * t_check))) + for d in model.decls(): + if d.arity() > 0 or not z3.is_string(d()) or not re.match(r'[\w/]+_\d+$', d.name()): + continue + s = d() + lo, hi = 0, model.eval(z3.Length(s), model_completion=True).as_long() + while lo < hi: + mid = (lo + hi) // 2 + solver.push() + solver.add(z3.Length(s) <= mid) + res = solver.check() + if res == z3.sat: + model = solver.model() + hi = model.eval(z3.Length(s), model_completion=True).as_long() + solver.pop() + elif res == z3.unsat: + solver.pop() + lo = mid + 1 + else: + solver.pop() + return model + # Keep this input at its length while shrinking the next ones. + solver.add(z3.Length(s) == hi) + return model @staticmethod def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, rlimit: int | None = None, @@ -459,11 +508,12 @@ def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, if len(node_exprs) > 0: # Negate all node constraint expressions, then add all path constraint expressions # (already parsed and cached) - assertions = [Not(expr) for expr in node_exprs] + all_exprs[len(node_exprs):] - solver.add(*Z3Handler.lift_int2bv(cache, assertions)) - - for expr in extra_exprs or []: - solver.add(expr) + # (The extra constraints restrict inputs too, so they are lifted with the rest.) + assertions = [Not(expr) for expr in node_exprs] + all_exprs[len(node_exprs):] + list(extra_exprs or []) + lifted, lifted_inputs = Z3Handler.lift_int2bv(cache, assertions) + solver.add(*lifted) + else: + lifted_inputs = {} # Building the solver is Z3 work (SMT-LIB parsing on cache misses, assertion # construction), so it counts towards the SMT solver stage rather than the @@ -508,6 +558,8 @@ def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, if str(res) == SATResult.SAT.value: t_start = time.perf_counter() sol = solver.model() + if Database.instance().prefer_short_strings: + sol = Z3Handler.shorten_strings(solver, sol, t_check) # Log model to disk for debugging (if enabled) if Database.instance().log_smt_formulas: @@ -535,6 +587,7 @@ def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, logger.warning(f"[SOLVER] Model does not satisfy assertion: {constraint}") encoded_sol = Z3Handler.extract_and_encode_values(sol) + Z3Handler.map_lifted_inputs(sol, lifted_inputs, encoded_sol) t_encode = time.perf_counter() - t_start TimingManager.instance().record_solver_time(t_encode, count=False) logger.debug(f"[SOLVER] build={t_path:.3f}s check={t_check:.3f}s model={t_encode:.3f}s rlimit={rlimit_used}") diff --git a/symbolic-explorer/strategy/StrategyService.py b/symbolic-explorer/strategy/StrategyService.py index 41098632..2cc44d3f 100755 --- a/symbolic-explorer/strategy/StrategyService.py +++ b/symbolic-explorer/strategy/StrategyService.py @@ -28,6 +28,74 @@ def declared_ufs(smt: str) -> frozenset[str]: return frozenset(name.strip("|") for name in _UF_DECLARATION.findall(smt)) +# Search orders for the branches to flip (--search-order): "dfs" is the walk's own pre-order, +# "shallow" takes the branches closest to the root first, "coverage" first those whose open side no +# trace has taken at any position (then the shallowest), "coverage-dfs" the same with DFS order. +# "generational" is "coverage", but among the branches that reach nothing new, it first takes those +# of the traces that covered the most sides first (as SAGE's generational search): a trace that +# found something new is where combinations with it are found. +SEARCH_ORDERS = ("dfs", "shallow", "coverage", "coverage-dfs", "generational") + +# The loop count in the top 6 bits of an iid; without it, an iid names the branch instruction +# (and switch case) wherever a loop runs it. +_STATIC_IID_MASK = (1 << 58) - 1 + + +def depth(node) -> int: + """The number of branches above node on its path (cached on the node).""" + d = getattr(node, '_depth', None) + if d is None: + chain = [] + n = node + while n is not None and getattr(n, '_depth', None) is None: + chain.append(n) + n = n.parent + d = -1 if n is None else n._depth + for m in reversed(chain): + d += 1 + m._depth = d + d = node._depth + return d + + +def open_side(node) -> tuple: + """The branch instruction and side that flipping node would take.""" + return node.id & _STATIC_IID_MASK, node.skipped is not None + + +def covered_sides(root) -> set: + """The (instruction, side) pairs some trace in the tree took.""" + return set(first_coverers(root)) + + +def first_coverers(root) -> dict: + """For each (instruction, side) pair some trace in the tree took, the node through which it + was taken first (nodes are numbered in the order they were added, by gid).""" + first = {} + stack = [root] + while stack: + n = stack.pop() + if not isinstance(n, Node): + continue + if n.kind == "Branch": + for side, child in ((True, n.branched), (False, n.skipped)): + if child is not None: + pair = (n.id & _STATIC_IID_MASK, side) + if pair not in first or n.gid < first[pair].gid: + first[pair] = n + stack.append(n.branched) + stack.append(n.skipped) + return first + + +def trace_scores(first: dict) -> dict: + """How many (instruction, side) pairs each trace took first, by trace id.""" + scores = {} + for n in first.values(): + scores[n.trace_id] = scores.get(n.trace_id, 0) + 1 + return scores + + class StrategyService: # is_symbolic_branch per (node gid, trace id) _symbolic_branches: dict[tuple[int, str], bool] = {} @@ -41,15 +109,32 @@ def select_branch(**kwargs): # changes, so which branches exist, and hence the verdict, does not. The sort is stable: # ties, and branches without SA information (ranked last), keep their DFS order. distances = {} if kwargs.get("rank_by_distance", False) else None + order = kwargs.get("search_order", "dfs") + covered = None + scores = {} # The walk is on the Database's tree itself, so dfs records where the SA walk fell out of # step there directly. The returned nodes are live: they gain children as traces arrive. def walk(tree, solved, unsat): + nonlocal covered, scores tree.loop_state_pruned = 0 # counted per walk; the tree itself persists found = dfs(visited, tree, tree.root, solved, unsat, kwargs.get("sa_node", None), distances=distances) + if order.startswith("coverage") or order == "generational": + first = first_coverers(tree.root) + covered = set(first) + scores = trace_scores(first) return found, tree.loop_state_pruned possible_branches, pruned = db.visit_tree(endpoint_id, walk) if pruned: logger.info(f'[DFS] Left out {pruned} subtrees below a repeated loop-head state') + # All sorts are stable: ties keep their DFS order. + if order == "shallow": + possible_branches.sort(key=depth) + elif order == "coverage": + possible_branches.sort(key=lambda n: (open_side(n) in covered, depth(n))) + elif order == "coverage-dfs": + possible_branches.sort(key=lambda n: open_side(n) in covered) + elif order == "generational": + possible_branches.sort(key=lambda n: (open_side(n) in covered, -scores.get(n.trace_id, 0), depth(n))) if distances: possible_branches.sort(key=lambda n: distances.get(n, math.inf)) diff --git a/symbolic-explorer/svcomp/PropertyPreCheck.py b/symbolic-explorer/svcomp/PropertyPreCheck.py index 624e6056..430d861d 100644 --- a/symbolic-explorer/svcomp/PropertyPreCheck.py +++ b/symbolic-explorer/svcomp/PropertyPreCheck.py @@ -1,8 +1,9 @@ """ Static property pre-check for the SV-COMP driver. -The executor jar contains a conservative bytecode analysis (de.uzl.its.swat.staticcheck. -ExceptionFreedomCheck) of the whole program on the classpath. It proves, or fails to prove: +A conservative bytecode analysis of the whole program on the classpath, part of the static +pre-analysis in cfg-extraction (de.uzl.its.cfg.staticcheck.ExceptionFreedomCheck, built as +cfg-extractor-precheck.jar). It proves, or fails to prove: - for no-runtime-exception: no RuntimeException can escape Main.main or a static initializer; - for valid-assert: no AssertionError is ever created, so no assert can fail. @@ -11,6 +12,9 @@ model, so the driver may answer SAFE even where context loss, precision loss, uncaught exceptions or an unexhausted path space would otherwise prevent it. A failed, crashed or timed-out check proves nothing, and the driver proceeds as without it. + +The check prints one JSON line: tool and version (cfg-extraction's git describe), and per property +whether it is proven and why (not). """ import json @@ -21,8 +25,16 @@ import log logger = log.get_logger() -CHECK_CLASS = "de.uzl.its.swat.staticcheck.ExceptionFreedomCheck" +CHECK_CLASS = "de.uzl.its.cfg.staticcheck.ExceptionFreedomCheck" CHECK_TIMEOUT_S = 60 +JAR_NAME = "cfg-extractor-precheck.jar" +_EXPLORER_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +# Where the jar is found without --precheck-jar: next to symbolic-explorer in the SV-COMP archive, +# and in the build output of the cfg-extraction checkout next to SWAT's in the workspace. +DEFAULT_JARS = ( + os.path.join(_EXPLORER_DIR, "..", "cfg-extraction", JAR_NAME), + os.path.join(_EXPLORER_DIR, "..", "..", "cfg-extraction", "build", "libs", JAR_NAME), +) # The property file name -> the field of the check's result that proves it. PROVES = { @@ -40,27 +52,40 @@ def __init__(self, args, prop: str): self.proven = False self.reason: str | None = None self.duration: float | None = None + self.version: str | None = None @staticmethod def _is_swat_library(path: str) -> bool: """Z3's Java bindings, which SWAT itself puts on the target's classpath: not part of the program.""" return os.path.basename(path) == "com.microsoft.z3.jar" + def jar(self) -> str | None: + """The check's jar: --precheck-jar, else the first of DEFAULT_JARS that exists.""" + given = getattr(self.args, "precheck_jar", None) + if given: + return given + return next((os.path.normpath(p) for p in DEFAULT_JARS if os.path.isfile(p)), None) + def command(self) -> list[str]: classpath = [os.path.abspath(p) for p in self.args.classpath if not self._is_swat_library(p)] - return [self.args.java_path, "-Xmx2g", "-cp", self.args.agent, CHECK_CLASS, *classpath] + return [self.args.java_path, "-Xmx2g", "-cp", self.jar(), CHECK_CLASS, *classpath] def run(self) -> bool: """Runs the check (blocking) and returns whether it proved the property.""" if not self.enabled: return False start = time.perf_counter() + if self.jar() is None: + logger.error(f'[PRECHECK] No {JAR_NAME} (looked in {", ".join(map(os.path.normpath, DEFAULT_JARS))}); skipping the property pre-check') + self.status = "missing_jar" + return False try: proc = subprocess.run(self.command(), capture_output=True, text=True, timeout=CHECK_TIMEOUT_S) result = json.loads(proc.stdout.strip().splitlines()[-1]) field, reason_field = PROVES[self.prop] self.proven = result.get(field) is True self.reason = result.get(reason_field) + self.version = result.get("version") self.status = "proven" if self.proven else "not_proven" except subprocess.TimeoutExpired: self.status = "timeout" @@ -68,7 +93,7 @@ def run(self) -> bool: logger.error(f'[PRECHECK] Property pre-check failed: {type(e).__name__}: {e}') self.status = "failed" self.duration = time.perf_counter() - start - logger.info(f'[PRECHECK] {self.prop}: {self.status} after {self.duration:.2f}s ({self.reason})') + logger.info(f'[PRECHECK] {self.prop}: {self.status} after {self.duration:.2f}s ({self.reason}; cfg-extraction {self.version})') return self.proven def stats(self) -> dict: @@ -78,4 +103,5 @@ def stats(self) -> dict: 'proven': self.proven, 'reason': self.reason, 'duration_s': self.duration, + 'version': self.version, } diff --git a/symbolic-explorer/svcomp/StaticPreAnalysis.py b/symbolic-explorer/svcomp/StaticPreAnalysis.py index 43070ca4..52de6bce 100644 --- a/symbolic-explorer/svcomp/StaticPreAnalysis.py +++ b/symbolic-explorer/svcomp/StaticPreAnalysis.py @@ -9,10 +9,12 @@ explorer never sees a half-loaded graph. ``cancel()`` kills the extractor and joins the thread, so no Java process outlives the explorer when exploration finishes first. -The graph's only targets are asserts (``new AssertionError`` sites), so pruning by it is only sound -for the valid-assert property; under any other property the pre-analysis is not run at all. A -graph whose program may run application code outside main's call tree (another thread, a shutdown -hook, an uncaught-exception handler) is not used either, see ``SAGraph.async_entry_sites``. +The graph names the target points of two properties: asserts (``new AssertionError`` sites) for +valid-assert, and the sites that may raise a RuntimeException for no-runtime-exception (found with +the property pre-check's value analysis, see cfg-extraction's RaiseSites). Under any other property +the pre-analysis is not run at all. A graph whose program may run application code outside main's +call tree (another thread, a shutdown hook, an uncaught-exception handler) is not used either, see +``SAGraph.async_entry_sites``. """ import os @@ -29,8 +31,11 @@ EXTRACTOR_TIMEOUT_S = 120 -# The only property whose violations are the graph's targets (assertion points). -SA_PROPERTY = "valid-assert.prp" +# The properties the graph has target points for, and the metadata field that lists them. +SA_TARGETS = { + "valid-assert.prp": "assertionPointIds", + "no-runtime-exception.prp": "runtimeExceptionPointIds", +} class SAStatus(Enum): @@ -68,13 +73,18 @@ def enabled(self) -> bool: @property def property_supported(self) -> bool: - return os.path.basename(getattr(self.args, "property", None) or "") == SA_PROPERTY + return self.targets is not None + + @property + def targets(self) -> str | None: + """The graph's metadata field with the target points of the property, or None.""" + return SA_TARGETS.get(os.path.basename(getattr(self.args, "property", None) or "")) def start(self): if not self.enabled: if self.requested: - logger.info(f'[EXPLORER] Static pre-analysis is disabled: its graph only targets asserts, ' - f'so it cannot prune for property {self.args.property} (only {SA_PROPERTY}).') + logger.info(f'[EXPLORER] Static pre-analysis is disabled: its graph has no target points ' + f'for property {self.args.property} (only {", ".join(SA_TARGETS)}).') else: logger.info(f'[EXPLORER] Static pre-analysis is disabled.') self._done.set() @@ -121,14 +131,15 @@ def _run(self): try: if self.args.sa_file: logger.info(f'[EXPLORER] Loading static pre-analysis graph from provided file...') - graph.load_json_graph(self.args.sa_file) + graph.load_json_graph(self.args.sa_file, self.targets) logger.info(f'[EXPLORER] Loaded static pre-analysis graph from provided file.') else: logger.info(f'[EXPLORER] Running static pre-analysis...') if not self._run_extractor(): return logger.info(f'[EXPLORER] Loading static pre-analysis graph...') - graph.load_json_graph(os.path.join(self.args.logdir, f"{self.args.target}_main_interprocedural.json")) + graph.load_json_graph(os.path.join(self.args.logdir, f"{self.args.target}_main_interprocedural.json"), + self.targets) logger.info(f'[EXPLORER] Loaded static pre-analysis graph.') async_sites = graph.async_entry_sites() if self._cancelled.is_set(): diff --git a/symbolic-explorer/tests/test_int2bv_lifting.py b/symbolic-explorer/tests/test_int2bv_lifting.py index 2b39618b..fbd2c811 100644 --- a/symbolic-explorer/tests/test_int2bv_lifting.py +++ b/symbolic-explorer/tests/test_int2bv_lifting.py @@ -15,7 +15,7 @@ sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) -from solver.Int2BvLifting import Int2BvLifting, lift_query, JAVA_MAX_STRING_LENGTH +from solver.Int2BvLifting import Int2BvLifting, lift_query, lift_inputs, bound_fact, JAVA_MAX_STRING_LENGTH def mixes_sorts(e): @@ -111,15 +111,22 @@ def test_random_comparisons_keep_their_truth_value(self): rnd = random.Random(7) terms = Terms(rnd) lifted = 0 + compared = 0 for _ in range(150): e = terms.bool_term(3) lifting = Int2BvLifting() r = lifting.rewrite(e) lifted += not r.eq(e) + bounds = [bound_fact(t) for t in lifting.needs(e)] for _ in range(12): a = terms.assignment() + # Equivalent only for Java strings: no char above 0xFFFF where the rewrite relied on that. + if not all(evaluate(b, a) for b in bounds): + continue + compared += 1 self.assertEqual(evaluate(e, a), evaluate(r, a), f'\n{e}\nrewritten to\n{r}\nunder {a}') self.assertGreater(lifted, 50) + self.assertGreater(compared, 1000) def test_string_length_comparisons_become_integer_comparisons(self): s = z3.String('s') @@ -135,6 +142,19 @@ def test_string_length_comparisons_become_integer_comparisons(self): self.assertEqual(solver.check(), z3.sat) self.assertTrue(z3.is_true(solver.model().eval(e, model_completion=True))) + def test_chars_lift_without_modulo(self): + # s.charAt(i) == '\\' over the Integers, with the char bound in the query + s = z3.String('s') + code = z3.StrToCode(z3.SubString(s, z3.IntVal(3), z3.IntVal(1))) + e = z3.Int2BV(code, 16) == z3.BitVecVal(92, 16) + out = lift_query(Int2BvLifting(), [e]) + self.assertFalse(any(mixes_sorts(x) for x in out)) + self.assertNotIn('mod', ' '.join(x.sexpr() for x in out)) + self.assertTrue(any(x.eq(code <= 0xFFFF) for x in out)) + # The char of a missing index (-1) is 0xFFFF as a Java char, as with int_to_bv. + r = Int2BvLifting().rewrite(z3.Int2BV(code, 16) == z3.BitVecVal(0xFFFF, 16)) + self.assertTrue(z3.is_true(z3.simplify(z3.substitute(r, (code, z3.IntVal(-1)))))) + def test_overflowing_length_arithmetic_wraps(self): # s.length() + 3 overflows for long strings: the lift must keep the wrap. s = z3.String('s') @@ -155,6 +175,83 @@ def test_signed_bv2int_of_a_length_is_the_length(self): out = lift_query(Int2BvLifting(), [e]) self.assertFalse(any(mixes_sorts(x) for x in out)) + def test_char_widened_to_int_is_the_char_code(self): + # (int) s.charAt(0) as the executor builds it: the signed bv2int of the zero-extended char, + # with ubv_to_int(concat ...) expanded as Z3 does it. + s = z3.String('s') + code = z3.StrToCode(z3.SubString(s, z3.IntVal(0), z3.IntVal(1))) + char = z3.Int2BV(code, 16) + x = z3.Concat(z3.BitVecVal(0, 16), char) + unsigned = 65536 * z3.BV2Int(z3.BitVecVal(0, 16)) + z3.BV2Int(char) + widened = z3.If(z3.BitVecVal(0, 32) <= x, unsigned, z3.IntVal(-2 ** 32) + unsigned) + e = z3.StrFromCode(widened) == z3.StringVal('a') + out = lift_query(Int2BvLifting(), [e]) + self.assertFalse(any(mixes_sorts(x) for x in out)) + solver = z3.Solver() + solver.add(*out) + self.assertEqual(solver.check(), z3.sat) + self.assertEqual(solver.model().eval(z3.SubString(s, 0, 1)).as_string(), 'a') + + def test_lifted_inputs_keep_the_truth_value(self): + # x and y replaced by Integer stand-ins where they are only used as numbers: under every + # assignment, with the stand-ins at the inputs' unsigned values, the query is unchanged. + rnd = random.Random(11) + terms = Terms(rnd) + lifted = compared = 0 + for _ in range(150): + e = terms.bool_term(3) + out, inputs = lift_inputs(Int2BvLifting(), [e]) + lifted += bool(inputs) + for _ in range(12): + a = terms.assignment() + values = dict((str(v), val) for v, val in a) + stand_ins = [(x, z3.IntVal(values[str(v)].as_long())) for x, v in inputs.values()] + # Bounds the rewrite relied on (chars up to 0xFFFF) are part of out. + if not all(evaluate(o, a + stand_ins) for o in out[1:]): + continue + compared += 1 + self.assertEqual(evaluate(e, a), evaluate(out[0], a + stand_ins), f'\n{e}\nlifted to\n{out[0]}\nunder {a}') + self.assertGreater(lifted, 30) + self.assertGreater(compared, 1000) + + def test_char_at_a_symbolic_int_index_is_solved_over_the_integers(self): + # s.charAt(i) == 'b' with i a Java int: (str.at s (signed bv2int i)) + s = z3.String('java/lang/String_0') + i = z3.BitVec('I_1', 32) + signed = z3.If(z3.BitVecVal(0, 32) <= i, z3.BV2Int(i), z3.IntVal(-2 ** 32) + z3.BV2Int(i)) + e = z3.And(z3.SubString(s, signed, z3.IntVal(1)) == z3.StringVal('b'), z3.Length(s) == 3, + z3.Not(z3.PrefixOf(z3.StringVal('b'), s)), i != z3.BitVecVal(2, 32)) + out, inputs = lift_inputs(Int2BvLifting(), [e]) + self.assertEqual([str(v) for x, v in inputs.values()], ['I_1']) + self.assertFalse(any(mixes_sorts(x) for x in out)) + solver = z3.Solver() + solver.add(*out) + self.assertEqual(solver.check(), z3.sat) + from solver.SolverHandler import Z3Handler + encoded = {} + Z3Handler.map_lifted_inputs(solver.model(), inputs, encoded) + self.assertEqual(encoded['I_1']['encoded_value'], '1') + self.assertEqual(encoded['I_1']['index'], '1') + + def test_negative_inputs_map_back_to_negative_ints(self): + i = z3.BitVec('I_4', 32) + e = z3.BV2Int(i) == z3.IntVal(2 ** 32 - 5) + out, inputs = lift_inputs(Int2BvLifting(), [e]) + solver = z3.Solver() + solver.add(*out) + self.assertEqual(solver.check(), z3.sat) + from solver.SolverHandler import Z3Handler + encoded = {} + Z3Handler.map_lifted_inputs(solver.model(), inputs, encoded) + self.assertEqual(encoded['I_4']['encoded_value'], '-5') + + def test_inputs_used_in_bit_operations_stay_bit_vectors(self): + i = z3.BitVec('I_1', 32) + e = z3.And(z3.BV2Int(i) < 10, z3.Extract(3, 0, i) == z3.BitVecVal(5, 4)) + out, inputs = lift_inputs(Int2BvLifting(), [e]) + self.assertEqual(inputs, {}) + self.assertTrue(out[0].eq(e)) + def test_terms_without_int2bv_are_left_alone(self): y = z3.BitVec('y', 32) e = z3.And(y + 1 > z3.BitVecVal(3, 32), z3.BV2Int(y) < 7) diff --git a/symbolic-explorer/tests/test_property_precheck.py b/symbolic-explorer/tests/test_property_precheck.py index 3fe61a29..d06a296e 100644 --- a/symbolic-explorer/tests/test_property_precheck.py +++ b/symbolic-explorer/tests/test_property_precheck.py @@ -11,6 +11,7 @@ import os import subprocess import sys +import tempfile import unittest from types import SimpleNamespace from unittest import mock @@ -20,12 +21,13 @@ from driver import SVCompDriver as svcomp from svcomp import PropertyPreCheck as precheck -RESULT = {"exception_free": True, "reason": "no throw", "assertion_free": False, "assertion_reason": "Main.main: assert"} +RESULT = {"tool": "cfg-extraction", "version": "v1-0-gabc", "exception_free": True, "reason": "no throw", + "assertion_free": False, "assertion_reason": "Main.main: assert"} def args(**kw): a = dict(classpath=['/task/common', '/task/Main', '/libs/com.microsoft.z3.jar'], agent='/swat/executor.jar', - java_path='java', no_property_precheck=False) + java_path='java', no_property_precheck=False, precheck_jar='/sa/cfg-extractor-precheck.jar') a.update(kw) return SimpleNamespace(**a) @@ -57,9 +59,29 @@ def test_valid_assert_uses_assertion_freedom(self): def test_command_leaves_out_z3(self): _, _, run = self.run_check('no-runtime-exception.prp') cmd = run.call_args[0][0] - self.assertEqual(cmd[:4], ['java', '-Xmx2g', '-cp', '/swat/executor.jar']) + self.assertEqual(cmd[:5], ['java', '-Xmx2g', '-cp', '/sa/cfg-extractor-precheck.jar', precheck.CHECK_CLASS]) self.assertEqual(cmd[-2:], ['/task/common', '/task/Main']) + def test_reported_version_is_recorded(self): + check, _, _ = self.run_check('no-runtime-exception.prp') + self.assertEqual(check.stats()['version'], 'v1-0-gabc') + + def test_without_the_option_the_jar_is_found_next_to_the_explorer(self): + with tempfile.TemporaryDirectory() as d: + jar = os.path.join(d, precheck.JAR_NAME) + open(jar, 'w').close() + with mock.patch.object(precheck, 'DEFAULT_JARS', (os.path.join(d, 'missing.jar'), jar)): + _, proven, run = self.run_check('no-runtime-exception.prp', precheck_jar=None) + self.assertTrue(proven) + self.assertEqual(run.call_args[0][0][3], jar) + + def test_a_missing_jar_proves_nothing(self): + with mock.patch.object(precheck, 'DEFAULT_JARS', ('/nonexistent/' + precheck.JAR_NAME,)): + check, proven, run = self.run_check('no-runtime-exception.prp', precheck_jar=None) + self.assertFalse(proven) + self.assertEqual(check.status, 'missing_jar') + run.assert_not_called() + def test_other_property_and_flag_disable_it(self): for check, proven, run in (self.run_check('no-deadlock.prp'), self.run_check('no-runtime-exception.prp', no_property_precheck=True)): diff --git a/symbolic-explorer/tests/test_sa_guards.py b/symbolic-explorer/tests/test_sa_guards.py index 6f6702c9..4ebe621b 100644 --- a/symbolic-explorer/tests/test_sa_guards.py +++ b/symbolic-explorer/tests/test_sa_guards.py @@ -105,8 +105,23 @@ def test_valid_assert_loads_the_graph(self): self.assertEqual(sa.status, SAStatus.LOADED) self.assertIsNotNone(graph) + def test_no_runtime_exception_uses_its_own_target_points(self): + g = hook_graph(statement_ok()) + assertion = g.asserts[0] + site = next(n['id'] for n in g.nodes if n['id'] != assertion) + g.metadata['runtimeExceptionPointIds'] = [site] + sa, graph = self.run_sa('no-runtime-exception.prp', g) + self.assertEqual(sa.status, SAStatus.LOADED) + self.assertTrue(graph.nodes[site].isAssert) + self.assertFalse(graph.nodes[assertion].isAssert) + + def test_no_runtime_exception_needs_a_graph_with_its_target_points(self): + sa, graph = self.run_sa('no-runtime-exception.prp') # an older extractor's graph + self.assertEqual(sa.status, SAStatus.FAILED) + self.assertIsNone(graph) + def test_other_properties_load_nothing(self): - for prop in ['no-runtime-exception.prp', 'no-deadlock.prp', None]: + for prop in ['no-deadlock.prp', None]: sa, graph = self.run_sa(prop) self.assertEqual(sa.status, SAStatus.DISABLED, prop) self.assertIsNone(graph) diff --git a/symbolic-explorer/tests/test_sa_walk.py b/symbolic-explorer/tests/test_sa_walk.py index d5f8f406..805c52b0 100644 --- a/symbolic-explorer/tests/test_sa_walk.py +++ b/symbolic-explorer/tests/test_sa_walk.py @@ -264,6 +264,42 @@ def inter_method_catch_graph(): .edge('u', 'h', 'EXCEPTIONAL_RETURN')) +class CannotRaiseTest(unittest.TestCase): + """Guards the property pre-check proves cannot raise (cannotRaise) lead nowhere on their exception side.""" + + def graph(self, cannot_raise: bool) -> SAGraph: + b = inter_method_catch_graph() + for n in b.nodes: + if n['id'] == 'g' and cannot_raise: + n['cannotRaise'] = True + return b.load() + + def test_exception_side_of_a_guard_that_cannot_raise_is_a_dead_end(self): + n = self.graph(True).nodes + dead = n['g'].get_fallthrough_child() + self.assertEqual(dead.id, 'dead[g]') + self.assertIs(n['g'].get_branched_child(), n['tx']) # the guard is still a branch + self.assertFalse(sagraph.is_interesting(dead, sagraph.push(None, n['c']))) + # The assert in main's handler was only reachable through the guard's failure. + self.assertFalse(n['c'].reachesAssertSameLevel) + self.assertIsNone(dead.walk_till_branch(sagraph.push(None, n['c']))) + + def test_unexplored_exception_side_is_no_candidate(self): + for cannot_raise, expected in ((False, {'n1'}), (True, set())): + g = keyed(self.graph(cannot_raise)) + n1 = branch_node('n1', skipped=None, branched=leaf(), key='g', pushes=('c',)) + self.assertEqual(candidates(n1, g), expected, f'cannotRaise={cannot_raise}') + + def test_statement_marks_change_nothing(self): + b = inter_method_catch_graph() + for n in b.nodes: + if n['id'] in ('c', 'tx'): + n['cannotRaise'] = True + n = b.load().nodes + self.assertIs(n['g'].get_fallthrough_child(), n['u']) + self.assertTrue(n['c'].reachesAssertSameLevel) + + class UnwindTest(unittest.TestCase): def test_escaping_exception_resumes_at_callers_handler(self): diff --git a/symbolic-explorer/tests/test_search_order.py b/symbolic-explorer/tests/test_search_order.py new file mode 100644 index 00000000..cfc691b0 --- /dev/null +++ b/symbolic-explorer/tests/test_search_order.py @@ -0,0 +1,77 @@ +""" +Unit tests for the search orders of strategy/StrategyService (--search-order): node depth, the +instruction and side a flip takes, and the sides the tree's traces covered. + +Run from symbolic-explorer/: + ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_search_order -v +""" + +import os +import sys +import unittest + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) + +from data.BinaryExecutionTree.Node import Node +from strategy.StrategyService import depth, open_side, covered_sides, first_coverers, trace_scores + +LOOP = 1 << 58 # one loop iteration in an iid + + +def node(iid, parent=None, gid=0, trace='t1'): + n = Node.__new__(Node) + n.id = iid + n.gid = gid + n.trace_id = trace + n.kind = "Branch" + n.parent = parent + n.branched = None + n.skipped = None + return n + + +class SearchOrderTest(unittest.TestCase): + + def setUp(self): + # root (iid 1) took its branched side twice around a loop (iid 2, then 2 + LOOP); + # the second iteration also went to the skipped side of iid 3, where the trace ended. + # (t1 ran first; t2 diverged from it at b's skipped side and added c.) + self.root = node(1, gid=1) + self.a = node(2, self.root, gid=2) + self.root.branched = self.a + self.b = node(2 + LOOP, self.a, gid=3) + self.a.branched = self.b + self.c = node(3, self.b, gid=4, trace='t2') + self.b.skipped = self.c + self.c.skipped = object() # a leaf + + def test_depth_counts_the_branches_above(self): + self.assertEqual([depth(n) for n in (self.root, self.a, self.b, self.c)], [0, 1, 2, 3]) + + def test_open_side_ignores_the_loop_count(self): + # a and b are the same instruction in different iterations: a has its skipped side open, + # b (which took the skipped side) its branched side + self.assertEqual(open_side(self.a), (2, False)) + self.assertEqual(open_side(self.b), (2, True)) + # c took its skipped side, so flipping it takes the branched one + self.assertEqual(open_side(self.c), (3, True)) + + def test_covered_sides_are_those_some_trace_took(self): + covered = covered_sides(self.root) + self.assertEqual(covered, {(1, True), (2, True), (2, False), (3, False)}) + # The two iterations took both sides of instruction 2: flipping either reaches nothing new. + self.assertIn(open_side(self.a), covered) + self.assertIn(open_side(self.b), covered) + self.assertNotIn(open_side(self.c), covered) + self.assertNotIn(open_side(self.root), covered) + + + def test_traces_score_the_sides_they_took_first(self): + first = first_coverers(self.root) + self.assertIs(first[(2, True)], self.a) # a was there before b + # t1 took 1-branched, 2-branched and 2-skipped (via b) first, t2 3-skipped + self.assertEqual(trace_scores(first), {'t1': 3, 't2': 1}) + + +if __name__ == '__main__': + unittest.main() diff --git a/symbolic-explorer/tests/test_shorten_strings.py b/symbolic-explorer/tests/test_shorten_strings.py new file mode 100644 index 00000000..eb15fecb --- /dev/null +++ b/symbolic-explorer/tests/test_shorten_strings.py @@ -0,0 +1,49 @@ +""" +Unit tests for Z3Handler.shorten_strings (--prefer-short-strings): the string inputs of a model are +made as short as the assertions allow, one input after the other. + +Needs z3, so run it with the harness venv, from symbolic-explorer/: + ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_shorten_strings -v +""" + +import os +import sys +import unittest + +import z3 + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) + +from solver.SolverHandler import Z3Handler + + +class ShortenStringsTest(unittest.TestCase): + + def test_inputs_get_the_shortest_length_the_query_allows(self): + s = z3.String('java/lang/String_0') + t = z3.String('java/lang/String_1') + solver = z3.Solver() + solver.add(z3.PrefixOf(z3.StringVal('-x'), s), z3.Length(s) + z3.Length(t) >= 7, z3.Length(t) >= 3) + solver.push() + solver.add(z3.Length(s) == 6, z3.Length(t) == 9) # a model with longer strings than needed + self.assertEqual(solver.check(), z3.sat) + model = solver.model() + solver.pop() + self.assertEqual(solver.check(), z3.sat) + shorter = Z3Handler.shorten_strings(solver, model, 0.01) + lengths = sorted(shorter.eval(z3.Length(v)).as_long() for v in (s, t)) + self.assertEqual(sum(lengths), 7) + self.assertTrue(shorter.eval(z3.PrefixOf(z3.StringVal('-x'), s))) + + def test_other_variables_are_left_alone(self): + i = z3.BitVec('I_0', 32) + tmp = z3.String('tmp') # not an input name + solver = z3.Solver() + solver.add(z3.Length(tmp) > 4, i == 3) + self.assertEqual(solver.check(), z3.sat) + model = Z3Handler.shorten_strings(solver, solver.model(), 0.01) + self.assertEqual(model.eval(i).as_long(), 3) + + +if __name__ == '__main__': + unittest.main() diff --git a/targets/applications/openolat/docker/run/Dockerfile b/targets/applications/openolat/docker/run/Dockerfile index 65ce5dbe..c41a0aa7 100644 --- a/targets/applications/openolat/docker/run/Dockerfile +++ b/targets/applications/openolat/docker/run/Dockerfile @@ -7,7 +7,7 @@ WORKDIR /usr/local/tomcat RUN mkdir -p /swat/libs/java-library-path COPY ./libs/z3/bin/libz3.so /swat/libs/java-library-path -COPY ./libs/z3/bin/com.microsoft.z3.jar /swat/libs/java-library-path +COPY ./libs/z3/java/com.microsoft.z3.jar /swat/libs/java-library-path COPY ./libs/z3/bin/libz3java.so /swat/libs/java-library-path COPY ./libs/z3/bin/z3 /swat/libs/java-library-path diff --git a/targets/applications/openolat/z3_extract_helper.sh b/targets/applications/openolat/z3_extract_helper.sh index 87b27782..8805de7b 100755 --- a/targets/applications/openolat/z3_extract_helper.sh +++ b/targets/applications/openolat/z3_extract_helper.sh @@ -1,7 +1,7 @@ pushd libs rm -r * -cp ../../../../libs/z3-4.13.3-x64-glibc-2.35.zip ./z3.zip +cp ../../../../libs/z3-5.3.1-x64-glibc-2.39.zip ./z3.zip unzip z3.zip -mv z3-4.13.3-x64-glibc-2.35 z3 +mv z3-5.3.1-x64-glibc-2.39 z3 rm z3.zip popd diff --git a/targets/examples/my-example-2/build.sh b/targets/examples/my-example-2/build.sh index acaf5972..5dced6ce 100755 --- a/targets/examples/my-example-2/build.sh +++ b/targets/examples/my-example-2/build.sh @@ -1,4 +1,4 @@ #!/bin/bash # Compile the target file -javac -cp ../../../annotations/build/libs/annotations-1.0.jar Example.java +javac -cp ../../../annotations/build/libs/annotations-1.0.jar -d build src/Example.java diff --git a/targets/examples/my-example-2/run.sh b/targets/examples/my-example-2/run.sh index dc3b065d..a1aa350d 100755 --- a/targets/examples/my-example-2/run.sh +++ b/targets/examples/my-example-2/run.sh @@ -4,7 +4,7 @@ ./../../../symbolic-explorer/.venv/bin/python3 ../../../symbolic-explorer/SymbolicExplorer.py \ --mode annotation \ --target Example \ - --classpath . \ + --classpath build \ --agent ../../../symbolic-executor/lib/symbolic-executor.jar \ --z3dir ../../../libs/java-library-path \ --config swat.cfg \ diff --git a/targets/examples/my-example-2/Example.java b/targets/examples/my-example-2/src/Example.java similarity index 66% rename from targets/examples/my-example-2/Example.java rename to targets/examples/my-example-2/src/Example.java index 0d767085..a5d03a62 100644 --- a/targets/examples/my-example-2/Example.java +++ b/targets/examples/my-example-2/src/Example.java @@ -8,13 +8,11 @@ public static void main(String[] args) { public static void test(@Symbolic int val, @Symbolic int distract) { if (distract > 0) { - int sum = 0; - for (int i = 0; i < 10; i++) { - if (distract > i) { - sum += i; + for (int i = 0; i < 100; i++) { + if (i < val) { + System.out.println(i); } } - System.out.println(sum); } else { assert val != 3141592; } diff --git a/targets/sv-comp/scripts/commands/test.py b/targets/sv-comp/scripts/commands/test.py index 434ff9f4..5a61465b 100644 --- a/targets/sv-comp/scripts/commands/test.py +++ b/targets/sv-comp/scripts/commands/test.py @@ -68,12 +68,14 @@ def list_tests(ctx, benchmark_dir, stats): @click.option('--sa-retry-without', 'sa_retry_without', is_flag=True, default=False, help='On a SAFE verdict reached with static pre-analysis, retry the exploration without it') @click.option('--parallel-sa', 'parallel_sa', is_flag=True, default=False, help='Run the static pre-analysis in the background while exploring, instead of waiting for it (nondeterministic)') @click.option('--sa-no-callback-targets', 'sa_no_callback_targets', is_flag=True, default=False, help='Do not count library calls as possible asserts when a callback from library code may reach one (unsound)') +@click.option('--sa-no-runtime-exception', 'sa_no_runtime_exception', is_flag=True, default=False, help='Also prune with the static pre-analysis under no-runtime-exception (by default only under valid-assert)') @click.option('--sa-rank-distance', 'sa_rank_distance', is_flag=True, default=False, help='Try branches closest to an assert in the static pre-analysis graph first') +@click.option('--search-order', 'search_order', type=click.Choice(['dfs', 'shallow', 'coverage', 'coverage-dfs', 'generational']), default='dfs', help='Order in which open branches are tried (see SymbolicExplorer.py --search-order)') @click.option('--solver-rlimit', 'solver_rlimit', type=int, default=0, help='Z3 resource limit for the first query of each branch, growing on retries (0: unlimited)') @click.option('--testcase-timeout-s', type=int, default=15 * 60, help='Timeout of the symbolic-explorer in seconds for each test case') @click.pass_context def run_tests(ctx, mode, workers, benchmark_dir, config_file: str | None, categories, suite, limit_nr_tests: int | None, target: str, - no_witness: bool, no_sa: bool, sa_retry_without: bool, parallel_sa: bool, sa_rank_distance: bool, sa_no_callback_targets: bool, solver_rlimit: int, testcase_timeout_s: int): + no_witness: bool, no_sa: bool, sa_retry_without: bool, parallel_sa: bool, sa_rank_distance: bool, sa_no_callback_targets: bool, solver_rlimit: int, search_order: str, testcase_timeout_s: int, sa_no_runtime_exception: bool): """Run verification tests.""" from lib import ( extract_testcases, @@ -138,7 +140,7 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file: str | None, catego # One timestamp ties this run's per-testcase logs to its results dir. run_timestamp = new_run_timestamp() - ver_tasks_with_commands = generate_commands(ver_tasks, config_file, run_timestamp=run_timestamp, no_sa=no_sa, sa_retry_without=sa_retry_without, parallel_sa=parallel_sa, sa_rank_distance=sa_rank_distance, sa_no_callback_targets=sa_no_callback_targets, solver_rlimit=solver_rlimit, cpu_limit_s=testcase_timeout_s) + ver_tasks_with_commands = generate_commands(ver_tasks, config_file, run_timestamp=run_timestamp, no_sa=no_sa, sa_retry_without=sa_retry_without, parallel_sa=parallel_sa, sa_rank_distance=sa_rank_distance, sa_no_callback_targets=sa_no_callback_targets, solver_rlimit=solver_rlimit, cpu_limit_s=testcase_timeout_s, search_order=search_order, sa_no_runtime_exception=sa_no_runtime_exception) click.echo(f"Generated {len(ver_tasks_with_commands)} commands") # Check port availability @@ -181,7 +183,8 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file: str | None, catego sa_retry_without=sa_retry_without and not no_sa, sa_rank_distance=sa_rank_distance and not no_sa, sa_callback_targets=not sa_no_callback_targets and not no_sa, - solver_rlimit=solver_rlimit) + solver_rlimit=solver_rlimit, search_order=search_order, + sa_no_runtime_exception=sa_no_runtime_exception and not no_sa) run_parallel(ver_tasks_with_commands, max_workers=workers, create_witness=not no_witness, run_dir=run_dir, testcase_timeout_s=testcase_timeout_s) diff --git a/targets/sv-comp/scripts/lib/command_gen.py b/targets/sv-comp/scripts/lib/command_gen.py index 6e135ff3..bc67613e 100644 --- a/targets/sv-comp/scripts/lib/command_gen.py +++ b/targets/sv-comp/scripts/lib/command_gen.py @@ -35,7 +35,7 @@ def is_port_available(port: int) -> bool: return False -def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=8087, config_file:str = 'swat.cfg', no_sa: bool = False, sa_retry_without: bool = False, parallel_sa: bool = False, sa_rank_distance: bool = False, sa_no_callback_targets: bool = False, solver_rlimit: int = 0, cpu_limit_s: Optional[int] = None) -> list[str]: +def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=8087, config_file:str = 'swat.cfg', no_sa: bool = False, sa_retry_without: bool = False, parallel_sa: bool = False, sa_rank_distance: bool = False, sa_no_callback_targets: bool = False, solver_rlimit: int = 0, cpu_limit_s: Optional[int] = None, search_order: str = 'dfs', sa_no_runtime_exception: bool = False) -> list[str]: test_case_dir = ver_task['file_path'].parent @@ -43,9 +43,12 @@ def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=80 config_path = SCRIPT_DIR / '..' / config_file library_path = BASE_PATH / 'libs' / 'java-library-path' sa_path = BASE_PATH.parent / 'cfg-extraction' - # The pre-analysis only targets asserts, so it can only prune for valid-assert (the explorer - # enforces this too). - no_sa = no_sa or ver_task['category'] != VerificationCategory.VALID_ASSERT_PRP + # The graph has target points for valid-assert and no-runtime-exception only (the explorer + # enforces this too, see StaticPreAnalysis.SA_TARGETS). Under no-runtime-exception it is opt-in: + # sound, but it costs more than it saves on sv-benchmarks so far (see CLAUDE.md, Targets per property). + sa_properties = (VerificationCategory.VALID_ASSERT_PRP,) + \ + ((VerificationCategory.NO_RUNTIME_EXCEPTION_PRP,) if sa_no_runtime_exception else ()) + no_sa = no_sa or ver_task['category'] not in sa_properties base_command: list[str] = [str(PYENV_PATH), "-u", str(BASE_PATH / 'symbolic-explorer' / 'SymbolicExplorer.py'), "-prp", ver_task['category'].value, @@ -62,6 +65,7 @@ def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=80 (["--sa-rank-distance"] if sa_rank_distance and not no_sa else []) + \ (["--sa-no-callback-targets"] if sa_no_callback_targets and not no_sa else []) + \ (["--solver-rlimit", str(solver_rlimit)] if solver_rlimit else []) + \ + (["--search-order", search_order] if search_order != 'dfs' else []) + \ (["--cpu-limit", str(cpu_limit_s)] if cpu_limit_s else []) cp: list[str] = [] @@ -105,7 +109,7 @@ def write_run_info(run_dir: Path, **settings) -> Path: return path -def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swat.cfg', run_timestamp: Optional[str] = None, no_sa: bool = False, sa_retry_without: bool = False, parallel_sa: bool = False, sa_rank_distance: bool = False, sa_no_callback_targets: bool = False, solver_rlimit: int = 0, cpu_limit_s: Optional[int] = None) -> list[VerificationTask]: +def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swat.cfg', run_timestamp: Optional[str] = None, no_sa: bool = False, sa_retry_without: bool = False, parallel_sa: bool = False, sa_rank_distance: bool = False, sa_no_callback_targets: bool = False, solver_rlimit: int = 0, cpu_limit_s: Optional[int] = None, search_order: str = 'dfs', sa_no_runtime_exception: bool = False) -> list[VerificationTask]: port = 9000 skipped_ports = [] @@ -150,7 +154,7 @@ def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swa 'target_dir': target_dir, 'target': target, 'log_dir': logging_dir, - 'command': generate_command(ver_task, logging_dir, port=port, config_file=config_file, no_sa=no_sa, sa_retry_without=sa_retry_without, parallel_sa=parallel_sa, sa_rank_distance=sa_rank_distance, sa_no_callback_targets=sa_no_callback_targets, solver_rlimit=solver_rlimit, cpu_limit_s=cpu_limit_s) + 'command': generate_command(ver_task, logging_dir, port=port, config_file=config_file, no_sa=no_sa, sa_retry_without=sa_retry_without, parallel_sa=parallel_sa, sa_rank_distance=sa_rank_distance, sa_no_callback_targets=sa_no_callback_targets, solver_rlimit=solver_rlimit, cpu_limit_s=cpu_limit_s, search_order=search_order, sa_no_runtime_exception=sa_no_runtime_exception) } ver_task['command'] = command port += 1 diff --git a/targets/sv-comp/scripts/requirements.txt b/targets/sv-comp/scripts/requirements.txt index c8515db1..8daedad2 100644 --- a/targets/sv-comp/scripts/requirements.txt +++ b/targets/sv-comp/scripts/requirements.txt @@ -12,5 +12,5 @@ starlette==0.46.2 typing-inspection==0.4.0 typing_extensions==4.13.2 uvicorn==0.34.1 -z3-solver==4.14.1.0 +z3-solver==5.3.1.0 requests