From 18f16bed714b6d05f21a6e99378f37699c2d0dbf Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 16 Jul 2026 18:45:24 +0200 Subject: [PATCH 1/3] test(#275): execution gate for the self-contained reachable call graph + non-vacuity hatch MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The DIRECT reachable call graph on the self-contained --cortex-m image was already implemented (#235, v0.11.28): compile_all_exports walks reachable_from_exports (transitive closure over static `call`) and the cortex-m builder patches every internal BL to the emitted callee's address. What was missing was a mechanical EXECUTION gate proving the standalone image runs correctly — presence in `nm` doesn't catch a mis-patched or dropped BL. Adds an artifact-derived execution differential (reachable_callgraph_275_selfcontained_differential.py) that runs the DEFAULT self-contained image (its own Reset_Handler startup) on unicorn and compares `entry(x)` to wasmtime for 7 vectors. `entry` (the only export) calls two non-exported helpers, one of which calls a third — result 8*x+8 depends on the whole transitive closure being compiled in and every BL resolved. An unreachable `dead` helper is confirmed ABSENT (a closure, not "emit all"). Non-vacuity: a TEST-ONLY `EXPORTS_ONLY_275=1` env hatch in compile_all_exports reverts to the pre-#235 exports-only behavior (drop non-exported callees). With helpers dropped, `entry`'s BL becomes an EXTERNAL relocation and the builder degrades to a link-me ET_REL object with no Reset_Handler — not self-contained. The gate detects this (ET_REL, not ET_EXEC) and goes RED, proving it catches the historical #275 drop; GREEN with the shipped reachability walk. Default path unchanged (hatch is an env-gated no-op) → frozen anchors byte-identical. call_indirect residual unchanged: a mixed module (direct helper + call_indirect) still per-function loud-declines the call_indirect export while the reachable direct-call helpers compile — the falcon shape, silicon-gated. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-cli/src/main.rs | 17 +- .../reachable_callgraph_275_selfcontained.wat | 34 ++++ ...allgraph_275_selfcontained_differential.py | 167 ++++++++++++++++++ 3 files changed, 217 insertions(+), 1 deletion(-) create mode 100644 scripts/repro/reachable_callgraph_275_selfcontained.wat create mode 100644 scripts/repro/reachable_callgraph_275_selfcontained_differential.py diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index f0578cbc..23c831f2 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -2679,7 +2679,22 @@ fn compile_all_exports( // num_imports) stay external — the linker resolves them. A module whose // exports call no internal function (every leaf fixture) yields exactly // the exports, so existing output stays bit-identical. - let reachable = reachable_from_exports(&module.functions, num_imports, &elem_func_indices); + let mut reachable = + reachable_from_exports(&module.functions, num_imports, &elem_func_indices); + // #275 non-vacuity hatch (TEST ONLY): `EXPORTS_ONLY_275=1` reverts to the + // pre-#235 exports-only behavior (drop every non-exported reachable + // callee) so the reachable-callgraph EXECUTION differential can prove it + // catches the historical drop — a self-contained export whose BL targets + // a now-absent helper. Never set in production; default path is the full + // reachable closure. + if std::env::var_os("EXPORTS_ONLY_275").is_some() { + reachable.retain(|idx| { + module + .functions + .iter() + .any(|f| f.index == *idx && f.export_name.is_some()) + }); + } // Preserve definition order; keep exports + reachable internal callees. let exports: Vec<_> = module .functions diff --git a/scripts/repro/reachable_callgraph_275_selfcontained.wat b/scripts/repro/reachable_callgraph_275_selfcontained.wat new file mode 100644 index 00000000..9d1fb74c --- /dev/null +++ b/scripts/repro/reachable_callgraph_275_selfcontained.wat @@ -0,0 +1,34 @@ +(module + ;; #275 — the DIRECT reachable call graph on the SELF-CONTAINED --cortex-m + ;; image. Only `entry` is exported; every helper below is NON-exported and is + ;; reached ONLY through a static `call`. Pre-#235 the self-contained builder + ;; emitted exports only, so these helpers were absent and `entry`'s BL had no + ;; target — the image could not execute. This fixture makes the omission + ;; observable at RUNTIME (a wrong numeric result), not just via `nm`. + + ;; leaf helper (func 0) — reached transitively (entry -> mid -> leaf) + (func $leaf (param i32) (result i32) + (i32.mul (local.get 0) (i32.const 7))) + + ;; mid helper (func 1) — reached from `entry`, and itself calls `leaf` + (func $mid (param i32) (result i32) + (i32.add (call $leaf (local.get 0)) (i32.const 3))) + + ;; a SECOND directly-reached helper (func 2) with a distinct constant, so a + ;; single wrong BL target (mid vs add5) is caught, not laundered. + (func $add5 (param i32) (result i32) + (i32.add (local.get 0) (i32.const 5))) + + ;; a NON-reachable dead helper (func 3) — must NOT be required for the image + ;; to run; its presence/absence is irrelevant to correctness (reachability is + ;; a closure, not "emit everything"). + (func $dead (param i32) (result i32) + (i32.sub (local.get 0) (i32.const 999))) + + ;; exported entry (func 4): result = mid(x) + add5(x) + ;; = (x*7 + 3) + (x + 5) = 8*x + 8 + ;; A dropped/mispatched helper changes this for every non-degenerate x. + (func (export "entry") (param i32) (result i32) + (i32.add + (call $mid (local.get 0)) + (call $add5 (local.get 0))))) diff --git a/scripts/repro/reachable_callgraph_275_selfcontained_differential.py b/scripts/repro/reachable_callgraph_275_selfcontained_differential.py new file mode 100644 index 00000000..2e711b46 --- /dev/null +++ b/scripts/repro/reachable_callgraph_275_selfcontained_differential.py @@ -0,0 +1,167 @@ +#!/usr/bin/env python3 +"""#275 — the DIRECT reachable call graph must EXECUTE on the self-contained +`--cortex-m` image (no --relocatable, no loader). + +Only `entry` is exported. It calls two NON-exported helpers (`mid`, `add5`), +and `mid` calls a third (`leaf`) — so the correct result depends on the whole +transitive closure of static `call`s being COMPILED INTO the image and every +internal BL patched to the emitted callee's address. `dead` is unreachable and +must be irrelevant. + +This is an EXECUTION differential (not an `nm`/symtab presence check): a helper +that is present but mis-patched, or a helper that is dropped, both change the +numeric result. Ground truth is wasmtime; the ARM image runs on unicorn with +its OWN Reset_Handler startup (the harness fabricates nothing in RAM). + +Non-vacuity — this gate PROVABLY catches the pre-#235 exports-only drop: set +EXPORTS_ONLY_275=1 to compile with a synth built with the reachability filter +bypassed (helpers absent). Then `entry`'s BL targets are missing and the image +diverges (RED). With the shipped reachability walk (#235) every helper is +present and BL-resolved, so it matches for every vector (GREEN). + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=./target/debug/synth /tmp/w29venv/bin/python \ + scripts/repro/reachable_callgraph_275_selfcontained_differential.py +""" + +import os +import subprocess +import sys +from pathlib import Path + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_ARM, UC_MODE_THUMB, Uc, UcError +from unicorn.arm_const import ( + UC_ARM_REG_LR, + UC_ARM_REG_R0, + UC_ARM_REG_SP, +) + +WAT = Path(__file__).with_name("reachable_callgraph_275_selfcontained.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") + +FLASH, RAM, RAM_SIZE = 0x0000_0000, 0x2000_0000, 0x40000 +RET = 0x000F_0000 # inside the flash map, far past any code + + +def compile_synth(out): + env = {"PATH": "/usr/bin:/bin"} + # Thread the non-vacuity hatch through the hermetic env (see module docstring). + if os.environ.get("EXPORTS_ONLY_275"): + env["EXPORTS_ONLY_275"] = os.environ["EXPORTS_ONLY_275"] + cmd = [SYNTH, "compile", str(WAT), "-o", out, "--all-exports", + "-b", "arm", "--target", "cortex-m3"] + cmd += os.environ.get("EXTRA_SYNTH_FLAGS", "").split() + r = subprocess.run(cmd, capture_output=True, text=True, env=env) + if r.returncode != 0: + sys.exit(f"compile failed: {r.stderr}") + + +def load(elf): + f = ELFFile(open(elf, "rb")) + etype = f["e_type"] # ET_EXEC = self-contained; ET_REL = needs a linker + text = f.get_section_by_name(".text") + code, base = text.data(), text["sh_addr"] + syms = {} + for sec in f.iter_sections(): + if sec.header.sh_type == "SHT_SYMTAB": + for sy in sec.iter_symbols(): + if sy.name and sy["st_info"]["type"] == "STT_FUNC": + syms[sy.name] = sy["st_value"] + return code, base, syms, etype + + +class ImageRunner: + """The DEFAULT self-contained image, startup included: one persistent + unicorn instance on ZEROED RAM. Only what the ARTIFACT's own reset path + copies to RAM is there — the harness fabricates nothing.""" + + def __init__(self, code, base, syms): + self.base, self.syms = base, syms + self.mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB) + self.mu.mem_map(FLASH, 0x100000) + self.mu.mem_map(RAM, RAM_SIZE) + self.mu.mem_map(0xE000E000, 0x1000) # SCS page + self.mu.mem_write(base, code) + self.sp = int.from_bytes(code[0:4], "little") + reset = syms.get("Reset_Handler") + if reset is None: + sys.exit("Reset_Handler missing from symtab") + # Execute the real startup UP TO the `LDR r0,[pc,#4]; BLX r0` scaffold. + stop = code.find(b"\x01\x48\x80\x47", (reset & ~1) - base) + if stop < 0: + sys.exit("startup call scaffold (LDR r0/BLX r0) not found") + self.mu.reg_write(UC_ARM_REG_SP, self.sp) + self.mu.emu_start(reset | 1, base + stop, count=100000) + + def call(self, fn, arg): + faddr = self.syms.get(fn) + if faddr is None: + return f"ERR:symbol {fn} missing" + self.mu.reg_write(UC_ARM_REG_SP, self.sp) + self.mu.reg_write(UC_ARM_REG_LR, RET | 1) + self.mu.reg_write(UC_ARM_REG_R0, arg & 0xFFFFFFFF) + try: + self.mu.emu_start(faddr | 1, RET, count=100000) + except UcError as e: + return f"ERR:{e}" + return self.mu.reg_read(UC_ARM_REG_R0) & 0xFFFFFFFF + + +class WasmtimeRunner: + def __init__(self): + engine = wasmtime.Engine() + module = wasmtime.Module.from_file(engine, str(WAT)) + self.store = wasmtime.Store(engine) + self.inst = wasmtime.Instance(self.store, module, []) + + def call(self, fn, arg): + r = self.inst.exports(self.store)[fn](self.store, arg) + return (r if r is not None else 0) & 0xFFFFFFFF + + +VECTORS = [0, 1, 2, 5, 17, 100, 0x1000] + + +def main(): + out = "/tmp/reachable275.elf" + compile_synth(out) + code, base, syms, etype = load(out) + mode = "EXPORTS-ONLY (reachability bypassed)" if os.environ.get( + "EXPORTS_ONLY_275") else "shipped reachability walk (#235)" + print(f"=== #275 self-contained reachable-callgraph EXECUTION [{mode}] ===") + # A self-contained --cortex-m image MUST be an executable (ET_EXEC). If a + # reachable helper was dropped, `entry`'s BL to it becomes an EXTERNAL + # relocation, and the builder degrades to a link-me ET_REL object with no + # Reset_Handler — not runnable standalone. That is the pre-#235 #275 drop. + if etype != "ET_EXEC": + print(f" [BUG] output is {etype}, not ET_EXEC — a reachable helper was " + "dropped, so the image is NOT self-contained (needs a linker).") + print("\nORACLE: FAIL (1 divergence — image is not self-contained)") + sys.exit(1) + img = ImageRunner(code, base, syms) + gt = WasmtimeRunner() + # Presence probe (informational — internal callees are emitted as func_N): + # func_0=leaf, func_1=mid, func_2=add5 are the reachable closure; func_3 + # (dead) is unreachable and must be ABSENT (a closure, not "emit all"). + for h in ("func_0", "func_1", "func_2"): + print(f" symtab: {h} {'present' if h in syms else 'ABSENT'}") + print(f" symtab: func_3 (dead) " + f"{'PRESENT (unexpected)' if 'func_3' in syms else 'absent (ok)'}") + fails = 0 + for x in VECTORS: + exp = gt.call("entry", x) + got = img.call("entry", x) + match = isinstance(got, int) and got == exp + if not match: + fails += 1 + shown = hex(got) if isinstance(got, int) else got + print(f" [{'ok ' if match else 'BUG'}] entry({x}) -> {shown} " + f"(wasmtime {exp:#x})") + print(f"\nORACLE: {'PASS' if fails == 0 else f'FAIL ({fails} divergences)'}") + sys.exit(0 if fails == 0 else 1) + + +if __name__ == "__main__": + main() From 2b931b28b52367383d78ffe7897247507292ad50 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 16 Jul 2026 18:46:47 +0200 Subject: [PATCH 2/3] ci(#275): wire the self-contained reachable-callgraph oracle (GREEN + RED non-vacuity) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds both directions to the trap-semantics-oracle job (already has wasmtime/unicorn/pyelftools): the GREEN gate runs the default self-contained image and diffs entry(x) vs wasmtime; the RED step asserts EXPORTS_ONLY_275=1 (pre-#235 exports-only drop) degrades to a non-self-contained ET_REL and the oracle fails — `! ...` because RED is the expected, gated outcome. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index febb9ea0..930d18b9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -549,6 +549,26 @@ jobs: # region (must stay 0). RED on v0.43.0 (4/5 read 0) -> GREEN. - name: Run self-contained data-segment oracle (#758, cortex-m3) run: SYNTH=./target/debug/synth python scripts/repro/self_contained_data_758_differential.py + # #275: the DIRECT reachable call graph must EXECUTE on the self-contained + # --cortex-m image (no --relocatable, no loader). Only `entry` is exported; + # it calls two non-exported helpers, one of which calls a third — result + # 8*x+8 depends on the whole transitive `call` closure being compiled in + # and every internal BL patched to the emitted callee. Runs the DEFAULT + # image (its own Reset_Handler startup) on unicorn vs wasmtime for 7 + # vectors; an unreachable helper is confirmed absent (closure, not + # emit-all). The reachability walk is #235 (v0.11.28) — this is the missing + # EXECUTION gate. + - name: Run self-contained reachable-callgraph oracle (#275, cortex-m3, GREEN) + run: SYNTH=./target/debug/synth python scripts/repro/reachable_callgraph_275_selfcontained_differential.py + # Non-vacuity: EXPORTS_ONLY_275=1 reverts to the pre-#235 exports-only drop + # (non-exported reachable callees removed). `entry`'s BL then becomes an + # external relocation and the builder degrades to a link-me ET_REL object + # with no Reset_Handler — NOT self-contained. The gate MUST go RED, proving + # it catches the historical #275 drop. `! ...` because RED = expected here. + - name: Reachable-callgraph oracle catches the pre-#235 drop (#275, RED) + run: | + ! EXPORTS_ONLY_275=1 SYNTH=./target/debug/synth \ + python scripts/repro/reachable_callgraph_275_selfcontained_differential.py # #406/#739-cluster coverage WIDENER: multi-chunk / multi-segment static # data across BOTH the self-contained (--cortex-m) and --relocatable # paths, segments at varied offsets — low, an UNALIGNED segment From 5e3aed21afb71e608b359b104b57b3f59180e18e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 16 Jul 2026 18:51:47 +0200 Subject: [PATCH 3/3] refactor(#275): feature-gate the non-vacuity hatch out of the release binary MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Cold-review fix: the previous EXPORTS_ONLY_275 env hatch was a permanent "regress to the fixed #275 defect" switch in the shipped compiler — a footgun with no precedent (SYNTH_SPILL_ON_EXHAUST/SYNTH_SHIFT_MASK_ELIDE gate real alternative behaviors, not reproductions of a fixed bug). Now gated behind a non-default cargo feature `exports_only_275_probe`. The default/release build physically cannot carry the hatch (the block is `#[cfg(feature = ...)]`-compiled out; the default binary ignores EXPORTS_ONLY_275 entirely). CI builds a SEPARATE probe binary (distinct --target-dir so it never shadows the default) only for the RED non-vacuity step; every GREEN step uses the normal binary. Verified: default binary + EXPORTS_ONLY_275=1 -> GREEN (hatch inert); probe binary + EXPORTS_ONLY_275=1 -> RED (ET_REL, not self-contained). clippy clean with and without the feature. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 18 ++++++++++++------ crates/synth-cli/Cargo.toml | 6 ++++++ crates/synth-cli/src/main.rs | 16 ++++++++++------ 3 files changed, 28 insertions(+), 12 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 930d18b9..634d7f80 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -560,14 +560,20 @@ jobs: # EXECUTION gate. - name: Run self-contained reachable-callgraph oracle (#275, cortex-m3, GREEN) run: SYNTH=./target/debug/synth python scripts/repro/reachable_callgraph_275_selfcontained_differential.py - # Non-vacuity: EXPORTS_ONLY_275=1 reverts to the pre-#235 exports-only drop - # (non-exported reachable callees removed). `entry`'s BL then becomes an - # external relocation and the builder degrades to a link-me ET_REL object - # with no Reset_Handler — NOT self-contained. The gate MUST go RED, proving - # it catches the historical #275 drop. `! ...` because RED = expected here. + # Non-vacuity: a SEPARATE probe binary (feature `exports_only_275_probe`, + # NEVER in the default/release build) exposes an `EXPORTS_ONLY_275=1` env + # hatch that reverts to the pre-#235 exports-only drop (non-exported + # reachable callees removed). `entry`'s BL then becomes an external + # relocation and the builder degrades to a link-me ET_REL object with no + # Reset_Handler — NOT self-contained. The gate MUST go RED, proving it + # catches the historical #275 drop. `! ...` because RED = expected here. + # The probe binary goes to a distinct target dir so it never shadows the + # default binary the GREEN steps use. + - name: Build #275 non-vacuity probe binary (non-default feature) + run: cargo build -p synth-cli --features exports_only_275_probe --target-dir target-275probe - name: Reachable-callgraph oracle catches the pre-#235 drop (#275, RED) run: | - ! EXPORTS_ONLY_275=1 SYNTH=./target/debug/synth \ + ! EXPORTS_ONLY_275=1 SYNTH=./target-275probe/debug/synth \ python scripts/repro/reachable_callgraph_275_selfcontained_differential.py # #406/#739-cluster coverage WIDENER: multi-chunk / multi-segment static # data across BOTH the self-contained (--cortex-m) and --relocatable diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 99b130fb..0aa2c6e8 100644 --- a/crates/synth-cli/Cargo.toml +++ b/crates/synth-cli/Cargo.toml @@ -45,6 +45,12 @@ awsm = ["synth-backend-awsm"] wasker = ["synth-backend-wasker"] riscv = ["synth-backend-riscv"] verify = ["synth-verify"] +# #275 non-vacuity probe (NEVER default): builds an `EXPORTS_ONLY_275` env hatch +# that reverts compile_all_exports to the pre-#235 exports-only drop, so the +# reachable-callgraph EXECUTION differential can prove it catches the historical +# #275 drop (the RED direction). Excluded from every release/default build — the +# release binary physically cannot carry a "regress to a fixed defect" switch. +exports_only_275_probe = [] # Uncomment when loom crate is available: # loom = ["dep:loom-opt"] diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 23c831f2..36bbc8de 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -2679,14 +2679,18 @@ fn compile_all_exports( // num_imports) stay external — the linker resolves them. A module whose // exports call no internal function (every leaf fixture) yields exactly // the exports, so existing output stays bit-identical. + #[cfg_attr(not(feature = "exports_only_275_probe"), allow(unused_mut))] let mut reachable = reachable_from_exports(&module.functions, num_imports, &elem_func_indices); - // #275 non-vacuity hatch (TEST ONLY): `EXPORTS_ONLY_275=1` reverts to the - // pre-#235 exports-only behavior (drop every non-exported reachable - // callee) so the reachable-callgraph EXECUTION differential can prove it - // catches the historical drop — a self-contained export whose BL targets - // a now-absent helper. Never set in production; default path is the full - // reachable closure. + // #275 non-vacuity probe (feature `exports_only_275_probe`, NEVER in a + // default/release build): `EXPORTS_ONLY_275=1` reverts to the pre-#235 + // exports-only behavior (drop every non-exported reachable callee) so the + // reachable-callgraph EXECUTION differential can prove it catches the + // historical drop — a self-contained export whose BL targets a now-absent + // helper (the image then degrades to a link-me ET_REL object). The default + // path is the full reachable closure and this block does not exist in the + // shipped binary. + #[cfg(feature = "exports_only_275_probe")] if std::env::var_os("EXPORTS_ONLY_275").is_some() { reachable.retain(|idx| { module