|
| 1 | +#!/usr/bin/env python3 |
| 2 | +"""#483 (epic #242) — EXECUTION-validate optimized-path block/br_if lowering. |
| 3 | +
|
| 4 | +On the OPTIMIZED (non-`--relocatable`) ARM path, a forward `block` + `br_if` |
| 5 | +lowered to a conditional branch whose target landed MID-INSTRUCTION: the branch |
| 6 | +targeted the id pushed for the `Block` opener, but the only emitted label sat at |
| 7 | +the matching `End` carrying the End's *own* id — so the target resolved against |
| 8 | +an id no label held and was left as the unpatched offset-0 placeholder. A |
| 9 | +companion size-estimator gap (i32.store16 → `Strh`, a 4-byte `.w` encoding, was |
| 10 | +sized as 2) drifted `byte_offsets` so even a resolved branch missed by 2 bytes. |
| 11 | +
|
| 12 | +This harness compiles the fixture via the optimized path, runs each function |
| 13 | +under unicorn (UC_ARCH_ARM / Thumb) with the linear memory mapped at the absolute |
| 14 | +base the optimized path materializes, and asserts the resulting MEMORY is |
| 15 | +bit-identical to wasmtime ground truth across both branch directions (taken / |
| 16 | +not-taken). The functions write memory and return nothing, so memory is the |
| 17 | +observable. Before the fix, `init_branch(0)` (br_if taken → block skipped) wrote |
| 18 | +the guarded fields anyway. |
| 19 | +
|
| 20 | +Run (needs wasmtime + unicorn + pyelftools): |
| 21 | + SYNTH=./target/debug/synth python scripts/repro/block_brif_483_differential.py |
| 22 | +Exits nonzero on any mismatch. |
| 23 | +""" |
| 24 | +import os |
| 25 | +import subprocess |
| 26 | +import sys |
| 27 | +from pathlib import Path |
| 28 | + |
| 29 | +import wasmtime |
| 30 | +from elftools.elf.elffile import ELFFile |
| 31 | +from unicorn import UC_ARCH_ARM, UC_MODE_THUMB, Uc |
| 32 | +from unicorn.arm_const import UC_ARM_REG_LR, UC_ARM_REG_R0, UC_ARM_REG_SP |
| 33 | + |
| 34 | +WAT = Path(__file__).with_name("block_brif_483.wat") |
| 35 | +SYNTH = os.environ.get("SYNTH", "./target/release/synth") |
| 36 | +# Absolute linear-memory base the optimized (non-relocatable) path materializes |
| 37 | +# for a const address: `movw ip,#0x100; movt ip,#0x2000` → 0x20000100 (see #197). |
| 38 | +LINMEM = 0x20000100 |
| 39 | +MEM_WINDOW = 64 # bytes of memory compared against ground truth |
| 40 | +# (function, [sel values exercising both branch directions]) |
| 41 | +CASES = {"init_branch": [0, 1], "nested": [0, 1]} |
| 42 | + |
| 43 | + |
| 44 | +def compile_optimized(out): |
| 45 | + r = subprocess.run( |
| 46 | + [SYNTH, "compile", str(WAT), "-o", out, "-b", "arm", |
| 47 | + "--target", "cortex-m4", "--all-exports"], |
| 48 | + capture_output=True, text=True, env={"PATH": "/usr/bin:/bin"}, |
| 49 | + ) |
| 50 | + if r.returncode != 0: |
| 51 | + sys.exit(f"compile failed: {r.stderr}") |
| 52 | + |
| 53 | + |
| 54 | +def load(elf): |
| 55 | + f = ELFFile(open(elf, "rb")) |
| 56 | + text = f.get_section_by_name(".text") |
| 57 | + data, base = text.data(), text["sh_addr"] |
| 58 | + syms = {} |
| 59 | + for s in f.iter_sections(): |
| 60 | + if s.header.sh_type == "SHT_SYMTAB": |
| 61 | + for sym in s.iter_symbols(): |
| 62 | + if sym.name: |
| 63 | + syms[sym.name] = sym["st_value"] |
| 64 | + return data, base, syms |
| 65 | + |
| 66 | + |
| 67 | +def wasm_mem(func, sel): |
| 68 | + eng = wasmtime.Engine() |
| 69 | + mod = wasmtime.Module(eng, WAT.read_bytes()) |
| 70 | + st = wasmtime.Store(eng) |
| 71 | + inst = wasmtime.Instance(st, mod, []) |
| 72 | + inst.exports(st)[func](st, sel) |
| 73 | + return bytes(inst.exports(st)["memory"].read(st, 0, MEM_WINDOW)) |
| 74 | + |
| 75 | + |
| 76 | +def run_rv(code, base, addr, sel): |
| 77 | + mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB) |
| 78 | + mu.mem_map(base & ~0xFFFF, 0x20000) |
| 79 | + mu.mem_write(base, code) |
| 80 | + mu.mem_map(LINMEM & ~0xFFFF, 0x20000) # page-aligned region covering LINMEM |
| 81 | + mu.mem_map(0x90000, 0x10000) |
| 82 | + ret = 0x90100 |
| 83 | + mu.mem_write(ret, b"\x00\xbf\x00\xbf") |
| 84 | + mu.reg_write(UC_ARM_REG_R0, sel & 0xFFFFFFFF) |
| 85 | + mu.reg_write(UC_ARM_REG_SP, 0x98000) |
| 86 | + mu.reg_write(UC_ARM_REG_LR, ret | 1) |
| 87 | + mu.emu_start(addr | 1, ret, timeout=5_000_000) |
| 88 | + return bytes(mu.mem_read(LINMEM, MEM_WINDOW)) |
| 89 | + |
| 90 | + |
| 91 | +def main(): |
| 92 | + if not os.path.exists(SYNTH): |
| 93 | + sys.exit(f"{SYNTH} not found — build synth first") |
| 94 | + elf = "/tmp/block_brif_483.elf" |
| 95 | + compile_optimized(elf) |
| 96 | + code, base, syms = load(elf) |
| 97 | + |
| 98 | + fails = 0 |
| 99 | + for func, sels in CASES.items(): |
| 100 | + for sel in sels: |
| 101 | + gt = wasm_mem(func, sel) |
| 102 | + got = run_rv(code, base, syms[func], sel) |
| 103 | + ok = got == gt |
| 104 | + if not ok: |
| 105 | + fails += 1 |
| 106 | + print(f"{'OK ' if ok else 'FAIL'} {func}(sel={sel})") |
| 107 | + if not ok: |
| 108 | + diff = [(i, gt[i], got[i]) for i in range(MEM_WINDOW) if gt[i] != got[i]] |
| 109 | + print(f" mem diffs (off, wasmtime, synth): {diff}") |
| 110 | + |
| 111 | + print("ORACLE:", "PASS" if fails == 0 else f"FAIL ({fails})") |
| 112 | + sys.exit(1 if fails else 0) |
| 113 | + |
| 114 | + |
| 115 | +if __name__ == "__main__": |
| 116 | + main() |
0 commit comments