diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 290d63ad..3c5158e9 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs index daaebf57..18d8130d 100644 --- a/crates/synth-backend/src/arm_backend.rs +++ b/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 diff --git a/scripts/repro/br_table_507_differential.py b/scripts/repro/br_table_507_differential.py new file mode 100644 index 00000000..6bae663c --- /dev/null +++ b/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(" 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()