fix(arm): optimized path declines br_table to the direct selector (#507, #242) (#508)

* fix(arm): optimized path declines br_table to the direct selector (#507, #242)

On the optimized (non-`--relocatable`) path, `synth compile` SILENTLY
miscompiled `br_table`: the dispatch is dropped during the wasm→IR lowering
(`optimize_full`), so `ir_to_arm` emitted the arm bodies in fall-through sequence
with no `cmp`/branch on the selector — the selector value isn't even loaded, so
every input hits the last arm (exit 0, no warning, violating the #180/#185
Ok-or-Err contract). The `--relocatable` direct path lowered the identical module
correctly, so gust and the shipped falcon firmware (both `--relocatable`) were
unaffected — this was an optimized-path-only hazard.

Because the dispatch is dropped BEFORE `ir_to_arm`, there's no `Err` to fall back
on. The fix detects `br_table` on the raw wasm op stream in `arm_backend` and
forces the direct selector (`select_with_stack`), which lowers it as a real
cmp-chain. Same decline-to-direct shape as #496 / issue-#120: honest degradation,
the function compiles correctly without IR-level optimization. The declined
output is byte-identical to `--no-optimize`.

Frozen-safe by construction: the frozen byte gate compiles `--relocatable`
(already direct), and no optimized-path fixture (control_step, flight_algo)
contains `br_table`, so they stay on the optimized path bit-identically.

Gated by scripts/repro/br_table_507_differential.py (CI: br-table-507-oracle):
two table shapes (sequential, shared-tail) × every selector incl. out-of-range,
compiled via the DEFAULT optimized path, execute bit-identically to wasmtime;
pre-fix every non-last selector mismatched. Unit test
test_507_br_table_declines_to_direct asserts the optimized-default bytes equal
the direct selector's. Frozen bit-identical; control_step (13/13), r12-spill-496,
stack-args-503, block-brif-483 oracles all green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* style: rustfmt the #507 test's I32Store literals

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: avrabe

.github/workflows/ci.yml

@@ -497,3 +497,42 @@ jobs:
         env:
           SYNTH: ./target/debug/synth
         run: python scripts/repro/stack_args_503_differential.py
+
+  br-table-507-oracle:
+    name: optimized-path br_table oracle
+    # VCR-ORACLE-001 (#242, #507): EXECUTE br_table dispatch compiled via the
+    # DEFAULT optimized path (no --relocatable) under unicorn (UC_ARCH_ARM /
+    # Thumb) and diff the resulting linear memory vs wasmtime across every
+    # selector (incl. out-of-range → default arm) and two table shapes. Guards
+    # the #507 fix: the optimized path DROPPED the br_table dispatch during
+    # wasm→IR, emitting the arm bodies in fall-through with no selector compare —
+    # a silent miscompile (every input hit the last arm). The fix detects
+    # br_table on the raw wasm op stream and forces the direct selector (which
+    # lowers it as a cmp-chain). The frozen byte gate only covers the
+    # --relocatable direct path, so nothing else exercises the default path's
+    # br_table lowering. Isolated job: emulation deps pip-installed here ONLY.
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v7
+      - uses: dtolnay/rust-toolchain@stable
+      - name: Cache Cargo dependencies
+        uses: actions/cache@v5
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: |
+            ${{ runner.os }}-cargo-
+      - name: Build synth
+        run: cargo build -p synth-cli
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.x"
+      - name: Install emulation deps
+        run: pip install wasmtime unicorn pyelftools
+      - name: Run br_table oracle
+        env:
+          SYNTH: ./target/debug/synth
+        run: python scripts/repro/br_table_507_differential.py

crates/synth-backend/src/arm_backend.rs

@@ -314,7 +314,23 @@ fn compile_wasm_to_arm(
     // host-linked object, where the linmem base arrives via `fp` at runtime and
     // callees follow AAPCS. `select_with_stack` (now i64-spill capable after
     // #171) handles fp-relative memory + caller-saved preservation correctly.
-    let arm_instrs = if config.no_optimize || config.relocatable {
+    //
+    // #507: `br_table` is DROPPED during the optimized path's wasm→IR lowering
+    // (`optimize_full`), so `ir_to_arm` never sees the dispatch — it emits the
+    // arm bodies in fall-through sequence with no `cmp`/branch on the selector, a
+    // SILENT miscompile (every input hits the last arm). The selector value isn't
+    // even loaded. Because the drop happens before `ir_to_arm`, there's no `Err`
+    // to fall back on; detect it on the raw wasm op stream here and force the
+    // direct selector (`select_with_stack` lowers `br_table` correctly as a
+    // cmp-chain — confirmed on the `--relocatable` path). Same honest-degradation
+    // contract as the issue-#120 f32 decline: the function still compiles
+    // correctly, just without IR-level optimization. Frozen-safe: the frozen
+    // fixtures compile `--relocatable` (already direct), and no optimized-path
+    // fixture (control_step, flight_algo) contains `br_table`.
+    let has_br_table = wasm_ops
+        .iter()
+        .any(|op| matches!(op, WasmOp::BrTable { .. }));
+    let arm_instrs = if config.no_optimize || config.relocatable || has_br_table {
         select_direct()?
     } else {
         let opt_config = if config.loom_compat {
@@ -1306,6 +1322,72 @@ mod tests {
         );
     }
 
+    /// #507: a `br_table` function compiled via the DEFAULT (optimized) config
+    /// must produce the SAME bytes as the direct (`no_optimize`) selector —
+    /// i.e. the optimized path declined it to direct, lowering the dispatch as a
+    /// real cmp-chain instead of silently dropping it (which left all arms in
+    /// fall-through). Pre-fix the two outputs differed (the optimized one had no
+    /// selector compare). Execution correctness is gated by
+    /// `scripts/repro/br_table_507_differential.py`.
+    #[test]
+    fn test_507_br_table_declines_to_direct() {
+        let backend = ArmBackend::new();
+        // dispatch(sel): br_table over 3 blocks, each storing a marker to mem[0].
+        let ops = vec![
+            WasmOp::Block,
+            WasmOp::Block,
+            WasmOp::Block,
+            WasmOp::LocalGet(0),
+            WasmOp::BrTable {
+                targets: vec![0, 1, 2],
+                default: 2,
+            },
+            WasmOp::End,
+            WasmOp::I32Const(0),
+            WasmOp::I32Const(10),
+            WasmOp::I32Store {
+                offset: 0,
+                align: 2,
+            },
+            WasmOp::Return,
+            WasmOp::End,
+            WasmOp::I32Const(0),
+            WasmOp::I32Const(20),
+            WasmOp::I32Store {
+                offset: 0,
+                align: 2,
+            },
+            WasmOp::Return,
+            WasmOp::End,
+            WasmOp::I32Const(0),
+            WasmOp::I32Const(30),
+            WasmOp::I32Store {
+                offset: 0,
+                align: 2,
+            },
+        ];
+        let opt = CompileConfig {
+            target: TargetSpec::cortex_m4(),
+            ..CompileConfig::default()
+        };
+        let direct = CompileConfig {
+            target: TargetSpec::cortex_m4(),
+            no_optimize: true,
+            ..CompileConfig::default()
+        };
+        let a = backend
+            .compile_function("dispatch", &ops, &opt)
+            .expect("optimized-default must compile br_table (via decline)");
+        let b = backend
+            .compile_function("dispatch", &ops, &direct)
+            .expect("direct must compile br_table");
+        assert_eq!(
+            a.code, b.code,
+            "#507: optimized-default br_table output must be byte-identical to the \
+             direct selector (i.e. declined to direct), not a dropped dispatch"
+        );
+    }
+
     /// Issue #94: end-to-end byte-size check for the canonical u64-packed
     /// FFI-return hi32 extract pattern. Compiles two near-identical
     /// functions — one with the optimized shift-by-32, one with a generic

scripts/repro/br_table_507_differential.py

@@ -0,0 +1,149 @@
+#!/usr/bin/env python3
+"""#507 (epic #242) — EXECUTION-validate the optimized-path br_table fix.
+
+On the optimized (non-`--relocatable`) path, `synth compile` silently
+miscompiled `br_table`: the dispatch is DROPPED during the wasm→IR lowering, so
+the arm bodies were emitted in fall-through sequence with no `cmp`/branch on the
+selector — every input hit the last arm (a silent wrong-code, exit 0). The
+`--relocatable` direct path lowered it correctly. The fix detects `br_table` on
+the raw wasm op stream and forces the direct selector (which lowers it as a
+cmp-chain), so the DEFAULT `synth compile` is correct too.
+
+This harness compiles the fixture via the DEFAULT optimized path (no
+`--relocatable`), runs `dispatch(sel)` under unicorn (UC_ARCH_ARM / Thumb) for
+each selector, and asserts the resulting linear memory matches wasmtime. Symbols
+come from the ELF symtab (SHT_SYMTAB); the linmem base is read from
+`__linear_memory_base` (mask the Thumb bit on the function symbol).
+
+NON-VACUITY: pre-fix every selector yielded mem[0]=40 (the last arm); the fix
+changed the function's bytes (the optimized fall-through became a cmp-chain,
+byte-identical to `--no-optimize`). A regression that re-drops the dispatch
+re-breaks every non-last selector here.
+
+Run (needs wasmtime + unicorn + pyelftools):
+  SYNTH=./target/debug/synth python scripts/repro/br_table_507_differential.py
+Exits nonzero on any mismatch or fault.
+"""
+import os
+import struct
+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_R11,
+    UC_ARM_REG_SP,
+)
+
+SYNTH = os.environ.get("SYNTH", "./target/release/synth")
+CODE, STK, RET = 0x100000, 0x900000, 0x300000
+LIN_SIZE = 0x10000  # 1 page
+
+# Three br_table shapes (sequential targets, shared-tail, value-returning) — the
+# three gale reproduced. Each stores a selector-dependent marker to mem[0].
+FIXTURES = {
+    # sequential distinct targets
+    "seq": """(module (memory (export "memory") 1)
+ (func (export "dispatch") (param i32)
+  (block (block (block (block
+    (br_table 0 1 2 3 (local.get 0)))
+    (i32.store (i32.const 0)(i32.const 10))(return))
+    (i32.store (i32.const 0)(i32.const 20))(return))
+    (i32.store (i32.const 0)(i32.const 30))(return))
+  (i32.store (i32.const 0)(i32.const 40))))""",
+    # shared-tail: targets 0 and 2 jump to the same arm
+    "shared": """(module (memory (export "memory") 1)
+ (func (export "dispatch") (param i32)
+  (block (block (block
+    (br_table 0 1 0 2 (local.get 0)))
+    (i32.store (i32.const 0)(i32.const 11))(return))
+    (i32.store (i32.const 0)(i32.const 22))(return))
+  (i32.store (i32.const 0)(i32.const 33))))""",
+}
+# selectors to test per fixture (incl. an out-of-range → default arm)
+SELECTORS = [0, 1, 2, 3, 4, 7]
+
+
+def compile_default(wat_text, elf):
+    wat = elf + ".wat"
+    Path(wat).write_text(wat_text)
+    r = subprocess.run(
+        [SYNTH, "compile", wat, "-o", elf, "--target", "cortex-m4", "--all-exports"],
+        capture_output=True, text=True, env={"PATH": "/usr/bin:/bin"},
+    )
+    if r.returncode != 0 or "skipping" in r.stderr:
+        sys.exit(f"compile failed/skipped for {elf}:\n{r.stderr}")
+    return wat
+
+
+def load(elf):
+    f = ELFFile(open(elf, "rb"))
+    text = f.get_section_by_name(".text")
+    code, base = text.data(), text["sh_addr"]
+    syms = {}
+    for s in f.iter_sections():
+        if s.header.sh_type == "SHT_SYMTAB":
+            for sym in s.iter_symbols():
+                if sym.name:
+                    syms[sym.name] = sym["st_value"]
+    return code, base, syms
+
+
+def wasmtime_mem0(wat_text, sel):
+    eng = wasmtime.Engine()
+    mod = wasmtime.Module(eng, wat_text)
+    st = wasmtime.Store(eng)
+    inst = wasmtime.Instance(st, mod, [])
+    inst.exports(st)["dispatch"](st, sel)
+    return struct.unpack("<i", bytes(inst.exports(st)["memory"].read(st, 0, 4)))[0]
+
+
+def unicorn_mem0(code, base, faddr, lin_base, sel):
+    foff = (faddr & ~1) - base
+    mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB)
+    mu.mem_map(CODE, 0x20000)
+    mu.mem_map(lin_base, LIN_SIZE)
+    mu.mem_map(STK - 0x10000, 0x20000)
+    mu.mem_map(RET & ~0xFFF, 0x1000)
+    mu.mem_write(CODE, code)
+    mu.reg_write(UC_ARM_REG_SP, STK)
+    mu.reg_write(UC_ARM_REG_R11, lin_base)
+    mu.reg_write(UC_ARM_REG_R0, sel & 0xFFFFFFFF)
+    mu.reg_write(UC_ARM_REG_LR, RET | 1)
+    try:
+        mu.emu_start((CODE + foff) | 1, RET, count=200000)
+    except UcError as e:
+        return f"ERR:{e}"
+    return struct.unpack("<i", bytes(mu.mem_read(lin_base, 4)))[0]
+
+
+def main():
+    if not os.path.exists(SYNTH):
+        sys.exit(f"{SYNTH} not found — build synth first")
+    fails = 0
+    for name, wat_text in FIXTURES.items():
+        elf = f"/tmp/bt507_{name}.elf"
+        wat = compile_default(wat_text, elf)
+        code, base, syms = load(elf)
+        lin_base = syms["__linear_memory_base"]
+        fa = syms.get("dispatch") or syms["func_0"]
+        wt_text = Path(wat).read_text()
+        for sel in SELECTORS:
+            exp = wasmtime_mem0(wt_text, sel)
+            got = unicorn_mem0(code, base, fa, lin_base, sel)
+            ok = isinstance(got, int) and got == exp
+            fails += 0 if ok else 1
+            g = str(got) if isinstance(got, int) else got
+            print(f"{'OK  ' if ok else 'FAIL'} {name} dispatch({sel}) -> mem[0]={g} "
+                  f"(wasmtime {exp})")
+    print("\nORACLE:", "PASS" if fails == 0 else f"FAIL ({fails})")
+    sys.exit(1 if fails else 0)
+
+
+if __name__ == "__main__":
+    main()