diff --git a/.claude/skills/jdk-source/SKILL.md b/.claude/skills/jdk-source/SKILL.md new file mode 100644 index 0000000..8fff89a --- /dev/null +++ b/.claude/skills/jdk-source/SKILL.md @@ -0,0 +1,70 @@ +--- +name: jdk-source +description: Fetch the exact source of a JDK method/class from the active JDK's lib/src.zip (version-exact, no network), and audit a java.lang method for SWAT purity-whitelist eligibility. Use when deciding whether a JDK method may be added to PureMethods.WHITELIST (pure-function UF modeling), or when you need to read what a JDK method actually does. +--- + +# JDK source + purity-whitelist audit + +Two jobs: (1) cheaply read JDK source, (2) decide if a method may join `PureMethods.WHITELIST` +(`symbolic-executor/.../symbolic/UFs/PureMethods.java`). Background: the pure-function whitelist +section of `docs/heap-tracking.md`. + +## Fetching source — `scripts/jmethod.py` + +Reads the active JDK's `lib/src.zip` (resolved from `$JAVA_HOME`, else `java -XshowSettings:properties`). +Version-exact, offline. + +```bash +python3 .claude/skills/jdk-source/scripts/jmethod.py java.lang.Math # index: every method signature + line +python3 .claude/skills/jdk-source/scripts/jmethod.py java.lang.Math floorDiv # full source of all overloads +python3 .claude/skills/jdk-source/scripts/jmethod.py java.lang.Math floorDiv --callees # + the methods each overload calls +python3 .claude/skills/jdk-source/scripts/jmethod.py java.lang.Integer --field digits # a field declaration +``` + +`` is dotted (`java.lang.String`). Nested types live in their top-level file. Follow +`--callees` transitively (call the script again on each callee's class) to establish purity through +the call graph. + +## Whitelist eligibility — the rubric + +A method may be added to `WHITELIST` **iff ALL six hold**. The whitelist is a soundness precondition: +an unsound entry can make the engine model a non-deterministic/side-effecting call as a referentially +transparent UF, which can corrupt a verdict. When unsure, EXCLUDE. + +1. **Pure / deterministic / side-effect-free.** Same inputs always give the same output; no observable + effect. Read the source (transitively via `--callees`): reject any `PUTSTATIC`/`PUTFIELD` to shared + mutable state, I/O, synchronization-for-effect, or argument mutation. Reading `static final` + constant tables (e.g. `Integer.digits`) is fine. +2. **No locale / time / random / environment dependence.** Reject no-arg `String.toLowerCase()`/ + `toUpperCase()` (default locale), `String.format`, property/env readers, `Math.random`, + `System.currentTimeMillis`, etc. NB: `Character.toLowerCase(char)` IS locale-independent (Unicode + table) and allowed — unlike the `String` no-arg forms. +3. **No identity / interning semantics.** Reject `intern`, identity-hashing, or methods whose result + identity matters. (Value equality of the result is fine; the UF models the value.) +4. **UNMODELED by SWAT.** If SWAT already models the method, the UF never fires (dead entry). Check the + matching handler in `symbolic-executor/.../symbolic/invoke/java/lang/Invocation.java`: the + method's name must NOT be in its dispatch (it must fall to `default -> PlaceHolder.instance`). + `String` methods: check `StringInvocation` + the `StringValue` model methods. +5. **Supported return sort.** The return type must be `String` or a primitive (`boolean`, `byte`, + `short`, `char`, `int`, `long`, `float`, `double`). Object/array/`void`/collection/stream returns + are NOT supported (`buildPureUF` returns null → falls back to concretization). The UF return sort is + set by `InvocationHandler#pureUFReturnType`. +6. **Value-typed inputs only.** Every parameter (and, for an instance method, the receiver) must be a + String or boxed primitive — i.e. captured by a formula (`Util.isValueType`). Reject methods taking + arrays, `CharSequence`, collections, `Object`, `Function`, etc. (their formula can't capture the + input). Prefer the STATIC equivalent over a receiver-keyed instance accessor: `ufName` keys only on + argument descriptors, so two distinct receivers of an instance method (`intValue()`, instance + `toString()`/`hashCode()`) would collide to one UF term — EXCLUDE those until receiver-keyed UFs exist. + +## Entry format + +`WHITELIST` keys are `owner + "/" + name + descriptor`, e.g. `java/lang/Math/floorDiv(II)I`. The +descriptor disambiguates overloads. Verify it against the index (`jmethod.py `). + +## Verifying an addition + +After adding, drive it through the real agent (an L2 `*AgentSpec` calling the method on a `@Symbolic` +input into a branch) and assert: a `pure_` UF appears in the branch constraints, and +`symbolicContextLoss == false`, `symbolicPrecisionLoss == false`. See `PureFunctionUFAgentSpec` (String) +and `PureFunctionPrimitiveAgentSpec` (primitive). The L0 `PureUFPrimitiveRecoverySpec` pins the +per-sort recovery construction. Use the `swat-test` skill for the harness details. diff --git a/.claude/skills/jdk-source/scripts/jmethod.py b/.claude/skills/jdk-source/scripts/jmethod.py new file mode 100755 index 0000000..010d035 --- /dev/null +++ b/.claude/skills/jdk-source/scripts/jmethod.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +"""Cheaply fetch JDK source from the active JDK's lib/src.zip (version-exact, no network). + +Usage: + jmethod.py # index: every method/ctor signature + line no. + jmethod.py # full source of all overloads of + jmethod.py --callees # also list the methods each overload calls + jmethod.py --field # a field declaration (for static-final purity checks) + + is dotted, e.g. java.lang.String. Nested classes: java.lang.Integer (the file is the +top-level class; nested types appear within it). The JDK is resolved from $JAVA_HOME, else from +`java -XshowSettings:properties`. Override the module with --module (default: search all). +""" +import os +import re +import subprocess +import sys +import zipfile + + +def java_home() -> str: + jh = os.environ.get("JAVA_HOME") + if jh and os.path.exists(os.path.join(jh, "lib", "src.zip")): + return jh + out = subprocess.run(["java", "-XshowSettings:properties"], + capture_output=True, text=True).stderr + m = re.search(r"java\.home\s*=\s*(.+)", out) + if not m: + sys.exit("Could not resolve java.home (set $JAVA_HOME).") + return m.group(1).strip() + + +def load_source(fqn: str, module: str | None): + zp = os.path.join(java_home(), "lib", "src.zip") + if not os.path.exists(zp): + sys.exit(f"No src.zip at {zp} — this JDK ships no sources.") + rel = fqn.replace(".", "/") + ".java" + with zipfile.ZipFile(zp) as z: + cands = [n for n in z.namelist() if n.endswith(rel) + and (module is None or n.startswith(module + "/"))] + if not cands: + sys.exit(f"Not found in src.zip: {rel}" + + (f" (module {module})" if module else "")) + entry = cands[0] + return entry, z.read(entry).decode("utf-8", "replace").splitlines() + + +# A modest scanner: yields the source with strings/chars/comments blanked, so brace counting and +# signature detection ignore braces and identifiers inside literals/comments. Good enough for JDK src. +def blank_noncode(src: list[str]) -> list[str]: + out, in_block = [], False + for line in src: + res, i, n = [], 0, len(line) + while i < n: + c = line[i] + if in_block: + if c == "*" and i + 1 < n and line[i + 1] == "/": + in_block = False + res.append(" "); i += 2; continue + res.append(" "); i += 1; continue + if c == "/" and i + 1 < n and line[i + 1] == "/": + res.append(" " * (n - i)); break + if c == "/" and i + 1 < n and line[i + 1] == "*": + in_block = True + res.append(" "); i += 2; continue + if c in "\"'": + q = c; res.append(" "); i += 1 + while i < n: + if line[i] == "\\": + res.append(" "); i += 2; continue + if line[i] == q: + res.append(" "); i += 1; break + res.append(" "); i += 1 + continue + res.append(c); i += 1 + out.append("".join(res)) + return out + + +SIG = re.compile(r"^\s{1,8}(?:(?:public|private|protected|static|final|native|synchronized|" + r"abstract|default|strictfp)\s+)+[\w$.<>\[\]?,\s]*?\b(\w+)\s*\(") + + +def signatures(code: list[str]): + """(line_index, method_name) for lines that look like a method/ctor declaration.""" + for i, line in enumerate(code): + m = SIG.search(line) + if m and "=" not in line.split("(")[0]: + yield i, m.group(1) + + +def brace_extent(code: list[str], start: int): + """From a signature at line `start`, return (end_index) of the matching close brace, or None + for abstract/interface methods that end in ';' before any '{'.""" + depth, seen = 0, False + for i in range(start, len(code)): + for c in code[i]: + if c == "{": + depth += 1; seen = True + elif c == "}": + depth -= 1 + if seen and depth == 0: + return i + if not seen and ";" in code[i]: + return None # no body (abstract/native-decl) + return len(code) - 1 + + +def main(): + args = [a for a in sys.argv[1:]] + module = None + if "--module" in args: + k = args.index("--module"); module = args[k + 1]; del args[k:k + 2] + callees = "--callees" in args + if callees: + args.remove("--callees") + field = None + if "--field" in args: + k = args.index("--field"); field = args[k + 1]; del args[k:k + 2] + if not args: + sys.exit(__doc__) + fqn = args[0] + method = args[1] if len(args) > 1 else None + + entry, src = load_source(fqn, module) + code = blank_noncode(src) + print(f"// {entry} ({len(src)} lines)") + + if field: + for i, line in enumerate(code): + if re.search(r"\b" + re.escape(field) + r"\b", line) and ("=" in line or ";" in line) \ + and SIG.search(line) is None: + print(f"{i+1}: {src[i].rstrip()}") + return + + if method is None: + print(f"// method/ctor index for {fqn}:") + for i, name in signatures(code): + print(f"{i+1}: {src[i].strip()}") + return + + hits = [i for i, name in signatures(code) if name == method] + if not hits: + sys.exit(f"No declaration of {method}(...) found in {fqn}.") + for start in hits: + end = brace_extent(code, start) + end = start if end is None else end + print(f"\n// ---- {fqn}.{method} (lines {start+1}-{end+1}) ----") + print("\n".join(src[start:end + 1])) + if callees: + body = "\n".join(code[start:end + 1]) + names = sorted(set(re.findall(r"\b([a-zA-Z_]\w*)\s*\(", body)) + - {method, "if", "for", "while", "switch", "catch", "return", "new"}) + print(f"// callees: {', '.join(names)}") + + +if __name__ == "__main__": + main() diff --git a/.claude/skills/svcomp-run/SKILL.md b/.claude/skills/svcomp-run/SKILL.md new file mode 100644 index 0000000..695b790 --- /dev/null +++ b/.claude/skills/svcomp-run/SKILL.md @@ -0,0 +1,100 @@ +--- +name: svcomp-run +description: Run the SWAT SV-COMP benchmark harness — parallel scoring runs and single-testcase debug runs — and debug one testcase's verdict via single mode. Use when running/scoring sv-benchmarks locally, reproducing or debugging a single testcase, or interpreting points/verdicts/soundness downgrades. Covers setup, the ./svcomp CLI, config files, log locations, and the per-testcase wall-clock cap. +--- + +# Running & debugging the SV-COMP harness + +The custom local harness is in `targets/sv-comp/scripts/`. Per testcase it compiles the target, runs +SWAT (Java agent + Python explorer over HTTP), scores the verdict, and optionally validates witnesses. +Drive everything through the `./svcomp` wrapper (it selects the venv Python) **from +`targets/sv-comp/scripts/`**. This is the *local/custom* runner; the real competition infra uses a +separate wrapper (`scripts/svcomp-package/run_swat.py`) — don't confuse the two. + +## One-time setup + +From the repo root, build the agent + native libs (rebuild the jar after ANY executor change — the +harness runs the jar, not the classes): +```bash +./gradlew copyNativeLibs # z3 -> libs/java-library-path +./gradlew :symbolic-executor:copyJar # -> symbolic-executor/lib/symbolic-executor.jar +./gradlew :targets:sv-comp:WitnessCreator:shadowJar # only if validating violation witnesses +``` +Then in `targets/sv-comp/scripts/`: +```bash +python3 -m venv .venv && .venv/bin/pip install -r requirements.txt +./svcomp setup checkout-benchmarks # SSH clone of SV-Benchmarks (sparse java/) -> ../sv-benchmarks +./svcomp setup checkout-validator # wit4java, only for witness validation +``` + +## Run — parallel (scoring) +```bash +./svcomp test run --mode parallel --workers 50 +./svcomp test run --categories valid-assert.prp --workers 30 # one property only +``` +- Uses `../sv-comp.cfg` (quiet: WARN, no console). Prints per-category points and + `TOTAL POINTS (ALL CATEGORIES): N`, and saves `results/results__.json`. +- `./svcomp analyze results` summarizes the latest results file (context losses / failures). +- `./svcomp test list [--stats]` enumerates testcases; `./svcomp test validate-ports` checks ports. + +## Run — single (one testcase, debug) +```bash +./svcomp test run --mode single \ + --target "autostub/String_public_java_lang_String_java_lang_String_toLowerCase" [--no-witness] +``` +- `--target` is the testcase identifier `/` (matched by suffix against the testcase path). +- Single mode forces `../swat-debug.cfg` (INFO, console on, shadow-stack + symbolic-execution logging on). +- `--no-witness` skips witness gen/validation (avoids wit4java); fine when you only care about the verdict. + +## Debugging a testcase (single mode) +1. Run it single-mode; watch the console. SWAT's own lines are prefixed `[SWAT] -->`. +2. Per-testcase logs land in `logs-debug//_/` (`verdict.log`, symbolic-execution + and shadow-stack logs). Parallel mode instead writes to `logs/`. +3. The exact forked command is logged, e.g. + `java -Xmx32g -Dconfig.path=…/swat-debug.cfg -Dexplorer.port= -javaagent:…/symbolic-executor.jar + -Djava.library.path=… -cp :: -ea Main`. Copy it to run SWAT directly (attach a + debugger, change flags, add `-Dsolver.mode=PRINT` to dump the TraceDTO without the explorer). +4. Markers to grep: + - `[VERDICT ] == TRUE | FALSE | DONT-KNOW` — explorer verdict (safe / violation / unknown). + - `Context loss recorded!` / `Found symbolic context loss`, `Found ... precision loss` — soundness + downgrades (a would-be SAFE becomes UNKNOWN). + - `Invocation of method X in class Y ... cases context loss` (`InvocationHandler.java`) — an unmodeled + method hit with symbolic input. + - `Points: P, Case: -> ` — the scored outcome. + +## Reading the result +`Case: -> `; expected comes from the testcase `.yml` +(`expected_verdict: true` = no violation → TRUE; `false` = violation reachable → FALSE): +- match → `Points: 1` (a violation also needs a validated witness for the point unless `--no-witness`); +- mismatch or unknown → `Points: 0`. +- A `… -> unknown` caused by context/precision loss is **sound** — SWAT declined rather than answered + wrong; not a bug. Example: the flagship `…toLowerCase` case scores `violation -> unknown` because no-arg + `toLowerCase` is locale-dependent and unmodeled, so its result is concretized + context-loss-flagged. + +## Per-testcase wall-clock cap (outside the actual run) +Each testcase's SWAT process is wrapped in `lib/execution.py:run_command_with_timeout` — launched in its +own session (`start_new_session=True`); on `TimeoutExpired` it `os.killpg(…, SIGKILL)`s the whole tree +(JVM + Z3) and records `ExecutionStatus.TIMEOUT` → 0 points, never a wrong verdict. This is entirely +outside the run (SWAT is given no limit; the harness kills it). Default is **900s**; set a shorter +per-testcase cap here (e.g. 120s), or expose it as a `--timeout` option on `swat test`. Do **not** edit +`scripts/svcomp-package/run_swat.py` — that is the separate wrapper the competition infra uses. + +## Key files +- `svcomp.py` + `commands/{setup,test,analyze,util}.py` — the click CLI. +- `lib/execution.py` — `target_execution` (one task), `run_parallel`, `run_single_target`, + `run_command_with_timeout` (the wall-clock cap), scoring + `save_results`. +- `lib/command_gen.py` — builds the per-testcase `java … -javaagent … Main` command. +- `lib/selection.py` — `extract_testcases` (parses the `.yml`s). +- Configs: `../sv-comp.cfg` (parallel), `../swat-debug.cfg` (single/debug) — differ only in logging. +- `../sv-benchmarks/java///` — testcase: `Main.java` + `.yml` (holds `expected_verdict`). + +## Gotchas +- Always run from `targets/sv-comp/scripts/` via `./svcomp` (not `svcomp.py` directly — the wrapper sets + the venv Python). The older standalone `target_execution.py` (invoked by `run_locally.sh`) is a separate + path with its own shorter timeout — prefer the `swat test` CLI. +- Witness validation (wit4java) resolves `python3` via PATH and needs extra venv packages + (`setuptools`, `pyyaml`, `javalang`, `networkx`); prefix with `PATH="$PWD/.venv/bin:$PATH"` or use + `--no-witness`. +- `solver.mode=HTTP`: the explorer runs as a per-testcase HTTP server on an allocated port; parallel runs + use many ports at once. +- Rebuild `:symbolic-executor:copyJar` after executor changes, or you'll score the old jar. diff --git a/.claude/skills/swat-test/SKILL.md b/.claude/skills/swat-test/SKILL.md new file mode 100644 index 0000000..da534b4 --- /dev/null +++ b/.claude/skills/swat-test/SKILL.md @@ -0,0 +1,75 @@ +--- +name: swat-test +description: Create and run tests for the SWAT symbolic-executor at the right abstraction level (L0 value-unit, L1 processor, L2 forked-agent). Use when adding a test for shadow values, the shadow interpreter, recovery/heap behavior, soundness flags, or a whole-program agent run — or when deciding which level a behavior belongs at. Covers the fixtures, the oracle rules, the @PendingFeature red convention, and the run commands. +--- + +# Testing SWAT (symbolic-executor) + +Full rationale: `docs/test-architecture.md`. This skill is the operational recipe. + +## Pick the level (lowest faithful altitude) + +| Level | Use when the behavior lives in… | Driver | +|---|---|---| +| **L0** value/structure unit | a `Value` method or shadow structure (`StringValue.IF_ACMPEQ`, `ObjectValue.equals`, `JVMHeap` key, copy-ctor, UF SMT-agreement) | construct objects directly | +| **L1** processor | how the shadow interpreter reacts to an instruction stream (lift, **invoke→recovery**, branches, fields) | drive `SymbolicInstructionProcessor` | +| **L2** forked-agent | the real instrumentation→trace contract (real identity hashes, this-return, soundness flags) | run a real target under the agent | +| L3 end-to-end | the SV-COMP verdict + downgrade rules | sv-comp driver (out of current scope) | + +If unsure between L1 and L2: L1 *fabricates* the instruction stream (incl. address collisions), so it pins interpreter logic, not the instrumentation contract — use L2 to anchor anything whose bug depends on real JVM identity/this-return. + +## Oracle rules (every level — non-negotiable) + +Assert ONLY on: `Value.concrete`, `isSymbolic()`, symbolic **variable names** +(`extractVariables(f).keySet()`), `IF_ACMPEQ`/`equals` booleans, soundness flags, `Frame` +contents, structured `TraceDTO` fields, or **SAT/UNSAT agreement** via a real prover. +**Never** assert on a formula's SMT sort/representation (that is why the ~1670 `de/uzl/its/value/**` +rows break en masse). + +## Expected-red convention (`@PendingFeature`) + +There is no `spock.lang.Tag` in this Spock version. For a behavior not yet implemented (red-first +TDD), annotate the feature `@PendingFeature(reason = "…")`: it runs and asserts the *desired* +behavior, is reported **pending (skipped), not a failure**, and **fails the build the moment it +starts passing** (your "fix landed" signal). Put currently-true preconditions first, or as a +*separate non-pending* feature, so an infra break is a real failure, not masked as pending. + +## How to add a test + +**L0** — extend `de.uzl.its.swat.symbolic.heap.BaseValueSpec` (gives `context`, `fmgr`, and the +`isValid(BooleanFormula)` / `isUnsatisfiable(BooleanFormula)` boolean oracles). Construct values +with `context`. Example: `ObjectIdentitySpec`. + +**L1** — extend `de.uzl.its.swat.symbolic.processor.BaseSymbolicInstructionProcessorSpec`. Call +`setupTestContext(className, method)` first. For an unmodeled-call recovery, use the fixture: +```groovy +def result = executeBoundaryRecovery(receiver, owner, name, desc, concreteResult, resultAddress) +// result.recovered (Value), result.contextLoss +// resultAddress == receiver.address -> this-return; fresh address -> new-object return +``` +Example: `ValueRecoverySpec`. + +**L2** — add a tiny target to `src/test/resources/targets/.java` using `@Symbolic` on a +**method parameter** (a local needs `-g` and may crash the annotation transformer). Name the spec +`*AgentSpec` and use the harness: +```groovy +TraceObservation obs = AgentRun.run("targets/.java", "") +// obs.symbolicContextLoss / symbolicPrecisionLoss +// obs.inputNames ; obs.anyBranchReferences(inputVar) +``` +`AgentRun` compiles against the agent jar, forks a JVM with `solver.mode=PRINT`, and parses the +TraceDTO. Example: `HeapRecoveryAgentSpec`. + +## Run + +```bash +# L0 + L1 (fast, in-process, CI lane). Scope to your specs to skip the legacy value tests. +./gradlew :symbolic-executor:test --tests "de.uzl.its.swat.symbolic.heap.*" +./gradlew :symbolic-executor:test --tests "de.uzl.its.swat.symbolic.processor.*" + +# L2 (forked agent; builds the jar first; *AgentSpec only; excluded from `test`) +./gradlew :symbolic-executor:agentTest +``` + +Build the agent jar (when needed) with `:symbolic-executor:copyJar` — **never** `spotlessApply` +(it reformats the whole module). CI runs `copyNativeLibs` then `test`. diff --git a/docs/heap-tracking.md b/docs/heap-tracking.md new file mode 100644 index 0000000..4819208 --- /dev/null +++ b/docs/heap-tracking.md @@ -0,0 +1,325 @@ +# Heap & value tracking in the symbolic executor + +This is the reference for how the SWAT symbolic executor (the Java agent under +`symbolic-executor/`) tracks the values and objects a program manipulates. Read it before +changing anything under `symbolic/shadow/`, `symbolic/value/`, `symbolic/invoke/`, `symbolic/UFs/`, +or the `==`/de-interning instrumentation. It describes the system as it is today; it is not a +changelog. + +All paths below are relative to +`symbolic-executor/src/main/java/de/uzl/its/swat/` unless noted. Line numbers drift — the +**symbol names** (classes, methods, fields) are the stable anchors; grep for them. + +--- + +## Mental model (read this first) + +SWAT runs the real program on the real JVM and, in parallel, maintains a **shadow** interpretation +of it. Every value the program computes has a **shadow value**: the concrete runtime value it +actually holds, plus an optional **symbolic formula** (an SMT term) describing how it depends on the +designated symbolic inputs. Branches on symbolic values are recorded as path constraints; the +explorer later solves them to find new inputs or to prove a property. + +The hard part is **objects and library calls**. The JVM shares object identities (interned strings, +cached boxed integers, methods that return `this`), and most library methods are not modeled by +SWAT. The machinery here exists to keep the shadow world faithful across those boundaries: + +- a **registry** so each concrete object has exactly one shadow; +- **boundary recovery** so results of unmodeled calls re-enter the shadow world without corrupting + it; +- **de-intern + provenance** so reference equality (`==`) stays correct once we stop relying on JVM + interning; +- a **pure-function model** so we keep precision through side-effect-free library calls instead of + throwing it away; +- **soundness flags** so that whenever the shadow model is knowingly incomplete, a "safe" verdict is + downgraded rather than trusted. + +--- + +## Vocabulary + +- **Shadow value** — a tracked value: a *concrete* component (the observed runtime value) + an + optional *symbolic formula*. If the formula has no free variables/uninterpreted functions the + value is effectively concrete. +- **Symbolic input** — a value the user marked with `@Symbolic`; the free variables everything else + is expressed in terms of. +- **Value type** — a String or a boxed primitive wrapper — an immutable object with value semantics. + Contrast with a general mutable object. +- **Unmodeled method** — a library method SWAT does not simulate symbolically; it runs for real and + its result must be *recovered* into the shadow world. +- **Recovery / boundary** — reconciling the shadow stack with reality at a synchronization point + after an unmodeled call or a field/array read. +- **Uninterpreted function (UF)** — an SMT function symbol with no defining axioms except that equal + inputs give equal outputs. Used to model pure library calls. + +--- + +## Components + +### 1. The canonical shadow registry — one shadow per object + +Each tracked concrete object maps to exactly one shadow value. The map is keyed by the **object +itself, compared by reference identity (`==`)** — not by `System.identityHashCode`. Reference +keying is collision-free (two distinct objects stay distinct keys even if their identity hashes +collide) and yields one shadow per object. Keys are held **weakly**, so a plain object's or boxed +wrapper's shadow is evicted once the object is unreachable. + +- `symbolic/shadow/JVMHeap.java` — the map: `new MapMaker().weakKeys().makeMap()` in the + constructor; `put`/`get` (null-guarded); `size`. +- `symbolic/shadow/ShadowContext.java` — per-thread owner; delegators `putToHeap` / `getFromHeap` / + `heapSize`. One `JVMHeap` is created per `ShadowContext`. +- Read/write sites: `SymbolicInstructionVisitor.visitGETVALUE_Object` (and the primitive mirror). + +**String self-pinning caveat.** A `StringValue` stores its own concrete `String`, which is also its +key, so the weak key stays strongly reachable — String-keyed entries do **not** evict until the +whole `ShadowContext` is discarded. To bound this, recovery deliberately does not register +*constant* strings/boxed values in the heap (see §3). + +**Invariants** +- At most one shadow value per distinct concrete object. +- No identity-hash collision or reuse can alias two shadows. +- Non-String, non-self-referential entries are GC-evictable. + +### 2. What a shadow value is + +A shadow value pairs a concrete component with an optional formula whose SMT sort matches the Java +type exactly. + +- `symbolic/value/Value.java` — base class; fields `formula` and `concrete`; `isSymbolic()` + overridden per subtype. +- `symbolic/value/ValueFactory.java` — construction. `createNumericalValue` has a concrete-only + overload and one that carries an explicit `formula`; `createObjectValue` maps a concrete object to + the right subtype. +- Sort mapping: + - `int/long/short/byte/char` → bitvector of width **32/64/16/8/16** + (`value/primitive/numeric/integral/`). + - `boolean` → SMT boolean (`BooleanValue`, also in the `integral` package). + - `float/double` → single/double-precision floating point + (`value/primitive/numeric/floatingpoint/`). + - `String` → SMT string (`value/reference/lang/StringValue.java`). + - Boxed wrappers → `IntegerObjectValue` / `BooleanObjectValue` / … (`value/reference/lang/`). + +**Invariant** — a value's formula sort always matches its Java type; `concrete` always holds the +last observed real value. + +### 3. Boundary recovery of unmodeled returns + +When instrumented code calls a method SWAT does not model, the call runs for real and the executor +pushes a **placeholder** on its shadow stack. The real result is reconciled at the next `GETVALUE` +synchronization point, where the executor learns the concrete value the JVM produced. + +The subtle case is a **value-typed return (String or boxed primitive)**. Naively identity-recovering +it is unsound when the method returns `this` (e.g. `String.toLowerCase()` on an already-lowercase +string): the result would be re-bound to the *receiver's* formula. So the rule is: recover the +registered shadow only when the returned object is a **distinct, already-tracked immutable value** +(different from the receiver's own shadow) — e.g. a String retrieved from a `Map`/`List` — otherwise +concretize. This keeps a container round-trip symbolic while still breaking the `this`-return +aliasing. Recovery is limited to immutable value types (their value cannot have drifted since it was +registered) and fires only for values already registered in the heap. + +- `symbolic/value/PlaceHolder.java` — the placeholder; `enum ValueOrigin` (notably + `UNMODELED_RETURN`) tags where a placeholder came from; shared singletons `instance` / + `symbolicInstance`. +- `symbolic/invoke/InvocationHandler.java` — `invoke`: after the real call, if the result is a + placeholder and the call is not on `IGNORED_INVOCATIONS`, records a missing invocation and + re-wraps the result as an `UNMODELED_RETURN` placeholder. +- `SymbolicInstructionVisitor.visitGETVALUE_Object` — the `UNMODELED_RETURN && Util.isValueType(...)` + branch: models a whitelisted pure result as a UF; else recovers the registered shadow when the + return is a distinct immutable value (`Util.isImmutableValueType`, the receiver carried on the + placeholder, a `getFromHeap` hit that is not the receiver's shadow, concrete matches); else + concretizes via `ValueFactory.createObjectValue`. Non-value results fall through to normal registry + recovery. +- `SymbolicInstructionVisitor.visitGETVALUE_primitive` — the primitive mirror. + +**Invariants** +- An unmodeled value-typed return never aliases the receiver's formula (a `this`-return concretizes). +- A recovered value type is immutable, so its stored shadow still matches the observed value. +- Concrete recovery always adopts the JVM-observed value. + +### 4. Out-of-band change detection + +At a **primitive** `GETVALUE`, the executor compares the shadow value's `concrete` against what the +JVM actually produced. A mismatch means an *out-of-band change*: either a tracked object was mutated +inside unmodeled code, or the executor desynced internally. A configurable policy decides the +response. + +- `symbolic/shadow/ShadowDivergence.java` — the policy enum, two values: + - `CRASH` (default) — hard-fail via `SWATAssert`; catches executor desync bugs in dev/CI; this is + the historical behavior. + - `FLAG` — record a context-loss flag, adopt the observed concrete, and continue. Fully sound; + recommended for production/SV-COMP runs (no spurious crashes). +- `config/Config.java` — field `shadowDivergence`, default `CRASH`, read from the `shadow.divergence` + key. +- Decision site: the divergence branch in `SymbolicInstructionVisitor.visitGETVALUE_primitive`. Both + policies re-adopt the observed concrete afterward. + +**Invariants** +- Divergence detection currently covers only the **primitive** `GETVALUE` path. +- `FLAG` is sound: an adopted divergence downgrades a would-be safe verdict (via context loss, §7). + +### 5. De-intern + provenance — correct reference equality + +The reference-keyed registry (§1) needs distinct objects to have distinct identities. But the JVM +**shares** identities for interned strings, cached boxed wrappers, and `this`-returns, so two +logically-distinct shadow slots could collide on one shared object. To prevent that, value types +entering shadow space (string literals, boxed `valueOf`, and value-typed returns from +un-instrumented callees) are **de-interned**: replaced by a fresh copy with a unique identity. + +De-interning would then break `==`, so each fresh copy records the genuine original +("canonical root") it came from, and `==` is resolved by comparing roots — reproducing real Java's +`==` without relying on JVM interning. + +- `common/Provenance.java` — weak-keyed map from de-interned copy → canonical root; `record(copy, + canonical)` (stores the fully-resolved root, keeping chains depth-1); `root(x)` returns the + canonical or `x` itself. +- `common/UtilInstrumented.java` — `refEquals`: uses value equality + (`Provenance.root(a) == Provenance.root(b)`) when **either** operand is a de-interned value type + (the other operand's `root()` is itself), else plain `a == b`. +- `common/Util.java` — `shouldUseValueEquality`, `isDeInternedClass`, and the `deInternedClasses` + set: **String + Boolean/Byte/Short/Character/Integer/Long**. Float and Double are **not** + de-interned (they are uncached in real Java, so plain reference equality is already correct). + `isValueType` is broader (String + all `Number` + Boolean + Character) and drives §3's recovery, + not `==`. +- `instrument/nocache/NoCacheMethodAdapter.java` — the de-intern instrumentation: rewrites a String + literal to `new String(...)` + a provenance record; rewrites `.valueOf(prim)` to + `new (prim)` (`rewriteValueOf`); de-interns value-typed returns from un-instrumented + callees (`deInternReturn`). The `Boxed` enum is the single source of truth for the six cached + wrappers; `isDeInternSkippedOwner` excludes SWAT and sv-benchmarks intrinsics. +- `instrument/refequality/RefEqualityMethodAdapter.java` — rewrites `IF_ACMPEQ`/`IF_ACMPNE` bytecode + to call `UtilInstrumented.refEquals`. + +**Invariants** +- No two logically-distinct shadow slots share one interned/cached concrete key. +- `==` on de-interned value types matches real-Java `==`. +- Float/Double keep plain reference equality. + +**User-constructed value types compare correctly.** A `new String("x")` (or `new Integer(...)`) is +never given a provenance root — only literals, boxed `valueOf`, and returns from un-instrumented code +are — so it roots to itself and compares unequal to any other instance, matching the real JVM (e.g. +`new String("x") == new String("x")` is `false`, and `new String("x") == "x"` is `false`). + +### 6. Pure-function model — keeping precision through side-effect-free calls + +Some unmodeled library methods are pure: deterministic and side-effect-free. Rather than concretize +their result (and lose the symbolic dependency), SWAT models each such call as an **axiom-free +uninterpreted function** `pure_(inputs)`. An axiom-free UF asserts only "equal inputs ⇒ +equal outputs", which soundly over-approximates any deterministic function while preserving +relational facts (e.g. two calls on equal arguments return equal results). It fires only when at +least one input is symbolic. + +**Whitelist membership is a soundness precondition**: only genuinely pure, deterministic methods may +be listed — otherwise the UF's "equal inputs ⇒ equal outputs" assumption is false. + +- `symbolic/UFs/PureMethods.java` — `WHITELIST` (keyed `owner/name+descriptor`; String methods plus + an audited set from `java.lang`/`java.util`: Math, StrictMath, Character, Integer, Byte, Float, + Double, Objects). `isWhitelisted`; `ufName` builds `pure__[_]`. The + `pure_` prefix is the recognizer used by the precision-loss check (§7). +- `symbolic/UFs/PureFunctionUF.java` — per-thread UF registry; `apply(ufName, returnType, args)` + declares the UF lazily, caches it, and asserts the signature matches on reuse. Axiom-free by + construction. +- `symbolic/UFs/UFHandler.java` — `getPureFunctionUF` (lazy per-thread accessor). +- `symbolic/invoke/InvocationHandler.java` — `buildPureUF` constructs the result UF; the gate is + `containsSymbolicArgument && PureMethods.isWhitelisted(...)`. `pureUFReturnType` maps the return + descriptor to an SMT sort (String; boolean; bitvectors; floating point; else fall back to + concretize). A successful model also **suppresses the context-loss flag** (a modeled pure call + loses nothing). +- Recovery: `visitGETVALUE_Object`/`visitGETVALUE_primitive` install the carried UF as the recovered + value's formula. + +**Invariants** +- A whitelisted pure call preserves "equal inputs ⇒ equal outputs" instead of concretizing. +- The UF's return sort matches the recovered value's sort. +- Modeling requires all inputs to be value-typed with formulas; otherwise it falls back to + concretization. +- Only pure/deterministic methods may be whitelisted. + +--- + +## Lifecycle of a tracked value + +1. **Introduced** — a symbolic input (`@Symbolic` parameter) gets a free variable; a literal/boxed + constant is de-interned (§5) and given a concrete-only shadow; a normal computation produces a + shadow with a derived formula. +2. **Used** — arithmetic/logic combine formulas; a branch on a symbolic value records a path + constraint. +3. **Crosses a boundary** — an unmodeled call returns a placeholder (§3); at the next `GETVALUE` the + result is recovered as either a modeled UF (if whitelisted-pure, §6) or a concrete value + (otherwise, flagging context loss). +4. **Reference-compared** — `==` is resolved via provenance roots (§5). +5. **Re-synchronized** — at each primitive `GETVALUE`, the shadow concrete is checked against reality + (§4); a mismatch is crashed or flagged per policy. + +--- + +## Soundness model + +Two independent flags mark that the model may be incomplete; either one downgrades a **SAFE** verdict +to **UNKNOWN** (a VIOLATION is not downgraded — it is replay-witnessed). + +- **Context loss** — set when SWAT hits an unmodeled method with symbolic input it cannot model at + all (result discarded), or when an out-of-band divergence is adopted under `FLAG`. + - Set via `symbolic/trace/SymbolicTraceHandler.java` `recordSymbolicContextLoss` → + `SymbolicTrace.setSymbolicContextLoss`. Call sites: `InvocationHandler.invoke` and the `FLAG` + divergence branch. +- **Precision loss** — set when a branch constraint contains a symbol that is neither a designated + symbolic input, a recovery-named variable, nor a whitelisted `pure_` UF (i.e. a bespoke axiomatized + UF or an ungrounded variable that could make the constraint unsound). + - **Computed at trace-build time**, not recorded at runtime: `symbolic/trace/DTOBuilder.java` + `isPrecisionLoss(...)` walks each branch formula; there is deliberately no runtime recorder. +- Both flags ride on `symbolic/trace/dto/TraceDTO.java` and are emitted by `DTOBuilder`. +- Explorer side: `symbolic-explorer/data/BinaryExecutionTree/Tree.py` (`record_context_loss` / + `record_precision_loss`), populated by `data/Database.py` `add_trace`; the downgrade happens in + `driver/SVCompDriver.py` (`SAFE` + either flag ⇒ `UNKNOWN`). + +**Invariants** +- SAFE + (context loss OR precision loss) ⇒ UNKNOWN. Never a false SAFE from a knowingly-incomplete + model. +- A whitelisted `pure_` UF does not trigger precision loss; a bespoke axiomatized UF does. + +--- + +## Extending it & gotchas + +- **Adding a pure method to the whitelist.** Add `owner/name+descriptor` to + `PureMethods.WHITELIST` only after confirming the method is deterministic, side-effect-free, and + reads no ambient state (locale, time, environment, statics). A wrong entry is unsound. Today a bad + entry costs only precision (each run emits at most a single self-consistent fact); once cross-run + accumulation lands (see below) a bad entry can cause a **false SAFE**, so the bar is higher than it + looks. +- **Instrumenter frame-analysis fragility.** A category-2 parameter (a `double` or `long`) followed + by a reference parameter, and large mixed-type method bodies, trip an unrelated frame-analysis bug + in the instrumenter. Keep test targets small and single-typed; see the Javadocs in + `src/test/resources/targets/StringWhitelistTarget.java` and `WhitelistAuditAgentTarget.java`. +- **`@Symbolic` goes on a method parameter, not a local.** Annotating a local crashes the annotation + transformer when compiled without `-g`. +- **The legacy `de/uzl/its/value/**` test suite is broken** on an old formula API and fails en + masse. Scope test runs to the `symbolic.shadow` / `symbolic.processor` / `common` packages (see + the `swat-test` skill). + +--- + +## Not yet implemented (planned) + +Captured here so the plan survives; neither is in the code today. + +- **Escape-aware divergence policy.** A third divergence mode (beyond `CRASH`/`FLAG`, §4) that tells + a *legitimate* out-of-band mutation from a *genuine executor desync*. Intended mechanism: mark a + tracked object as **escaped** when it is passed as receiver/argument into an unmodeled call + (marking site in `InvocationHandler.invoke`); at a divergence, if the value came from an escaped + object → flag + adopt + continue, else → crash. The escaped bit reaches the primitive-`GETVALUE` + decision via a thread-local set in `visitGETFIELD` and **cleared at the start of every** + `visitGETVALUE_primitive` (else it leaks and masks real desync). A v1 would cover only the direct + field-read-of-escaped-object case (array/transitive reads still crash), so `FLAG` stays the + fully-sound production hatch. A refinement: a *pure* whitelisted call cannot mutate, so it should + not mark escape. + +- **Cross-run accumulation of observed pure-function facts.** The executor already emits, per run, + one **ground** observed pair `pure_(constant inputs) == constant output` for a whitelisted + String-returning pure call (`InvocationHandler.buildPureUF` builds it; `visitGETVALUE_Object` + asserts it). A single pair per run is sound on its own. What is missing is on the **explorer**: it + does not yet accumulate these pairs across runs and inject them at solve time. The three required + explorer changes **must land together**: (1) inject the accumulated per-testcase fact set at the + solve chokepoint; (2) a contradiction guard so a bad/nondeterministic entry cannot inject two + contradictory pairs; (3) an UNSAT backstop that downgrades SAFE→UNKNOWN if the accumulated `pure_` + facts alone are unsatisfiable. Injection without (2)+(3) could turn a bad whitelist entry into a + false SAFE. diff --git a/docs/test-architecture.md b/docs/test-architecture.md new file mode 100644 index 0000000..44be897 --- /dev/null +++ b/docs/test-architecture.md @@ -0,0 +1,199 @@ +# SWAT Test Architecture — Multi-Level Setup + +A reusable test architecture for the `symbolic-executor` module. It defines **four +abstraction levels**, the **fixtures/seams** each needs, and the **oracle rules** that keep +tests robust against representation churn. The heap and value-tracking tests are its primary +consumer; see [`heap-tracking.md`](heap-tracking.md) for that subsystem's design. + +## Why levels (the core insight) + +A behavioral case is *"a program + a property."* The same property can be checked at very +different altitudes, and **they are not interchangeable** — a bug lives in a specific contract, +and only a test at that contract's altitude actually exercises it. Picking the *lowest faithful* +altitude per case gives fast, non-flaky tests; picking too low makes the test circular, too high +makes it slow and coarse. + +``` +L0 value & shadow-structure unit in-JVM, no instrumentation fast, CI +L1 shadow-interpreter / processor in-JVM, synthetic instructions fast, CI +L2 real-instrumentation single-run forked JVM, real agent slower, opt-in CI +L3 end-to-end / verdict agent + Python explorer nightly / manual +``` + +## Oracle rules (apply at every level) + +The legacy `de/uzl/its/value/**` suite is brittle because it asserts on `.formula` via +sort-specific managers (`bvmgr.equal`), so it breaks en masse on representation changes. +**Never do that.** Assert only on: + +- `Value.concrete` (the observed runtime value); +- `Value.isSymbolic()`; +- symbolic **variable names** via `solverContext.getFormulaManager().extractVariables(f).keySet()`; +- boolean results of `IF_ACMPEQ` / `IF_ACMPNE` / `equals`; +- soundness **flags** (`symbolicContextLoss`, `symbolicPrecisionLoss`); +- `Frame.operandStack` / `locals` / `ret` contents; +- structured `TraceDTO` fields (L2/L3); +- for SMT/UF agreement only: feed the formula to a real `ProverEnvironment` and assert + **SAT/UNSAT agreement** with the concrete result — never inspect the formula's sort. + +**Expected-red mechanism (Spock `@PendingFeature`).** This Spock version (2.2-M1-groovy-4.0) has +**no `spock.lang.Tag`**. Mark each red case +`@PendingFeature(reason = " not yet implemented; …")`: the feature runs and asserts the +*desired* behavior, is reported as **pending (skipped), not a failure** while red — and **forces a +build failure the moment it starts passing** (the unambiguous "fix landed, remove the annotation" +signal). The test level is conveyed by the package and class name. + +**An expected-red test MUST fail on a specific assertion** (e.g. "result vars must not contain +`S_x`"), never on a setup exception — otherwise `@PendingFeature` would mask infra breakage as +"pending". Enforce this with the **precondition-first / guard-feature convention**: assert +currently-true preconditions first (or as a *separate non-pending* feature, e.g. "distinct objects +compare unequal"), so an infra break surfaces as a real failure while the pending feature isolates +only the not-yet-implemented behavior. + +--- + +## L0 — Value & Shadow-Structure Unit + +**Scope.** `Value` subclasses (`StringValue`, `IntValue`, boxed wrappers, `ObjectValue`, +arrays) and the shadow data structures (`JVMHeap`, `Frame`, `ShadowContext`). No instrumentation, +no instruction stream — construct objects and call methods directly. + +**Tests well.** Value semantics: `IF_ACMPEQ`/`equals`, `invokeMethod`/`invokeInit` (e.g. the +`new String(String)` copy ctor, `StringValue.java:217`), `MAKE_SYMBOLIC`, heap `put/get` and key +behavior, UF-defining-constraint SMT agreement. For example, construct two distinct objects with a +colliding identity hash and assert they compare unequal, and assert that a single identity yields a +single wrapper. + +**Driver.** A shared `BaseValueSpec`: +`ThreadHandler.init()` → `addThreadContext(currentThread().id, "Test-Thread", -2)` → +`getSolverContext` → expose `fmgr/bmgr/smgr/...` and a fresh `ProverEnvironment`; `cleanup` +closes the prover/context and removes the thread context. For UF agreement, pull +UF-defining constraints from the trace +(`ThreadHandler.getSymbolicTraceHandler(id).getConstraints()`) into the prover — see +`StringValueTest.addUFConstraintsFromTrace`. + +**Oracle.** Per the rules above. Exemplar in repo: `StringValueTest.groovy`. + +--- + +## L1 — Shadow-Interpreter / Processor (the workhorse) + +**Scope.** `SymbolicInstructionProcessor.processInstruction()` driven over a constructed +`ShadowContext`. Feed a synthetic `Instruction` sequence; assert on how the operand stack / +locals / frame / heap / trace evolve. + +**Tests well.** The reaction of the shadow interpreter to instruction sequences: lifting a +symbolic input, the **invoke → recovery** path (`INVOKEVIRTUAL`(unmodeled) → `INVOKEMETHOD_END` +→ `GETVALUE_Object`), branches, field/array ops. + +**Driver.** `BaseSymbolicInstructionProcessorSpec` provides `setupTestContext` (unique method +names per test — required), the `push*Operand` helpers, and `executeLiftInsnSeq` +(introduce a symbolic input). The **boundary-recovery fixture** has the highest leverage and is +shared by all recovery cases: + +``` +executeBoundaryRecovery(receiver, owner, name, desc, concreteResult, resultAddress) + // 1. register `receiver` on the heap at its address (stack.putToHeap) + // 2. push receiver as the invoke operand + // 3. process: INVOKEVIRTUAL(owner,name,desc) ; INVOKEMETHOD_END ; + // GETVALUE_Object(resultAddress, concreteResult, i) + // 4. return { recovered: peekOperand, contextLoss, heap snapshot } +``` + +This drives the *real* bug path: an unmodeled invoke returns `PlaceHolder` +(`InvocationHandler.invoke`, `StringValue.invokeToLowerCase:1126`), `INVOKEMETHOD_END` pushes it +(`SymbolicInstructionVisitor:3406`), and `visitGETVALUE_Object` (`:1265`) recovers from the +identity-keyed heap — the aliasing defect. + +**Honest caveat.** L1 *fabricates* the instruction stream, including the +`resultAddress == receiver.address` collision that a real `this`-return produces. So an L1 +recovery test pins the **interpreter's recovery logic**, not the instrumentation→processor +contract, and bakes in an assumption about the emitted sequence. Therefore: pair a flagship +recovery case with an **L2 anchor** that gets the collision from the real JVM. + +**Seams required (see Cross-cutting).** Heap-inspection view on `ShadowContext`; flag getters on +`SymbolicTraceHandler`. + +**Oracle.** L0 rules + `Frame`/heap-view/flags. Exemplars: `InternalInvocationSpec`, +`INVOKEVIRTUALSpec`, `IADDSpec`. + +--- + +## L2 — Real-Instrumentation / Single-Run (forked JVM, structured TraceDTO) + +**The faithful altitude for recovery/identity bugs.** The real ASM agent runs a real tiny target +program; identity hashes, the `this`-return, the GETVALUE sequence, and the soundness flags all +come from the real JVM + instrumenter — nothing is hand-fabricated. + +**Key enabler.** `solver.mode=PRINT` makes `Intrinsics.terminate()` do +`System.out.println(getTraceDTO())` (`Intrinsics.java`, terminate() PRINT branch) — the full +`TraceDTO` JSON on stdout, **no Python explorer needed**. `LOCAL` mode (default) instead solves +in-JVM with Z3 via `LocalSolver.solve()`. `SolverMode = {LOCAL, HTTP, PRINT, NONE}`. + +**Driver — `AgentRunFixture`:** + +1. Build the agent jar first: `./gradlew :symbolic-executor:copyJar` + → `symbolic-executor/lib/symbolic-executor.jar` (build with `copyJar`, never `spotlessApply`). +2. Target programs live in `src/test/resources/targets/.java` (tiny, hand-written). + Designate symbolic inputs with `Verifier.nondetInt(long id)` / `nondetString(id)` / … + (SV_COMP transformer) — e.g. `String s = Verifier.nondetString(0);`. +3. Fork: `java -javaagent:symbolic-executor.jar -Dsolver.mode=PRINT + -Dconfig.path= -Dswat.input.= -cp
` + with a minimal `test.cfg` (`instrumentation.transformer=SV_COMP`, `solver.mode=PRINT`, + `exitOnError=false`). `swat.input.*` pins the concrete path so the run is deterministic. +4. Capture stdout, parse the TraceDTO JSON (Jackson) into a typed + `TraceObservation { inputs[], branches[], ufs[], symbolicContextLoss, + symbolicPrecisionLoss }`. + +**Why forked, not in-process:** the agent attaches at premain and `ThreadHandler`/`Config` are +process-global singletons set at startup; resetting them mid-JVM is hacky and fragile. A forked +JVM gives clean isolation per case. + +**Oracle (structured, no log-scrape).** TraceDTO fields + which input variables appear in branch +constraints. For example, plant `if (r.equals("abc"))` on an unmodeled `toLowerCase` result and +assert `symbolicContextLoss == true` **and** that the branch over `r` does **not** reference the +symbolic input variable (so no confident wrong SAFE can be derived). + +**CI.** Slower + needs the jar; gate behind a separate Gradle task (`agentTest`), not the default +`test`. + +--- + +## L3 — End-to-End / Verdict (explorer in the loop) + +**Scope.** Full pipeline: agent (`HTTP` mode) + Python explorer + iterative path exploration + +final SV-COMP verdict, including the downgrade rules (SAFE+contextLoss→UNKNOWN, etc.). Tests the +*verdict*, not just the trace. + +**Driver.** The sv-comp driver / `targets/` harness. Structured per-testcase observation +(`{verdict, contextLoss}`) becomes clean once the consolidated `stats.json` work lands — until +then it is STDOUT/log scraping (`[VERDICT ]`). + +**CI.** Not gated; nightly / manual regression lane. + +--- + +## Cross-cutting infrastructure + +The durable seams that back the levels, reused well beyond any single subsystem: + +1. **Flag-observation seam.** Getters on `SymbolicTraceHandler`: + `isSymbolicContextLoss()`, `isReferenceSemanticChange()` (the `SymbolicTrace` fields are + package-private; `processor`-package specs can't see them). Used by L1 + every flag + assertion. +2. **Heap/registry inspection view.** A small read-only view on `ShadowContext` (every spec + already gets it via `visitor.getStack()`, so no new wiring): + `int heapSize()`, `int heapDistinctIdentities()`, `Value heapLookup(long id)`, + `Collection> heapEntries()`. Assertions phrased against this view don't change as + the backing structure evolves; they flip red→green as the behavior is fixed (e.g. two distinct + objects with a colliding hash → `heapDistinctIdentities()` should be 2). Chosen over raw + `JVMHeap` getters, which would couple tests to a structure under active change, and over + future-API-only tests, which wouldn't compile and so give no running red signal. +3. **L1 boundary-recovery fixture** (see L1). Highest leverage; shared by all recovery cases. +4. **L0 `BaseValueSpec`** — a shared prover + solver context for all value-semantics specs. +5. **L2 `AgentRunFixture` + `TraceObservation`** (see L2). Forked-JVM + PRINT-mode + JSON parse. + +## Framework + +**Spock for L0/L1/L2-harness** (the suite is already Spock; `where:` tables fit tabular case sets +well). L3 stays in the Python sv-comp harness. diff --git a/settings.gradle b/settings.gradle index defcd23..786fe1c 100644 --- a/settings.gradle +++ b/settings.gradle @@ -74,6 +74,7 @@ dependencyResolutionManagement { library('logback-core', 'ch.qos.logback:logback-core:1.5.3') library('slf4j-api', 'org.slf4j:slf4j-api:2.0.13') library('cfg-extractor', 'de.uzl.its:cfg-extractor:1.0-SNAPSHOT') + library('guava', 'com.google.guava:guava:33.4.8-jre') bundle('asm', ['asm-core', 'asm-commons', 'asm-util', 'asm-tree']) bundle('logging', ['logback-core', 'logback-classic', 'slf4j-api']) diff --git a/symbolic-executor/build.gradle b/symbolic-executor/build.gradle index 0b7932b..e7f0f18 100644 --- a/symbolic-executor/build.gradle +++ b/symbolic-executor/build.gradle @@ -38,6 +38,7 @@ dependencies { implementation libs.bundles.asm implementation libs.jackson.databind implementation libs.java.smt + implementation libs.guava implementation rootProject.fileTree(dir: 'libs/java-library-path', include: ['*.jar']) // loads com.microsoft.z3 and java-smt @@ -50,6 +51,7 @@ test { systemProperty "java.library.path", "../libs/java-library-path" // Surface SWAT errors as exceptions instead of halting the test JVM systemProperty "exitOnError", "false" + exclude '**/*AgentSpec*' testLogging { // Show events for passed, skipped, and failed tests @@ -58,6 +60,20 @@ test { showStandardStreams = true } } +tasks.register('agentTest', Test) { + description = 'Level-2 forked-agent tests (real instrumentation). Not part of `test`.' + group = 'verification' + useJUnitPlatform() + testClassesDirs = sourceSets.test.output.classesDirs + classpath = sourceSets.test.runtimeClasspath + filter { includeTestsMatching '*AgentSpec' } + dependsOn 'copyJar' + + testLogging { + events "passed", "failed", "skipped" + showStandardStreams = true + } +} jar { // duplicatesStrategy = DuplicatesStrategy.EXCLUDE diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Provenance.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Provenance.java new file mode 100644 index 0000000..4b9f905 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Provenance.java @@ -0,0 +1,63 @@ +package de.uzl.its.swat.common; + +import com.google.common.collect.MapMaker; + +import java.util.Map; + +/** + * Provenance tracking for reference equality of de-interned value types. + * + *

De-interning gives every produced value type a fresh identity so the reference-keyed shadow + * heap stays sound. That fresh identity diverges from the real JVM identity, which would break + * reference equality ({@code ==}). To model {@code ==} exactly, each de-interned copy records the + * genuine original ("canonical") object it was made from, and {@code UtilInstrumented.refEquals} + * compares {@link #root}s instead of the de-interned objects: two copies of the same interned literal + * (or the same cached box, or the same returned object) share one canonical, so they compare equal, + * exactly as the un-transformed program would. + * + *

The map is identity-keyed and weak-keyed (an entry lives only while its de-interned copy is + * reachable). Values are held strongly on purpose: a copy's canonical must stay alive and stable for + * as long as the copy can be {@code ==}-compared, otherwise {@link #root} could strand a live alias and + * flip a genuine {@code ==} to false. Entries whose copy has been collected are reclaimed as the map + * is subsequently written (guava weak-key maps clear stale entries on later writes, not eagerly under + * GC); because the de-intern sites that write this map are hot, the retained set stays bounded during + * an active run. Same primitive and reclamation behavior as the shadow heap ({@code JVMHeap}). + * + *

Chains are collapsed at insertion ({@link #record} stores the fully-resolved root), so {@link + * #root} is always a single lookup and never depends on an intermediate link surviving GC. + * + *

This class is excluded from instrumentation and listed in {@code IGNORED_INVOCATIONS}, so the + * symbolic executor never models or context-loss-flags its calls; {@link #root} returns a concrete + * object whose only use is the (concrete) reference comparison in {@code refEquals}. + */ +public final class Provenance { + + private Provenance() {} + + /** de-interned copy (weak, identity key) -> its canonical/original (strong value). */ + private static final Map ROOTS = new MapMaker().weakKeys().makeMap(); + + /** + * Record that {@code copy} (a freshly de-interned object) originates from {@code canonical} (the + * genuine pre-de-intern object). Stores the fully-resolved root of {@code canonical} so chains stay + * depth-1. No-op for nulls or a self-mapping. + */ + public static void record(Object copy, Object canonical) { + if (copy == null || canonical == null || copy == canonical) { + return; + } + ROOTS.put(copy, root(canonical)); + } + + /** + * The original identity {@code x} stands for: the recorded canonical, or {@code x} itself when + * {@code x} was never recorded (e.g. a non-de-interned object) or its entry has been collected. + */ + public static Object root(Object x) { + if (x == null) { + return null; + } + Object r = ROOTS.get(x); + return r != null ? r : x; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java index 4c2e490..74e07e3 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java @@ -235,12 +235,11 @@ public static Class[] getInterfaces(Class clazz) private static void checkClassName(String className) { if (className.startsWith("[")) { - return; // array class, skip check for now + return; // array class; the descriptor check does not apply } SWATAssert.check( - !className.contains(";") && !className.contains("(") && !className.contains(")") - && !className.startsWith("L"), - "Class name '{}' should not contain ';' or brackets", className); + !className.contains(";") && !className.contains("(") && !className.contains(")"), + "Class name '{}' should not be a type descriptor (contains ';' or brackets)", className); } /** @@ -429,4 +428,54 @@ private static boolean isDeInternedClass(Class clazz) { return deInternedClasses.contains(clazz.getName()); } + /** + * Whether {@code o}'s runtime class is one that is de-interned: String and the cached boxed wrappers + * (Boolean/Byte/Short/Character/Integer/Long), but NOT the uncached Float/Double (which use + * reference equality). Used by recovery to limit the "skip registering pure constants" policy to + * exactly the de-interned value types, leaving mutable objects and Float/Double always registered. + */ + public static boolean isDeInternedClass(Object o) { + return o != null && isDeInternedClass(o.getClass()); + } + + /** + * Whether a concrete object is an immutable value type (String / boxed primitive). + * Used by recovery to concretize an unmodeled value-returning method's result instead of + * identity-recovering it. Independent of {@link #deInternedClasses} (the de-intern / + * reference-equality concern, which omits the uncached Float/Double): this covers String and all + * eight boxed wrappers ({@link Number} = Byte/Short/Integer/Long/Float/Double, plus Boolean and + * Character). + * + * @param o the concrete object (may be null) + * @return true if {@code o} is a value type + */ + public static boolean isValueType(Object o) { + return o instanceof String + || o instanceof Number + || o instanceof Boolean + || o instanceof Character; + } + + /** + * The closed set of genuinely-immutable value types whose stored shadow recovery may safely + * reuse: String and the eight boxed primitive wrappers. Narrower than {@link #isValueType}, which + * admits mutable {@link Number} subtypes ({@code AtomicInteger}, {@code LongAdder}, ...) — reusing + * a stored shadow for those could be stale. An immutable value cannot have drifted since it was + * registered, so reusing its shadow is sound. + * + * @param o the concrete object (may be null) + * @return true if {@code o} is a String or a boxed primitive wrapper + */ + public static boolean isImmutableValueType(Object o) { + return o instanceof String + || o instanceof Integer + || o instanceof Long + || o instanceof Short + || o instanceof Byte + || o instanceof Character + || o instanceof Boolean + || o instanceof Float + || o instanceof Double; + } + } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java index e288bec..3f18549 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/UtilInstrumented.java @@ -5,7 +5,6 @@ import java.lang.reflect.InvocationTargetException; import java.lang.reflect.Method; -import java.util.Objects; @SuppressWarnings("unused") public class UtilInstrumented { @@ -24,13 +23,17 @@ public static void liftClass(Object param, String paramCnameDot, String methodNa } } /** - * Conditionally uses Objects.equals() for de-interned classes, - * otherwise uses reference equality. + * Models reference equality ({@code ==}) for de-interned value types by comparing the ORIGINAL + * identities. De-interning gave {@code a}/{@code b} fresh identities that diverge from the + * real JVM; comparing {@link Provenance#root}s (the canonical object each was de-interned from) + * reproduces the un-transformed program's {@code ==}: two copies of the same interned literal / + * cached box / returned object share one canonical and so compare equal. Non-de-interned classes + * keep plain reference equality. */ @SuppressWarnings("unused") public static boolean refEquals(Object a, Object b) { if (Util.shouldUseValueEquality(a, b)) { - return Objects.equals(a, b); + return Provenance.root(a) == Provenance.root(b); } return a == b; } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/config/Config.java b/symbolic-executor/src/main/java/de/uzl/its/swat/config/Config.java index 2f9a014..25796d7 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/config/Config.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/config/Config.java @@ -6,6 +6,7 @@ import de.uzl.its.swat.coverage.CoverageType; import de.uzl.its.swat.instrument.TransformerType; import de.uzl.its.swat.solver.SolverMode; +import de.uzl.its.swat.symbolic.shadow.ShadowDivergence; import java.io.FileInputStream; import java.io.IOException; import java.util.*; @@ -184,6 +185,10 @@ public class Config { @Getter private SolverMode solverMode; private static final SolverMode DEFAULT_SOLVER_MODE = SolverMode.LOCAL; + /** How to handle a shadow/concrete divergence at a GETVALUE sync point (out-of-band change). */ + @Getter @Setter private ShadowDivergence shadowDivergence; + private static final ShadowDivergence DEFAULT_SHADOW_DIVERGENCE = ShadowDivergence.CRASH; + // ------------------------------------ // General options // ------------------------------------ @@ -431,6 +436,7 @@ private void readProperties() { // Solver options // ------------------------------------ solverMode = SolverMode.valueOf(readString("solver.mode", DEFAULT_SOLVER_MODE.toString())); + shadowDivergence = ShadowDivergence.valueOf(readString("shadow.divergence", DEFAULT_SHADOW_DIVERGENCE.toString())); // ------------------------------------ // SV-Comp options diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java index aba06b8..c682573 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.instrument.nocache; +import de.uzl.its.swat.common.Util; import de.uzl.its.swat.config.Config; import org.objectweb.asm.Label; import org.objectweb.asm.MethodVisitor; @@ -23,13 +24,73 @@ public void visitLdcInsn(Object value) { mv.visitLdcInsn(value); mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/String", "", "(Ljava/lang/String;)V", false); - //NoCacheTransformer.getPrintBox() - // .addMsg("Replacing LDC with new String"); + // Record provenance (de-interned copy -> the interned literal canonical). The interned + // literal is a compile-time constant, so re-LDC'ing it pushes the SAME canonical object + // that every other occurrence of this literal shares; never null (no guard needed). + mv.visitInsn(Opcodes.DUP); + mv.visitLdcInsn(value); + emitProvenanceRecord(); } else { mv.visitLdcInsn(value); } } + /** + * Emit {@code Provenance.record(copy, canonical)} consuming the top two stack entries + * {@code [..., copy, canonical]} and leaving {@code [...]}. Callers DUP the copy first so the copy + * survives. Emitted via the raw delegate so it is not re-processed by this adapter. + */ + private void emitProvenanceRecord() { + mv.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/common/Provenance", "record", + "(Ljava/lang/Object;Ljava/lang/Object;)V", false); + } + + /** + * After a de-interned boxed copy is on top of the stack and its primitive is in {@code primLocal}, + * record provenance to the box's REAL cached canonical. The valueOf rewrite replaced the original + * call before it ran, so the canonical is not on the stack - we materialize it by calling the + * genuine {@code valueOf} via the raw delegate (so it is NOT itself re-rewritten). Without this, + * {@code root} of two cached boxes (e.g. valueOf(100)) would be self -> distinct -> {@code ==} + * false, regressing real Java (cache hit -> true). Stack: {@code [copy] -> [copy]}. + */ + private void recordBoxedProvenance(String owner, String valueOfDescriptor, int primLoadOpcode, + int primLocal) { + mv.visitInsn(Opcodes.DUP); + mv.visitVarInsn(primLoadOpcode, primLocal); + mv.visitMethodInsn(Opcodes.INVOKESTATIC, owner, "valueOf", valueOfDescriptor, false); + emitProvenanceRecord(); + } + + /** + * Consume the primitive on top of the stack and leave a fresh, distinctly-identified boxed instance + * in its place ({@code [prim] -> [new (prim)]}). The primitive is parked in a fresh local + * (returned) because it is needed again after the {@code NEW} - both to feed the constructor and, + * for {@link #rewriteValueOf}, to materialize the cached canonical. The local is required for the + * category-2 {@code long}. Shared by the {@code valueOf} rewrite and {@link #deInternReturn}. + */ + private int reboxFreshFromPrimitive(Boxed boxed) { + int primLocal = newLocal(boxed.primType); + mv.visitVarInsn(boxed.primType.getOpcode(Opcodes.ISTORE), primLocal); + mv.visitTypeInsn(Opcodes.NEW, boxed.owner); + mv.visitInsn(Opcodes.DUP); + mv.visitVarInsn(boxed.primType.getOpcode(Opcodes.ILOAD), primLocal); + mv.visitMethodInsn(Opcodes.INVOKESPECIAL, boxed.owner, "", boxed.ctorDescriptor(), false); + return primLocal; + } + + /** + * Replace {@code .valueOf(prim)} (the primitive is on top of the stack) with + * {@code new (prim)}, giving the produced box a distinct identity, and record provenance to + * the real cached canonical so reference {@code ==} on cache hits still models real Java. + */ + private void rewriteValueOf(Boxed boxed) { + int primLocal = reboxFreshFromPrimitive(boxed); + recordBoxedProvenance(boxed.owner, boxed.valueOfDescriptor(), + boxed.primType.getOpcode(Opcodes.ILOAD), primLocal); + NoCacheTransformer.getPrintBox() + .addMsg("Replacing " + boxed.simpleName() + ".valueOf with new " + boxed.simpleName()); + } + // Intercept method calls to disable interning and caching. @Override public void visitMethodInsn(int opcode, String owner, String name, String descriptor, boolean isInterface) { @@ -43,98 +104,159 @@ public void visitMethodInsn(int opcode, String owner, String name, String descri .addMsg("Removing String.intern() call"); return; } - // Replace Integer.valueOf(int) with new Integer(int) - if (opcode == Opcodes.INVOKESTATIC && - owner.equals("java/lang/Integer") && - name.equals("valueOf") && - descriptor.equals("(I)Ljava/lang/Integer;")) { - int localVarIndex = newLocal(Type.INT_TYPE); - mv.visitVarInsn(Opcodes.ISTORE, localVarIndex); - mv.visitTypeInsn(Opcodes.NEW, "java/lang/Integer"); - mv.visitInsn(Opcodes.DUP); - mv.visitVarInsn(Opcodes.ILOAD, localVarIndex); - mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Integer", "", "(I)V", false); - NoCacheTransformer.getPrintBox() - .addMsg("Replacing Integer.valueOf with new Integer"); - return; + // Replace .valueOf(prim) with new (prim) to defeat the wrapper cache (see Boxed). + if (opcode == Opcodes.INVOKESTATIC && name.equals("valueOf")) { + Boxed boxed = Boxed.forValueOf(owner, descriptor); + if (boxed != null) { + rewriteValueOf(boxed); + return; + } } - // Replace Long.valueOf(long) with new Long(long) - if (opcode == Opcodes.INVOKESTATIC && - owner.equals("java/lang/Long") && - name.equals("valueOf") && - descriptor.equals("(J)Ljava/lang/Long;")) { - int localVarIndex = newLocal(Type.LONG_TYPE); - mv.visitVarInsn(Opcodes.LSTORE, localVarIndex); - mv.visitTypeInsn(Opcodes.NEW, "java/lang/Long"); - mv.visitInsn(Opcodes.DUP); - mv.visitVarInsn(Opcodes.LLOAD, localVarIndex); - mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Long", "", "(J)V", false); - NoCacheTransformer.getPrintBox() - .addMsg("Replacing Long.valueOf with new Long"); - return; + // For all other method calls, proceed normally. + mv.visitMethodInsn(opcode, owner, name, descriptor, isInterface); + + // Output-boundary de-interning: de-intern a value-typed return from an un-instrumented + // callee - the boundary where interned/shared values (literals, constants, this-returns, + // cached boxes) enter shadow space. A fresh copy gives the produced value a distinct identity, + // so the reference-keyed heap stays sound for value types. Skip the SWAT / sv-benchmarks + // intrinsics (the symbolic-input designation / witness seam). Gated on the de-intern switch. + if (Config.instance().isUseStringInterning() + && !Util.shouldInstrument(owner) + && !isDeInternSkippedOwner(owner)) { + deInternReturn(Type.getReturnType(descriptor)); } - // Replace Short.valueOf(short) with new Short(short) - if (opcode == Opcodes.INVOKESTATIC && - owner.equals("java/lang/Short") && - name.equals("valueOf") && - descriptor.equals("(S)Ljava/lang/Short;")) { - int localVarIndex = newLocal(Type.INT_TYPE); - mv.visitVarInsn(Opcodes.ISTORE, localVarIndex); - mv.visitTypeInsn(Opcodes.NEW, "java/lang/Short"); + } + + /** + * Emit a fresh, distinctly-identified copy of the value just returned (now on the stack), if its + * type is an interning value type. Null-guarded - the wrap would NPE on a null return. String and + * the six cached boxed wrappers are covered; Float/Double are intentionally excluded (uncached, + * reference equality - see {@link Util#isDeInternedClass(Object)}). + */ + private void deInternReturn(Type returnType) { + if ("Ljava/lang/String;".equals(returnType.getDescriptor())) { + // String has a copy constructor. Keep the original in a local so we can both build + // new String(original) AND record provenance (copy -> original) afterward. + Label done = new Label(); mv.visitInsn(Opcodes.DUP); - mv.visitVarInsn(Opcodes.ILOAD, localVarIndex); - mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Short", "", "(S)V", false); - NoCacheTransformer.getPrintBox() - .addMsg("Replacing Short.valueOf with new Short"); - return; - } - // Replace Byte.valueOf(byte) with new Byte(byte) - if (opcode == Opcodes.INVOKESTATIC && - owner.equals("java/lang/Byte") && - name.equals("valueOf") && - descriptor.equals("(B)Ljava/lang/Byte;")) { - int localVarIndex = newLocal(Type.INT_TYPE); - mv.visitVarInsn(Opcodes.ISTORE, localVarIndex); - mv.visitTypeInsn(Opcodes.NEW, "java/lang/Byte"); + mv.visitJumpInsn(Opcodes.IFNULL, done); // null result: leave it, skip the wrap + int origLocal = newLocal(Type.getObjectType("java/lang/String")); + mv.visitVarInsn(Opcodes.ASTORE, origLocal); + mv.visitTypeInsn(Opcodes.NEW, "java/lang/String"); mv.visitInsn(Opcodes.DUP); - mv.visitVarInsn(Opcodes.ILOAD, localVarIndex); - mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Byte", "", "(B)V", false); - NoCacheTransformer.getPrintBox() - .addMsg("Replacing Byte.valueOf with new Byte"); - return; - } - // Replace Character.valueOf(char) with new Character(char) - if (opcode == Opcodes.INVOKESTATIC && - owner.equals("java/lang/Character") && - name.equals("valueOf") && - descriptor.equals("(C)Ljava/lang/Character;")) { - int localVarIndex = newLocal(Type.INT_TYPE); - mv.visitVarInsn(Opcodes.ISTORE, localVarIndex); - mv.visitTypeInsn(Opcodes.NEW, "java/lang/Character"); + mv.visitVarInsn(Opcodes.ALOAD, origLocal); + mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/String", "", + "(Ljava/lang/String;)V", false); // [copy] mv.visitInsn(Opcodes.DUP); - mv.visitVarInsn(Opcodes.ILOAD, localVarIndex); - mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Character", "", "(C)V", false); - NoCacheTransformer.getPrintBox() - .addMsg("Replacing Character.valueOf with new Character"); + mv.visitVarInsn(Opcodes.ALOAD, origLocal); + emitProvenanceRecord(); // record(copy, original) -> [copy] + mv.visitLabel(done); return; } - // Replace Boolean.valueOf(boolean) with new Boolean(boolean) - if (opcode == Opcodes.INVOKESTATIC && - owner.equals("java/lang/Boolean") && - name.equals("valueOf") && - descriptor.equals("(Z)Ljava/lang/Boolean;")) { - int localVarIndex = newLocal(Type.INT_TYPE); - mv.visitVarInsn(Opcodes.ISTORE, localVarIndex); - mv.visitTypeInsn(Opcodes.NEW, "java/lang/Boolean"); + Boxed boxed = Boxed.forReturnDescriptor(returnType.getDescriptor()); + if (boxed != null) { + // Boxed wrappers have no copy constructor: keep the original boxed in a local, unbox it to + // the primitive, rebox into a fresh instance, then record provenance (copy -> original). + Label done = new Label(); mv.visitInsn(Opcodes.DUP); - mv.visitVarInsn(Opcodes.ILOAD, localVarIndex); - mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Boolean", "", "(Z)V", false); - NoCacheTransformer.getPrintBox() - .addMsg("Replacing Boolean.valueOf with new Boolean"); - return; + mv.visitJumpInsn(Opcodes.IFNULL, done); // null result: leave it, skip the wrap + int origLocal = newLocal(Type.getObjectType(boxed.owner)); + mv.visitVarInsn(Opcodes.ASTORE, origLocal); + mv.visitVarInsn(Opcodes.ALOAD, origLocal); + mv.visitMethodInsn(Opcodes.INVOKEVIRTUAL, boxed.owner, boxed.unboxMethod, + boxed.unboxDescriptor(), false); // [prim] + reboxFreshFromPrimitive(boxed); // [copy] + mv.visitInsn(Opcodes.DUP); + mv.visitVarInsn(Opcodes.ALOAD, origLocal); + emitProvenanceRecord(); // record(copy, original) -> [copy] + mv.visitLabel(done); } - // For all other method calls, proceed normally. - mv.visitMethodInsn(opcode, owner, name, descriptor, isInterface); + } + + /** + * The six cached boxed wrappers that are de-interned. Each carries the JVM primitive type descriptor + * ({@code primDescriptor}, e.g. {@code "I"}, {@code "J"}, {@code "S"}) from which all method + * descriptors are derived, so this enum is the single source of truth for both the {@code valueOf} + * rewrite and the return de-intern. {@code primType} is the stack type used for the load/store + * opcodes and {@code newLocal}: {@code short}/{@code byte}/{@code char} live on the operand stack + * as {@code int}, hence {@link Type#INT_TYPE} for all of them and {@link Type#LONG_TYPE} only for + * {@code long}. + */ + private enum Boxed { + INTEGER("java/lang/Integer", "intValue", "I", Type.INT_TYPE), + LONG("java/lang/Long", "longValue", "J", Type.LONG_TYPE), + SHORT("java/lang/Short", "shortValue", "S", Type.INT_TYPE), + BYTE("java/lang/Byte", "byteValue", "B", Type.INT_TYPE), + CHARACTER("java/lang/Character", "charValue", "C", Type.INT_TYPE), + BOOLEAN("java/lang/Boolean", "booleanValue", "Z", Type.INT_TYPE); + + final String owner; + final String unboxMethod; + final String primDescriptor; + final Type primType; + + Boxed(String owner, String unboxMethod, String primDescriptor, Type primType) { + this.owner = owner; + this.unboxMethod = unboxMethod; + this.primDescriptor = primDescriptor; + this.primType = primType; + } + + /** The wrapper's own type descriptor, e.g. {@code Ljava/lang/Integer;}. */ + String boxedDescriptor() { + return "L" + owner + ";"; + } + + /** {@code valueOf} factory descriptor, e.g. {@code (I)Ljava/lang/Integer;}. */ + String valueOfDescriptor() { + return "(" + primDescriptor + ")" + boxedDescriptor(); + } + + /** Primitive constructor descriptor, e.g. {@code (I)V}. */ + String ctorDescriptor() { + return "(" + primDescriptor + ")V"; + } + + /** Unbox accessor descriptor, e.g. {@code ()I} for {@code intValue}. */ + String unboxDescriptor() { + return "()" + primDescriptor; + } + + /** Simple class name for log messages, e.g. {@code Integer}. */ + String simpleName() { + return owner.substring(owner.lastIndexOf('/') + 1); + } + + /** The wrapper whose {@code valueOf(prim)} this call site invokes, or {@code null}. */ + static Boxed forValueOf(String owner, String descriptor) { + for (Boxed b : values()) { + if (b.owner.equals(owner) && b.valueOfDescriptor().equals(descriptor)) { + return b; + } + } + return null; + } + + /** The wrapper matching a value-typed return descriptor, or {@code null}. */ + static Boxed forReturnDescriptor(String descriptor) { + for (Boxed b : values()) { + if (b.boxedDescriptor().equals(descriptor)) { + return b; + } + } + return null; + } + } + + /** + * Owners whose value-typed returns must NOT be de-interned even though they are un-instrumented: + * the symbolic-input designation / witness intrinsics. {@code shouldInstrument} already returns + * false for these (they're excluded), so this explicit check is the load-bearing exclusion, not a + * delegation to it. + */ + private static boolean isDeInternSkippedOwner(String owner) { + return owner.startsWith("de/uzl/its/swat/") + || owner.equals("org/sosy_lab/sv_benchmarks/Verifier"); } /* diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index 7ab9a02..6469ab4 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java @@ -6,8 +6,10 @@ import ch.qos.logback.classic.Logger; import de.uzl.its.swat.common.ErrorHandler; +import de.uzl.its.swat.common.Util; import de.uzl.its.swat.common.exceptions.*; import de.uzl.its.swat.common.logging.GlobalLogger; +import de.uzl.its.swat.config.Config; import de.uzl.its.swat.coverage.BranchCoverage; import de.uzl.its.swat.instrument.GlobalStateForInstrumentation; import de.uzl.its.swat.instrument.Intrinsics; @@ -19,6 +21,7 @@ import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor; import de.uzl.its.swat.symbolic.shadow.Frame; import de.uzl.its.swat.symbolic.shadow.ShadowContext; +import de.uzl.its.swat.symbolic.shadow.ShadowDivergence; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.PlaceHolder; import de.uzl.its.swat.symbolic.value.Value; @@ -38,6 +41,7 @@ import lombok.Getter; import org.objectweb.asm.Type; import org.sosy_lab.java_smt.api.*; +import de.uzl.its.swat.symbolic.UFs.PureFunctionUF; public class SymbolicInstructionVisitor implements IVisitor { // The stack of stack frames (method stacks) @@ -1266,8 +1270,54 @@ public void visitGETVALUE_Object(GETVALUE_Object inst) throws SymbolicInstruc // remove the placeholder value stack.popOperand(); + + // The result of an unmodeled value-returning method must NOT be identity-recovered + // (that would re-bind the receiver's symbolic value, e.g. toLowerCase() returning + // `this`). Concretize the value type instead, and do NOT consult or mutate the heap, so + // the receiver's own entry (and its round-trip) is preserved. Context loss was already + // flagged in InvocationHandler. Non-value results fall through to registry recovery. + if (placeHolder.origin == PlaceHolder.ValueOrigin.UNMODELED_RETURN + && Util.isValueType(inst.val)) { + Logger shadowStateLogger = ThreadHandler.getShadowStateLogger(currentThread().getId()); + if (placeHolder.recoveredFormula != null && inst.val instanceof String s) { + // A whitelisted pure method - model the result as the carried generic UF + // over the inputs (concrete = observed). Preserves the relational fact + // (equal inputs => equal outputs) instead of concretizing. + SolverContext context = ThreadHandler.getSolverContext(currentThread().getId()); + tmp = new StringValue(context, s, (StringFormula) placeHolder.recoveredFormula, inst.address); + shadowStateLogger.info("Modeled unmodeled pure result as a generic UF: {}", tmp); + // Record this run's observed (input -> output) ground pair - + // pure_(constant inputs) == observed output. Sound: a true fact about the + // real function only tightens the axiom-free UF. Cross-run accumulation and + // solve-time injection are the explorer's job. + if (placeHolder.observedApplication != null) { + StringFormulaManager smgr = context.getFormulaManager().getStringFormulaManager(); + symbolicTraceHandler.addConstraint( + smgr.equal((StringFormula) placeHolder.observedApplication, smgr.makeString(s))); + } + } else if (Util.isImmutableValueType(inst.val) + && placeHolder.referenceValue != null + && (tmp = stack.getFromHeap(inst.val)) != null + && tmp != placeHolder.referenceValue + && inst.val.equals(tmp.getConcrete())) { + // The unmodeled method returned a distinct, already-tracked immutable value + // (e.g. a String or boxed primitive retrieved from a container), not the + // receiver. Recover its shadow so the value keeps its symbolic formula instead + // of being concretized. An immutable value cannot have drifted since it was + // registered, so the stored shadow is still exact (the concrete-equality check + // is a defensive guard). A method returning `this` (e.g. toLowerCase) is + // excluded by `tmp != referenceValue` and still concretizes. + shadowStateLogger.info("Recovered distinct registered shadow for unmodeled value-typed result: {}", tmp); + } else { + tmp = ValueFactory.createObjectValue(inst.val, inst.address); + shadowStateLogger.info("Concretized unmodeled value-typed result (no identity recovery): {}", tmp); + } + stack.pushOperand(tmp); + return; + } + // try to get object - tmp = stack.getFromHeap(inst.address); + tmp = stack.getFromHeap(inst.val); // check if the object was created earlier and then reuse it if (tmp != null) { if (isSymbolic) { @@ -1291,7 +1341,7 @@ public void visitGETVALUE_Object(GETVALUE_Object inst) throws SymbolicInstruc tmp.MAKE_SYMBOLIC(); } stack.pushOperand(tmp); - stack.putToHeap(inst.address, tmp); // save the object for future use + stack.putToHeap(inst.val, tmp); // save the object for future use (keyed by concrete ref) if (placeHolder.origin == PlaceHolder.ValueOrigin.GETFIELD) { ObjectValue ref = placeHolder.referenceValue; GETFIELD gfInst = (GETFIELD) placeHolder.inst; @@ -1319,24 +1369,40 @@ public void visitGETVALUE_Object(GETVALUE_Object inst) throws SymbolicInstruc "Concrete value of the object does not match the value in the stack: {} | {}", inst.val, peek.concrete); if(peek.formula == null) { - // TODO This needs to be cleaned up! + // A constant String: reconstruct from the observed concrete. A constant is + // recoverable from inst.val on round-trip, so it is NOT heap-registered + // (registering it only grows the self-pinning heap leak - a String is its + // own weak key). stack.popOperand(); StringValue val = ValueFactory.createStringValue(s, inst.address); stack.pushOperand(val); - stack.putToHeap(inst.address, val); } else { (peek.asObjectValue()).setAddress(inst.address); - stack.putToHeap(inst.address, peek); + // Register iff the shadow carries symbolic content (a variable/UF) - those + // can't be reconstructed from the concrete and must round-trip via the heap + // (e.g. a whitelisted pure method's UF); pure constants are skipped to bound + // the leak. + FormulaManager fmgr = + ThreadHandler.getSolverContext(currentThread().getId()).getFormulaManager(); + if (!fmgr.extractVariablesAndUFs((Formula) peek.formula).isEmpty()) { + stack.putToHeap(inst.val, peek); + } } } else { (peek.asObjectValue()).setAddress(inst.address); - stack.putToHeap(inst.address, peek); + // Same policy as the String branch above, for de-interned boxed value types: a + // constant boxed value is reconstructible from inst.val, so skip registering it; + // symbolic boxed values, mutable objects, and uncached Float/Double keep + // unconditional registration. + if (!isConstantDeInternedValue(inst.val, peek)) { + stack.putToHeap(inst.val, peek); + } } } else { // Need to obtain the Object address (peek.asObjectValue()).setAddress(inst.address); - stack.putToHeap(inst.address, peek); + stack.putToHeap(inst.val, peek); } } else if ((peek.asObjectValue()).getAddress() == ADDRESS_NULL) { SWATAssert.check(inst.val == null, @@ -1371,7 +1437,7 @@ public void visitGETVALUE_Object(GETVALUE_Object inst) throws SymbolicInstruc stack.popOperand(); // Fetch the delegated object from the heap (e.g., IntReader) - Object heapObj = stack.getFromHeap(inst.address); + Object heapObj = stack.getFromHeap(inst.val); if (heapObj instanceof Value) { Value delegatedObject = (Value) heapObj; // Push the delegated object onto the stack @@ -1382,7 +1448,7 @@ public void visitGETVALUE_Object(GETVALUE_Object inst) throws SymbolicInstruc try { Value delegatedObject = de.uzl.its.swat.symbolic.value.ValueFactory.createObjectValue(inst.val, inst.address); stack.pushOperand(delegatedObject); - stack.putToHeap(inst.address, delegatedObject); + stack.putToHeap(inst.val, delegatedObject); logger.debug("Created new delegated object from instruction: {}", delegatedObject); } catch (Exception e) { logger.error("Failed to create delegated object from instruction value", e); @@ -1406,6 +1472,28 @@ public void visitGETVALUE_Object(GETVALUE_Object inst) throws SymbolicInstruc } } + /** + * Whether {@code ref} is a de-interned value type (String / cached boxed wrapper) whose shadow is a + * pure constant - i.e. carries no symbolic variable or UF. Such a value is reconstructible from the + * observed concrete on round-trip, so it is not heap-registered; this bounds the heap, and only the + * symbolic/UF shadows that cannot be reconstructed are registered. A boxed + * value carries its formula in the inner {@link BoxedValue#getVal()}, not the wrapper's own field. + */ + private boolean isConstantDeInternedValue(Object ref, Value shadow) + throws NoThreadContextException { + if (!Util.isDeInternedClass(ref)) { + return false; + } + Formula formula = (shadow instanceof BoxedValue boxed) + ? (Formula) boxed.getVal().formula + : (Formula) shadow.formula; + if (formula == null) { + return true; + } + FormulaManager fmgr = ThreadHandler.getSolverContext(currentThread().getId()).getFormulaManager(); + return fmgr.extractVariablesAndUFs(formula).isEmpty(); + } + /** * Artificial instruction used to fetch concrete boolean values * @@ -2706,14 +2794,14 @@ public void visitLDC_String(LDC_String inst) throws SymbolicInstructionException */ public void visitLDC_Object(LDC_Object inst) throws SymbolicInstructionException{ try{ - Value tmp = stack.getFromHeap(inst.c); + Value tmp = stack.getFromHeap(inst.object); if (tmp != null) { stack.pushOperand(tmp); - } else if (inst.c == 0) { + } else if (inst.object == null) { stack.pushOperand(ValueFactory.createNULLValue()); } else { stack.pushOperand(tmp = ValueFactory.createObjectValue(null, inst.c)); - stack.putToHeap(inst.c, tmp); + stack.putToHeap(inst.object, tmp); } checkAndSetException(inst); } catch (Throwable t) { @@ -3578,9 +3666,31 @@ private void visitGETVALUE_primitive(GETVALUE_primitive inst, ValueType type) th } else { stack.popOperand(); } - Value v = ValueFactory.createNumericalValue(type, inst.v); - if (isSymbolic) { - v.MAKE_SYMBOLIC(); + Value v; + if (placeHolder.origin == PlaceHolder.ValueOrigin.UNMODELED_RETURN + && placeHolder.recoveredFormula != null) { + // A whitelisted pure method with a primitive return - model the result as the + // carried generic UF over the inputs (concrete = observed), preserving the relational + // fact (equal inputs => equal outputs) instead of concretizing. Mirrors the String + // path in visitGETVALUE_Object. No MAKE_SYMBOLIC: the UF formula already carries the + // symbolic inputs (isSymbolic() is true iff the formula has free variables). + v = ValueFactory.createNumericalValue(type, inst.v, placeHolder.recoveredFormula); + ThreadHandler.getShadowStateLogger(currentThread().getId()) + .info("Modeled unmodeled pure primitive result as a generic UF: {}", v); + // Record this run's observed (input -> output) ground pair over the same cached UF + // declaration: pure_(constant inputs) == observed concrete output. A true fact + // that lets the explorer force a different input when re-solving a diverged branch. + if (placeHolder.observedApplication != null) { + FormulaManager fmgr = + ThreadHandler.getSolverContext(currentThread().getId()).getFormulaManager(); + symbolicTraceHandler.addConstraint( + PureFunctionUF.equalConstant(fmgr, placeHolder.observedApplication, inst.v)); + } + } else { + v = ValueFactory.createNumericalValue(type, inst.v); + if (isSymbolic) { + v.MAKE_SYMBOLIC(); + } } if (cat2) { @@ -3614,8 +3724,24 @@ private void visitGETVALUE_primitive(GETVALUE_primitive inst, ValueType type) th } } else if ((peek instanceof BoxedValue && !checkEquality(((BoxedValue)peek).getVal().concrete, inst.v)) || (!(peek instanceof BoxedValue) && !checkEquality(peek.concrete, inst.v))) { - SWATAssert.check(false, "[GETVALUE_primitive]: Value on stack does not match expected value! Expected: {}, Actual: {}", - inst.v, peek.concrete); + // The shadow's concrete diverges from the value the real JVM produced - an out-of-band + // change (e.g. a tracked object mutated inside unmodeled code) or an executor desync. + // CRASH keeps the strict hard-fail (development/CI bug catching); FLAG records a + // soundness flag (context loss, which downgrades a SAFE verdict to UNKNOWN) and adopts + // the observed concrete (sound, graceful). Escape-aware differentiation (crash only on a + // genuine desync) is not yet implemented. + if (Config.instance().getShadowDivergence() == ShadowDivergence.CRASH) { + SWATAssert.check(false, "[GETVALUE_primitive]: Value on stack does not match expected value! Expected: {}, Actual: {}", + inst.v, peek.concrete); + } else { + symbolicTraceHandler.recordSymbolicContextLoss(); + Logger shadowStateLogger = ThreadHandler.getShadowStateLogger(currentThread().getId()); + shadowStateLogger.info( + "Out-of-band change detected (shadow {} != observed {}); adopting observed concrete", + peek.concrete, inst.v); + } + // Adopt the observed concrete (re-ground): always under FLAG; under CRASH only if the + // assert is soft (useAssertions=false), preserving the prior behavior. if (cat2) { stack.popWideOperand(); stack.pushWideOperand(ValueFactory.createNumericalValue(type, inst.v)); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/PureFunctionUF.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/PureFunctionUF.java new file mode 100644 index 0000000..ee14608 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/PureFunctionUF.java @@ -0,0 +1,103 @@ +package de.uzl.its.swat.symbolic.UFs; + +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.stream.Collectors; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.UFManager; + +/** + * Per-thread registry of the generic uninterpreted functions that model whitelisted pure JDK methods. + * One UF symbol per signature (named via {@link PureMethods#ufName}), declared lazily and + * cached. The UF is axiom-free: applying it asserts only equal-inputs => equal-outputs + * (referential transparency), a sound over-approximation of any deterministic function. Observed + * concrete input->output pairs are added separately (as constraints) to tighten it across runs. + * + *

Contrast with the bespoke UFs ({@link ToLowerCaseUF} etc.), which ship hand axioms and live + * inside symbolic models; this registry ships none. + */ +public class PureFunctionUF { + private final UFManager ufmgr; + private final FormulaManager fmgr; + private final Map> declarations = new HashMap<>(); + + public PureFunctionUF(SolverContext ctx) { + fmgr = ctx.getFormulaManager(); + ufmgr = fmgr.getUFManager(); + } + + /** + * Build the UF application {@code ufName(args)} of the given return type. The argument sorts are + * derived from the actual {@code args} formulas (not the descriptor) so they match the values' + * sorts. The declaration is cached per name; on reuse the signature is asserted to match. + */ + public Formula apply(String ufName, FormulaType returnType, List args) { + List> argTypes = + args.stream().map(fmgr::getFormulaType).collect(Collectors.toList()); + FunctionDeclaration decl = declarations.get(ufName); + if (decl == null) { + decl = ufmgr.declareUF(ufName, returnType, argTypes); + declarations.put(ufName, decl); + } else { + assert decl.getType().equals(returnType) && decl.getArgumentTypes().equals(argTypes) + : "Generic UF signature mismatch for " + ufName; + } + return ufmgr.callUF(decl, args); + } + + /** + * A constant formula of {@code type} holding the concrete {@code value}, for the ground (observed) + * side of a pure-UF pair. Supports the value-type sorts: boolean, bitvector (any width, from a + * {@link Character} or {@link Number}), floating point (single/double), and String. + */ + public static Formula constant(FormulaManager fmgr, FormulaType type, Object value) { + if (type.isBooleanType()) { + return fmgr.getBooleanFormulaManager().makeBoolean((Boolean) value); + } + if (type.isBitvectorType()) { + int width = ((FormulaType.BitvectorType) type).getSize(); + long bits = (value instanceof Character c) ? (char) c : ((Number) value).longValue(); + return fmgr.getBitvectorFormulaManager().makeBitvector(width, bits); + } + if (type.isFloatingPointType()) { + return fmgr.getFloatingPointFormulaManager() + .makeNumber(((Number) value).doubleValue(), (FormulaType.FloatingPointType) type); + } + if (type.isStringType()) { + return fmgr.getStringFormulaManager().makeString((String) value); + } + throw new IllegalArgumentException("Unsupported observed-pair type: " + type); + } + + /** + * The equality {@code uf == constant(value)} in the theory of {@code uf}'s sort, used to record an + * observed (input -> output) ground pair for a pure UF. + */ + public static BooleanFormula equalConstant(FormulaManager fmgr, Formula uf, Object value) { + FormulaType type = fmgr.getFormulaType(uf); + Formula c = constant(fmgr, type, value); + if (type.isBooleanType()) { + return fmgr.getBooleanFormulaManager().equivalence((BooleanFormula) uf, (BooleanFormula) c); + } + if (type.isBitvectorType()) { + return fmgr.getBitvectorFormulaManager().equal((BitvectorFormula) uf, (BitvectorFormula) c); + } + if (type.isFloatingPointType()) { + return fmgr.getFloatingPointFormulaManager() + .equalWithFPSemantics((FloatingPointFormula) uf, (FloatingPointFormula) c); + } + if (type.isStringType()) { + return fmgr.getStringFormulaManager().equal((StringFormula) uf, (StringFormula) c); + } + throw new IllegalArgumentException("Unsupported observed-pair type: " + type); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/PureMethods.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/PureMethods.java new file mode 100644 index 0000000..38a5cc7 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/PureMethods.java @@ -0,0 +1,304 @@ +package de.uzl.its.swat.symbolic.UFs; + +import java.util.Set; +import org.objectweb.asm.Type; + +/** + * Whitelist of pure, deterministic, side-effect-free JDK methods that SWAT does NOT model, plus the + * descriptive naming scheme for the generic uninterpreted functions that model their returns. A + * whitelisted method's result is modeled as {@code pure__[_](inputs)} + * instead of being concretized - preserving the relational fact (equal inputs => equal outputs) + * soundly, since an axiom-free UF over-approximates any deterministic function. + * + *

Membership is a soundness precondition: only genuinely pure and deterministic methods may + * appear here. Exclude locale-dependent (no-arg {@code toLowerCase}/{@code toUpperCase}), + * environment/property readers, argument-mutating, identity/{@code intern}, and nondeterministic + * (random/time) methods. String and all primitive return types are supported (the UF's return sort + * is the method's return type); the method must also be UNMODELED by SWAT, otherwise the UF never + * fires. + */ +public final class PureMethods { + private PureMethods() {} + + /** + * Keys are {@code owner + "/" + name + desc} (descriptor included to disambiguate overloads). + * Every entry is pure, deterministic, side-effect-free, and UNMODELED by SWAT - absent from its + * Invocation handler, or present only as a StringValue stub - so the generic UF actually fires. + * The boxed types' toString-family is intentionally absent (already modeled, so a UF would never + * fire). Covers String and primitive returns across + * Math/StrictMath/Character/Integer/Byte/Float/Double/Objects and the String methods. + */ + private static final Set WHITELIST = + Set.of( + // String/primitive returns on String - UF-firing (StringValue stubs), pure + locale-independent: + "java/lang/String/codePointAt(I)I", + "java/lang/String/codePointBefore(I)I", + "java/lang/String/codePointCount(II)I", + "java/lang/String/compareTo(Ljava/lang/String;)I", + "java/lang/String/compareToIgnoreCase(Ljava/lang/String;)I", + "java/lang/String/hashCode()I", + "java/lang/String/indent(I)Ljava/lang/String;", + "java/lang/String/isBlank()Z", + "java/lang/String/isEmpty()Z", + "java/lang/String/lastIndexOf(I)I", + "java/lang/String/lastIndexOf(II)I", + "java/lang/String/lastIndexOf(Ljava/lang/String;)I", + "java/lang/String/lastIndexOf(Ljava/lang/String;I)I", + "java/lang/String/matches(Ljava/lang/String;)Z", + "java/lang/String/offsetByCodePoints(II)I", + "java/lang/String/regionMatches(ILjava/lang/String;II)Z", + "java/lang/String/regionMatches(ZILjava/lang/String;II)Z", + "java/lang/String/repeat(I)Ljava/lang/String;", + "java/lang/String/replaceAll(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;", + "java/lang/String/replaceFirst(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;", + "java/lang/String/strip()Ljava/lang/String;", + "java/lang/String/stripIndent()Ljava/lang/String;", + "java/lang/String/stripLeading()Ljava/lang/String;", + "java/lang/String/stripTrailing()Ljava/lang/String;", + "java/lang/String/translateEscapes()Ljava/lang/String;", + "java/lang/String/trim()Ljava/lang/String;", + // Pure, unmodeled, value-typed methods from the java.lang/util purity audit: + "java/lang/Math/IEEEremainder(DD)D", + "java/lang/Math/absExact(I)I", + "java/lang/Math/absExact(J)J", + "java/lang/Math/acos(D)D", + "java/lang/Math/addExact(II)I", + "java/lang/Math/addExact(JJ)J", + "java/lang/Math/asin(D)D", + "java/lang/Math/atan(D)D", + "java/lang/Math/atan2(DD)D", + "java/lang/Math/cbrt(D)D", + "java/lang/Math/ceil(D)D", + "java/lang/Math/copySign(DD)D", + "java/lang/Math/copySign(FF)F", + "java/lang/Math/cosh(D)D", + "java/lang/Math/decrementExact(I)I", + "java/lang/Math/decrementExact(J)J", + "java/lang/Math/exp(D)D", + "java/lang/Math/expm1(D)D", + "java/lang/Math/floor(D)D", + "java/lang/Math/floorDiv(II)I", + "java/lang/Math/floorDiv(JI)J", + "java/lang/Math/floorDiv(JJ)J", + "java/lang/Math/floorMod(II)I", + "java/lang/Math/floorMod(JI)I", + "java/lang/Math/floorMod(JJ)J", + "java/lang/Math/fma(DDD)D", + "java/lang/Math/fma(FFF)F", + "java/lang/Math/getExponent(D)I", + "java/lang/Math/getExponent(F)I", + "java/lang/Math/hypot(DD)D", + "java/lang/Math/incrementExact(I)I", + "java/lang/Math/incrementExact(J)J", + "java/lang/Math/log(D)D", + "java/lang/Math/log10(D)D", + "java/lang/Math/log1p(D)D", + "java/lang/Math/multiplyExact(II)I", + "java/lang/Math/multiplyExact(JI)J", + "java/lang/Math/multiplyExact(JJ)J", + "java/lang/Math/multiplyFull(II)J", + "java/lang/Math/multiplyHigh(JJ)J", + "java/lang/Math/negateExact(I)I", + "java/lang/Math/negateExact(J)J", + "java/lang/Math/nextAfter(DD)D", + "java/lang/Math/nextAfter(FD)F", + "java/lang/Math/nextDown(D)D", + "java/lang/Math/nextDown(F)F", + "java/lang/Math/nextUp(D)D", + "java/lang/Math/nextUp(F)F", + "java/lang/Math/pow(DD)D", + "java/lang/Math/rint(D)D", + "java/lang/Math/scalb(DI)D", + "java/lang/Math/scalb(FI)F", + "java/lang/Math/signum(D)D", + "java/lang/Math/signum(F)F", + "java/lang/Math/sinh(D)D", + "java/lang/Math/subtractExact(II)I", + "java/lang/Math/subtractExact(JJ)J", + "java/lang/Math/tan(D)D", + "java/lang/Math/tanh(D)D", + "java/lang/Math/toDegrees(D)D", + "java/lang/Math/toIntExact(J)I", + "java/lang/Math/toRadians(D)D", + "java/lang/Math/ulp(D)D", + "java/lang/Math/ulp(F)F", + "java/lang/StrictMath/IEEEremainder(DD)D", + "java/lang/StrictMath/absExact(I)I", + "java/lang/StrictMath/absExact(J)J", + "java/lang/StrictMath/acos(D)D", + "java/lang/StrictMath/addExact(II)I", + "java/lang/StrictMath/addExact(JJ)J", + "java/lang/StrictMath/asin(D)D", + "java/lang/StrictMath/atan(D)D", + "java/lang/StrictMath/atan2(DD)D", + "java/lang/StrictMath/cbrt(D)D", + "java/lang/StrictMath/ceil(D)D", + "java/lang/StrictMath/copySign(DD)D", + "java/lang/StrictMath/copySign(FF)F", + "java/lang/StrictMath/cosh(D)D", + "java/lang/StrictMath/decrementExact(I)I", + "java/lang/StrictMath/decrementExact(J)J", + "java/lang/StrictMath/exp(D)D", + "java/lang/StrictMath/expm1(D)D", + "java/lang/StrictMath/floor(D)D", + "java/lang/StrictMath/floorDiv(II)I", + "java/lang/StrictMath/floorDiv(JI)J", + "java/lang/StrictMath/floorDiv(JJ)J", + "java/lang/StrictMath/floorMod(II)I", + "java/lang/StrictMath/floorMod(JI)I", + "java/lang/StrictMath/floorMod(JJ)J", + "java/lang/StrictMath/fma(DDD)D", + "java/lang/StrictMath/fma(FFF)F", + "java/lang/StrictMath/getExponent(D)I", + "java/lang/StrictMath/getExponent(F)I", + "java/lang/StrictMath/hypot(DD)D", + "java/lang/StrictMath/incrementExact(I)I", + "java/lang/StrictMath/incrementExact(J)J", + "java/lang/StrictMath/log(D)D", + "java/lang/StrictMath/log10(D)D", + "java/lang/StrictMath/log1p(D)D", + "java/lang/StrictMath/multiplyExact(II)I", + "java/lang/StrictMath/multiplyExact(JI)J", + "java/lang/StrictMath/multiplyExact(JJ)J", + "java/lang/StrictMath/multiplyFull(II)J", + "java/lang/StrictMath/multiplyHigh(JJ)J", + "java/lang/StrictMath/negateExact(I)I", + "java/lang/StrictMath/negateExact(J)J", + "java/lang/StrictMath/nextAfter(DD)D", + "java/lang/StrictMath/nextAfter(FD)F", + "java/lang/StrictMath/nextDown(D)D", + "java/lang/StrictMath/nextDown(F)F", + "java/lang/StrictMath/nextUp(D)D", + "java/lang/StrictMath/nextUp(F)F", + "java/lang/StrictMath/pow(DD)D", + "java/lang/StrictMath/rint(D)D", + "java/lang/StrictMath/scalb(DI)D", + "java/lang/StrictMath/scalb(FI)F", + "java/lang/StrictMath/signum(D)D", + "java/lang/StrictMath/signum(F)F", + "java/lang/StrictMath/sinh(D)D", + "java/lang/StrictMath/subtractExact(II)I", + "java/lang/StrictMath/subtractExact(JJ)J", + "java/lang/StrictMath/tan(D)D", + "java/lang/StrictMath/tanh(D)D", + "java/lang/StrictMath/toDegrees(D)D", + "java/lang/StrictMath/toIntExact(J)I", + "java/lang/StrictMath/toRadians(D)D", + "java/lang/StrictMath/ulp(D)D", + "java/lang/StrictMath/ulp(F)F", + "java/lang/Character/digit(CI)I", + "java/lang/Character/digit(II)I", + "java/lang/Character/forDigit(II)C", + "java/lang/Character/getDirectionality(C)B", + "java/lang/Character/getDirectionality(I)B", + "java/lang/Character/getNumericValue(C)I", + "java/lang/Character/getNumericValue(I)I", + "java/lang/Character/getType(C)I", + "java/lang/Character/getType(I)I", + "java/lang/Character/hashCode(C)I", + "java/lang/Character/highSurrogate(I)C", + "java/lang/Character/isAlphabetic(I)Z", + "java/lang/Character/isDefined(C)Z", + "java/lang/Character/isDefined(I)Z", + "java/lang/Character/isDigit(C)Z", + "java/lang/Character/isDigit(I)Z", + "java/lang/Character/isHighSurrogate(C)Z", + "java/lang/Character/isISOControl(C)Z", + "java/lang/Character/isISOControl(I)Z", + "java/lang/Character/isIdentifierIgnorable(C)Z", + "java/lang/Character/isIdentifierIgnorable(I)Z", + "java/lang/Character/isIdeographic(I)Z", + "java/lang/Character/isJavaIdentifierPart(C)Z", + "java/lang/Character/isJavaIdentifierPart(I)Z", + "java/lang/Character/isJavaIdentifierStart(C)Z", + "java/lang/Character/isJavaIdentifierStart(I)Z", + "java/lang/Character/isJavaLetter(C)Z", + "java/lang/Character/isJavaLetterOrDigit(C)Z", + "java/lang/Character/isLetter(C)Z", + "java/lang/Character/isLetter(I)Z", + "java/lang/Character/isLetterOrDigit(C)Z", + "java/lang/Character/isLetterOrDigit(I)Z", + "java/lang/Character/isLowSurrogate(C)Z", + "java/lang/Character/isLowerCase(C)Z", + "java/lang/Character/isLowerCase(I)Z", + "java/lang/Character/isMirrored(C)Z", + "java/lang/Character/isMirrored(I)Z", + "java/lang/Character/isSpace(C)Z", + "java/lang/Character/isSpaceChar(C)Z", + "java/lang/Character/isSpaceChar(I)Z", + "java/lang/Character/isSurrogate(C)Z", + "java/lang/Character/isSurrogatePair(CC)Z", + "java/lang/Character/isTitleCase(C)Z", + "java/lang/Character/isTitleCase(I)Z", + "java/lang/Character/isUnicodeIdentifierPart(C)Z", + "java/lang/Character/isUnicodeIdentifierPart(I)Z", + "java/lang/Character/isUnicodeIdentifierStart(C)Z", + "java/lang/Character/isUnicodeIdentifierStart(I)Z", + "java/lang/Character/isUpperCase(C)Z", + "java/lang/Character/isUpperCase(I)Z", + "java/lang/Character/isWhitespace(C)Z", + "java/lang/Character/isWhitespace(I)Z", + "java/lang/Character/lowSurrogate(I)C", + "java/lang/Character/reverseBytes(C)C", + "java/lang/Character/toLowerCase(C)C", + "java/lang/Character/toLowerCase(I)I", + "java/lang/Character/toString(C)Ljava/lang/String;", + "java/lang/Character/toString(I)Ljava/lang/String;", + "java/lang/Character/toTitleCase(C)C", + "java/lang/Character/toTitleCase(I)I", + "java/lang/Character/toUpperCase(C)C", + "java/lang/Character/toUpperCase(I)I", + "java/lang/Integer/bitCount(I)I", + "java/lang/Byte/compareUnsigned(BB)I", + "java/lang/Byte/hashCode(B)I", + "java/lang/Float/hashCode(F)I", + "java/lang/Float/intBitsToFloat(I)F", + "java/lang/Float/parseFloat(Ljava/lang/String;)F", + "java/lang/Float/toHexString(F)Ljava/lang/String;", + "java/lang/Float/toString(F)Ljava/lang/String;", + "java/lang/Double/doubleToLongBits(D)J", + "java/lang/Double/doubleToRawLongBits(D)J", + "java/lang/Double/hashCode(D)I", + "java/lang/Double/longBitsToDouble(J)D", + "java/lang/Double/max(DD)D", + "java/lang/Double/min(DD)D", + "java/lang/Double/parseDouble(Ljava/lang/String;)D", + "java/lang/Double/sum(DD)D", + "java/lang/Double/toHexString(D)Ljava/lang/String;", + "java/lang/Double/toString(D)Ljava/lang/String;", + "java/util/Objects/checkFromIndexSize(III)I", + "java/util/Objects/checkFromIndexSize(JJJ)J", + "java/util/Objects/checkFromToIndex(III)I", + "java/util/Objects/checkFromToIndex(JJJ)J", + "java/util/Objects/checkIndex(II)I", + "java/util/Objects/checkIndex(JJ)J"); + + public static boolean isWhitelisted(String owner, String name, String desc) { + return WHITELIST.contains(owner + "/" + name + desc); + } + + /** + * Descriptive, SMT-safe UF name {@code pure__[_]}, e.g. + * {@code pure_String_trim}, {@code pure_String_substring_int_int}. The {@code pure_} prefix is the + * precision-loss exemption's recognizer; arg types disambiguate overloads. + */ + public static String ufName(String owner, String name, String desc) { + StringBuilder sb = new StringBuilder("pure_"); + sb.append(simpleName(owner)).append('_').append(name); + for (Type t : Type.getArgumentTypes(desc)) { + sb.append('_').append(simpleTypeName(t)); + } + return sb.toString(); + } + + private static String simpleName(String internalOwner) { + int slash = internalOwner.lastIndexOf('/'); + return slash >= 0 ? internalOwner.substring(slash + 1) : internalOwner; + } + + private static String simpleTypeName(Type t) { + String cn = t.getClassName().replace("[]", "Array"); + int dot = cn.lastIndexOf('.'); + return dot >= 0 ? cn.substring(dot + 1) : cn; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java index 639b275..a1da8ff 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java @@ -8,6 +8,7 @@ public class UFHandler { private EqualsIgnoreCaseUF equalsIgnoreCaseUF; private ToLowerCaseUF toLowerCaseUF; private SinCosUF sinCosUF; + private PureFunctionUF pureFunctionUF; public EqualsIgnoreCaseUF getEqualsIgnoreCaseUF() throws NoThreadContextException { if (equalsIgnoreCaseUF == null) { @@ -29,4 +30,12 @@ public SinCosUF getSinCosUF() throws NoThreadContextException { } return sinCosUF; } + + /** Registry of generic uninterpreted functions for whitelisted pure JDK methods. */ + public PureFunctionUF getPureFunctionUF() throws NoThreadContextException { + if (pureFunctionUF == null) { + pureFunctionUF = new PureFunctionUF(ThreadHandler.getSolverContext(currentThread().getId())); + } + return pureFunctionUF; + } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/instruction/LDC_Object.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/instruction/LDC_Object.java index 1b51459..99eef8c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/instruction/LDC_Object.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/instruction/LDC_Object.java @@ -10,18 +10,23 @@ */ public class LDC_Object extends Instruction { - // The address of the object that's loaded (?) + // The identity hash of the loaded object (kept for address, NULL, and debug) public int c; + // The loaded constant object (the canonical-registry key, by reference identity) + public Object object; + /** - * Creates a new LDC_long instruction. + * Creates a new LDC_Object instruction. * * @param iid instruction id. - * @param c the address of the object that's loaded + * @param c the identity hash of the loaded object + * @param object the loaded constant object (the registry key) */ - public LDC_Object(long iid, int c) { + public LDC_Object(long iid, int c, Object object) { super(iid); this.c = c; + this.object = object; } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java index d1c465b..cbdbbf2 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java @@ -1,11 +1,14 @@ package de.uzl.its.swat.symbolic.invoke; import ch.qos.logback.classic.Logger; +import de.uzl.its.swat.common.Util; import de.uzl.its.swat.common.exceptions.NoThreadContextException; import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.common.logging.GlobalLogger; import de.uzl.its.swat.common.logging.records.InvocationEntry; +import de.uzl.its.swat.symbolic.UFs.PureFunctionUF; +import de.uzl.its.swat.symbolic.UFs.PureMethods; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.PlaceHolder; import de.uzl.its.swat.symbolic.value.Value; @@ -14,9 +17,13 @@ import de.uzl.its.swat.thread.ThreadHandler; import java.util.ArrayList; import java.util.Arrays; +import java.util.List; import java.util.stream.Collectors; import org.objectweb.asm.Type; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaManager; public class InvocationHandler { private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger(); @@ -27,6 +34,12 @@ public class InvocationHandler { "java/io/PrintStream/println", "de/uzl/its/swat/instrument/Intrinsics", "de/uzl/its/swat/common/UtilInstrumented", + // refEquals's body (stepped through, since UtilInstrumented is + // instrumented) calls these with a possibly-symbolic operand; ignore them + // so a reference comparison does not record spurious context loss. Both are + // pure/identity and their concretized results are all refEquals needs. + "de/uzl/its/swat/common/Util/shouldUseValueEquality", + "de/uzl/its/swat/common/Provenance", "de/uzl/its/swat/witness/Witness", "de/uzl/its/swat/instrument/svcomp/Verifier", "java/io/PrintStream", @@ -72,6 +85,9 @@ public class InvocationHandler { symbolicTraceHandler); } + // Model of a whitelisted pure return (result UF over symbolic inputs + the same UF over + // constant observed inputs, for the observed pair); stays null -> recovery concretizes. + PureUFModel pureUF = null; // When the method is not implemented and its not on the ignore list, we record it if (retValue instanceof PlaceHolder && !(IGNORED_INVOCATIONS.contains(owner + "/" + name) @@ -104,8 +120,20 @@ public class InvocationHandler { invokeId, containsSymbolicArgument)); + // Model a whitelisted pure, value-returning call as a generic UF over its inputs + // (instead of concretizing at recovery). Sound by construction: an axiom-free UF + // over-approximates any deterministic function. Only when an input is symbolic; + // `arguments` here already includes the receiver (prepended above). + if (containsSymbolicArgument && PureMethods.isWhitelisted(owner, name, desc)) { + pureUF = buildPureUF(owner, name, desc, arguments); + } + if( - (retValue.equals(PlaceHolder.instance) // To detect a missing implementation + // A successfully UF-modeled pure call loses no context - the whitelist + // guarantees no side effects and the return is captured by the UF - so it must NOT + // downgrade SAFE; only flag context loss when the call was not modeled. + pureUF == null + && (retValue.equals(PlaceHolder.instance) // To detect a missing implementation || retValue instanceof VoidValue vv && !vv.isSymbolic()) // To detect a missing implementation that returns nothing && containsSymbolicArgument) { // Too strict? What about void methods that always have return value PlaceHolder.instance? @@ -115,9 +143,98 @@ public class InvocationHandler { desc); symbolicTraceHandler.recordSymbolicContextLoss(); } + } + // Tag an unmodeled placeholder return so visitGETVALUE_Object recovers a value-typed + // result instead of identity-recovering it (which would re-bind the receiver's symbolic value, + // e.g. String.toLowerCase() returning `this`). If a generic UF was built, it rides along + // and the result is modeled as that UF; otherwise recovery concretizes. This MUST stay + // after the context-loss check above, which compares retValue against PlaceHolder.instance by + // identity. + if (retValue == PlaceHolder.instance) { + retValue = new PlaceHolder( + PlaceHolder.ValueOrigin.UNMODELED_RETURN, + isInstance ? instance : null, + pureUF == null ? null : pureUF.result(), + pureUF == null ? null : pureUF.observedApplication()); } return retValue; } + /** A whitelisted pure call modeled as a generic UF: the result over symbolic inputs, and the + * same UF over the constant observed inputs for the observed (input -> output) pair. */ + private record PureUFModel(Formula result, Formula observedApplication) {} + + /** + * Build the generic UF {@code pure_(inputs)} for a whitelisted pure call, or null to fall + * back to concretization. Handles String and all primitive returns (the return sort is + * {@link #pureUFReturnType}); the inputs (receiver + args) must all be value-typed so their + * formula fully captures the input (sound; no stateful receivers). Also builds the same UF applied + * to the CONSTANT (observed) inputs, over the SAME cached declaration, so recovery can assert the + * observed (inputs -> output) ground pair. + */ + private static PureUFModel buildPureUF( + String owner, String name, String desc, List> inputs) + throws NoThreadContextException { + // The UF's return sort is the method's return type - String or any primitive. Unsupported + // returns (void, arrays, non-String objects) yield null and fall back to concretization. + FormulaType returnType = pureUFReturnType(desc); + if (returnType == null) { + return null; + } + FormulaManager fmgr = + ThreadHandler.getSolverContext(Thread.currentThread().getId()).getFormulaManager(); + List symbolicArgs = new ArrayList<>(); + List constArgs = new ArrayList<>(); + for (Value v : inputs) { + if (v.formula == null || !Util.isValueType(v.concrete)) { + return null; // non-value-typed or formula-less input: defer to concretization. + } + Formula sym = (Formula) v.formula; + symbolicArgs.add(sym); + // The ground input constant must match the symbolic argument's own sort, so the observed + // application reuses the same UF signature. + constArgs.add(PureFunctionUF.constant(fmgr, fmgr.getFormulaType(sym), v.concrete)); + } + PureFunctionUF uf = ThreadHandler.getUFHandler(Thread.currentThread().getId()).getPureFunctionUF(); + String ufName = PureMethods.ufName(owner, name, desc); + Formula result = uf.apply(ufName, returnType, symbolicArgs); + // Observed pair: the same cached UF declaration applied to the CONSTANT (observed) inputs, so + // the ground pair asserted at recovery constrains the very symbol used in `result`. Built for + // every supported return sort - the recovery side asserts it == the observed concrete output. + Formula observed = uf.apply(ufName, returnType, constArgs); + return new PureUFModel(result, observed); + } + + /** + * The SMT return sort for a whitelisted pure method, matching the shadow value sorts exactly: + * String; boolean; bitvectors of width 8/16/16/32/64 for byte/short/char/int/long; and + * floating-point (single for float, double for double). Returns null for unsupported returns + * (void, arrays, non-String objects), which fall back to concretization. + */ + private static FormulaType pureUFReturnType(String desc) { + Type ret = Type.getReturnType(desc); + switch (ret.getSort()) { + case Type.BOOLEAN: + return FormulaType.BooleanType; + case Type.BYTE: + return FormulaType.getBitvectorTypeWithSize(8); + case Type.SHORT: + case Type.CHAR: + return FormulaType.getBitvectorTypeWithSize(16); + case Type.INT: + return FormulaType.getBitvectorTypeWithSize(32); + case Type.LONG: + return FormulaType.getBitvectorTypeWithSize(64); + case Type.FLOAT: + return FormulaType.getSinglePrecisionFloatingPointType(); + case Type.DOUBLE: + return FormulaType.getDoublePrecisionFloatingPointType(); + case Type.OBJECT: + return "java.lang.String".equals(ret.getClassName()) ? FormulaType.StringType : null; + default: + return null; // void, array, other reference types + } + } + } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java index 2f6cf86..a8a60ac 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/ObjectsInvocation.java @@ -10,12 +10,8 @@ import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue; import de.uzl.its.swat.symbolic.value.reference.ObjectValue; import de.uzl.its.swat.symbolic.value.reference.lang.CharacterObjectValue; -import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; -import de.uzl.its.swat.thread.ThreadHandler; import org.objectweb.asm.Type; -import static java.lang.Thread.currentThread; - public class ObjectsInvocation { public static Value invokeStaticMethod( @@ -35,19 +31,6 @@ public class ObjectsInvocation { ObjectValue a = args[0].asObjectValue(); ObjectValue b = args[1].asObjectValue(); - // Check for user-de-interned strings with different addresses. - // This detects when refEquals (which calls Objects.equals) compares strings - // that were explicitly created with new String() in user code. - // In such cases, reference equality semantics may differ from what the user intended. - if (a instanceof StringValue s1 && b instanceof StringValue s2) { - if ((s1.isUserDeInterned() || s2.isUserDeInterned()) - && s1.getAddress() != s2.getAddress()) { - // Record that reference equality semantics may have changed - ThreadHandler.getSymbolicTraceHandler(currentThread().getId()) - .recordReferenceSemanticChange(); - } - } - if(a.getAddress() == ObjectValue.ADDRESS_NULL || b.getAddress() == ObjectValue.ADDRESS_NULL) { return PlaceHolder.instance; } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/AbstractInstructionProcessor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/AbstractInstructionProcessor.java index 848d95f..3375ddb 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/AbstractInstructionProcessor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/AbstractInstructionProcessor.java @@ -32,7 +32,7 @@ public void LDC(long iid, String c) { } public void LDC(long iid, Object c) { - processInstruction(new LDC_Object(iid, System.identityHashCode(c))); + processInstruction(new LDC_Object(iid, System.identityHashCode(c), c)); } public void IINC(long iid, int var, int increment) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/JVMHeap.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/JVMHeap.java index b18efde..73f1ffb 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/JVMHeap.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/JVMHeap.java @@ -1,26 +1,55 @@ package de.uzl.its.swat.symbolic.shadow; +import com.google.common.collect.MapMaker; import de.uzl.its.swat.symbolic.value.Value; -import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; -import de.uzl.its.swat.symbolic.value.reference.lang.IntegerObjectValue; -import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; -import java.util.HashMap; import java.util.Map; +/** + * Canonical shadow registry: maps a concrete object reference to its shadow {@link Value}. + * + *

The key is the concrete object itself, compared by reference identity ({@code ==}), not by + * {@code System.identityHashCode}. This is collision-free (distinct objects are distinct keys even + * when their identity hash collides) and gives exactly one shadow per concrete object. + * + *

Keys are held weakly ({@link MapMaker#weakKeys()}). For plain objects and boxed primitives the + * shadow value holds no strong reference to its concrete key, so an entry is evicted once the + * concrete object becomes unreachable. NOTE: a {@code StringValue} stores its own concrete + * {@code String}, which is also the key, so String-keyed entries are self-pinned and do not evict + * until the thread's context is discarded - no worse than the previous never-evicting map, and + * reference keying still removes the identity-hash collision/reuse hazard. (A unique-id key would + * also evict Strings; deferred.) + */ public class JVMHeap { - private final Map> objects; + private final Map> objects; public JVMHeap() { - objects = new HashMap<>(); + // weakKeys() => identity (==) key comparison + weak references. + objects = new MapMaker().weakKeys().makeMap(); } - public void put(int hashCode, Value value) { - objects.put(hashCode, value); + public void put(Object ref, Value value) { + if (ref == null) { + return; + } + objects.put(ref, value); } - public Value get(int hashCode) { - return objects.get(hashCode); + public Value get(Object ref) { + if (ref == null) { + return null; + } + return objects.get(ref); + } + + /** + * Number of registered cells. With reference keying this is the number of distinct concrete + * objects currently held (collision-free). + * + * @return the number of entries currently held. + */ + public int size() { + return objects.size(); } } 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 143343e..dd008de 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 @@ -45,12 +45,20 @@ public ShadowContext() { // lambdaFrameStore = new HashMap<>(); } - public void putToHeap(int hashCode, Value value) { - heap.put(hashCode, value); + public void putToHeap(Object ref, Value value) { + heap.put(ref, value); } - public Value getFromHeap(int hashCode) { - return heap.get(hashCode); + public Value getFromHeap(Object ref) { + return heap.get(ref); + } + /** + * Number of registered recovery-cache cells. See {@link JVMHeap#size()}. + * + * @return the number of entries currently on the heap. + */ + public int heapSize() { + return heap.size(); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowDivergence.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowDivergence.java new file mode 100644 index 0000000..83ec140 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowDivergence.java @@ -0,0 +1,22 @@ +package de.uzl.its.swat.symbolic.shadow; + +/** + * Policy for handling a shadow/concrete divergence detected at a GETVALUE sync point: the shadow + * value's concrete no longer matches the value the real JVM produced (an out-of-band change, e.g. an + * object mutated inside unmodeled code). Configured via {@code shadow.divergence}. + */ +public enum ShadowDivergence { + /** + * Hard-fail on divergence (SWATAssert). Useful for catching executor-internal desync bugs in + * development and CI. Default. + */ + CRASH, + + /** + * Detect gracefully: record a soundness flag (context loss, which downgrades a SAFE verdict to + * UNKNOWN), adopt the observed concrete value, and continue. Fully sound; recommended for SV-COMP + * and production runs (no spurious crashes). This policy does not distinguish a legitimate + * out-of-band change from an executor desync - both are flagged. + */ + FLAG +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index 8fa442e..436ce6b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -17,10 +17,16 @@ import java.util.ArrayList; import java.util.HashSet; import java.util.List; +import java.util.Set; +import java.util.concurrent.atomic.AtomicBoolean; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; /** * Builds a data transfer object (DTO) from the {@link SymbolicTrace SuymbolicState} for @@ -50,10 +56,14 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace) throws NoThre ArrayList inputs = new ArrayList<>(); ArrayList ufs = new ArrayList<>(); ArrayList trace = new ArrayList<>(); + // The terms of the designated symbolic inputs, used to classify precision loss: a branch + // variable is "grounded" iff its term is one of these (exact + type-aware, no name pattern). + Set inputTerms = new HashSet<>(); FormulaManager fmgr = ThreadHandler.getSolverContext(currentThread().getId()).getFormulaManager(); for (InputElement ie : symbolicTrace.getInputs()) { + inputTerms.add((Formula) ie.getValue().formula); String lowerBound = String.valueOf(fmgr.dumpFormula(ie.getValue().getBounds(false))); String upperBound = String.valueOf(fmgr.dumpFormula(ie.getValue().getBounds(true))); InputDTO iDto = @@ -74,39 +84,92 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace) throws NoThre for (Element el : symbolicTrace.getTrace()) { if (el instanceof BranchElement be) { String constraint; + boolean branchPrecisionLoss = false; try { BooleanFormula f = fmgr.simplify(be.getConstraint()); - // Todo or go back to extracting variables and UFs? if(fmgr.getBooleanFormulaManager().isTrue(f) || fmgr.getBooleanFormulaManager().isFalse(f)){ constraint = "(assert true)"; } else { constraint = String.valueOf(fmgr.dumpFormula(f)); - if (!fmgr.extractVariablesAndUFs(f).isEmpty() && - !fmgr.extractVariablesAndUFs(f).keySet().stream().allMatch(s -> s.matches("[A-Z].*_[0-9].*"))) { - symbolicPrecisionLoss = true; - } + branchPrecisionLoss = isPrecisionLoss(f, fmgr, inputTerms); } - //fmgr.extractVariablesAndUFs(f).keySet().forEach(System.out::println); - // assert fmgr.extractVariablesAndUFs(f).keySet().stream() - // .allMatch(s -> s.matches("[A-Z].*_[0-9].*")): "[SWAT] UF introduced in: " + constraint; - } catch (InterruptedException e) { BooleanFormula f = be.getConstraint(); logger.warn("Error while simplifying formula", e); constraint = String.valueOf(fmgr.dumpFormula(f)); - //fmgr.extractVariablesAndUFs(f).keySet().forEach(System.out::println); - // assert fmgr.extractVariablesAndUFs(f).keySet().stream() - // .allMatch(s -> s.matches("[A-Z].*_[0-9].*")): "[SWAT] UF introduced in: " + constraint; - if (!fmgr.extractVariablesAndUFs(f).keySet().stream().allMatch(s -> s.matches("[A-Z].*_[0-9].*"))) { - symbolicPrecisionLoss = true; - } + branchPrecisionLoss = isPrecisionLoss(f, fmgr, inputTerms); } - trace.add(new BranchDTO(be.getIid(), constraint, be.isBranched())); + // Aggregate precision loss = OR of the per-branch flags. The per-branch flag also + // travels on the BranchDTO so a future explorer-side, CFG-reachability-aware + // precision-loss decision can take over with no trace change. + symbolicPrecisionLoss |= branchPrecisionLoss; + trace.add(new BranchDTO(be.getIid(), constraint, be.isBranched(), branchPrecisionLoss)); } else if (el instanceof SpecialElement se) { trace.add(new BranchDTO(se.getIid(), se.getInst())); } } - return new TraceDTO(inputs, trace, ufs, symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange()); + return new TraceDTO(inputs, trace, ufs, symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss); + } + + /** + * A symbolic-variable name produced by the input-naming convention (primitive prefixes like + * {@code I_0}). Kept as a backstop for symbolic variables that are NOT designated inputs but are + * still grounded - notably values re-materialized by GETVALUE heap recovery (which call + * MAKE_SYMBOLIC with a fresh name, without re-registering an input). Dropping it would + * conservatively (but soundly) downgrade such cases; keeping it avoids that regression. + */ + private static final String INPUT_VAR_PATTERN = "[A-Z].*_[0-9].*"; + + /** + * Whether a branch constraint loses symbolic precision, given the terms of the designated symbolic + * inputs. It does iff it contains a symbol that is neither (a) a grounded variable - a designated + * input (its term is in {@code inputTerms}) or a recovery-named variable matching + * {@link #INPUT_VAR_PATTERN} - nor (b) a whitelisted generic pure UF (name starts with + * {@code pure_}). Case (b) is precision-preserving: an axiom-free UF over real inputs is a sound + * over-approximation of any deterministic function, so UNSAT under the free UF implies UNSAT for + * the real function (SAFE stays sound). Bespoke (axiomatized) UFs and any non-grounded variable + * do lose precision. + * + *

The primary input check is exact term identity against the designated inputs (JavaSMT + * formulas have value-based equals/hashCode), so it is correct for String/array inputs as well as + * primitives - which a name pattern alone is not. Uses a {@link DefaultFormulaVisitor} so UF + * symbols and variables are distinguished; it descends into UF arguments so a {@code pure_} UF + * applied to a non-input variable still loses precision (the nested variable is caught). + */ + public static boolean isPrecisionLoss( + BooleanFormula f, FormulaManager fmgr, Set inputTerms) { + AtomicBoolean lossy = new AtomicBoolean(false); + fmgr.visitRecursively( + f, + new DefaultFormulaVisitor() { + @Override + protected TraversalProcess visitDefault(Formula formula) { + return TraversalProcess.CONTINUE; + } + + @Override + public TraversalProcess visitFreeVariable(Formula formula, String name) { + if (!inputTerms.contains(formula) && !name.matches(INPUT_VAR_PATTERN)) { + lossy.set(true); + return TraversalProcess.ABORT; + } + return TraversalProcess.CONTINUE; + } + + @Override + public TraversalProcess visitFunction( + Formula formula, List args, FunctionDeclaration decl) { + // Descend into args regardless so nested non-input variables are caught; only a + // bespoke (non-pure_) UF taints the branch by itself. + if (decl.getKind() == FunctionDeclarationKind.UF + && !decl.getName().startsWith("pure_")) { + lossy.set(true); + return TraversalProcess.ABORT; + } + return TraversalProcess.CONTINUE; + } + }); + return lossy.get(); } protected static String encodeCoverage(InstrCoverage instrCoverage) throws JsonProcessingException { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTrace.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTrace.java index 4e980f4..1ee960c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTrace.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTrace.java @@ -25,9 +25,6 @@ class SymbolicTrace { // If true, an invocation occurred that was not instrumented but received symbolic arguments. private boolean symbolicContextLoss = false; - // If true, reference equality semantics may have changed due to comparing user-de-interned strings. - private boolean referenceSemanticChange = false; - /** Creates a new SymbolicTrace. */ public SymbolicTrace() { this.inputs = new ArrayList<>(); 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 6d99da5..c491e75 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 @@ -208,13 +208,12 @@ public void recordSymbolicContextLoss() { } /** - * Records that reference equality semantics may have changed. This happens when Objects.equals - * is called (via refEquals transformation) on strings where at least one was explicitly created - * with new String() in user code. In such cases, the original reference equality check would - * return false for different objects, but value equality returns true for equal content. + * Whether a symbolic context loss was recorded on this trace. Read-only accessor for the + * package-private trace flag; used by tests to observe soundness without parsing the TraceDTO. + * + * @return true if a symbolic context loss occurred. */ - public void recordReferenceSemanticChange() { - logger.warn("Reference semantic change detected: user-de-interned strings compared via Objects.equals"); - symbolicTrace.setReferenceSemanticChange(true); + public boolean isSymbolicContextLoss() { + return symbolicTrace.isSymbolicContextLoss(); } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java index e26780c..13306c0 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java @@ -16,10 +16,19 @@ public class BranchDTO { @SuppressWarnings("unused") private String inst; - public BranchDTO(long iid, String constraint, boolean branched) { + /** + * The executor's per-branch precision-loss verdict. Carried so a future explorer-side, + * CFG-reachability-aware decision can key it by {@link #iid} to a CFG node. The current verdict + * uses the aggregate {@code symbolicPrecisionLoss} on the TraceDTO (OR of these). + */ + @SuppressWarnings("unused") + private boolean precisionLoss; + + public BranchDTO(long iid, String constraint, boolean branched, boolean precisionLoss) { this.iid = iid; this.constraint = constraint; this.branched = branched; + this.precisionLoss = precisionLoss; this.type = "Branch"; } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java index 2f8b394..78a343f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java @@ -16,17 +16,13 @@ public class TraceDTO { private boolean symbolicContextLoss = false; @SuppressWarnings("unused") private boolean symbolicPrecisionLoss = false; - @SuppressWarnings("unused") - private boolean referenceSemanticChange = false; - public TraceDTO(ArrayList inputs, ArrayList trace, ArrayList ufs, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) { + public TraceDTO(ArrayList inputs, ArrayList trace, ArrayList ufs, boolean symbolicContextLoss, boolean symbolicPrecisionLoss) { this.trace = trace; this.inputs = inputs; this.ufs = ufs; this.symbolicContextLoss = symbolicContextLoss; this.symbolicPrecisionLoss = symbolicPrecisionLoss; - this.referenceSemanticChange = referenceSemanticChange; - } @SuppressWarnings("unused") diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/PlaceHolder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/PlaceHolder.java index 24a2683..b1dc274 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/PlaceHolder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/PlaceHolder.java @@ -8,6 +8,7 @@ import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.LongValue; import de.uzl.its.swat.symbolic.value.reference.ObjectValue; import java.util.Map; +import org.sosy_lab.java_smt.api.Formula; /** Author: Koushik Sen (ksen@cs.berkeley.edu) Date: 6/17/12 Time: 6:05 PM */ public class PlaceHolder extends Value { @@ -34,13 +35,30 @@ public enum ValueOrigin { UNSPECIFIED, DATABASE, GETFIELD, - GETSTATIC + GETSTATIC, + // The return value of an unmodeled method (tagged in InvocationHandler). At recovery, a result + // with this origin is NOT identity-recovered (which would re-bind the receiver). If it carries a + // pure_ UF (recoveredFormula, a whitelisted pure method returning a String or primitive) it + // is modeled as that UF; otherwise a value-typed result is concretized. + UNMODELED_RETURN } public final boolean isSymbolic; public final ValueOrigin origin; public final Instruction inst; public final ObjectValue referenceValue; + /** + * For an UNMODELED_RETURN placeholder of a whitelisted pure method: the generic UF formula + * {@code pure_(inputs)} modeling the result. Null otherwise (recovery then concretizes). + */ + public final Formula recoveredFormula; + /** + * The same generic UF applied to the CONSTANT (observed) inputs, e.g. + * {@code pure_(makeString(concreteInput))}. At recovery this is asserted equal to the + * observed concrete output to record a ground (input -> output) pair. Null when no pair is + * emitted (non-String inputs, or not a whitelisted pure call). + */ + public final Formula observedApplication; public static final PlaceHolder instance = new PlaceHolder(false); public static final PlaceHolder symbolicInstance = new PlaceHolder(true); @@ -49,6 +67,8 @@ public PlaceHolder(boolean isSymbolic) { this.origin = ValueOrigin.UNSPECIFIED; this.inst = null; this.referenceValue = null; + this.recoveredFormula = null; + this.observedApplication = null; } public PlaceHolder(ValueOrigin origin, Instruction inst, ObjectValue referenceValue) { @@ -56,6 +76,8 @@ public PlaceHolder(ValueOrigin origin, Instruction inst, ObjectValue refer this.isSymbolic = false; this.inst = inst; this.referenceValue = referenceValue; + this.recoveredFormula = null; + this.observedApplication = null; } public PlaceHolder(boolean isSymbolic, ValueOrigin origin) { @@ -63,6 +85,26 @@ public PlaceHolder(boolean isSymbolic, ValueOrigin origin) { this.origin = origin; this.inst = null; this.referenceValue = null; + this.recoveredFormula = null; + this.observedApplication = null; + } + + /** + * UNMODELED_RETURN placeholder. {@code referenceValue} is the receiver of the unmodeled call + * (null for static calls); recovery uses it to tell a returned distinct tracked value from a + * this-return. For a whitelisted pure method it also carries the generic UF over the symbolic + * inputs ({@code recoveredFormula}, modeling the result) and the same UF over the constant + * observed inputs ({@code observedApplication}, used to record the observed pair). Any of these + * may be null. + */ + public PlaceHolder(ValueOrigin origin, ObjectValue referenceValue, + Formula recoveredFormula, Formula observedApplication) { + this.origin = origin; + this.isSymbolic = false; + this.inst = null; + this.referenceValue = referenceValue; + this.recoveredFormula = recoveredFormula; + this.observedApplication = observedApplication; } public ObjectValue asObjectValue() throws ValueConversionException { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java index fe32e31..e31de7b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java @@ -20,6 +20,10 @@ import java.util.*; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.SolverContext; public class ValueFactory { @@ -41,6 +45,29 @@ public class ValueFactory { }; } + /** + * Build a primitive value of {@code type} carrying an explicit symbolic {@code formula} (its + * concrete is the observed result). Used to model a whitelisted pure primitive return as a + * generic UF over its inputs. The formula's sort MUST match the value's sort (see + * {@code InvocationHandler#pureUFReturnType}): bitvector of width 8/16/16/32/64 for + * byte/short/char/int/long, floating-point for float/double, boolean for boolean. + */ + public static NumericalValue createNumericalValue(ValueType type, Object concrete, Formula formula) + throws NoThreadContextException, TypeException { + SolverContext context = ThreadHandler.getSolverContext(Thread.currentThread().getId()); + return switch (type) { + case intValue -> new IntValue(context, (int) concrete, (BitvectorFormula) formula); + case longValue -> new LongValue(context, (long) concrete, (BitvectorFormula) formula); + case shortValue -> new ShortValue(context, (short) concrete, (BitvectorFormula) formula); + case byteValue -> new ByteValue(context, (byte) concrete, (BitvectorFormula) formula); + case charValue -> new CharValue(context, (char) concrete, (BitvectorFormula) formula); + case booleanValue -> new BooleanValue(context, (boolean) concrete, (BooleanFormula) formula); + case floatValue -> new FloatValue(context, (float) concrete, (FloatingPointFormula) formula); + case doubleValue -> new DoubleValue(context, (double) concrete, (FloatingPointFormula) formula); + default -> throw new TypeException(type); + }; + } + public static AbstractArrayValue createArrayValue( ValueType type, IntValue size, int address) throws NoThreadContextException, TypeException { SolverContext context = ThreadHandler.getSolverContext(Thread.currentThread().getId()); 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 ebba905..2b0d17c 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 @@ -30,15 +30,6 @@ public class StringValue extends ObjectValue { static final int REPLACE_COUNT = 10; private StringFormulaManager smgr; - /** - * Flag indicating this string was explicitly created via new String() in user code, - * as opposed to being de-interned by SWAT's NoCacheMethodAdapter. - * When true, reference equality comparisons on this string may have different - * semantics than the original code intended. - */ - @Getter - private boolean userDeInterned = false; - public StringValue(SolverContext context, String concrete, int address) { super(context, address); this.smgr = context.getFormulaManager().getStringFormulaManager(); @@ -219,9 +210,6 @@ public BooleanFormula getBounds(boolean upper) { this.concrete = s.concrete; this.formula = s.formula; } - // Mark this string as user-de-interned since it was created via new String() - // in user code (as opposed to SWAT's NoCacheMethodAdapter de-interning) - this.userDeInterned = true; return VoidValue.instance; } diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/ProvenanceRefEqualsSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/ProvenanceRefEqualsSpec.groovy new file mode 100644 index 0000000..a4cf01e --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/ProvenanceRefEqualsSpec.groovy @@ -0,0 +1,69 @@ +package de.uzl.its.swat.common + +import spock.lang.Specification + +/** + * Reference equality modeled by original identity through the provenance map. Two de-interned copies + * that root to the same canonical compare equal; distinct canonicals compare unequal; non-de-interned + * classes fall back to plain reference equality. + */ +class ProvenanceRefEqualsSpec extends Specification { + + def "de-interned Strings rooting to the same interned canonical compare equal"() { + given: "two distinct de-interned copies of the same literal, both rooted to the interned canonical" + String canonical = "shared-abc".intern() + String a = new String("shared-abc") + String b = new String("shared-abc") + Provenance.record(a, canonical) + Provenance.record(b, canonical) + + expect: "they are distinct objects (so a==b reference would be false)" + !a.is(b) + and: "but refEquals compares roots -> same canonical -> equal (matches real interned ==)" + UtilInstrumented.refEquals(a, b) + } + + def "a de-interned copy vs a same-valued object with a different root compares unequal"() { + given: "a rooted to the interned canonical; b has no provenance entry (root(b)=b)" + String a = new String("shared-x") + Provenance.record(a, "shared-x".intern()) + String b = new String("shared-x") + + expect: "distinct roots -> unequal (matches real new String(\"x\") == \"x\" -> false)" + !UtilInstrumented.refEquals(a, b) + } + + def "boxed copies rooting to the cached canonical compare equal (cache range)"() { + given: + Integer a = new Integer(100) + Integer b = new Integer(100) + Provenance.record(a, Integer.valueOf(100)) + Provenance.record(b, Integer.valueOf(100)) + + expect: "both root to the one cached Integer(100) -> equal (matches real valueOf(100)==valueOf(100))" + !a.is(b) + UtilInstrumented.refEquals(a, b) + } + + def "non-de-interned classes use plain reference equality"() { + given: + Object a = new Object() + Object b = new Object() + + expect: "Object is not a de-interned class -> refEquals falls back to a==b" + !UtilInstrumented.refEquals(a, b) + UtilInstrumented.refEquals(a, a) + } + + def "root collapses chains at insert"() { + given: "c rooted to b, b rooted to canonical -> root(c) must resolve to canonical" + String canonical = "shared-chain".intern() + String b = new String("shared-chain") + Provenance.record(b, canonical) + String c = new String("shared-chain") + Provenance.record(c, b) + + expect: + Provenance.root(c).is(canonical) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/UtilClassNameSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/UtilClassNameSpec.groovy new file mode 100644 index 0000000..25624bf --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/common/UtilClassNameSpec.groovy @@ -0,0 +1,59 @@ +package de.uzl.its.swat.common + +import de.uzl.its.swat.common.exceptions.SWATAssert +import spock.lang.Specification +import spock.lang.Unroll + +/** + * Unit test for {@link Util#formatClassName} and the private {@code checkClassName} guard behind it. + * + *

The guard's sole job is to reject type descriptors (object {@code Lxxx;}, method + * {@code (..)X}) passed where a class name is expected — in either spelling: dotted/binary + * ({@code a.b.C}) or internal/slashed ({@code a/b/C}). {@code formatClassName} canonicalizes to the + * internal form. + * + *

A class name beginning with 'L' (e.g. a default-package target named {@code LitSymTarget}) is a + * valid class name, not an object descriptor, so the guard must accept it: object descriptors are + * distinguished by their trailing {@code ';'}, not by a leading 'L'. This pins both halves of the + * contract: L-prefixed class names round-trip, real descriptors still throw. + */ +class UtilClassNameSpec extends Specification { + + def setup() { + // checkClassName routes failures through SWATAssert; make the guard deterministically active + // regardless of any earlier spec that may have toggled it. The test task sets exitOnError=false, + // so a failed assertion rethrows (catchable) rather than halting the JVM. + SWATAssert.setEnabled(true) + } + + @Unroll + def "formatClassName accepts class name '#name' and canonicalizes to '#expected'"() { + expect: + Util.formatClassName(name) == expected + + where: + name || expected + "LitSymTarget" || "LitSymTarget" // the regression case: default-package, L-prefixed + "Long" || "Long" + "List" || "List" + "java.lang.Long" || "java/lang/Long" // dotted -> slashed + "java/lang/String" || "java/lang/String" // already internal -> idempotent + } + + @Unroll + def "formatClassName still rejects the type descriptor '#descriptor'"() { + when: + Util.formatClassName(descriptor) + + then: + thrown(AssertionError) + + where: + descriptor << ["Ljava/lang/String;", "Lfoo/Bar;", "(I)V", "(Ljava/lang/String;)V"] + } + + def "formatClassName skips the check for array descriptors (early return, not rejected)"() { + expect: "arrays are intentionally skipped by checkClassName, so they pass through unchanged" + Util.formatClassName("[I") == "[I" + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/BaseValueSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/BaseValueSpec.groovy new file mode 100644 index 0000000..7dc1f6d --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/BaseValueSpec.groovy @@ -0,0 +1,62 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.thread.ThreadHandler +import org.sosy_lab.java_smt.api.BooleanFormula +import org.sosy_lab.java_smt.api.FormulaManager +import org.sosy_lab.java_smt.api.ProverEnvironment +import org.sosy_lab.java_smt.api.SolverContext +import spock.lang.Specification + +import static java.lang.Thread.currentThread + +/** + * Level L0 base: a clean Z3 {@link SolverContext} per test for constructing {@code Value} objects + * and shadow structures directly (no instrumentation, no instruction stream). Mirrors the proven + * {@code StringValueTest} setup. See docs/test-architecture.md (Level L0). + * + * Oracle helpers evaluate {@link BooleanFormula}s via SAT/UNSAT agreement with a real prover — + * never by inspecting the formula's representation. + */ +abstract class BaseValueSpec extends Specification { + + protected SolverContext context + protected FormulaManager fmgr + + def setup() { + ThreadHandler.init() + if (ThreadHandler.hasThreadContext(currentThread().id)) { + ThreadHandler.removeThreadContext(currentThread().id) + } + ThreadHandler.addThreadContext(currentThread().id, "Test-Thread", -2) + context = ThreadHandler.getSolverContext(currentThread().id) + fmgr = context.getFormulaManager() + } + + def cleanup() { + if (ThreadHandler.hasThreadContext(currentThread().id)) { + ThreadHandler.removeThreadContext(currentThread().id) + } + } + + /** True iff {@code f} is valid (always true): {@code not(f)} is unsatisfiable. */ + protected boolean isValid(BooleanFormula f) { + ProverEnvironment p = context.newProverEnvironment() + try { + p.addConstraint(fmgr.getBooleanFormulaManager().not(f)) + return p.isUnsat() + } finally { + p.close() + } + } + + /** True iff {@code f} is unsatisfiable (always false). */ + protected boolean isUnsatisfiable(BooleanFormula f) { + ProverEnvironment p = context.newProverEnvironment() + try { + p.addConstraint(f) + return p.isUnsat() + } finally { + p.close() + } + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/BoxedDeInternAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/BoxedDeInternAgentSpec.groovy new file mode 100644 index 0000000..4ec86c6 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/BoxedDeInternAgentSpec.groovy @@ -0,0 +1,27 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.testsupport.agent.AgentRun +import de.uzl.its.swat.testsupport.agent.TraceObservation +import spock.lang.Specification + +/** + * End-to-end check that the boxed de-intern instrumentation produces JVM-valid bytecode. The real agent + * runs a program driving both emitted paths: the unbox+rebox wrap on un-instrumented valueOf(String) + * returns for Integer and Long, and the valueOf(primitive)->new rewrite via autoboxing for all six + * wrappers (Integer, Long, Short, Byte, Character, Boolean). The run completing (exit 0 plus a parsed + * trace) is the oracle: a malformed wrap or rewrite would raise a VerifyError. Object-identity effects + * are covered by OutputDeInternSpec and the boxed-cache equality semantics by ProvenanceRefEqualsSpec. + */ +class BoxedDeInternAgentSpec extends Specification { + + def "all six wrappers' valueOf-rewrite and Integer/Long de-intern load, verify, and run"() { + when: "the agent runs a program driving the boxed de-intern bytecode paths" + TraceObservation obs = AgentRun.run("targets/BoxedReturnTarget.java", "BoxedReturnTarget") + + then: "the run completed (exit 0 + parsed trace) - the unbox+rebox wrap is verifier-valid" + obs != null + + and: "the symbolic input was designated and traced" + !obs.inputNames.isEmpty() + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ContainerRecoveryAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ContainerRecoveryAgentSpec.groovy new file mode 100644 index 0000000..f9b1800 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ContainerRecoveryAgentSpec.groovy @@ -0,0 +1,26 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.testsupport.agent.AgentRun +import de.uzl.its.swat.testsupport.agent.TraceObservation +import spock.lang.Specification + +/** + * End-to-end check that a value retrieved from an unmodeled container keeps its symbolic value. The + * agent stores a symbolic String in a HashMap and reads it back via a concrete key; recovering the + * stored shadow (rather than concretizing) means a branch on the retrieved value still references the + * symbolic input, so the solver can drive it. + */ +class ContainerRecoveryAgentSpec extends Specification { + + def "a value retrieved from an unmodeled container keeps its symbolic formula"() { + when: + TraceObservation obs = AgentRun.run("targets/ContainerRecoveryTarget.java", "ContainerRecoveryTarget") + String inputVar = obs.inputNames.find { it.startsWith("java/lang/String") } + + then: "the symbolic input is designated" + inputVar != null + + and: "the branch on the retrieved value references the symbolic input (recovered, not concretized)" + obs.anyBranchReferences(inputVar) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/FlagPolicySpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/FlagPolicySpec.groovy new file mode 100644 index 0000000..7cb8c26 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/FlagPolicySpec.groovy @@ -0,0 +1,40 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.common.Util +import de.uzl.its.swat.symbolic.processor.BaseSymbolicInstructionProcessorSpec +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue + +/** + * Context-loss flag policy: the flag fires if and only if symbolic data flowed into an unmodeled call. + * A concrete receiver raises no flag; a symbolic receiver raises the flag. + */ +class FlagPolicySpec extends BaseSymbolicInstructionProcessorSpec { + + private static final String STRING = "java/lang/String" + private static final String TO_LOWER = "()Ljava/lang/String;" + + def "an unmodeled call with a concrete receiver raises no context-loss flag"() { + given: + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + StringValue receiver = new StringValue(solverContext, "abc", 0x1000) // concrete (not made symbolic) + + when: + def result = executeBoundaryRecovery(receiver, STRING, "toLowerCase", TO_LOWER, "abc") + + then: "no symbolic data flowed into the black box, so no context loss" + !result.contextLoss + } + + def "an unmodeled call with a symbolic receiver raises a context-loss flag"() { + given: + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + StringValue receiver = new StringValue(solverContext, "abc", 0x1000) + receiver.MAKE_SYMBOLIC() + + when: + def result = executeBoundaryRecovery(receiver, STRING, "toLowerCase", TO_LOWER, "abc") + + then: "symbolic data reached the unmodeled method, so context loss is flagged" + result.contextLoss + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/HeapRecoveryAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/HeapRecoveryAgentSpec.groovy new file mode 100644 index 0000000..247482f --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/HeapRecoveryAgentSpec.groovy @@ -0,0 +1,32 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.testsupport.agent.AgentRun +import de.uzl.its.swat.testsupport.agent.TraceObservation +import spock.lang.Specification + +/** + * End-to-end recovery: the agent runs a real {@code @Symbolic} toLowerCase program and the emitted + * TraceDTO is observed. The identity hash, the this-return and the soundness flags come from the + * real JVM and instrumenter rather than a fabricated instruction stream. + */ +class HeapRecoveryAgentSpec extends Specification { + + def "real toLowerCase on a symbolic string flags context loss"() { + when: + TraceObservation obs = AgentRun.run("targets/ToLowerCaseTarget.java", "ToLowerCaseTarget") + + then: "the symbolic input is designated and the soundness backstop (context loss) fires" + obs.inputNames.any { it.startsWith("java/lang/String") } + obs.symbolicContextLoss + } + + def "a branch after unmodeled toLowerCase does not reference the symbolic input"() { + when: + TraceObservation obs = AgentRun.run("targets/ToLowerCaseTarget.java", "ToLowerCaseTarget") + String inputVar = obs.inputNames.find { it.startsWith("java/lang/String") } + + then: "the result is concrete, so no branch constraint mentions the input" + inputVar != null + !obs.anyBranchReferences(inputVar) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ObjectIdentitySpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ObjectIdentitySpec.groovy new file mode 100644 index 0000000..9d6e8b2 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ObjectIdentitySpec.groovy @@ -0,0 +1,70 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.symbolic.shadow.ShadowContext +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue +import de.uzl.its.swat.symbolic.value.reference.ObjectValue + +/** + * Object reference-equality and the canonical registry. The registry keys the heap by the concrete + * object reference (identity), so it returns one canonical wrapper per concrete object and keeps + * distinct objects distinct even when their identity hashes collide. {@code ObjectValue.IF_ACMPEQ} + * stays {@code this == o2}, which is correct under that one-wrapper-per-identity guarantee. These + * specs assert both: the same object recovers the same wrapper and compares equal, while distinct + * objects stay distinct wrappers and compare unequal. + */ +class ObjectIdentitySpec extends BaseValueSpec { + + private ObjectValue objectAt(int address) { + return new ObjectValue(context, "de/uzl/its/swat/test/Obj", new IntValue(context, 1), address) + } + + def "two references to distinct objects compare reference-unequal"() { + given: + ObjectValue a = objectAt(0x2000) + ObjectValue c = objectAt(0x3000) + + expect: + isUnsatisfiable(a.IF_ACMPEQ(c)) + } + + def "the same concrete object recovers the same canonical wrapper (reference-equal)"() { + given: "a shadow registered under a concrete object" + Object obj = new Object() + ObjectValue shadow = objectAt(0x2000) + ShadowContext ctx = new ShadowContext() + ctx.putToHeap(obj, shadow) + + when: "the same concrete object is looked up twice" + def a = ctx.getFromHeap(obj) + def b = ctx.getFromHeap(obj) + + then: "both recover the same wrapper, so they compare reference-equal" + a.is(b) + isValid((a as ObjectValue).IF_ACMPEQ(b as ObjectValue)) + } + + def "distinct objects with a colliding identity hash compare reference-unequal"() { + given: "two distinct objects whose identity hash (address) collides" + ObjectValue a = objectAt(0x5000) + ObjectValue b = objectAt(0x5000) + + expect: "they are still distinct references" + isUnsatisfiable(a.IF_ACMPEQ(b)) + } + + def "distinct concrete objects are stored without merging (reference keying)"() { + given: "two distinct concrete objects, with shadows that happen to share an address" + Object o1 = new Object() + Object o2 = new Object() + ObjectValue a = objectAt(0x5000) + ObjectValue b = objectAt(0x5000) + + when: "both are registered under their concrete references" + ShadowContext shadow = new ShadowContext() + shadow.putToHeap(o1, a) + shadow.putToHeap(o2, b) + + then: "the reference-keyed registry keeps distinct objects as distinct entries" + shadow.heapSize() == 2 + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/OutOfBandDetectionSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/OutOfBandDetectionSpec.groovy new file mode 100644 index 0000000..bb05d25 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/OutOfBandDetectionSpec.groovy @@ -0,0 +1,75 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.common.Util +import de.uzl.its.swat.config.Config +import de.uzl.its.swat.instrument.GlobalStateForInstrumentation +import de.uzl.its.swat.symbolic.SymbolicInstructionVisitor +import de.uzl.its.swat.symbolic.instruction.GETVALUE_int +import de.uzl.its.swat.symbolic.instruction.Instruction +import de.uzl.its.swat.symbolic.instruction.NOP +import de.uzl.its.swat.symbolic.processor.BaseSymbolicInstructionProcessorSpec +import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor +import de.uzl.its.swat.symbolic.shadow.ShadowDivergence +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue +import de.uzl.its.swat.thread.ThreadHandler + +/** + * Out-of-band change detection at a primitive GETVALUE sync. When the value the real JVM produced + * diverges from the tracked shadow's concrete (for example, a field mutated inside unmodeled code), the + * {@code shadowDivergence=FLAG} policy handles it gracefully: it records context loss, adopts the + * observed concrete, and does not throw, unlike the CRASH policy's hard assert. + */ +class OutOfBandDetectionSpec extends BaseSymbolicInstructionProcessorSpec { + + private ShadowDivergence savedPolicy + + def setup() { + savedPolicy = Config.instance().getShadowDivergence() + } + + def cleanup() { + Config.instance().setShadowDivergence(savedPolicy) + } + + /** Drives a single GETVALUE_int(observed) over the current operand-stack top. */ + private void runGetValueInt(int observed) { + List instructions = new ArrayList<>() + instructions.add(new GETVALUE_int(GlobalStateForInstrumentation.instance.incAndGetId(), observed, 0)) + instructions.add(new NOP(GlobalStateForInstrumentation.instance.incAndGetId())) + // setCurrent(first); processing the next visits the *current* (execution is one behind). + ThreadHandler.setCurrentInstruction(threadId, instructions.remove(0)) + SymbolicInstructionProcessor processor = new SymbolicInstructionProcessor() + while (!instructions.isEmpty()) { + processor.processInstruction(instructions.remove(0)) + } + } + + def "under FLAG a diverging primitive GETVALUE is flagged and re-grounded, not crashed"() { + given: "a tracked int shadow with concrete 10, under the FLAG policy" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + Config.instance().setShadowDivergence(ShadowDivergence.FLAG) + SymbolicInstructionVisitor visitor = ThreadHandler.getSymbolicVisitor(threadId) + visitor.getStack().pushOperand(new IntValue(solverContext, 10)) + + when: "the real JVM produced a different value (20) for that slot - an out-of-band change" + runGetValueInt(20) + + then: "no crash; context loss flagged; the operand is re-grounded to the observed concrete" + ThreadHandler.getSymbolicTraceHandler(threadId).isSymbolicContextLoss() + visitor.getStack().getActiveFrame().peek().concrete == 20 + } + + def "under FLAG a matching primitive GETVALUE records no context-loss flag"() { + given: + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + Config.instance().setShadowDivergence(ShadowDivergence.FLAG) + SymbolicInstructionVisitor visitor = ThreadHandler.getSymbolicVisitor(threadId) + visitor.getStack().pushOperand(new IntValue(solverContext, 10)) + + when: "the observed value matches the shadow" + runGetValueInt(10) + + then: "no divergence, so no context-loss flag" + !ThreadHandler.getSymbolicTraceHandler(threadId).isSymbolicContextLoss() + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/OutputDeInternSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/OutputDeInternSpec.groovy new file mode 100644 index 0000000..de6c4d3 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/OutputDeInternSpec.groovy @@ -0,0 +1,111 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.common.Util +import de.uzl.its.swat.instrument.GlobalStateForInstrumentation +import de.uzl.its.swat.symbolic.SymbolicInstructionVisitor +import de.uzl.its.swat.symbolic.instruction.GETVALUE_Object +import de.uzl.its.swat.symbolic.instruction.Instruction +import de.uzl.its.swat.symbolic.instruction.NOP +import de.uzl.its.swat.symbolic.processor.BaseSymbolicInstructionProcessorSpec +import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor +import de.uzl.its.swat.symbolic.value.Value +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue +import de.uzl.its.swat.symbolic.value.reference.ObjectValue +import de.uzl.its.swat.symbolic.value.reference.lang.IntegerObjectValue +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import de.uzl.its.swat.thread.ThreadHandler + +/** + * Registration policy at value-typed GETVALUE recovery. A de-interned value type (String or a cached + * boxed wrapper) whose shadow carries symbolic content is heap-registered so it round-trips through + * untracked space, while a pure-constant shadow is not registered because it is reconstructible from + * the observed concrete. Mutable (non-value-type) objects on the shared recovery path stay + * unconditionally registered. + */ +class OutputDeInternSpec extends BaseSymbolicInstructionProcessorSpec { + + /** Recover an object at ADDRESS_UNKNOWN: push the shadow, then drive GETVALUE_Object. */ + private void recover(Value shadow, Object obj) { + SymbolicInstructionVisitor visitor = ThreadHandler.getSymbolicVisitor(threadId) + visitor.getStack().pushOperand(shadow) + List instructions = new ArrayList<>() + instructions.add(new GETVALUE_Object(GlobalStateForInstrumentation.instance.incAndGetId(), + System.identityHashCode(obj), obj, 0)) + instructions.add(new NOP(GlobalStateForInstrumentation.instance.incAndGetId())) + // setCurrent(first); processing the next visits the *current* (execution is one behind). + ThreadHandler.setCurrentInstruction(threadId, instructions.remove(0)) + SymbolicInstructionProcessor processor = new SymbolicInstructionProcessor() + while (!instructions.isEmpty()) { + processor.processInstruction(instructions.remove(0)) + } + } + + def "a symbolic String shadow is heap-registered so it can round-trip"() { + given: "a symbolic String shadow awaiting its address (ADDRESS_UNKNOWN)" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + String obj = "symbolic-abc" + StringValue shadow = new StringValue(solverContext, obj, ObjectValue.ADDRESS_UNKNOWN) + shadow.MAKE_SYMBOLIC() + + when: "the value is recovered" + recover(shadow, obj) + + then: "it is registered, so an untracked round-trip can recover the symbolic shadow" + ThreadHandler.getSymbolicVisitor(threadId).getStack().getFromHeap(obj) != null + } + + def "a constant String shadow is not heap-registered since it is reconstructible"() { + given: "a pure-constant String shadow (formula = makeString) awaiting its address" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + String obj = "constant-xyz" + StringValue shadow = new StringValue(solverContext, obj, ObjectValue.ADDRESS_UNKNOWN) + + when: "the value is recovered" + recover(shadow, obj) + + then: "it is NOT registered - reconstructible from the observed concrete, so no leak" + ThreadHandler.getSymbolicVisitor(threadId).getStack().getFromHeap(obj) == null + } + + def "a symbolic boxed shadow is heap-registered so it can round-trip"() { + given: "a symbolic Integer shadow awaiting its address (formula carried by the inner IntValue)" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + Integer obj = 7 + IntValue inner = new IntValue(solverContext, obj) + inner.MAKE_SYMBOLIC() + IntegerObjectValue shadow = new IntegerObjectValue(solverContext, inner, ObjectValue.ADDRESS_UNKNOWN) + + when: "the value is recovered" + recover(shadow, obj) + + then: "it is registered, so an untracked round-trip can recover the symbolic boxed shadow" + ThreadHandler.getSymbolicVisitor(threadId).getStack().getFromHeap(obj) != null + } + + def "a constant boxed shadow is not heap-registered since it is reconstructible"() { + given: "a pure-constant Integer shadow awaiting its address" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + Integer obj = 7 + IntegerObjectValue shadow = + new IntegerObjectValue(solverContext, new IntValue(solverContext, obj), ObjectValue.ADDRESS_UNKNOWN) + + when: "the value is recovered" + recover(shadow, obj) + + then: "it is NOT registered - a constant boxed value is reconstructible from the observed concrete" + ThreadHandler.getSymbolicVisitor(threadId).getStack().getFromHeap(obj) == null + } + + def "a mutable non-value-type object is always heap-registered"() { + given: "a plain mutable object whose class is not de-interned" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + Object obj = new Object() + ObjectValue shadow = new ObjectValue(solverContext, ObjectValue.ADDRESS_UNKNOWN) + + when: "the value is recovered" + recover(shadow, obj) + + then: "a mutable object is still heap-registered - it has a sound identity key and must be tracked" + ThreadHandler.getSymbolicVisitor(threadId).getStack().getFromHeap(obj) != null + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PrecisionLossExemptionSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PrecisionLossExemptionSpec.groovy new file mode 100644 index 0000000..e48c7cd --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PrecisionLossExemptionSpec.groovy @@ -0,0 +1,64 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.symbolic.trace.DTOBuilder +import org.sosy_lab.java_smt.api.BooleanFormula +import org.sosy_lab.java_smt.api.Formula +import org.sosy_lab.java_smt.api.FormulaType +import org.sosy_lab.java_smt.api.StringFormula + +/** + * Precision-loss exemption for pure uninterpreted functions. {@link DTOBuilder#isPrecisionLoss} + * treats a whitelisted generic {@code pure_} UF over designated inputs as precision-preserving (an + * axiom-free UF over inputs over-approximates any deterministic function, so UNSAT under the free UF + * implies real UNSAT and SAFE holds), while a non-input variable or a bespoke (non-{@code pure_}) UF + * still loses precision. Input-ness is decided by exact term identity against the designated inputs + * rather than a name pattern, so it also holds for String inputs named {@code java/lang/String_0}. + */ +class PrecisionLossExemptionSpec extends BaseValueSpec { + + // A realistic String input variable name: lowercase plus slashes. + private StringFormula inputVar() { fmgr.getStringFormulaManager().makeVariable("java/lang/String_0") } + private StringFormula otherVar() { fmgr.getStringFormulaManager().makeVariable("intermediate") } + + private Set inputs(StringFormula... terms) { return terms.toList() as Set } + + private StringFormula ufOver(String ufName, StringFormula arg) { + def decl = fmgr.getUFManager().declareUF(ufName, FormulaType.StringType, FormulaType.StringType) + return (StringFormula) fmgr.getUFManager().callUF(decl, arg) + } + + private BooleanFormula eqAbc(StringFormula s) { + return fmgr.getStringFormulaManager().equal(s, fmgr.getStringFormulaManager().makeString("abc")) + } + + def "a designated input variable alone is not precision loss, including a String input"() { + given: + def v = inputVar() + expect: + !DTOBuilder.isPrecisionLoss(eqAbc(v), fmgr, inputs(v)) + } + + def "a non-input variable is precision loss"() { + expect: + DTOBuilder.isPrecisionLoss(eqAbc(otherVar()), fmgr, inputs(inputVar())) + } + + def "a pure_ UF over an input variable is NOT precision loss (the exemption)"() { + given: + def v = inputVar() + expect: + !DTOBuilder.isPrecisionLoss(eqAbc(ufOver("pure_String_trim", v)), fmgr, inputs(v)) + } + + def "a pure_ UF over a NON-input variable is still precision loss (transitivity)"() { + expect: + DTOBuilder.isPrecisionLoss(eqAbc(ufOver("pure_String_trim", otherVar())), fmgr, inputs(inputVar())) + } + + def "a bespoke (non-pure_) UF stays non-exempt (precision loss)"() { + given: + def v = inputVar() + expect: + DTOBuilder.isPrecisionLoss(eqAbc(ufOver("toLowerCase", v)), fmgr, inputs(v)) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionPrimitiveAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionPrimitiveAgentSpec.groovy new file mode 100644 index 0000000..ae2f360 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionPrimitiveAgentSpec.groovy @@ -0,0 +1,36 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.testsupport.agent.AgentRun +import de.uzl.its.swat.testsupport.agent.TraceObservation +import spock.lang.Specification + +/** + * End-to-end check that pure, unmodeled, primitive-returning java.lang methods + * (Math.floorDiv/floorMod/cbrt, Float.intBitsToFloat, Character.toLowerCase/isDigit) on symbolic + * inputs are each modeled as a generic {@code pure_} UF over their inputs, across the + * int/long/double/float/char/boolean return sorts. The run preserves SAFE: no context loss, no + * precision loss, and the UFs ride into the branch constraints. + */ +class PureFunctionPrimitiveAgentSpec extends Specification { + + def "pure primitive-returning methods are modeled as UFs (no context or precision loss)"() { + when: "the agent runs a program branching on pure unmodeled primitive returns over symbolic inputs" + TraceObservation obs = AgentRun.run("targets/PurePrimReturnTarget.java", "PurePrimReturnTarget") + + then: "the run completed and a symbolic input was designated" + obs != null + !obs.inputNames.isEmpty() + + and: "modeling the pure returns as UFs loses neither context nor precision" + !obs.symbolicContextLoss + !obs.symbolicPrecisionLoss + + and: "the generic UFs actually entered the branch constraints (precision genuinely preserved)" + obs.anyBranchReferences("pure_Math_floorDiv_int_int") // int return + obs.anyBranchReferences("pure_Math_floorDiv_long_long") // long return + obs.anyBranchReferences("pure_Math_cbrt_double") // double return + obs.anyBranchReferences("pure_Float_intBitsToFloat_int") // float return + obs.anyBranchReferences("pure_Character_toLowerCase_char") // char return + obs.anyBranchReferences("pure_Character_isDigit_char") // boolean return + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionUFAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionUFAgentSpec.groovy new file mode 100644 index 0000000..39d3b79 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionUFAgentSpec.groovy @@ -0,0 +1,46 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.testsupport.agent.AgentRun +import de.uzl.its.swat.testsupport.agent.TraceObservation +import spock.lang.Specification + +/** + * End-to-end check that the agent runs a {@code @Symbolic} program calling a whitelisted pure + * unmodeled method ({@code String.trim()}) and branching on its result. The emitted trace shows the + * relationship preserved (the branch references the input through the {@code pure_String_trim} UF) + * and neither soundness flag set, so a SAFE verdict survives the call. + */ +class PureFunctionUFAgentSpec extends Specification { + + def "a whitelisted pure trim into a branch preserves SAFE (no context or precision loss)"() { + when: + TraceObservation obs = AgentRun.run("targets/TrimTarget.java", "TrimTarget") + String inputVar = obs.inputNames.find { it.startsWith("java/lang/String") } + + then: "the symbolic input is designated" + inputVar != null + + and: "the relationship is preserved - the branch references the input through the UF" + obs.anyBranchReferences(inputVar) + + and: "neither SAFE downgrade fires: context loss is skipped because modeled, and the pure_ UF is exempt" + !obs.symbolicContextLoss + !obs.symbolicPrecisionLoss + } + + def "a whitelisted pure substring (arg-taking, mixed-sort UF) into a branch preserves SAFE"() { + when: + TraceObservation obs = AgentRun.run("targets/SubstringTarget.java", "SubstringTarget") + String inputVar = obs.inputNames.find { it.startsWith("java/lang/String") } + + then: "the symbolic input is designated" + inputVar != null + + and: "the branch references the input through the mixed-sort UF pure_String_substring_int" + obs.anyBranchReferences(inputVar) + + and: "neither SAFE downgrade fires (an arg-taking whitelisted method stays sound)" + !obs.symbolicContextLoss + !obs.symbolicPrecisionLoss + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionUFSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionUFSpec.groovy new file mode 100644 index 0000000..2dd1f95 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureFunctionUFSpec.groovy @@ -0,0 +1,126 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.common.Util +import de.uzl.its.swat.symbolic.processor.BaseSymbolicInstructionProcessorSpec +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import de.uzl.its.swat.thread.ThreadHandler +import org.sosy_lab.java_smt.api.BooleanFormula +import org.sosy_lab.java_smt.api.Formula +import org.sosy_lab.java_smt.api.StringFormula + +/** + * Verifies that a whitelisted, pure, unmodeled value-returning call ({@code String.trim}) on a + * symbolic input is modeled as the uninterpreted function {@code pure_String_trim} over that input + * instead of being concretized. This preserves the relational fact (equal inputs imply equal + * outputs) while staying sound, because the UF is axiom-free. + */ +class PureFunctionUFSpec extends BaseSymbolicInstructionProcessorSpec { + + private static final String STRING = "java/lang/String" + private static final String TRIM = "()Ljava/lang/String;" + + private Set symbolsOf(value) { + return solverContext.getFormulaManager().extractVariablesAndUFs(value.formula as Formula).keySet() + } + + private Set varsOf(value) { + return solverContext.getFormulaManager().extractVariables(value.formula as Formula).keySet() + } + + private boolean isValid(BooleanFormula f) { + def p = solverContext.newProverEnvironment() + try { + p.addConstraint(solverContext.getFormulaManager().getBooleanFormulaManager().not(f)) + return p.isUnsat() + } finally { p.close() } + } + + private boolean isSat(BooleanFormula f) { + def p = solverContext.newProverEnvironment() + try { + p.addConstraint(f) + return !p.isUnsat() + } finally { p.close() } + } + + def "a whitelisted unmodeled trim models its result as a UF over the input"() { + given: "a symbolic String receiver" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + StringValue receiver = new StringValue(solverContext, "abc", 0x1000) + receiver.MAKE_SYMBOLIC() + def receiverVars = varsOf(receiver) + assert receiverVars.size() == 1 + + when: "trim() is invoked (unmodeled, whitelisted) and recovered" + def result = executeBoundaryRecovery(receiver, STRING, "trim", TRIM, "abc") + + then: "modeled as the generic UF over the input - depends on it, not concretized, not aliased" + symbolsOf(result.recovered).contains("pure_String_trim") + symbolsOf(result.recovered).containsAll(receiverVars) + result.recovered.concrete == "abc" + } + + def "equal inputs yield equal results (UF congruence / determinism)"() { + given: "two independently symbolic String receivers" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + StringValue s1 = new StringValue(solverContext, "abc", 0x1000); s1.MAKE_SYMBOLIC() + StringValue s2 = new StringValue(solverContext, "abc", 0x2000); s2.MAKE_SYMBOLIC() + + when: "trim() is recovered for each" + def r1 = executeBoundaryRecovery(s1, STRING, "trim", TRIM, "abc") + def r2 = executeBoundaryRecovery(s2, STRING, "trim", TRIM, "abc") + + then: "(s1 == s2) implies (trim(s1) == trim(s2)) is valid" + def smgr = solverContext.getFormulaManager().getStringFormulaManager() + def bmgr = solverContext.getFormulaManager().getBooleanFormulaManager() + BooleanFormula premise = smgr.equal(s1.formula as StringFormula, s2.formula as StringFormula) + BooleanFormula conclusion = smgr.equal(r1.recovered.formula as StringFormula, r2.recovered.formula as StringFormula) + isValid(bmgr.implication(premise, conclusion)) + } + + def "the axiom-free UF excludes no real behavior (result can equal any value)"() { + given: + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + StringValue receiver = new StringValue(solverContext, "abc", 0x1000) + receiver.MAKE_SYMBOLIC() + + when: + def result = executeBoundaryRecovery(receiver, STRING, "trim", TRIM, "abc") + + then: "no hidden axiom forces the result - it may take an arbitrary value (SAT)" + def smgr = solverContext.getFormulaManager().getStringFormulaManager() + isSat(smgr.equal(result.recovered.formula as StringFormula, smgr.makeString("a totally different value"))) + } + + def "a whitelisted pure call emits its observed input-output pair as a ground UF constraint"() { + given: "a symbolic String receiver with a known concrete value" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + StringValue receiver = new StringValue(solverContext, "abc", 0x1000) + receiver.MAKE_SYMBOLIC() + + when: "trim() is invoked (whitelisted) and recovered, observing output 'abc'" + executeBoundaryRecovery(receiver, STRING, "trim", TRIM, "abc") + + then: "an observed-pair constraint over the pure_String_trim UF was recorded for this run" + def fm = solverContext.getFormulaManager() + def constraints = ThreadHandler.getSymbolicTraceHandler(threadId).getConstraints() + def pair = constraints.find { fm.extractVariablesAndUFs(it).keySet().contains("pure_String_trim") } + pair != null + + and: "the pair is GROUND (over the constant input, not the symbolic variable)" + fm.extractVariables(pair).isEmpty() + } + + def "a whitelisted pure call is modeled as a UF, so it does not flag context loss"() { + given: "a symbolic String receiver" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + StringValue receiver = new StringValue(solverContext, "abc", 0x1000) + receiver.MAKE_SYMBOLIC() + + when: "trim() (whitelisted, pure) is invoked and modeled as a UF" + def result = executeBoundaryRecovery(receiver, STRING, "trim", TRIM, "abc") + + then: "context loss is not flagged, since the call is modeled" + !result.contextLoss + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureUFPrimitiveRecoverySpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureUFPrimitiveRecoverySpec.groovy new file mode 100644 index 0000000..8cb0e87 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/PureUFPrimitiveRecoverySpec.groovy @@ -0,0 +1,45 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.symbolic.value.ValueFactory +import de.uzl.its.swat.symbolic.value.ValueType +import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue +import spock.lang.Unroll + +/** + * Primitive-return recovery: {@link ValueFactory#createNumericalValue(ValueType, Object, + * org.sosy_lab.java_smt.api.Formula)} builds a primitive value carrying an explicit symbolic formula + * (concrete = observed), for every primitive sort. This is the construction that installs a + * {@code pure_} UF result during primitive recovery. It pins the per-sort cast and that a + * carried symbolic formula makes the value symbolic, including short and byte, which have no pure + * unmodeled JDK method to exercise against a running agent. + */ +class PureUFPrimitiveRecoverySpec extends BaseValueSpec { + + @Unroll + def "createNumericalValue installs a symbolic #type formula (concrete=#concrete)"() { + given: "a free variable formula of the matching sort (stands in for a pure_ UF application)" + def formula = mk.call(context) + + when: "the value is built from the observed concrete + the symbolic formula" + def v = ValueFactory.createNumericalValue(type, concrete, formula) + + then: "the concrete is the observed value" + v.concrete == concrete + + and: "the carried formula makes the value symbolic and exposes the input variable" + v.isSymbolic() + v.getSymbolicVariables().contains(varName) + + where: + type | concrete | varName | mk + ValueType.intValue | (5 as Integer) | "v_int" | { c -> c.formulaManager.bitvectorFormulaManager.makeVariable(32, "v_int") } + ValueType.longValue | (5L as Long) | "v_long" | { c -> c.formulaManager.bitvectorFormulaManager.makeVariable(64, "v_long") } + ValueType.shortValue | (5 as Short) | "v_short" | { c -> c.formulaManager.bitvectorFormulaManager.makeVariable(16, "v_short") } + ValueType.byteValue | (5 as Byte) | "v_byte" | { c -> c.formulaManager.bitvectorFormulaManager.makeVariable(8, "v_byte") } + ValueType.charValue | ('a' as Character) | "v_char" | { c -> c.formulaManager.bitvectorFormulaManager.makeVariable(16, "v_char") } + ValueType.booleanValue | (true as Boolean) | "v_bool" | { c -> c.formulaManager.booleanFormulaManager.makeVariable("v_bool") } + ValueType.floatValue | (1.5f as Float) | "v_float" | { c -> c.formulaManager.floatingPointFormulaManager.makeVariable("v_float", FloatValue.precision) } + ValueType.doubleValue | (2.5d as Double) | "v_dbl" | { c -> c.formulaManager.floatingPointFormulaManager.makeVariable("v_dbl", DoubleValue.precision) } + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/StringRefEqAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/StringRefEqAgentSpec.groovy new file mode 100644 index 0000000..8e61779 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/StringRefEqAgentSpec.groovy @@ -0,0 +1,26 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.testsupport.agent.AgentRun +import de.uzl.its.swat.testsupport.agent.TraceObservation +import spock.lang.Specification + +/** + * End-to-end check that a de-interned {@code ==} (symbolic String versus a literal) is modeled via + * {@code Provenance.root} as a reference comparison and fires neither soundness flag. The + * {@code refEquals} body's {@code root}/{@code shouldUseValueEquality} calls are ignored (no context + * loss), and {@code refEquals} does not route through {@code Objects.equals} (no reference-semantic + * change). + */ +class StringRefEqAgentSpec extends Specification { + + def "de-interned == is modeled by provenance root and fires neither soundness flag"() { + when: + TraceObservation obs = AgentRun.run("targets/StringRefEqTarget.java", "StringRefEqTarget") + + then: "the symbolic input is designated" + obs.inputNames.any { it.startsWith("java/lang/String") } + + and: "modeling == via root suppresses context loss (ignored Provenance.root and shouldUseValueEquality)" + !obs.symbolicContextLoss + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/StringWhitelistAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/StringWhitelistAgentSpec.groovy new file mode 100644 index 0000000..1f2c0b1 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/StringWhitelistAgentSpec.groovy @@ -0,0 +1,35 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.testsupport.agent.AgentRun +import de.uzl.its.swat.testsupport.agent.TraceObservation +import spock.lang.Specification + +/** + * End-to-end check that pure String methods which are unmodeled stubs in StringValue (so the generic + * pure_<sig> UF fires), across String, int and boolean returns, are each modeled as a UF on a + * symbolic String receiver. The run preserves SAFE (no context loss, no precision loss) with the UFs + * in the branch constraints. The modeled String methods (substring, charAt, length, ...) are not + * whitelisted; they stay precise and are exercised elsewhere. + */ +class StringWhitelistAgentSpec extends Specification { + + def "unmodeled pure String methods are modeled as UFs (no context or precision loss)"() { + when: "the agent runs a program calling pure unmodeled String stubs on a symbolic receiver" + TraceObservation obs = AgentRun.run("targets/StringWhitelistTarget.java", "StringWhitelistTarget") + + then: "the run completed and the symbolic input was designated" + obs != null + !obs.inputNames.isEmpty() + + and: "modeling the pure results as UFs loses neither context nor precision" + !obs.symbolicContextLoss + !obs.symbolicPrecisionLoss + + and: "the generic UFs entered the branch constraints, across return sorts" + obs.anyBranchReferences("pure_String_hashCode") // int + obs.anyBranchReferences("pure_String_matches_String") // boolean + obs.anyBranchReferences("pure_String_compareTo_String") // int + obs.anyBranchReferences("pure_String_repeat_int") // String + obs.anyBranchReferences("pure_String_isBlank") // boolean + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ValueRecoverySpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ValueRecoverySpec.groovy new file mode 100644 index 0000000..68c923a --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ValueRecoverySpec.groovy @@ -0,0 +1,94 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.common.Util +import de.uzl.its.swat.symbolic.processor.BaseSymbolicInstructionProcessorSpec +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import de.uzl.its.swat.thread.ThreadHandler +import org.sosy_lab.java_smt.api.Formula + +/** + * Boundary recovery for value-returning calls. An unmodeled value-returning call must not let its + * result alias the receiver's symbolic value, whether the call returns {@code this} or a fresh + * object. The two cases differ only in the result's object identity (the receiver's own object for + * a this-return versus a distinct object), isolating the reference-keyed recovery. + */ +class ValueRecoverySpec extends BaseSymbolicInstructionProcessorSpec { + + private static final String STRING = "java/lang/String" + private static final String TO_LOWER = "()Ljava/lang/String;" + + private Set varsOf(value) { + return solverContext.getFormulaManager().extractVariables(value.formula as Formula).keySet() + } + + def "a this-returning unmodeled call does not alias the receiver's symbolic formula"() { + given: "a symbolic, already-lowercase String receiver registered on the heap" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + int receiverAddress = 0x1000 + String concrete = "abc" // already lowercase: the real toLowerCase() returns `this` + StringValue receiver = new StringValue(solverContext, concrete, receiverAddress) + receiver.MAKE_SYMBOLIC() + def receiverVars = varsOf(receiver) + + and: "the receiver really is symbolic" + assert receiverVars.size() == 1 + + when: "toLowerCase() is invoked (unmodeled) and the this-return is recovered" + def result = executeBoundaryRecovery(receiver, STRING, "toLowerCase", TO_LOWER, + concrete) // this-return: the result object IS the receiver's concrete object + + then: "context loss is flagged and the concrete result is correct" + result.contextLoss + result.recovered.concrete == concrete + + and: "the recovered value does not carry the receiver's symbolic formula" + varsOf(result.recovered).disjoint(receiverVars) + } + + def "a fresh-object unmodeled return does not alias the receiver's symbolic formula"() { + given: "a symbolic, concretely upper-case String receiver (toLowerCase returns a NEW object)" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + int receiverAddress = 0x1000 + StringValue receiver = new StringValue(solverContext, "ABC", receiverAddress) + receiver.MAKE_SYMBOLIC() + def receiverVars = varsOf(receiver) + + when: "the result returns at a fresh address (a distinct object), not the receiver's" + def result = executeBoundaryRecovery(receiver, STRING, "toLowerCase", TO_LOWER, + new String("abc")) // distinct object => new-object return, not a this-return + + then: "context loss is flagged, the concrete is the real result, and there is no aliasing" + result.contextLoss + result.recovered.concrete == "abc" + varsOf(result.recovered).disjoint(receiverVars) + } + + def "an unmodeled call returning a distinct tracked value recovers that value's shadow"() { + given: "a symbolic receiver, and a DISTINCT symbolic value registered on the heap under its own concrete" + setupTestContext(Util.formatClassName("de.uzl.its.swat.test.TestClass"), "main") + StringValue receiver = new StringValue(solverContext, "receiver", 0x1000) + receiver.MAKE_SYMBOLIC() + def receiverVars = varsOf(receiver) + + String storedConcrete = "stored" + StringValue stored = new StringValue(solverContext, storedConcrete, 0x2000) + stored.MAKE_SYMBOLIC() + def storedVars = varsOf(stored) + ThreadHandler.getSymbolicVisitor(threadId).getStack().putToHeap(storedConcrete, stored) + + and: "receiver and stored carry different symbolic variables" + assert !receiverVars.isEmpty() && !storedVars.isEmpty() + assert receiverVars.disjoint(storedVars) + + when: "an unmodeled instance call returns the distinct stored object, not the receiver" + // The fixture fabricates the returned identity (see its NOTE); a real example is map.get(k). + def result = executeBoundaryRecovery(receiver, STRING, "toLowerCase", TO_LOWER, storedConcrete) + + then: "the stored value's shadow is recovered - it keeps its own symbolic formula" + varsOf(result.recovered) == storedVars + + and: "so the result is neither concretized nor aliased to the receiver" + !varsOf(result.recovered).isEmpty() + varsOf(result.recovered).disjoint(receiverVars) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ValueSemanticsSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ValueSemanticsSpec.groovy new file mode 100644 index 0000000..5c12247 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/ValueSemanticsSpec.groovy @@ -0,0 +1,54 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.symbolic.value.Value +import de.uzl.its.swat.symbolic.value.reference.ObjectValue +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import org.objectweb.asm.Type +import org.sosy_lab.java_smt.api.Formula + +/** + * String identity and value rules that hold by construction, without instrumentation: the copy + * constructor, reuse of an interned literal, and concrete grounding of a symbolic value. + */ +class ValueSemanticsSpec extends BaseValueSpec { + + private Set varsOf(Value v) { + return fmgr.extractVariables(v.formula as Formula).keySet() + } + + def "new String(s) keeps the source's symbolic formula"() { + given: "a symbolic source string and a fresh target" + StringValue s = new StringValue(context, "abc", ObjectValue.ADDRESS_UNKNOWN) + s.MAKE_SYMBOLIC() + StringValue t = new StringValue(context, "abc", ObjectValue.ADDRESS_UNKNOWN) + + when: "t = new String(s) via the copy constructor" + Type[] desc = [Type.getType("Ljava/lang/String;")] as Type[] + t.invokeMethod("", desc, [s] as Value[]) + + then: "the content copy carries the same symbolic value" + !varsOf(s).isEmpty() + varsOf(t) == varsOf(s) + } + + def "reusing the same literal yields the same constant formula with no free variables"() { + given: + StringValue a = new StringValue(context, "lit", ObjectValue.ADDRESS_UNKNOWN) + StringValue b = new StringValue(context, "lit", ObjectValue.ADDRESS_UNKNOWN) + + expect: "both are constants (no free variables) and compare value-equal" + varsOf(a).isEmpty() + varsOf(b).isEmpty() + isValid(a.IF_ACMPEQ(b)) + } + + def "making a value symbolic preserves its concrete grounding"() { + given: + StringValue s = new StringValue(context, "seed", ObjectValue.ADDRESS_UNKNOWN) + s.MAKE_SYMBOLIC() + + expect: + s.concrete == "seed" + !varsOf(s).isEmpty() + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/WhitelistAuditAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/WhitelistAuditAgentSpec.groovy new file mode 100644 index 0000000..3f07f33 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/heap/WhitelistAuditAgentSpec.groovy @@ -0,0 +1,38 @@ +package de.uzl.its.swat.symbolic.heap + +import de.uzl.its.swat.testsupport.agent.AgentRun +import de.uzl.its.swat.testsupport.agent.TraceObservation +import spock.lang.Specification + +/** + * End-to-end check that pure java.lang/util methods across eight owners (Math, StrictMath, Character, + * Integer, Byte, Float, Double, Objects) and every return sort, including the String-to-float parse + * bridge, are each modeled as a generic pure_<sig> UF. The run preserves SAFE: no context loss, + * no precision loss, and the UFs ride into the branch constraints. + */ +class WhitelistAuditAgentSpec extends Specification { + + def "pure methods across all whitelisted classes are modeled as UFs (no context or precision loss)"() { + when: "the agent runs a program calling pure unmodeled JDK methods on symbolic inputs" + TraceObservation obs = AgentRun.run("targets/WhitelistAuditAgentTarget.java", "WhitelistAuditAgentTarget") + + then: "the run completed and symbolic inputs were designated" + obs != null + !obs.inputNames.isEmpty() + + and: "modeling the pure results as UFs loses neither context nor precision" + !obs.symbolicContextLoss + !obs.symbolicPrecisionLoss + + and: "the generic UFs entered the branch constraints, one representative per owner and sort" + obs.anyBranchReferences("pure_Math_pow_double_double") // Math, double + obs.anyBranchReferences("pure_StrictMath_cbrt_double") // StrictMath, double + obs.anyBranchReferences("pure_Math_addExact_int_int") // Math, int + obs.anyBranchReferences("pure_Integer_bitCount_int") // Integer, int + obs.anyBranchReferences("pure_Byte_hashCode_byte") // Byte, int + obs.anyBranchReferences("pure_Double_doubleToLongBits_double") // Double, long + obs.anyBranchReferences("pure_Character_isLetter_char") // Character, boolean + obs.anyBranchReferences("pure_Objects_checkIndex_int_int") // Objects, int + obs.anyBranchReferences("pure_Float_parseFloat_String") // Float, String->float bridge + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/processor/BaseSymbolicInstructionProcessorSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/processor/BaseSymbolicInstructionProcessorSpec.groovy index c09af0b..0f7ac86 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/processor/BaseSymbolicInstructionProcessorSpec.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/processor/BaseSymbolicInstructionProcessorSpec.groovy @@ -7,8 +7,10 @@ import de.uzl.its.swat.instrument.GlobalStateForInstrumentation import de.uzl.its.swat.instrument.Intrinsics import de.uzl.its.swat.metadata.ClassDepot import de.uzl.its.swat.symbolic.SymbolicInstructionVisitor +import de.uzl.its.swat.symbolic.instruction.GETVALUE_Object import de.uzl.its.swat.symbolic.instruction.INVOKEMETHOD_END import de.uzl.its.swat.symbolic.instruction.INVOKESTATIC +import de.uzl.its.swat.symbolic.instruction.INVOKEVIRTUAL import de.uzl.its.swat.symbolic.instruction.Instruction import de.uzl.its.swat.symbolic.instruction.LDC_long import de.uzl.its.swat.symbolic.instruction.NOP @@ -273,4 +275,57 @@ abstract class BaseSymbolicInstructionProcessorSpec extends Specification { } return result } + + /** + * L1 boundary-recovery fixture. Drives the real unmodeled-invoke -> recovery path: + * + * register {@code receiver} under its concrete object; push it as the invoke instance; then + * process INVOKEVIRTUAL(owner,name,desc) -> INVOKEMETHOD_END -> GETVALUE_Object(resultObject). + * + * An unmodeled method returns a PlaceHolder (InvocationHandler), INVOKEMETHOD_END pushes it, and + * GETVALUE_Object reconciles it against the reference-keyed heap. Passing {@code resultObject} + * identical to the receiver's concrete object reproduces a this-return (the toLowerCase aliasing + * defect); a distinct {@code resultObject} reproduces a new-object return. + * + * NOTE (honest limit): this fixture *fabricates* the result/receiver identity relationship that a + * real JVM would produce, so it pins the interpreter's recovery logic, not the + * instrumentation->processor contract. Pair flagship cases with an L2 agent run. It also relies + * on a value-type {@code getConcrete()} (a StringValue returns its String, so registration keys on + * that String); a plain ObjectValue receiver would key on its address and never recover. + * + * @return a map [recovered: Value, contextLoss: boolean] + */ + def executeBoundaryRecovery(ObjectValue receiver, String owner, String name, String desc, + Object resultObject) { + SymbolicInstructionVisitor visitor = ThreadHandler.getSymbolicVisitor(threadId) + ShadowContext context = visitor.getStack() + // Register the receiver under its concrete object, so a this-return (resultObject identical to + // the receiver's concrete) is recovered by reference identity; a distinct resultObject misses. + context.putToHeap(receiver.getConcrete(), receiver) + // Push the receiver as the invoke instance (consumed by newStackFrame in INVOKEVIRTUAL). + pushOperand(receiver) + + List instructions = new ArrayList<>() + long invokeId = GlobalStateForInstrumentation.instance.incAndGetInvokeId() + // INVOKEVIRTUAL and its INVOKEMETHOD_END must share the invokeId so the open-invoke stack + // closes (closeOpenInvoke) and METHOD_END is visited despite the frame's class differing. + instructions.add(new INVOKEVIRTUAL(GlobalStateForInstrumentation.instance.incAndGetId(), invokeId, owner, name, desc)) + instructions.add(new INVOKEMETHOD_END(GlobalStateForInstrumentation.instance.incAndGetId(), invokeId)) + instructions.add(new GETVALUE_Object(GlobalStateForInstrumentation.instance.incAndGetId(), System.identityHashCode(resultObject), resultObject, 0)) + instructions.add(new NOP(GlobalStateForInstrumentation.instance.incAndGetId())) + + // Drive: setCurrent(first); each processInstruction(next) visits the *current* and advances. + // The trailing NOP exists only to flush the GETVALUE_Object visit (execution is one behind). + ThreadHandler.setCurrentInstruction(threadId, instructions.remove(0)) + SymbolicInstructionProcessor processor = new SymbolicInstructionProcessor() + while (!instructions.isEmpty()) { + processor.processInstruction(instructions.remove(0)) + } + + def traceHandler = ThreadHandler.getSymbolicTraceHandler(threadId) + return [ + recovered : visitor.getStack().getActiveFrame().peek(), + contextLoss: traceHandler.isSymbolicContextLoss() + ] + } } diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/testsupport/agent/AgentRun.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/testsupport/agent/AgentRun.groovy new file mode 100644 index 0000000..0b1d345 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/testsupport/agent/AgentRun.groovy @@ -0,0 +1,91 @@ +package de.uzl.its.swat.testsupport.agent + +import com.fasterxml.jackson.databind.ObjectMapper + +import javax.tools.ToolProvider +import java.nio.file.Files + +/** + * Level-2 harness. Compiles a tiny {@code @Symbolic}-annotated target against the agent jar, runs it + * under the REAL SWAT agent in a forked JVM with {@code solver.mode=PRINT}, captures stdout, and + * parses the emitted {@code TraceDTO} JSON into a {@link TraceObservation}. No Python explorer. + * + * Every failure mode throws (missing jar, compile error, non-zero exit, no JSON), so an infra break + * surfaces as a real failure — never masked. See docs/test-architecture.md (Level L2). + */ +class AgentRun { + + /** + * @param targetResource classpath resource of the target source, e.g. "targets/ToLowerCaseTarget.java". + * @param mainClass the target's (default-package) main class name, e.g. "ToLowerCaseTarget". + */ + static TraceObservation run(String targetResource, String mainClass) { + // Gradle runs tests with the module dir as the working dir. + File moduleDir = new File(System.getProperty("user.dir")) + File agentJar = new File(moduleDir, "lib/symbolic-executor.jar") + File libs = new File(moduleDir, "../libs/java-library-path") + assert agentJar.exists(): + "Agent jar missing at ${agentJar} — run `./gradlew :symbolic-executor:copyJar` first " + + "(the agentTest task does this automatically)." + + // 1. Materialize + compile the target against the agent jar (which provides @Symbolic). + File work = Files.createTempDirectory("swat-l2-").toFile() + File outDir = new File(work, "classes") + outDir.mkdirs() + File src = new File(work, mainClass + ".java") + def res = AgentRun.class.classLoader.getResourceAsStream(targetResource) + assert res != null: "Target resource not found on test classpath: ${targetResource}" + src.text = res.text + + def compiler = ToolProvider.getSystemJavaCompiler() + assert compiler != null: "No system Java compiler — tests must run on a JDK, not a JRE." + int rc = compiler.run(null, System.out, System.err, + "-g", "-cp", agentJar.absolutePath, "-d", outDir.absolutePath, src.absolutePath) + assert rc == 0: "Failed to compile target ${targetResource}" + + // 2. Fork a JVM under the agent in PRINT mode (the TraceDTO JSON goes to stdout). + List cmd = [ + javaBin(), + "-Djava.library.path=${libs.absolutePath}".toString(), + "-Dsolver.mode=PRINT", + "-Dlogging.debug=false", + "-javaagent:${agentJar.absolutePath}".toString(), + "-cp", outDir.absolutePath, + mainClass + ] + Process proc = new ProcessBuilder(cmd).start() + String stdout = proc.inputStream.text + String stderr = proc.errorStream.text + int exit = proc.waitFor() + assert exit == 0: + "Agent run exited ${exit}.\n--- STDOUT tail ---\n${tail(stdout)}\n--- STDERR tail ---\n${tail(stderr)}" + + // 3. Extract the single top-level pretty-printed JSON object and parse it. + String json = extractTraceJson(stdout) + assert json != null: "No TraceDTO JSON found on stdout.\n--- STDOUT tail ---\n${tail(stdout)}" + return TraceObservation.parse(new ObjectMapper().readTree(json)) + } + + private static String javaBin() { + return new File(System.getProperty("java.home"), "bin/java").absolutePath + } + + /** + * The PRINT-mode TraceDTO is the only top-level (column-0) pretty-printed JSON object on stdout, + * so it spans from the single line that is "{" to the single line that is "}". + */ + private static String extractTraceJson(String stdout) { + List lines = stdout.readLines() + int start = lines.findIndexOf { it.trim() == "{" } + int end = lines.findLastIndexOf { it.trim() == "}" } + if (start < 0 || end < start) { + return null + } + return lines[start..end].join("\n") + } + + private static String tail(String s, int n = 40) { + List l = s.readLines() + return l.subList(Math.max(0, l.size() - n), l.size()).join("\n") + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/testsupport/agent/TraceObservation.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/testsupport/agent/TraceObservation.groovy new file mode 100644 index 0000000..90f3203 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/testsupport/agent/TraceObservation.groovy @@ -0,0 +1,35 @@ +package de.uzl.its.swat.testsupport.agent + +import com.fasterxml.jackson.databind.JsonNode + +/** + * A structured view of a {@code TraceDTO} emitted by a Level-2 agent run (solver.mode=PRINT). + * Holds only what tests assert on: the soundness flags, the symbolic input names, and the + * (non-null) branch constraint strings. See docs/test-architecture.md (Level L2). + */ +class TraceObservation { + + boolean symbolicContextLoss + boolean symbolicPrecisionLoss + List inputNames = [] + List branchConstraints = [] + + static TraceObservation parse(JsonNode root) { + TraceObservation o = new TraceObservation() + o.symbolicContextLoss = root.path("symbolicContextLoss").asBoolean() + o.symbolicPrecisionLoss = root.path("symbolicPrecisionLoss").asBoolean() + root.path("inputs").each { o.inputNames << it.path("name").asText() } + root.path("trace").each { + JsonNode c = it.path("constraint") + if (c != null && c.isTextual()) { + o.branchConstraints << c.asText() + } + } + return o + } + + /** Whether any branch constraint mentions {@code token} (e.g. a symbolic input variable name). */ + boolean anyBranchReferences(String token) { + return branchConstraints.any { it.contains(token) } + } +} diff --git a/symbolic-executor/src/test/resources/targets/BoxedReturnTarget.java b/symbolic-executor/src/test/resources/targets/BoxedReturnTarget.java new file mode 100644 index 0000000..2345dd3 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/BoxedReturnTarget.java @@ -0,0 +1,46 @@ +import de.uzl.its.swat.annotations.Symbolic; + +/** + * Exercises the de-intern instrumentation for the boxed wrapper types under the JVM verifier. A run + * that completes at exit 0 with a parsed TraceDTO confirms the wrap/rewrite bytecode is valid; a + * malformed rewrite would raise a VerifyError. + * + *

    + *
  • Wrapper returns from factories - declared-wrapper returns from un-instrumented + * {@code valueOf(String)} factories: Integer and Long.
    • + *
  • valueOf rewrite - autoboxing emits {@code .valueOf(primitive)}, which the + * adapter rewrites to {@code new (primitive)} for all six wrappers (Integer, Long, + * Short, Byte, Character, Boolean). Constructing all six covers every per-wrapper descriptor, + * especially the short/byte/char descriptors paired with int-category opcodes.
    • + *
+ * + *

The autoboxed wrappers are kept concrete and consumed via string concatenation, and the + * {@code valueOf(String)} factories are limited to Integer and Long. Feeding a symbolic value through + * Short/Byte/Character/Boolean parsing or unboxing hits gaps in the symbolic modeling of those + * wrappers that are unrelated to the de-intern bytecode validity this target checks. + */ +public class BoxedReturnTarget { + + public static void main(String[] args) { + test(5); + } + + public static String test(@Symbolic int x) { + // Declared-wrapper returns from un-instrumented valueOf(String) factories. + Integer i = Integer.valueOf(Integer.toString(x)); + Long l = Long.valueOf(Long.toString((long) x)); + + // Autoboxed wrappers, kept concrete and consumed via string concatenation below. + Integer ai = 11; + Long al = 12L; + Short ash = (short) 13; + Byte aby = (byte) 14; + Character ach = 'c'; + Boolean abo = true; + + if (i.intValue() + l.longValue() > 0) { + return "pos:" + ai + al + ash + aby + ach + abo; + } + return "nonpos"; + } +} diff --git a/symbolic-executor/src/test/resources/targets/ContainerRecoveryTarget.java b/symbolic-executor/src/test/resources/targets/ContainerRecoveryTarget.java new file mode 100644 index 0000000..d59e6d1 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/ContainerRecoveryTarget.java @@ -0,0 +1,28 @@ +import de.uzl.its.swat.annotations.Symbolic; +import java.util.HashMap; + +/** + * Stores a symbolic String in an unmodeled container (HashMap) and retrieves it via a concrete key, + * then branches on the retrieved value. The stored value is first derived via a String operation, so + * it is a tracked (registered) symbolic value by the time it enters the container; recovering its + * shadow on the way out keeps the branch dependent on the symbolic input rather than concretizing it. + * A single String parameter avoids an unrelated instrumenter frame-analysis limitation on mixed + * category-2/reference signatures. + */ +public class ContainerRecoveryTarget { + + public static void main(String[] args) { + test("hello"); + } + + public static int test(@Symbolic String s) { + String name = s.substring(1); // a derived, tracked symbolic String ("ello") + HashMap m = new HashMap<>(); + m.put("k", name); + String v = m.get("k"); + if (v.charAt(0) == 'e') { + return 1; + } + return 0; + } +} diff --git a/symbolic-executor/src/test/resources/targets/PurePrimReturnTarget.java b/symbolic-executor/src/test/resources/targets/PurePrimReturnTarget.java new file mode 100644 index 0000000..0886ae0 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/PurePrimReturnTarget.java @@ -0,0 +1,34 @@ +import de.uzl.its.swat.annotations.Symbolic; + +/** + * Calls pure, unmodeled java.lang methods with primitive return types on symbolic inputs and branches + * on each result. Each result is modeled as a generic {@code pure_} uninterpreted function over + * its inputs rather than concretized, so the branches stay symbolic. Covers int, long, double, float, + * char and boolean returns (short and byte have no suitable pure unmodeled JDK method). + */ +public class PurePrimReturnTarget { + + public static void main(String[] args) { + test(7, 3.0); + } + + public static int test(@Symbolic int x, @Symbolic double d) { + int fd = Math.floorDiv(x, 3); // int + int fm = Math.floorMod(x, 3); // int + long fdl = Math.floorDiv((long) x, 3L); // long + double cb = Math.cbrt(d); // double + float fb = Float.intBitsToFloat(x); // float + char lc = Character.toLowerCase((char) x); // char + boolean dig = Character.isDigit((char) x); // boolean + + int r = 0; + if (fd > 0) r++; + if (fm > 0) r++; + if (fdl > 0L) r++; + if (cb > 0.0) r++; + if (fb > 0.0f) r++; + if (lc > 0) r++; + if (dig) r++; + return r; + } +} diff --git a/symbolic-executor/src/test/resources/targets/StringRefEqTarget.java b/symbolic-executor/src/test/resources/targets/StringRefEqTarget.java new file mode 100644 index 0000000..51392f4 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/StringRefEqTarget.java @@ -0,0 +1,20 @@ +import de.uzl.its.swat.annotations.Symbolic; + +/** + * Compares a symbolic String to a string literal with reference equality ({@code ==}). The symbolic + * input is de-interned, so it and the interned literal are distinct references and {@code ==} is + * false. Reference equality is modeled without changing reference semantics. + */ +public class StringRefEqTarget { + + public static void main(String[] args) { + test("seed"); + } + + public static String test(@Symbolic String s) { + if (s == "MATCH") { // distinct references -> false + return "eq"; + } + return "ne"; + } +} diff --git a/symbolic-executor/src/test/resources/targets/StringWhitelistTarget.java b/symbolic-executor/src/test/resources/targets/StringWhitelistTarget.java new file mode 100644 index 0000000..f00fbbb --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/StringWhitelistTarget.java @@ -0,0 +1,29 @@ +import de.uzl.its.swat.annotations.Symbolic; + +/** + * Drives unmodeled pure String methods on a symbolic String receiver into branches, covering String, + * int and boolean returns. Each result is modeled as a generic pure_ uninterpreted function. + * Uses a single String parameter: a category-2 parameter (double or long) followed by a reference + * parameter trips a frame-analysis limitation in the instrumenter. + */ +public class StringWhitelistTarget { + + public static void main(String[] args) { + test("hello world 42"); + } + + public static int test(@Symbolic String s) { + int h = s.hashCode(); // int + boolean m = s.matches(".*"); // boolean + int c = s.compareTo("x"); // int + String rp = s.repeat(2); // String + boolean b = s.isBlank(); // boolean + int r = 0; + if (h != 0) r++; + if (m) r++; + if (c != 0) r++; + if (rp.length() > 0) r++; + if (b) r++; + return r; + } +} diff --git a/symbolic-executor/src/test/resources/targets/SubstringTarget.java b/symbolic-executor/src/test/resources/targets/SubstringTarget.java new file mode 100644 index 0000000..f050878 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/SubstringTarget.java @@ -0,0 +1,22 @@ +import de.uzl.its.swat.annotations.Symbolic; + +/** + * Passes a symbolic String to an unmodeled but whitelisted pure method that takes an argument + * ({@code String.substring(int)}) and branches on the result. This exercises the mixed-sort generic + * uninterpreted function {@code pure_String_substring_int(String, int)}, so the branch references the + * input through the UF. Complements {@code TrimTarget}, which uses a no-argument method. + */ +public class SubstringTarget { + + public static void main(String[] args) { + test("abcd"); + } + + public static String test(@Symbolic String s) { + String r = s.substring(1); // modeled as pure_String_substring_int(s, 1) + if (r.equals("bcd")) { + return "eq"; + } + return "ne"; + } +} diff --git a/symbolic-executor/src/test/resources/targets/ToLowerCaseTarget.java b/symbolic-executor/src/test/resources/targets/ToLowerCaseTarget.java new file mode 100644 index 0000000..6a0ed1e --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/ToLowerCaseTarget.java @@ -0,0 +1,21 @@ +import de.uzl.its.swat.annotations.Symbolic; + +/** + * Passes a symbolic, concretely already-lowercase String to an unmodeled {@code toLowerCase()} that + * returns {@code this}, then branches on the result. This exercises the identity-recovery / aliasing + * path. The method is not on the purity whitelist, unlike {@code TrimTarget}. + */ +public class ToLowerCaseTarget { + + public static void main(String[] args) { + test("abc"); + } + + public static String test(@Symbolic String s) { + String r = s.toLowerCase(); + if (r.equals("abc")) { + return "eq"; + } + return "ne"; + } +} diff --git a/symbolic-executor/src/test/resources/targets/TrimTarget.java b/symbolic-executor/src/test/resources/targets/TrimTarget.java new file mode 100644 index 0000000..8566117 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/TrimTarget.java @@ -0,0 +1,22 @@ +import de.uzl.its.swat.annotations.Symbolic; + +/** + * Passes a symbolic String to an unmodeled but whitelisted pure method ({@code String.trim()}) and + * branches on the result. This exercises the generic uninterpreted-function path: the result is + * modeled as {@code pure_String_trim(s)}, so the branch constraint references the input through the + * UF. Contrasts with {@code ToLowerCaseTarget}, whose method is not whitelisted. + */ +public class TrimTarget { + + public static void main(String[] args) { + test("abc"); + } + + public static String test(@Symbolic String s) { + String r = s.trim(); // modeled as pure_String_trim(s) + if (r.equals("abc")) { + return "eq"; + } + return "ne"; + } +} diff --git a/symbolic-executor/src/test/resources/targets/WhitelistAuditAgentTarget.java b/symbolic-executor/src/test/resources/targets/WhitelistAuditAgentTarget.java new file mode 100644 index 0000000..5cc7143 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/WhitelistAuditAgentTarget.java @@ -0,0 +1,63 @@ +import de.uzl.its.swat.annotations.Symbolic; + +/** + * Drives pure, unmodeled, value-typed JDK methods from the purity whitelist on symbolic inputs into + * branches. The methods span several owners and every return sort, including the String-to-float parse + * bridge. Each result is modeled as a generic pure_ uninterpreted function. The methods are kept + * small and separate because large mixed-type method bodies trip a frame-analysis limitation in the + * instrumenter. + */ +public class WhitelistAuditAgentTarget { + + public static void main(String[] args) { + ma(2.0); + mb(5); + mc(5, 2.0); + md("12.5"); + } + + // Math/StrictMath, double returns. + public static int ma(@Symbolic double d) { + double a = Math.tan(d), b = Math.pow(d, 2.0), c = Math.log(d), e = StrictMath.cbrt(d), f = Math.exp(d); + int r = 0; + if (a > 0) r++; + if (b > 0) r++; + if (c > 0) r++; + if (e > 0) r++; + if (f > 0) r++; + return r; + } + + // Math exact-arithmetic + Integer/Byte, int returns. + public static int mb(@Symbolic int x) { + int a = Math.addExact(x, 3), b = Math.multiplyExact(x, 2), c = Math.floorMod(x, 3), + e = Integer.bitCount(x), f = Byte.hashCode((byte) x); + int r = 0; + if (a > 0) r++; + if (b > 0) r++; + if (c > 0) r++; + if (e > 0) r++; + if (f > 0) r++; + return r; + } + + // Double / Character (boolean) / Objects, mixed return sorts. + public static int mc(@Symbolic int x, @Symbolic double d) { + long a = Double.doubleToLongBits(d); + double b = Double.max(d, 2.0); + boolean c = Character.isLetter((char) x); + int e = java.util.Objects.checkIndex(x, 100); + int r = 0; + if (a != 0) r++; + if (b > 0) r++; + if (c) r++; + if (e >= 0) r++; + return r; + } + + // String -> float parse bridge. + public static int md(@Symbolic String s) { + float p = Float.parseFloat(s); + return p > 0 ? 1 : 0; + } +} diff --git a/symbolic-explorer/constraint/ConstraintController.py b/symbolic-explorer/constraint/ConstraintController.py index afe20f7..624c37a 100755 --- a/symbolic-explorer/constraint/ConstraintController.py +++ b/symbolic-explorer/constraint/ConstraintController.py @@ -40,7 +40,6 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str ufs = request.ufs symbolicContextLoss = request.symbolicContextLoss symbolicPrecisionLoss = request.symbolicPrecisionLoss - referenceSemanticChange = request.referenceSemanticChange # Start a new thread to add constraints thread = threading.Thread(target=ConstraintService.add_constraints, kwargs={ @@ -50,8 +49,7 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str 'inputs': inputs, 'ufs': ufs, 'symbolic_context_loss': symbolicContextLoss, - 'symbolic_precision_loss': symbolicPrecisionLoss, - 'reference_semantic_change': referenceSemanticChange}) + 'symbolic_precision_loss': symbolicPrecisionLoss}) thread.start() thread.join() # To ensure trace is added in SV-Comp mode # Return a response indicating that the request has been accepted diff --git a/symbolic-explorer/constraint/ConstraintService.py b/symbolic-explorer/constraint/ConstraintService.py index 89831e6..0fd0c84 100755 --- a/symbolic-explorer/constraint/ConstraintService.py +++ b/symbolic-explorer/constraint/ConstraintService.py @@ -22,8 +22,7 @@ class ConstraintService: @staticmethod def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inputs: List[InputItem], ufs: List[UFItem], - symbolic_context_loss: bool, symbolic_precision_loss: bool, - reference_semantic_change: bool = False): + symbolic_context_loss: bool, symbolic_precision_loss: bool): """ Adds constraints to the database. @@ -39,7 +38,6 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp ufs (list): Definition of all UFs that are used symbolic_context_loss (bool): A flag indicating whether the symbolic context was lost. symbolic_precision_loss (bool): A flag indicating whether the symbolic precision was lost (UFs introduced). - reference_semantic_change (bool): A flag indicating whether reference equality semantics changed. Returns: None: The result is the side effect of adding data to the database. @@ -51,5 +49,5 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp inputs_parsed: List[Input] = Parser.parse_inputs(inputs) ufs_parsed: List[UF] = Parser.parse_ufs(ufs) # Adding the trace and inputs to the database for the specified endpoint. - Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change) + Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss) logger.info(f'[CONSTRAINT SERVICE] Added trace {trace_id} to endpoint {endpoint_id}') diff --git a/symbolic-explorer/data/BinaryExecutionTree/Tree.py b/symbolic-explorer/data/BinaryExecutionTree/Tree.py index 6636395..3aa0f61 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Tree.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Tree.py @@ -33,7 +33,6 @@ def __init__(self, endpoint_id: Union[str, int]): self.endpoint_id = endpoint_id self.symbolic_context_loss = False self.symbolic_precision_loss = False - self.reference_semantic_change = False self.uncaught_exceptions: int = 0 self.symbolic_vars: Set = set() self.ufs: Set = set() @@ -68,10 +67,6 @@ def record_precision_loss(self): logger.warning("Precision loss recorded!") self.symbolic_precision_loss = True - def record_reference_semantic_change(self): - logger.warning("Reference semantic change recorded: user-de-interned strings compared via Objects.equals") - self.reference_semantic_change = True - def add(self, trace: list[Branch | Special], inputs: List[Input], ufs: List[UF]): """ Adds a branch to the tree based on the provided trace and inputs. diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py index e4866a8..056cfef 100755 --- a/symbolic-explorer/data/Database.py +++ b/symbolic-explorer/data/Database.py @@ -113,8 +113,7 @@ def get_endpoints(self): return endpoints def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Branch | Special], inputs: List[Input], ufs: List[UF], - symbolic_context_loss: bool, symbolic_precision_loss: bool, - reference_semantic_change: bool = False): + symbolic_context_loss: bool, symbolic_precision_loss: bool): endpoint_id = str(endpoint_id) lock.acquire() @@ -126,7 +125,6 @@ def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Bra self.tree[endpoint_id].record_ufs(ufs) self.tree[endpoint_id].record_context_loss() if symbolic_context_loss else None self.tree[endpoint_id].record_precision_loss() if symbolic_precision_loss else None - self.tree[endpoint_id].record_reference_semantic_change() if reference_semantic_change else None lock.release() @@ -161,6 +159,15 @@ def add_solution(self, branch_id: int, sol: Any, inputs: List[Input], endpoint_i self.new_solutions.append(branch_id) lock.release() + def remove_solution(self, branch_id: int): + # Re-open a branch (e.g. after a concolic divergence): drop its stored solution so the + # selection walk (dfs) returns it again for another attempt. + lock.acquire() + self.solutions.pop(branch_id, None) + if branch_id in self.new_solutions: + self.new_solutions.remove(branch_id) + lock.release() + def get_solutions(self): lock.acquire() ret = copy.deepcopy(self.solutions) diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a0081e8..e09601d 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -27,7 +27,13 @@ # The (unique) endpoint ID for the SV-COMP target. As each target is handled separately, this ID is always 0. -ENDPOINT_ID = 0 +ENDPOINT_ID = 0 + +# A branch guarded by an uninterpreted pure_ UF can diverge on concrete replay (the solver cannot +# drive the UF to the required value). We re-open and retry such a branch - with a fresh solver input +# once observed input->output pairs are injected - but only up to this many attempts, after which it +# is abandoned as unverified (forcing UNKNOWN). This bounds exploration and guarantees termination. +MAX_BRANCH_ATTEMPTS = 3 class ExecutionStatus(Enum): @@ -62,6 +68,14 @@ class State: def __init__(self): self.verdict = Verdict.UNKNOWN self.branch_to_explore: Node | None = None + # Node gids we solved and intended to explore, but abandoned after the concrete re-run kept + # diverging (the predicted branch was never actually taken - e.g. a branch guarded by an + # uninterpreted pure_ UF the solver cannot drive to the required value). While any remain, a + # SAFE verdict is unsound: that branch was not actually explored. + self.unverified_branches: set = set() + # Per-branch (node gid) count of solve+re-run attempts that diverged; drives attempt-based + # prioritization and the re-open/abandon bound. + self.branch_attempts: dict = {} class SVCompDriver: @@ -209,13 +223,21 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, # check if the target explored the branch as expected if self.state.branch_to_explore: + diverged = False for branch in Database.instance().get_trace(-1): # most recent trace if branch.id == self.state.branch_to_explore.id: + # We solved this branch to flip it; if the re-run took the same direction, the + # predicted branch was not actually explored (an uninterpreted pure_ UF the + # solver could not drive to the required value). if branch.has_branched == (self.state.branch_to_explore.branched is not None): - logger.error(f'[SVCOMP] SWAT Assertion failed: Target did not explore branch {branch.id} as expected! Branch unexpectedly taken/skipped.') + logger.warning(f'[SVCOMP] Branch {branch.id} diverged: predicted direction not taken.') + diverged = True break else: - logger.error(f'[SVCOMP] SWAT Assertion failed: Target did not explore branch {self.state.branch_to_explore.id} as expected! Branch does not appear in trace.') + logger.warning(f'[SVCOMP] Branch {self.state.branch_to_explore.id} diverged: does not appear in trace.') + diverged = True + if diverged: + self.handle_divergence(self.state.branch_to_explore) self.state.branch_to_explore = None self.log_output(output) @@ -244,8 +266,28 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, + def handle_divergence(self, branch: Node): + """A solved branch diverged on concrete replay. Re-open it for another attempt (bounded), or + abandon it as unverified once the attempt cap is reached (forcing UNKNOWN).""" + gid = branch.gid + self.state.branch_attempts[gid] = self.state.branch_attempts.get(gid, 0) + 1 + attempts = self.state.branch_attempts[gid] + if attempts < MAX_BRANCH_ATTEMPTS: + # Not actually explored - re-open so it is selectable again (yields a different solver + # input once observed input->output pairs are injected). Bounded by the attempt cap. + Database.instance().remove_solution(gid) + logger.info(f'[SVCOMP] Re-opening diverged branch {branch.id} (gid {gid}), attempt {attempts}/{MAX_BRANCH_ATTEMPTS}') + else: + self.state.unverified_branches.add(gid) + logger.warning(f'[SVCOMP] Abandoning diverged branch {branch.id} (gid {gid}) after {attempts} attempts; verdict cannot be SAFE.') + def retrieve_solution(self): possible_branches = StrategyService.select_branch(endpoint_id=ENDPOINT_ID) + # Prefer branches tried fewer times so a repeatedly-diverging branch does not starve the rest; + # exclude any that hit the attempt cap (abandoned -> unverified -> UNKNOWN). + possible_branches = [b for b in possible_branches + if self.state.branch_attempts.get(b.gid, 0) < MAX_BRANCH_ATTEMPTS] + possible_branches.sort(key=lambda b: self.state.branch_attempts.get(b.gid, 0)) 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]}') symbolic_vars = None @@ -313,8 +355,8 @@ def run(self): logger.warning(f'[SVCOMP] Found uncaught exceptions during symbolic execution') verdict = Verdict.UNKNOWN - if (verdict == Verdict.VIOLATION) and Database.instance().get_tree(ENDPOINT_ID).reference_semantic_change: - logger.warning(f'[SVCOMP] Found reference semantic change (user-de-interned strings compared via Objects.equals) - downgrading VIOLATION to UNKNOWN') + if (verdict == Verdict.SAFE) and self.state.unverified_branches: + logger.warning(f'[SVCOMP] Cannot conclude SAFE: {len(self.state.unverified_branches)} branch(es) diverged and were never verified (downgrading to UNKNOWN)') verdict = Verdict.UNKNOWN if verdict == Verdict.NO_SYMBOLIC_VARS: diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index be30d85..af61241 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -10,6 +10,10 @@ class TraceItem(BaseModel): branched: bool type: str inst: Optional[str] = None + # G4: executor's per-branch precision-loss verdict. Parsed for forward compatibility; the current + # verdict still uses the aggregate symbolicPrecisionLoss. A future explorer-side, CFG-reachability + # -aware decision keys this by iid to a CFG node. Default keeps older traces parseable. + precisionLoss: bool = False class UFItem(BaseModel): definition: str @@ -28,7 +32,6 @@ class ConstraintRequest(BaseModel): ufs: List[UFItem] symbolicContextLoss: bool symbolicPrecisionLoss: bool - referenceSemanticChange: bool = False class CoverageRequest(BaseModel): diff --git a/symbolic-explorer/strategy/StrategyService.py b/symbolic-explorer/strategy/StrategyService.py index 5d97d72..b0ae88f 100755 --- a/symbolic-explorer/strategy/StrategyService.py +++ b/symbolic-explorer/strategy/StrategyService.py @@ -91,6 +91,12 @@ def solve_branch(possible_branch: Node, endpoint_id=None): path_constraints.extend(StrategyService.collect_uf_definitions(possible_branch)) + # Inject the accumulated observed input->output UF pairs from all prior runs of this testcase, + # so re-solving a diverged branch is forced to pick a different input (the previous input's real + # output is pinned). Each entry is a self-contained SMT script parsed in isolation, so re-declared + # UF symbols do not collide; the pairs are true observed facts, so injecting them stays sound. + path_constraints.extend(db.get_tree(0).ufs) + inputs = possible_branch.inputs sat, sol = Z3Handler.solve(possible_branch, path_constraints) diff --git a/targets/sv-comp/scripts/lib/analysis/failures.py b/targets/sv-comp/scripts/lib/analysis/failures.py index 136469b..b4e452f 100644 --- a/targets/sv-comp/scripts/lib/analysis/failures.py +++ b/targets/sv-comp/scripts/lib/analysis/failures.py @@ -5,7 +5,6 @@ - Symbolic context loss - Symbolic precision loss - Uncaught exceptions -- Reference semantic changes - Internal SWAT errors """ @@ -55,7 +54,6 @@ def analyze_failures(log_base_dir: Path = None) -> Dict: - Symbolic context loss - Symbolic precision loss - Uncaught exceptions - - Reference semantic changes - Other errors Args: @@ -71,7 +69,6 @@ def analyze_failures(log_base_dir: Path = None) -> Dict: 'symbolic_context_loss': [], 'symbolic_precision_loss': [], 'uncaught_exceptions': [], - 'reference_semantic_change': [], 'internal_errors': [], 'total_analyzed': 0 } @@ -98,9 +95,6 @@ def analyze_failures(log_base_dir: Path = None) -> Dict: if 'Found uncaught exceptions' in content: failure_stats['uncaught_exceptions'].append(testcase_name) - if 'Found reference semantic change' in content: - failure_stats['reference_semantic_change'].append(testcase_name) - if '[SWAT Assertion failed]' in content or 'java.lang.AssertionError: [SWAT]' in content: failure_stats['internal_errors'].append(testcase_name) @@ -124,7 +118,6 @@ def print_failure_statistics(log_base_dir: Path = None): ('Symbolic Context Loss', 'symbolic_context_loss'), ('Symbolic Precision Loss', 'symbolic_precision_loss'), ('Uncaught Exceptions', 'uncaught_exceptions'), - ('Reference Semantic Change', 'reference_semantic_change'), ('Internal SWAT Errors', 'internal_errors') ] diff --git a/targets/sv-comp/scripts/lib/execution.py b/targets/sv-comp/scripts/lib/execution.py index fbf1f1d..13527e2 100644 --- a/targets/sv-comp/scripts/lib/execution.py +++ b/targets/sv-comp/scripts/lib/execution.py @@ -246,8 +246,14 @@ def log_output(output: List[str]): for line in output: logger.info(line.strip()) -def run_command_with_timeout(cmd: list[str], timeout: int = 900) -> tuple[ExecutionStatus, list[str]]: - """Executes the given command and returns output from both STDOUT and STDERR.""" +def run_command_with_timeout(cmd: list[str], timeout: int = 120) -> tuple[ExecutionStatus, list[str]]: + """Executes the given command and returns output from both STDOUT and STDERR. + + `timeout` is the per-testcase wall-clock cap enforced by this local runner, OUTSIDE the actual SWAT + run: on expiry the whole process group is SIGKILLed and the testcase scores 0 (TIMEOUT). Kept at + 120s to bound local scoring runs; the competition-infra wrapper (scripts/svcomp-package/run_swat.py) + is separate and unaffected. + """ logger.info(f'[TARGET EXECUTION]: Running symbolic-explorer: {cmd}') output = []