test(#275): execution gate for the self-contained reachable call graph

.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

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"]
 

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

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)))))

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()