diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index febb9ea0..634d7f80 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -549,6 +549,32 @@ 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: 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-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 # paths, segments at varied offsets — low, an UNALIGNED segment 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 f0578cbc..36bbc8de 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -2679,7 +2679,26 @@ 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); + #[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 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 + .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()