Fix/heap design

.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
+```
+
+`<class-fqn>` 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/<Class>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 <class>`).
+
+## 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_<sig>` 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.

.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 <class-fqn>                       # index: every method/ctor signature + line no.
+  jmethod.py <class-fqn> <method>              # full source of all overloads of <method>
+  jmethod.py <class-fqn> <method> --callees    # also list the methods each overload calls
+  jmethod.py <class-fqn> --field <name>        # a field declaration (for static-final purity checks)
+
+<class-fqn> 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()

.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_<category>_<timestamp>.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 `<group>/<Name>` (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/<group>/<Name>_<property>/` (`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=<port> -javaagent:…/symbolic-executor.jar
+   -Djava.library.path=… -cp <common>:<z3>:<testcase> -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 <prop>] == 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: <expected> -> <got>` — the scored outcome.
+
+## Reading the result
+`Case: <expected_verdict> -> <swat_verdict>`; 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/<group>/<Name>/` — testcase: `Main.java` + `<Name>.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.