diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 843bd958..8d61aa92 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -260,7 +260,7 @@ jobs: run: | set -euo pipefail python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \ - --min-emulation-floor 295726 \ + --min-emulation-floor 298754 \ | tee /tmp/oracle-wiring.log python3 - <<'PY' import json, sys @@ -3508,6 +3508,76 @@ jobs: set -euo pipefail python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 11 + repro-sweep-arm-corpus-oracle: + name: "repro sweep — ARM corpus (#973: CI never compiled these for ARM)" + # RQ-58-SELECT973, the second half and the larger one. #973 — `select` on an + # i64-comparison condition returning the then-arm on every vector where the + # else-arm was due — was found only because a lane compiled + # `scripts/repro/*.wat` for ARM BY HAND. Nothing in CI did that. The + # `repro-sweep-*` jobs above run hand-listed oracles, each pinned to the one + # fixture its issue was about, so a fixture written for RV32 or aarch64 never + # reached the ARM backend even when its shape is backend-independent. + # `rv32_cmp_select_472.wat` carried the #973 shape as `sel_cmp_i64` since + # v0.11 and no ARM build ever saw it — MEASURED: run against the PRE-fix + # binary this sweep reports 7 wrong vectors for exactly that export, so the + # leg is red-first against the defect it was built for, using a fixture that + # was already in the tree. + # + # Two phases, because compiling alone would NOT have caught #973 (it compiled + # perfectly and returned the wrong number): a no-wildcard COMPILE census over + # every fixture, then an EXECUTION differential against wasmtime over every + # all-i32 export of every module pure enough to emulate faithfully. + # + # Turning this on surfaced 48 pre-existing wrong vectors unrelated to #973 — + # #989 (a local.set/tee clobbers a live local.get of the same local) and #990 + # (a local written on one arm of a br_if is never zero-inited, so the merge + # reads uninitialised stack). They are LISTED by name against their issue + # inside the harness and ratcheted in both directions, not narrowed away. + runs-on: ubuntu-latest + env: + SYNTH: ./target/debug/synth + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + 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@v7 + with: + python-version: "3.x" + # Deliberately NO wabt. Both oracles here assemble `.wat` with wasmtime's + # OWN assembler (`wasmtime.wat2wasm` / `Module.from_file`), so the + # reference side is ONE toolchain: what parses and what runs cannot + # disagree, and the executed population does not depend on the runner's + # wabt build. That host-dependency class (#850/#881) is the one thing a + # never-before-run job discovers the hard way. + - name: Install emulation deps + 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: "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 + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2 + repro-sweep-wcet-oracle: name: repro sweep — WCET bound soundness cross-checks (phases 2-6) # #890: the SOUNDNESS evidence for --emit-wcet. The cargo gate diff --git a/claims.yaml b/claims.yaml index fc34e02e..4ad1ca00 100644 --- a/claims.yaml +++ b/claims.yaml @@ -1143,7 +1143,7 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910 doc: scripts/repro/ORACLE_WIRING.md - text: "**296,059 emulator entries**" + text: "**298,754 emulator entries**" evidence: - kind: file-exists path: scripts/oracle_run.py @@ -1156,13 +1156,13 @@ claims: - kind: count-min # the EXECUTION population, per script pattern: '^# ci-checks: emulations >= ' glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] - min: 144 + min: 146 - kind: count-max # the "nothing can be bound" hatch pattern: '^# ci-checks: none' glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] max: 1 - kind: verbatim # the doc carries the per-mode split - text: "**144 oracles**" + text: "**146 oracles**" - kind: verbatim text: "Reported per mode and never summed across modes." - kind: verbatim # the itemized weak-floor list stays @@ -1183,14 +1183,14 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX doc: scripts/templates/feature_matrix.md.tmpl - text: "**144 oracles assert 296,059 emulator" + text: "**146 oracles assert 298,754 emulator" evidence: - kind: file-exists path: scripts/oracle_run.py - kind: count-min # same population the other two pin pattern: '^# ci-checks: emulations >= ' glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] - min: 144 + min: 146 # --------------------------------------------------------------------------- # #910 — the CI side of the same claim, pinned so the doc's number and the @@ -1200,7 +1200,7 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910-CI doc: .github/workflows/ci.yml - text: "--min-emulation-floor 295726" + text: "--min-emulation-floor 298754" evidence: - kind: count-min # oracle steps routed through the driver pattern: 'oracle_run\.py scripts/repro/' diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 4d657a28..72a3844e 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -1192,6 +1192,87 @@ fn pop_operand( } } +/// #973 — [`pop_operand`] for a MULTI-operand op, reserving what the op has +/// ALREADY committed to, and PROVING the reload honoured it. +/// +/// [`pop_operand`]'s reload allocates against the *remaining* vstack plus +/// `reserved`. A value this same op popped a moment ago is on NEITHER list — +/// it left the vstack when it was popped, and the caller has to thread it +/// through by hand — so the allocator is free to hand back exactly the +/// register the op still needs. That is #973: an `i64` comparison's +/// [`alloc_consecutive_pair`] spilled a `select`'s then-arm (unconditionally — +/// this is not the opt-in `SYNTH_SPILL_ON_EXHAUST` rung), and the reload during +/// the select's own pops landed in the register still holding the LIVE +/// else-arm, so both `it` arms moved the same register and the select always +/// returned the then-value. +/// +/// `committed` is the op-local half of the reservation (already-popped +/// operands, a destination allocated ahead of the pops, the condition +/// register); `live_params` is the #193 reservation the whole op loop carries. +/// The union is what the reload must avoid. Same discipline #677 already +/// applies in [`bulk_mutable_operand`] — "every popped operand of the op" — +/// generalized so the next multi-pop site cannot forget it. +/// +/// The post-check ([`reload_clobbers_committed`]) is not redundant with the +/// reservation: it is the invariant stated where a future edit would break it. +/// With the reservation in place it is UNREACHABLE by construction, so it is +/// honest to say it is a tripwire and not a live path — the predicate itself is +/// unit-tested directly (`reload_clobbers_committed_*_973`), the integration +/// cannot be. It only consults a RELOAD, because a register-resident operand +/// legitimately aliases a live param and `select (local.get 0) (local.get 0) c` +/// legitimately pops the same register twice. A fired check is an internal +/// compiler bug, so it returns the honest recoverable `Err` the rest of this +/// allocator uses rather than emitting code known to be wrong. +fn pop_operand_committed( + stack: &mut Vec, + next_temp: &mut u8, + instructions: &mut Vec, + spill: &mut SpillState, + live_params: &[Reg], + committed: &[Reg], + line: usize, +) -> Result { + let reloaded = match stack.last() { + Some(StackVal::Spilled { is_i64, .. }) => Some(*is_i64), + _ => None, + }; + let mut reserved: Vec = live_params.to_vec(); + reserved.extend_from_slice(committed); + let reg = pop_operand(stack, next_temp, instructions, spill, &reserved, line)?; + if let Some(is_i64) = reloaded + && let Some(clobbered) = reload_clobbers_committed(reg, is_i64, committed)? + { + return Err(synth_core::Error::synthesis(format!( + "#973 internal compiler bug: reloading a spilled operand landed in \ + {clobbered:?}, a register this operation had already committed to \ + ({committed:?}) — the reload would destroy a value the operation \ + still needs. Refusing to emit the miscompile." + ))); + } + Ok(reg) +} + +/// #973 tripwire predicate: did a reload into `reg` (a PAIR when `is_i64`) land +/// on a register the operation had already committed to? +/// +/// Split out from [`pop_operand_committed`] so the invariant is testable on its +/// own. Checking the pair's HIGH half matters as much as the low: an i64 reload +/// allocates `(lo, lo+1)` and writes both, so a committed register sitting in +/// the implicit high slot is destroyed just as thoroughly and is invisible to a +/// check that only looks at the returned `lo`. +fn reload_clobbers_committed(reg: Reg, is_i64: bool, committed: &[Reg]) -> Result> { + if committed.contains(®) { + return Ok(Some(reg)); + } + if is_i64 { + let hi = i64_pair_hi(reg)?; + if committed.contains(&hi) { + return Ok(Some(hi)); + } + } + Ok(None) +} + /// Peek the top operand WITHOUT consuming it, returning its `lo` register (#171). /// If the top was spilled, reload it into a fresh consecutive pair and rewrite /// the stack entry to [`StackVal::Reg`] (so the value is register-resident again @@ -15259,23 +15340,33 @@ impl InstructionSelector { )?; // Reserve the dst pair through the (possibly reloading) // pops so a spilled operand cannot reload into it. - resv.push(dlo); - resv.push(dhi); - let val2 = pop_operand( + // #973: `val2`'s PAIR joins the reservation for the + // second pop for the same reason — it is off the vstack + // but still read by the two EQ moves below. (This path + // measured GREEN on the #973 fixture pre-fix; the + // omission is the identical latent shape, closed here + // rather than left for the next pressure change to + // expose.) + let mut committed = vec![cond_reg, dlo, dhi]; + let val2 = pop_operand_committed( &mut stack, &mut next_temp, &mut instructions, &mut spill, - &resv, + &live_params, + &committed, idx, )?; let hi2 = i64_pair_hi(val2)?; - let val1 = pop_operand( + committed.push(val2); + committed.push(hi2); + let val1 = pop_operand_committed( &mut stack, &mut next_temp, &mut instructions, &mut spill, - &resv, + &live_params, + &committed, idx, )?; let hi1 = i64_pair_hi(val1)?; @@ -15306,20 +15397,31 @@ impl InstructionSelector { stack.push(StackVal::i64(dlo)); continue; } - let val2 = pop_operand( + // #973: both pops may RELOAD a spilled operand, and the + // allocator only avoids what is still on the vstack plus + // what it is told. `cond_reg` came off the vstack above but + // is not read until the CMP below; `val2` is not read until + // the EQ move. Commit both so a reload cannot land on them — + // the i64-comparison condition spills the then-arm every + // time (`alloc_consecutive_pair` frees a pair by spilling + // the deepest entry), and the reload used to pick the + // else-arm's register. + let val2 = pop_operand_committed( &mut stack, &mut next_temp, &mut instructions, &mut spill, &live_params, + &[cond_reg], idx, )?; - let val1 = pop_operand( + let val1 = pop_operand_committed( &mut stack, &mut next_temp, &mut instructions, &mut spill, &live_params, + &[cond_reg, val2], idx, )?; // #209/VCR-SEL-002 — in-place select. `val2` is consumed by @@ -27652,6 +27754,127 @@ mod tests { assert_eq!(spill.alloc(), Some(0), "slot 0 reusable after reload"); } + // ── #973: a reload must not land on a register the op still needs ── + + /// Drive one pop off a stack holding a single SPILLED entry, with + /// `next_temp` parked so the allocator's first candidate is R5. + fn spilled_top(slot: i32, is_i64: bool) -> (Vec, SpillState) { + let mut spill = SpillState::new(0); + assert_eq!(spill.alloc(), Some(slot), "test wants slot {slot}"); + ( + vec![StackVal::Spilled { + lo_slot: slot, + is_i64, + }], + spill, + ) + } + + /// RED: the hazard is real, not hypothetical. With the reservation the + /// pre-#973 `Select` arm used (`live_params` only), the reload of the + /// spilled then-arm lands squarely on R5 — the register the else-arm was + /// still living in. This is the miscompile, reproduced at the allocator. + #[test] + fn pop_operand_red_973_reload_lands_on_the_live_operand() { + let (mut stack, mut spill) = spilled_top(0, false); + let mut instructions: Vec = Vec::new(); + let mut next_temp: u8 = 5; // ALLOCATABLE_REGS[5] == R5 + let reg = pop_operand( + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &[Reg::R0, Reg::R1], // live params only — what the old code passed + 0, + ) + .unwrap(); + assert_eq!( + reg, + Reg::R5, + "#973: the reload takes R5 even though the op still needs it — the \ + already-popped operand is on neither the vstack nor `reserved`" + ); + } + + /// GREEN: committing R5 moves the reload off it. Same state, same + /// `next_temp`, one extra fact told to the allocator. + #[test] + fn pop_operand_committed_keeps_the_reload_clear_973() { + let (mut stack, mut spill) = spilled_top(0, false); + let mut instructions: Vec = Vec::new(); + let mut next_temp: u8 = 5; + let reg = pop_operand_committed( + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &[Reg::R0, Reg::R1], + &[Reg::R4, Reg::R5], // cond_reg + the already-popped else-arm + 0, + ) + .unwrap(); + assert_ne!(reg, Reg::R5, "the committed else-arm register survives"); + assert_ne!(reg, Reg::R4, "the committed condition register survives"); + assert!( + instructions + .iter() + .any(|i| matches!(&i.op, ArmOp::Ldr { rd, .. } if *rd == reg)), + "the value really was reloaded into the register that was returned" + ); + } + + /// A register-resident operand is NOT a reload, so committing its register + /// must not fire the tripwire: `select (local.get 0) (local.get 0) c` + /// legitimately pops R0 twice, and both `it` arms reading it is correct. + #[test] + fn pop_operand_committed_allows_a_register_resident_alias_973() { + let mut stack = vec![StackVal::i32(Reg::R0)]; + let mut instructions: Vec = Vec::new(); + let mut spill = SpillState::new(0); + let mut next_temp: u8 = 0; + let reg = pop_operand_committed( + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &[Reg::R0], + &[Reg::R0], // the same register, already committed + 0, + ) + .expect("a register-resident duplicate is legal, not an internal bug"); + assert_eq!(reg, Reg::R0); + assert!(instructions.is_empty(), "no reload, so nothing emitted"); + } + + /// The tripwire predicate itself. Unreachable through + /// `pop_operand_committed` once the reservation holds, so it is exercised + /// here directly rather than left as untested prose — including the i64 + /// case, where the IMPLICIT high half is what gets clobbered. + #[test] + fn reload_clobbers_committed_detects_lo_and_hi_973() { + assert_eq!( + reload_clobbers_committed(Reg::R5, false, &[Reg::R4, Reg::R5]).unwrap(), + Some(Reg::R5), + "a 32-bit reload onto a committed register is caught" + ); + assert_eq!( + reload_clobbers_committed(Reg::R5, false, &[Reg::R4, Reg::R6]).unwrap(), + None, + "a 32-bit reload clear of every committed register is silent" + ); + assert_eq!( + reload_clobbers_committed(Reg::R4, true, &[Reg::R5]).unwrap(), + Some(Reg::R5), + "an i64 reload into (R4,R5) destroys a committed R5 via the IMPLICIT \ + high half, which a lo-only check would miss entirely" + ); + assert_eq!( + reload_clobbers_committed(Reg::R4, false, &[Reg::R5]).unwrap(), + None, + "the same registers as i32: only the lo half is written, so R5 is safe" + ); + } + // ── #326: arg-move cycles break via the parallel-move resolver ── /// Minimal layout for driving `emit_arg_moves` directly. diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index b32cd65e..ecc218f4 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -150,7 +150,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. the newly wired ones; exactly 8 asserted a printed verdict or count. Every `wired` oracle now declares a `# ci-checks:` floor that `scripts/oracle_run.py` enforces per run by counting real emulator entries, - wasmtime executions and compilations: **144 oracles assert 296,059 emulator + wasmtime executions and compilations: **146 oracles assert 298,754 emulator entries**, 7 assert a printed count, 9 assert compilations, and 1 (`aarch64_matrix.sh`, a POSIX shell oracle the in-process driver cannot instrument) is itemized as unbindable in `scripts/repro/ORACLE_WIRING.md` diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 4377484b..de396ba1 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -306,8 +306,8 @@ whole lane is about. So the counter keeps the name of the thing it counts. | mode | oracles | floor total | |---|---|---| -| `emulations` | **144 oracles** | **296,059 emulator entries** | -| `stdout` | 7 oracles | 458 printed counts | +| `emulations` | **146 oracles** | **298,754 emulator entries** | +| `stdout` | 7 oracles | 460 printed counts | | `compiles` | 9 oracles | 43 compilations | | `none` | **1 oracle** | — | @@ -315,7 +315,7 @@ whole lane is about. So the counter keeps the name of the thing it counts. compilations and printed counts are three different units; one impressive combined figure is precisely the instrument defect #910 is about. -`scripts/oracle_wiring_check.py --min-emulation-floor 295621` enforces the +`scripts/oracle_wiring_check.py --min-emulation-floor 298754` enforces the emulations total, in the **already-required** `Claim Check` job. It shares the driver's header parser by import rather than re-implementing the grammar. Pinned in `claims.yaml` (`SYNTH-ORACLE-CHECK-FLOORS-910`) so the number here, the diff --git a/scripts/repro/arm_corpus_sweep_973.py b/scripts/repro/arm_corpus_sweep_973.py new file mode 100644 index 00000000..aab8c1be --- /dev/null +++ b/scripts/repro/arm_corpus_sweep_973.py @@ -0,0 +1,535 @@ +#!/usr/bin/env python3 +# ci-status: wired +# ci-checks: emulations >= 2335 +"""#973 — the ARM leg of the repro-corpus sweep: CI never compiled these for ARM. + +WHY THIS EXISTS (the second half of #973, and the larger half) +----------------------------------------------------------------------------- +#973 — `select` on an i64-comparison condition returning the then-arm on every +vector where the else-arm was due — was found only because a lane compiled +`scripts/repro/*.wat` for ARM by hand. Nothing in CI does that. The individual +`repro-sweep-*` jobs run 30-odd HAND-LISTED oracles, each pinned to the one +fixture its issue was about; a fixture written for RV32 or aarch64 is never put +through the ARM backend even when the shape it encodes is backend-independent. +`rv32_cmp_select_472.wat` has carried the #973 shape as `sel_cmp_i64` since +v0.11 and no ARM build ever saw it. + +So this sweeps the WHOLE corpus, and it does it in two phases, because the +weaker phase alone would not have caught #973: + + PHASE A — COMPILE COVERAGE. Every `scripts/repro/*.wat` through the ARM + backend. A fixture either compiles or is on the DECLINES list BY NAME with + the reason. Both directions are red: an undeclared failure is a regression, + and a listed fixture that starts compiling must be taken OFF the list, so the + list cannot rot into a permanent excuse. This is a NO-WILDCARD tripwire, the + same shape as the #615 silent-NOP guard. + + PHASE B — EXECUTION DIFFERENTIAL. Compiling proves nothing about the values. + #973 compiled perfectly and returned the wrong number. So every export with + an all-i32 signature, in every module PURE enough to emulate faithfully, is + run under unicorn and compared against wasmtime on a fixed argument matrix. + +PURITY, AND WHY IT IS DECIDED FROM THE WASM BINARY +----------------------------------------------------------------------------- +Phase B only runs a module with no import, memory, table, global, elem or data +section — decided by walking the WASM section ids (2/4/5/6/9/11), not by +grepping the `.wat`. A module with a data segment would read initialized bytes +under wasmtime and zeros under unicorn, and the resulting "disagreement" would +be an artifact of the harness rather than a defect: a differential that reports +its own setup gaps as miscompiles trains people to ignore it. + +That exclusion is a REAL GAP, not a claim of coverage — the memory-touching +fixtures are covered by `repro-sweep-memory-oracle`, which sets up their images +properly. What this leg adds is the population nobody was executing at all. + +HONEST SKIPS, ALL COUNTED AND PRINTED +----------------------------------------------------------------------------- + * a vector where wasmtime TRAPS (div-by-zero, unreachable) — the ARM side is + a `udf`, and comparing a trap to a return value is not a comparison + * a vector too LONG for either budget. Both sides get one: wasmtime runs on + FUEL and unicorn on an instruction count, and a vector that exhausts either + is skipped on both. `aarch64_ctrlflow_851.wat:countdown(-1)` is the shape — + a counted loop with 2^32 iterations, 1.4 s under the wasmtime interpreter + and far longer under unicorn. Calling that a miscompile because the emulator + stopped early would be the harness reporting its own budget as a defect. + * an export with more than 4 params (AAPCS stack args) or a non-i32 signature + * a module Phase A could not compile +A unicorn fault where wasmtime RETURNED WITHIN BUDGET is NOT a skip — it is a +failure. So is a value disagreement. Both budgets are deliberately generous +(2M fuel / 400k instructions) so a skip means "genuinely long-running", and the +skip counts are PRINTED so a change that starts skipping everything is visible +rather than a smaller green number. + +TWO FLOORS, because one of them is weaker than it looks +----------------------------------------------------------------------------- +`# ci-checks: emulations >= 2335` is the CI-enforced floor and counts +`emu_start` ENTRIES — measured, not guessed. But a run that entered the emulator +and then discarded every result on budget grounds would still clear it, so the +harness carries its own `MIN_COMPARED` floor on vectors actually COMPARED +against wasmtime (2327, likewise measured). A known mismatch is SUPPRESSED, not +skipped, so listing debt cannot buy slack in that floor either. + +Run (needs wasmtime + unicorn + pyelftools — no wabt): + SYNTH=./target/debug/synth python scripts/repro/arm_corpus_sweep_973.py +""" +import os +import struct +import subprocess +import sys +import tempfile +import time +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") + +# cortex-m4f, not cortex-m4: the FPU-bearing target is the ARM superset, and on +# plain cortex-m4 sixteen float fixtures decline for a reason that has nothing +# to do with the sweep (measured: 143 compile on m4f vs 139 on m4). +TARGET = "cortex-m4f" + +CODE, LIN = 0x100000, 0x40000 +RET_PAD = CODE + 0x38000 +STACK_BASE, STACK_SIZE = 0x80000, 0x10000 +SP0 = STACK_BASE + 0xC000 + +# Budgets. Symmetric by intent: a vector is compared only when BOTH engines +# finished it. Sized ~20x the longest real fixture run measured here. +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 + +# ── PHASE A: the declines, BY NAME and BY REASON ───────────────────────────── +# Every entry is a LOUD `#952` decline (synth refuses to ship an object missing +# a requested export) for an operation the ARM backend does not lower — NOT a +# crash, and NOT a wrong answer. Measured on the v0.58 tree at `--target +# cortex-m4f --relocatable --all-exports`. +# +# Taking a name off this list is the only way to record that a gap closed, and +# leaving one on after it closes is red. Adding one requires saying why here. +EXPECTED_DECLINES = { + "aarch64_brtable_blockvals_851.wat": "i64/f32/f64 block result values", + "aarch64_divrem_851.wat": "i64 f64-reinterpret round trip", + "aarch64_float_completion_851.wat": "f32/f64 ceil/floor/trunc/nearest + i64<->float", + "aarch64_m3_floats_538.wat": "f64 arithmetic set (aarch64-shaped fixture)", + "aarch64_m4_trunc_minmax_538.wat": "f64 trunc + f32/f64 min/max/copysign", + "aarch64_surface_851.wat": "i64 self-call return", + "f64_369.wat": "f64 surface as a whole on the relocatable path", + "float_select_return_782.wat": "f64 select + f64 return", + "i64_float_conv_869.wat": "i64<->f32/f64 conversions", + "rv32_br_value_931.wat": "i64 br-with-value", + "trunc_sat_782.wat": "f64 and i64 saturating truncations", + "vfp_spill_881.wat": "f64 spill shapes", +} + +# Compile floor: a FLOOR, so adding fixtures cannot redden the job. Measured +# 144/156 on the v0.58 tree (143/155 before this lane's own fixture). +MIN_COMPILED = 144 + +# ── PHASE B: the debt this leg SURFACED, by name and by issue ──────────────── +# Turning the ARM leg on found 48 wrong vectors that have nothing to do with +# #973 and everything to do with nobody having executed these fixtures on ARM. +# They are listed rather than fixed here (two different defect classes, both +# filed) and rather than narrowed away, which would have meant shipping a leg +# shaped to pass: +# +# #989 — a `local.set`/`local.tee` CLOBBERS an earlier `local.get` of the SAME +# local still on the operand stack. `war_set` returns 200 for every +# input; `get_set_get_param_no_alias` never reads its argument at all. +# RV32 has the protection (`snapshot_aliases`), ARM does not. +# #990 — a local written on only ONE arm of a `br_if` is never zero-inited, so +# the merge reads uninitialised stack. Provable, not inferred: the +# returned values are this harness's 0xDEADBEEF poison +/- 1. +# +# BOTH DIRECTIONS ARE RED. An entry that starts passing must be deleted (that is +# how a fix records itself), and a mismatch NOT on this list fails the job. The +# vectors are still COMPARED and still counted toward MIN_COMPARED — a known +# 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, + ("provenance_branches_396.wat", "decide"): 990, +} + +# Phase B floor on COMPARISONS, not on emulator entries. `# ci-checks: +# emulations >= N` counts `emu_start` calls, and a run that entered the emulator +# and then skipped every result on budget grounds would still clear it — the +# exact "green number that measured nothing" shape #910 exists to reject. Set +# from the measured population; a FLOOR, so new fixtures only raise it. +MIN_COMPARED = 2327 + +# ── PHASE B: the argument matrix ───────────────────────────────────────────── +# Small, signed/unsigned boundary-heavy, and the same for every export, so the +# population is a property of the corpus rather than of per-fixture tuning. +ARG_TUPLES = [ + (0, 0, 0, 0), + (1, 2, 3, 4), + (7, 5, 3, 1), + (5, 7, 11, 13), + (100, 100, 100, 100), + (-1, 1, -1, 1), + (1, -1, 1, -1), + (-5, -7, -9, -11), + (0x7FFFFFFF, -1, 0x7FFFFFFF, -1), + (-1, 0x7FFFFFFF, 1, 0), + (0, -1, 0, -1), + (0xFFFF, 0x10000, 3, 2), +] + +WASM_SECTION_FORBIDDEN = { + 2: "import", + 4: "table", + 5: "memory", + 6: "global", + 9: "elem", + 11: "data", +} + + +def uleb(buf, pos): + val = shift = 0 + while True: + b = buf[pos] + pos += 1 + val |= (b & 0x7F) << shift + if not b & 0x80: + return val, pos + shift += 7 + + +def impure_sections(wasm): + """Section ids that make a module unfaithful to emulate here.""" + found, pos = [], 8 # skip magic + version + while pos < len(wasm): + sid = wasm[pos] + pos += 1 + size, pos = uleb(wasm, pos) + if sid in WASM_SECTION_FORBIDDEN: + found.append(WASM_SECTION_FORBIDDEN[sid]) + pos += size + return found + + +def to_wasm(wat): + """Assemble the fixture with WASMTIME'S OWN assembler, or None if refused. + + Deliberately not `wat2wasm`: the reference side must be ONE toolchain. wabt + needs `--enable-all` for the post-MVP proposals several fixtures use + (multi-memory, bulk-memory), which makes the executed population depend on + the runner's wabt build — a host dependency this repo has been bitten by + twice, and one this leg would only discover the first time CI ran it. + `wasmtime.wat2wasm` is the same library that then instantiates the module, + so what parses and what runs cannot disagree. Measured across all 156 + fixtures: wabt and wasmtime accept exactly the same set, and the purity + classification below is identical for every one of them. + + A refusal is a Phase-B skip with its own counter, never a silent one: synth + compiled the fixture in Phase A, so the gap is on the reference side, and + calling that a miscompile would be the harness blaming the compiler for its + own tooling. + """ + try: + return wasmtime.wat2wasm(wat.read_text()) + except Exception: + return None + + +def compile_arm(wat, out): + p = subprocess.run( + [SYNTH, "compile", str(wat), "--target", TARGET, "--relocatable", + "--all-exports", "-o", out], + capture_output=True, text=True, + ) + return p.returncode, (p.stderr or "") + (p.stdout or "") + + +def encode_thm_bl(pc_at_reloc, target): + 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, relocated .text, base) or (None, reason, None) if unrunnable.""" + 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: + return None, "no .text", None + 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(): + name = symtab.get_symbol(r["r_info_sym"]).name + if r["r_info_type"] not in (R_ARM_THM_CALL, R_ARM_THM_JUMP24): + return None, f"reloc type {r['r_info_type']} ({name})", None + if name not in syms: + return None, f"undefined reloc target {name}", None + off = r["r_offset"] + hw1, hw2 = encode_thm_bl(CODE + off, CODE + ((syms[name] - base) & ~1)) + struct.pack_into("= 360 +"""#973 — ARM: `select` on an i64-comparison condition with COMPUTED arms. + +THE DEFECT, as MEASURED (not as reported — the mechanism was re-derived here +from the emitted bytes and from execution, because a reported mechanism has +been wrong three times in the last release). + +`sel_i64_lt_s(a, b) = (i64)a < (i64)b ? a + 100 : b + 200`, compiled +`--target cortex-m4 --relocatable`, lowered to (capstone over the ELF +`.text`, never `synth disasm` text): + + 0008: add.w r3, r0, #0x64 ; then-arm -> r3 + 000c: add.w r5, r1, #0xc8 ; else-arm -> r5 (LIVE from here on) + 0010: mov r6, r0 + 0012: asr.w r7, r6, #0x1f ; sign-extend a (pair r6:r7) + 0016: str.w r3, [sp] ; SPILL the then-arm to free a pair + 001a: mov r2, r1 + 001c: asr.w r3, r2, #0x1f ; sign-extend b (pair r2:r3) + 0020: cmp r6, r2 + 0022: sbcs.w r4, r7, r3 + 0026: ite lt + 0028: movlt r4, #1 + 002a: movge r4, #0 + 002c: ldr.w r5, [sp] ; RELOAD the then-arm INTO r5 == else-arm + 0030: cmp r4, #0 + 0032: it ne + 0034: movne r6, r5 + 0036: it eq + 0038: moveq r6, r5 ; both arms move the SAME register + +The spill is NOT the opt-in `SYNTH_SPILL_ON_EXHAUST` rung: `alloc_consecutive_pair` +spills the deepest register-resident vstack entry UNCONDITIONALLY when no free +consecutive pair remains, and the i64 comparison needs two pairs. The reload +then allocated against `live_params` only — the already-popped `val2` (else-arm) +and `cond_reg` are on neither the vstack nor the reserved list, so the allocator +was free to hand out exactly the register the select still needed. + +Executed on the pre-fix binary, 5 of 8 argument pairs were wrong and every one +of them returned the THEN-arm: + + BUG sel_i64_lt_s(7,5): want=205 got=107 + BUG sel_i64_lt_s(0,0): want=200 got=100 + BUG sel_i64_lt_s(1,-1): want=199 got=101 + BUG sel_i64_lt_s(100,100): want=300 got=200 + BUG sel_i64_lt_s(-5,-7): want=193 got=95 + ok cmp_i64_lt_s(...) 8/8 -- the comparison ALONE was always correct + +WHY THE ARMS MUST BE COMPUTED: with `i32.const` arms nothing needs spilling and +the bug is invisible; with EQUAL arms the two `mov`s reading one register is +correct. `guard_const_arms` and `guard_same_arm` are in the fixture precisely so +those two non-signatures are on the record. + +Ground truth is wasmtime on the same `.wat`. Both ARM lowering paths are run: +`--relocatable` (the direct selector, `select_with_stack`, where #973 lives) and +the self-contained/optimized path, so a fix that only moves one is visible. + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=./target/debug/synth python scripts/repro/select_i64cmp_973_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, +) + +WAT = Path(__file__).with_name("select_i64cmp_973.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") + +CODE, LIN = 0x100000, 0x40000 +RET_PAD = CODE + 0x18000 +STACK_BASE, STACK_SIZE = 0x80000, 0x10000 +SP0 = STACK_BASE + 0xC000 + +MEM_POISON = 0xDEADBEEF # every stack word below the entry SP +REG_POISON = 0xFEEDFACE # every argument register the signature does not use +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 + +# Every export of the fixture. The two `cmp_*` are the CONTRAST (always +# correct); the four `guard_*` are the shapes the fix must not disturb. +EXPORTS = [ + "sel_i64_lt_s", + "sel_i64_lt_u", + "sel_i64_gt_s", + "sel_i64_le_s", + "sel_i64_ge_u", + "sel_i64_eq", + "sel_i64_ne", + "sel_i64_deep", + "sel_wide_i64cmp", + "cmp_i64_lt_s", + "cmp_i64_ge_u", + "guard_const_arms", + "guard_i32cmp", + "guard_same_arm", + "guard_nested", +] + +# Argument pairs chosen so BOTH arms are exercised on every comparison kind, +# including the a == b case (which distinguishes le/lt and ge/gt) and the +# sign-boundary pairs where the i64 sign-extension itself matters. +ARGS = [ + (5, 7), + (7, 5), + (0, 0), + (-1, 1), + (1, -1), + (100, 100), + (-5, -7), + (-7, -5), + (0x7FFFFFFF, -1), + (-1, 0x7FFFFFFF), + (0, -1), + (-1, 0), +] + + +def die(msg): + print(f"#973 ARM ORACLE: FAIL — {msg}") + sys.exit(1) + + +def compile_fixture(out, relocatable): + cmd = [SYNTH, "compile", str(WAT), "--target", "cortex-m4", "--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("