From 0c14b475d2bfb0d41e2849cce740e81e77795b5d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 20 Aug 2026 23:17:42 +0200 Subject: [PATCH 1/2] =?UTF-8?q?test(#989):=20RED-FIRST=20=E2=80=94=20unico?= =?UTF-8?q?rn-vs-wasmtime=20WAR-aliasing=20differential,=20both=20ARM=20le?= =?UTF-8?q?gs=20(RQ-59-WARALIAS)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Executed on this commit (the unfixed tree) the oracle FAILS with 110 wrong vectors — the red is on the record before the fix, per the #973 template: BUG [rv32_local_promotion_472.wat:relocatable] war_set(42): want=142 got=200 (11 vectors, constant 200) BUG [rv32_local_promotion_472.wat:relocatable] war_tee(42): want=242 got=300 (11 vectors, constant 300) BUG [rv32_local_promotion_472.wat:self-contained] war_set/war_tee: same constants (optimized path) BUG [aarch64_param_homing_851.wat:relocatable] get_set_get_param_no_alias: constant 10 (11 vectors) BUG [aarch64_param_homing_851.wat:relocatable] tee_param_no_alias: constant 30 (12 vectors) BUG [aarch64_param_homing_851.wat:self-contained] get_set_get_param_no_alias(42): want=47 got=84 (= 2p: the param store is DROPPED on the optimized path, a distinct mechanism) BUG [aarch64_param_homing_851.wat:self-contained] write_last_of_three / swap_two_params: stores dropped #989 CHECKS=225/335 — FAIL Every all-i32 export of both existing fixtures is compared against wasmtime on a 12-tuple boundary matrix, on BOTH ARM lowering paths (--relocatable direct selector AND the self-contained/optimized path), sub-SP stack poisoned, symmetric fuel/instruction budgets. Floors are the fixed tree's steady state (344 emulations / 340 compared), so this commit is red on the mismatches AND the comparison floor; the fix commit turns both green. Wired into the repro-sweep-arm-corpus job next to the #973 differential (evidence ledger floor 2 -> 3). Refs #989 --- .github/workflows/ci.yml | 4 +- .../war_aliasing_989_arm_differential.py | 284 ++++++++++++++++++ 2 files changed, 287 insertions(+), 1 deletion(-) create mode 100644 scripts/repro/war_aliasing_989_arm_differential.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a7e30030..380336a3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3624,6 +3624,8 @@ jobs: run: pip install wasmtime unicorn pyelftools capstone - name: "#973 i64-cmp select execution differential (both ARM legs)" run: python scripts/oracle_run.py scripts/repro/select_i64cmp_973_arm_differential.py + - name: "#989 local.set/tee WAR-aliasing execution differential (both ARM legs)" + run: python scripts/oracle_run.py scripts/repro/war_aliasing_989_arm_differential.py - name: "ARM corpus sweep — compile census + execution differential (#973)" run: python scripts/oracle_run.py scripts/repro/arm_corpus_sweep_973.py # #910: close the job with what it EXECUTED. Asserts every oracle @@ -3636,7 +3638,7 @@ jobs: if: always() run: | set -euo pipefail - python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2 + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 3 repro-sweep-wcet-oracle: name: repro sweep — WCET bound soundness cross-checks (phases 2-6) diff --git a/scripts/repro/war_aliasing_989_arm_differential.py b/scripts/repro/war_aliasing_989_arm_differential.py new file mode 100644 index 00000000..738d31da --- /dev/null +++ b/scripts/repro/war_aliasing_989_arm_differential.py @@ -0,0 +1,284 @@ +#!/usr/bin/env python3 +# ci-status: wired +# ci-checks: emulations >= 344 +"""#989 — ARM: `local.set`/`local.tee` CLOBBERS an earlier `local.get` of the +same local still on the operand stack (WAR aliasing). + +THE DEFECT. On ARM, `local.get $x` of a REGISTER-HOMED local (a param in +r0-r3, or a #390-promoted local in r4-r8) pushes the local's HOME REGISTER +onto the operand stack by reference — no copy. A later `local.set`/`local.tee` +of the SAME local writes that home register directly (`mov home, val`), +destroying the value the earlier `local.get` pushed. Every consumer downstream +reads the post-write value. No register pressure, no i64, no spill is needed — +it is a bare `local.get`/`local.set` pair: + + war_set(a) = old_x + new_x where x=a then x=100 — correct: a + 100 + 0046: mov r0, r0 ; local.set $x (local.get $a) -> x lives in r0 + 0048: movw r1, #0x64 + 004c: mov r0, r1 ; local.set $x = 100 — OVERWRITES the pushed old x + 004e: adds r2, r0, r0 ; 100 + 100 + -> returns 200 for EVERY input. + +RV32 has carried the guard since #472 (`snapshot_aliases` — its fixture's own +comment: "Without it these miscompile"). This differential is the ARM leg's +red-first evidence: it asserts the CORRECT values (wasmtime ground truth), so +it FAILS on the unfixed tree — 44 wrong vectors across 4 exports, measured — +and records the fix the moment the snapshot lands. + +THE FIXTURES ARE THE EXISTING ONES. `rv32_local_promotion_472.wat` (war_set / +war_tee — promoted non-param locals) and `aarch64_param_homing_851.wat` +(get_set_get_param_no_alias / tee_param_no_alias — register-homed PARAMS, +where the incoming argument is never read at all). Both files carry many +NON-aliasing exports (accum, rbw, swap_two_params, param_write_if_else, ...); +those are the contrast population the fix must NOT disturb, so every all-i32 +export of both modules is compared, not just the four wrong ones. + +Both ARM lowering paths are run: `--relocatable` (the direct selector, +`select_with_stack`, where #989 lives) and the self-contained/optimized path, +so a fix that only moves one is visible. + +Budgets are SYMMETRIC (wasmtime fuel / unicorn instruction count): a vector +that exhausts either side is skipped on both (`param_countdown_sum(-1)` is a +2^32-iteration counted loop). A unicorn fault where wasmtime returned within +budget is a FAILURE, never a skip. + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=./target/debug/synth python scripts/repro/war_aliasing_989_arm_differential.py +""" +import os +import struct +import subprocess +import sys +import tempfile +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_PC, + UC_ARM_REG_R0, + UC_ARM_REG_R1, + UC_ARM_REG_R2, + UC_ARM_REG_R3, + UC_ARM_REG_R11, + UC_ARM_REG_SP, +) + +REPRO = Path(__file__).resolve().parent +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") +TARGET = "cortex-m4f" + +FIXTURES = [ + "rv32_local_promotion_472.wat", + "aarch64_param_homing_851.wat", +] + +CODE, LIN = 0x100000, 0x40000 +RET_PAD = CODE + 0x38000 +STACK_BASE, STACK_SIZE = 0x80000, 0x10000 +SP0 = STACK_BASE + 0xC000 + +WASMTIME_FUEL = 2_000_000 +UNICORN_INSNS = 400_000 + +MEM_POISON = 0xDEADBEEF +REG_POISON = 0xFEEDFACE +CORE_ARGS = [UC_ARM_REG_R0, UC_ARM_REG_R1, UC_ARM_REG_R2, UC_ARM_REG_R3] +R_ARM_THM_CALL, R_ARM_THM_JUMP24 = 10, 30 +M32 = 0xFFFFFFFF + +# Boundary-heavy and the same for every export (sliced to its arity), so the +# population is a property of the corpus, not of per-export tuning. Includes +# the issue's own vectors (0, -5, 65535, 0x7FFFFFFF) — the pre-fix tree +# returns a CONSTANT (200 / 300 / 10 / 30) on every one of them. +ARG_TUPLES = [ + (0, 0, 0, 0), + (1, 2, 3, 4), + (7, 5, 3, 1), + (-5, -7, -9, -11), + (100, 100, 100, 100), + (-1, 1, -1, 1), + (1, -1, 1, -1), + (0xFFFF, 0x10000, 3, 2), + (0x7FFFFFFF, -1, 0x7FFFFFFF, -1), + (-1, 0x7FFFFFFF, 1, 0), + (0, -1, 0, -1), + (42, 13, 7, 99), +] + +# Floor on vectors actually COMPARED (not merely entered): a run that skipped +# everything on budget grounds would still clear an entry count. Measured on +# this corpus: 15 all-i32 exports x 12 vectors x 2 legs = 360, minus the 20 +# genuine budget skips (the 2^32-iteration countdown vectors on +# param_countdown_sum / cond_write_param_loop). Steady-state of the FIXED +# tree; the unfixed tree compares 335 (its WAR codegen pushes 5 more vectors +# over the symmetric budget) and fails on 110 mismatches long before this +# floor matters. +MIN_COMPARED = 340 + +emulations = 0 + + +def die(msg): + print(f"#989 ARM WAR ORACLE: FAIL — {msg}") + sys.exit(1) + + +def compile_fixture(wat, out, relocatable): + cmd = [SYNTH, "compile", str(wat), "--target", TARGET, "--all-exports", "-o", out] + if relocatable: + cmd.append("--relocatable") + p = subprocess.run(cmd, capture_output=True, text=True) + if p.returncode != 0: + die(f"synth compile failed ({' '.join(cmd)}):\n{p.stdout}\n{p.stderr}") + return out + + +def encode_thm_bl(pc_at_reloc, target): + """Re-encode a Thumb-2 BL, exactly as `ld` resolves R_ARM_THM_CALL.""" + off = (target - (pc_at_reloc + 4)) & 0x01FFFFFF + s = (off >> 24) & 1 + i1, i2 = (off >> 23) & 1, (off >> 22) & 1 + imm10, imm11 = (off >> 12) & 0x3FF, (off >> 1) & 0x7FF + j1, j2 = (~i1 & 1) ^ s, (~i2 & 1) ^ s + return 0xF000 | (s << 10) | imm10, 0xD000 | (j1 << 13) | (j2 << 11) | imm11 + + +def load(path): + """(symbols, .text with in-module branch relocations applied, base_vaddr).""" + with open(path, "rb") as fh: + e = ELFFile(fh) + symtab = [s for s in e.iter_sections() if s["sh_type"] == "SHT_SYMTAB"][0] + syms = {s.name: s["st_value"] for s in symtab.iter_symbols() if s.name} + sec = e.get_section_by_name(".text") + if sec is None: + die("no .text section in the compiled object") + base = sec["sh_addr"] + text = bytearray(sec.data()) + for rel in e.iter_sections(): + if rel["sh_type"] not in ("SHT_REL", "SHT_RELA"): + continue + for r in rel.iter_relocations(): + t = r["r_info_type"] + name = symtab.get_symbol(r["r_info_sym"]).name + if t not in (R_ARM_THM_CALL, R_ARM_THM_JUMP24): + die(f"unexpected reloc type {t} against {name!r}") + if name not in syms: + die(f"reloc names {name!r}, not a defined symbol") + off = r["r_offset"] + hw1, hw2 = encode_thm_bl(CODE + off, CODE + ((syms[name] - base) & ~1)) + struct.pack_into(" Date: Thu, 20 Aug 2026 23:28:38 +0200 Subject: [PATCH 2/2] =?UTF-8?q?fix(#989):=20ARM=20local.set/tee=20WAR=20al?= =?UTF-8?q?iasing=20=E2=80=94=20snapshot=20home-register=20aliases=20befor?= =?UTF-8?q?e=20the=20overwrite=20(RQ-59-WARALIAS)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ROOT CAUSE, both ARM lowering paths, determined by SYNTH_PATH_DEBUG tracing and capstone/objdump over the emitted bytes: 1. DIRECT selector (select_with_stack — the path --relocatable forces and the fallback for everything the optimizer declines). LocalGet of a register-homed local (param r0-r3 via local_to_reg, promoted local r4-r8) pushes StackVal::Reg{reg: HOME} — by reference, no copy. The LocalSet/LocalTee register-homed arms then emit `mov HOME, val`, destroying the value every earlier get of the same local pushed. FIX: `snapshot_home_reg_aliases` (the ARM analogue of RV32's #472 `snapshot_aliases`, placed at the same point in the write path): before the overwrite, copy any still-live alias of HOME to a freshly allocated temp and rewrite those stack entries. Fires only when an alias exists (code without the WAR shape stays byte-identical — measured: all 10 frozen anchors unchanged). tee skips its own kept top. i64 defence in depth: a pair overlapping HOME is snapshotted into a fresh CONSECUTIVE pair (ARM derives hi = lo+1, so a half-rewrite is unrepresentable). 2. OPTIMIZED IR path (OptimizerBridge/ir_to_arm — self-contained straight-line functions). Same by-reference model (`Load` maps its dest vreg to the home register), PLUS a second defect my differential surfaced: `Store` to a PARAM emitted NO instruction at all — the write was silently dropped (swap_two_params returned p0-p1 instead of p1-p0, write_last_of_three read the stale third param). FIX: honest degradation per the #500/#188 precedent — wasm_to_ir declines local.set/local.tee while an earlier get of the same local is live on the slot stack (exact, computed on the same slot_stack the IR builder already maintains), and ir_to_arm declines the param-Store arm outright; both fall back to the direct selector, which is now correct. EVIDENCE (red-first, previous commit): war_aliasing_989_arm_differential.py failed 110 vectors on the unfixed tree (constants 200/300/10/30 and the dropped-store shapes); this commit turns it 340/340 green on BOTH legs. The four #989 KNOWN_ARM_MISMATCHES entries are deleted per the sweep's both-direction ratchet; sweep PASSES (2375 vectors, 3 residual mismatches all #990). EXPECTED_DECLINES untouched (compiled 146/158, exact set green). Frozen anchors: byte-identical (cargo test --workspace 146 suites green) — no frozen fixture carries the WAR shape; the differential is the execution oracle for every function whose bytes DID change. Ratchet: selector_lines_code 17961 -> 18134 (+173, waiver in claims.yaml — new soundness decisions, zero new wildcard arms; wildcard ceiling unchanged at 55). MC/DC: counts bit-identical to the pristine v0.58.0 baseline in the same environment (17/121/51 locally; the local-vs-CI floor delta is a local witness/toolchain artifact — main CI's pinned job is green at 22/130/57 floors). RV32 guard non-vacuity (checked while here): force-eliding RV32 snapshot_aliases reds exactly ONE test — the STRUCTURAL forced-promotion unit test local_promotion_forced_war_snapshot_still_sound_472; no executed differential observes the guard because the promotion cost model declines the WAR shape end-to-end in production. Not vacuous, but structural-only. Refs #989 --- CHANGELOG.md | 24 ++++ artifacts/status.json | 4 +- claims.yaml | 21 +++- .../src/instruction_selector.rs | 110 ++++++++++++++++++ .../instruction_selector/select_with_stack.rs | 63 ++++++++++ .../synth-synthesis/src/optimizer_bridge.rs | 70 ++++++++++- scripts/repro/arm_corpus_sweep_973.py | 8 +- 7 files changed, 291 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a96eb4ab..90ebd1b2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,30 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Fixed + +- **#989 (RQ-59-WARALIAS): ARM `local.set`/`local.tee` clobbered an earlier + `local.get` of the same local still on the operand stack (WAR aliasing).** + `local.get` of a register-homed local (param in r0-r3, promoted local in + r4-r8) pushed the HOME register by reference; a later write to the same + local destroyed the pushed value — `war_set` returned 200 for every input. + Fixed on BOTH ARM lowering paths, gated by a new executed unicorn-vs-wasmtime + differential (`war_aliasing_989_arm_differential.py`, 110 wrong vectors → 0, + wired in CI) landed RED-FIRST before the fix: + - direct selector (`select_with_stack`, the `--relocatable`/production + path): new `snapshot_home_reg_aliases` guard — the ARM analogue of RV32's + #472 `snapshot_aliases` — copies still-live aliases to a fresh temp before + the home register is overwritten (i64 pairs snapshotted as consecutive + pairs, defence in depth); + - optimized IR path (self-contained straight-line functions): the same WAR + shape now LOUD-DECLINES to the direct selector (#500/#188-style honest + degradation), and a `local.set` of a PARAMETER — whose write the IR + lowering silently DROPPED (`swap_two_params` returned p0−p1 instead of + p1−p0) — declines likewise instead of miscompiling. + The four #989 entries left `KNOWN_ARM_MISMATCHES` (the sweep's + both-direction ratchet records the fix); all 10 frozen anchors are + byte-identical — no frozen fixture carries the WAR shape. + ## [0.58.0] - 2026-08-20 **Delete the thing you replaced.** diff --git a/artifacts/status.json b/artifacts/status.json index e9df0d51..49f56f2f 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -28,8 +28,8 @@ "sel_dsl_rule_qed": 74, "sel_dsl_rules": 74, "sel_rules_simplified_basis": 74, - "selector_lines_code": 17961, - "selector_lines_total": 28582, + "selector_lines_code": 18134, + "selector_lines_total": 28755, "selector_wildcard_arms_code": 55, "selector_wildcard_arms_total": 90, "version": "0.58.0", diff --git a/claims.yaml b/claims.yaml index 8d5db792..6ac4d100 100644 --- a/claims.yaml +++ b/claims.yaml @@ -1255,7 +1255,7 @@ claims: - kind: ratchet name: selector_lines_code direction: down - value: 17961 + value: 18134 baseline: 17897 waivers: - to: 17961 @@ -1299,6 +1299,20 @@ claims: the hand-written imm-fold/conversion/select emissions, each byte-identity-gated — the residual 15 above baseline is the #946 enumeration, still justified as stated above. + - to: 18134 + reason: >- + RQ-59-WARALIAS (#989): the executed local.set/local.tee WAR + miscompile — `local.get` of a register-homed local pushed the + HOME register by reference, and a later write to the SAME + local destroyed it (war_set returned 200 for every input, 44 + wrong vectors across 4 exports). +173 lines are the + `snapshot_home_reg_aliases` guard (the ARM analogue of RV32's + #472 `snapshot_aliases`) plus its four call sites in the + LocalSet/LocalTee register-homed arms — new SOUNDNESS + decisions, zero wildcards, gated by the executed + war_aliasing_989_arm_differential (110 wrong vectors -> 0, + both ARM legs) and the corpus sweep's both-direction ratchet + (the four #989 KNOWN_ARM_MISMATCHES entries deleted). # The whole-file figures the release plan and the sibling lanes quote. An # unpinned quoted number is the drift class this release is about — but # they are `track`, not `down`, and the distinction is deliberate. Both @@ -1327,7 +1341,10 @@ claims: # the 2,503 moved lines themselves are ±0 under the family glob. # 28559 -> 28582 (RQ-58-SPLIT unit 2): +23 module plumbing for the # select_with_stack.rs relocation; the 7,754 moved lines are ±0. - value: 28582 + # 28582 -> 28755 (RQ-59-WARALIAS #989): +173 code, all in the + # snapshot_home_reg_aliases WAR guard + its four call sites (see the + # lines_code waiver); zero test-module movement. + value: 28755 # RQ-58-WILDCARD's real denominator, and THE directed wildcard pin. 62 # absorbing arms are in the lowering code; the other 43 of the plan's 105 # are assertion helpers in the test module, where a `_ =>` is not a diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index d046d32a..e1e67080 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -1037,6 +1037,116 @@ fn spill_deepest_reg( Ok(true) } +/// #989 — the ARM analogue of the RV32 selector's `snapshot_aliases` (#472): +/// before a `local.set`/`local.tee` overwrites a register-homed local's HOME +/// register `target` (a param in r0-r3 or a #390-promoted local in r4-r8), +/// copy any operand-stack entry that still ALIASES `target` — pushed by an +/// EARLIER `local.get` of the same local, which aliases the home register +/// by reference rather than copying — into a fresh temp, and rewrite those +/// entries to the temp. Without this, the `mov target, val` destroys the +/// earlier value (the get→set→use WAR hazard): `war_set` returned 200 for +/// EVERY input (44 wrong vectors across 4 exports, executed in #989). +/// +/// `skip` is the operand-stack index NOT to rewrite — `local.tee`'s own kept +/// top IS the value being written and stays aliased to its producer. Fires +/// only when an alias is present, so code without the WAR shape emits nothing +/// and stays byte-identical. +/// +/// The aliased entries are still ON the stack during allocation, so the +/// allocators cannot return `target` itself; `reserved` must carry the +/// just-popped/peeked `val` (plus the live params) so the temp cannot land on +/// the value about to be written either. The spill fallback inside the +/// allocators is sound here: spilling an ALIASED entry stores `target`'s +/// current (pre-write) value — exactly the value the entry needs — and the +/// entry stops aliasing. +/// +/// i64 defence in depth (RV32 checks pair halves too): an i64 entry whose +/// pair overlaps `target` (lo == target or hi == target) is snapshotted as a +/// whole pair into a fresh CONSECUTIVE pair — ARM i64 stack entries derive +/// hi = lo+1 (`i64_pair_hi`), so rewriting one half alone is unrepresentable. +fn snapshot_home_reg_aliases( + target: Reg, + skip: Option, + stack: &mut [StackVal], + next_temp: &mut u8, + instructions: &mut Vec, + spill: &mut SpillState, + reserved: &[Reg], + line: usize, +) -> Result<()> { + let overlaps = |v: &StackVal| -> bool { + if let StackVal::Reg { reg, is_i64 } = v { + *reg == target || (*is_i64 && i64_pair_hi(*reg).is_ok_and(|hi| hi == target)) + } else { + false // spilled/VFP entries hold no core register + } + }; + let aliased = |stack: &[StackVal], wide: bool| -> bool { + stack + .iter() + .enumerate() + .any(|(i, v)| Some(i) != skip && v.is_i64() == wide && overlaps(v)) + }; + if aliased(stack, false) { + let tmp = alloc_temp_or_spill(next_temp, stack, instructions, spill, reserved, line)?; + instructions.push(ArmInstruction { + op: ArmOp::Mov { + rd: tmp, + op2: Operand2::Reg(target), + }, + source_line: Some(line), + }); + for (i, v) in stack.iter_mut().enumerate() { + if Some(i) != skip + && let StackVal::Reg { reg, is_i64: false } = v + && *reg == target + { + *reg = tmp; + } + } + } + // The allocator's spill fallback may itself de-alias entries (see above), + // so re-check after every pair allocation rather than trusting the first + // scan — a dead snapshot MOV for an entry that just got spilled would be + // harmless but is refused on principle (emit only what is still needed). + while aliased(stack, true) { + let (new_lo, new_hi) = + alloc_consecutive_pair(next_temp, stack, instructions, spill, &[], reserved, line)?; + let mut found = None; + for (i, v) in stack.iter().enumerate() { + if Some(i) != skip + && let StackVal::Reg { reg, is_i64: true } = v + && overlaps(v) + { + found = Some(*reg); + break; + } + } + let Some(old_lo) = found else { + break; // the pair allocation's spill fallback de-aliased everything + }; + let old_hi = i64_pair_hi(old_lo)?; + for (rd, rs) in [(new_lo, old_lo), (new_hi, old_hi)] { + instructions.push(ArmInstruction { + op: ArmOp::Mov { + rd, + op2: Operand2::Reg(rs), + }, + source_line: Some(line), + }); + } + for (i, v) in stack.iter_mut().enumerate() { + if Some(i) != skip + && let StackVal::Reg { reg, is_i64: true } = v + && *reg == old_lo + { + *reg = new_lo; + } + } + } + Ok(()) +} + /// Reconcile one if-result position between the two arms (#313): make the /// else-arm's result register(s) hold the SAME value the then-arm's do, by /// emitting `MOV R_then, R_else` (i64: lo and hi) on the ELSE path when the two diff --git a/crates/synth-synthesis/src/instruction_selector/select_with_stack.rs b/crates/synth-synthesis/src/instruction_selector/select_with_stack.rs index 39dabfe0..b4c5baad 100644 --- a/crates/synth-synthesis/src/instruction_selector/select_with_stack.rs +++ b/crates/synth-synthesis/src/instruction_selector/select_with_stack.rs @@ -5174,6 +5174,22 @@ impl InstructionSelector { } else if *local_idx < num_params.min(4) { let target = index_to_reg(*local_idx as u8); if val != target { + // #989: an EARLIER `local.get` of this same param + // pushed `target` by reference — copy any such + // still-live stack entry out before the overwrite + // destroys it (the get→set→use WAR hazard). + let mut rsv = live_params.clone(); + rsv.push(val); + snapshot_home_reg_aliases( + target, + None, + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &rsv, + idx, + )?; instructions.push(ArmInstruction { op: ArmOp::Mov { rd: target, @@ -5193,6 +5209,21 @@ impl InstructionSelector { // only elides a redundant self-move. Checked before // `layout.locals` so the dead frame slot is never written. if val != target { + // #989: same WAR snapshot as the param arm — + // `local.get` of a promoted local aliases r4..r8 + // by reference. + let mut rsv = live_params.clone(); + rsv.push(val); + snapshot_home_reg_aliases( + target, + None, + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &rsv, + idx, + )?; instructions.push(ArmInstruction { op: ArmOp::Mov { rd: target, @@ -5293,6 +5324,23 @@ impl InstructionSelector { } else if *local_idx < num_params.min(4) { let target = index_to_reg(*local_idx as u8); if val != target { + // #989: snapshot earlier `local.get` aliases of this + // param's home register before overwriting it. The + // tee's own kept top is SKIPPED — it is the value + // being written and stays aliased to its producer. + let mut rsv = live_params.clone(); + rsv.push(val); + let top_idx = stack.len() - 1; + snapshot_home_reg_aliases( + target, + Some(top_idx), + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &rsv, + idx, + )?; instructions.push(ArmInstruction { op: ArmOp::Mov { rd: target, @@ -5310,6 +5358,21 @@ impl InstructionSelector { // later `local.get` both see the same value from independent // homes. Reserved like LocalSet, so `val != target`. if val != target { + // #989: same WAR snapshot as the param arm, top + // skipped (tee semantics). + let mut rsv = live_params.clone(); + rsv.push(val); + let top_idx = stack.len() - 1; + snapshot_home_reg_aliases( + target, + Some(top_idx), + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &rsv, + idx, + )?; instructions.push(ArmInstruction { op: ArmOp::Mov { rd: target, diff --git a/crates/synth-synthesis/src/optimizer_bridge.rs b/crates/synth-synthesis/src/optimizer_bridge.rs index 40e71686..8bebc776 100644 --- a/crates/synth-synthesis/src/optimizer_bridge.rs +++ b/crates/synth-synthesis/src/optimizer_bridge.rs @@ -1246,6 +1246,21 @@ impl OptimizerBridge { // documents the invariant rather than masking a real bug. let mut slot_stack: Vec = Vec::new(); + // #989: vreg -> local index for every vreg that ALIASES a local's home + // register in `ir_to_arm`'s by-reference model (a `Load`'s dest maps to + // the param/local register itself, and a `TeeStore`'s dest maps to the + // home register it just wrote — neither is a copy). A later + // `local.set`/`local.tee` of the SAME local writes that home register, + // so any such vreg still on `slot_stack` at that point would silently + // hold the POST-write value (the get→set→use WAR hazard: `war_tee` + // returned 300 for every input on this path, executed in #989). This + // path has no snapshot machinery, so the WAR shape DECLINES loudly to + // the direct selector (which has `snapshot_home_reg_aliases`) — the + // same honest-degradation contract as the #500 if/else and #188 local- + // call declines. + let mut local_alias_origin: std::collections::HashMap = + std::collections::HashMap::new(); + // Analyze which LocalGets should produce i64 values (using 2 register slots) let i64_local_gets = Self::analyze_i64_local_gets(wasm_ops); @@ -1548,10 +1563,15 @@ impl OptimizerBridge { // Memory and locals // For i64 LocalGets, we use I64Load which produces 2 register slots WasmOp::LocalGet(idx) => { + // #989: the dest vreg(s) alias the local's home register + // in `ir_to_arm` (no copy) — record the origin so a later + // write to this local can detect the WAR shape. + local_alias_origin.insert(inst_id as u32, *idx); if i64_local_gets.contains(&wasm_idx) { // i64 LocalGet pushes (lo, hi) onto slot_stack. let lo = inst_id as u32; let hi = (inst_id + 1) as u32; + local_alias_origin.insert(hi, *idx); let opcode = Opcode::I64Load { dest_lo: OptReg(lo), dest_hi: OptReg(hi), @@ -1587,6 +1607,21 @@ impl OptimizerBridge { "wasm stack underflow in wasm_to_ir (slot_stack pop on empty)", ) })?; + // #989: an EARLIER `local.get` (or tee) of this same local + // is still live on the operand stack — the Store would + // overwrite the home register that entry aliases. Decline + // to the direct selector, which snapshots the alias. + if slot_stack + .iter() + .any(|v| local_alias_origin.get(v) == Some(idx)) + { + return Err(synth_core::Error::synthesis(format!( + "optimized path: local.set {idx} while an earlier \ + local.get of the same local is live on the operand \ + stack (WAR aliasing, #989) — declining to the \ + direct selector" + ))); + } Opcode::Store { src: OptReg(src), addr: *idx, @@ -2361,6 +2396,24 @@ impl OptimizerBridge { "wasm stack underflow in wasm_to_ir (slot_stack pop on empty)", ) })?; + // #989: same WAR decline as LocalSet — the TeeStore writes + // the home register any still-live earlier get aliases. + // (The tee's own value was just popped, so it is not on + // the scanned stack; it is re-pushed as the fresh dest.) + if slot_stack + .iter() + .any(|v| local_alias_origin.get(v) == Some(idx)) + { + return Err(synth_core::Error::synthesis(format!( + "optimized path: local.tee {idx} while an earlier \ + local.get of the same local is live on the operand \ + stack (WAR aliasing, #989) — declining to the \ + direct selector" + ))); + } + // The dest vreg maps to the home register in `ir_to_arm`'s + // TeeStore lowering — it is an alias too (#989). + local_alias_origin.insert(inst_id as u32, *idx); Opcode::TeeStore { dest: OptReg(inst_id as u32), src: OptReg(src_v), @@ -3984,8 +4037,23 @@ impl OptimizerBridge { }); } local_to_reg.insert(*addr, local_reg); + } else { + // #989: a `Store` to a PARAM used to fall through here + // with NO instruction — the write was silently DROPPED + // and every later read of the param returned the stale + // incoming value (`swap_two_params` returned p0-p1 + // instead of p1-p0, executed). Emitting the mov here + // would be wrong too: earlier `Load`s of the param + // alias its home register by reference, so the write + // would clobber them (the WAR hazard). Decline to the + // direct selector, which homes the param and snapshots + // aliases (`snapshot_home_reg_aliases`). + return Err(synth_core::Error::synthesis(format!( + "optimized path: local.set of param {addr} is not \ + modeled (the write was silently dropped pre-#989) \ + — declining to the direct selector" + ))); } - // For param locals (addr < num_params), value stays in param register // Mark source vreg as dead (unless it's a local vreg) if !local_vregs.contains(&src.0) { dead_vregs.insert(src.0); diff --git a/scripts/repro/arm_corpus_sweep_973.py b/scripts/repro/arm_corpus_sweep_973.py index aab8c1be..d2151cc0 100644 --- a/scripts/repro/arm_corpus_sweep_973.py +++ b/scripts/repro/arm_corpus_sweep_973.py @@ -166,10 +166,10 @@ # mismatch is suppressed, never skipped, so the debt cannot buy slack in the # floor. KNOWN_ARM_MISMATCHES = { - ("rv32_local_promotion_472.wat", "war_set"): 989, - ("rv32_local_promotion_472.wat", "war_tee"): 989, - ("aarch64_param_homing_851.wat", "get_set_get_param_no_alias"): 989, - ("aarch64_param_homing_851.wat", "tee_param_no_alias"): 989, + # #989 (WAR aliasing) carried 4 entries here; fixed by RQ-59-WARALIAS + # (snapshot_home_reg_aliases in select_with_stack + the optimized-path + # WAR/param-store declines), so per the both-direction ratchet the + # entries are deleted — that deletion IS how the fix records itself. ("provenance_branches_396.wat", "decide"): 990, }