From 60ab22785beaf147951da795b8c5ba5807837c24 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 18 Aug 2026 20:09:15 +0200 Subject: [PATCH 1/6] =?UTF-8?q?wip(fix/arm-select-i64cmp-973):=20salvage?= =?UTF-8?q?=20partial=20lane=20work=20=E2=80=94=20agent=20hit=20the=20WEEK?= =?UTF-8?q?LY=20API=20limit?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Committed by the hub coordinator so the work survives. NOT reviewed and NOT complete: the lane stopped mid-task. This is a restore point, not a claim that anything is verified. Co-Authored-By: Claude Opus 5 --- scripts/repro/select_i64cmp_973.wat | 123 ++++++++++++++++++++++++++++ 1 file changed, 123 insertions(+) create mode 100644 scripts/repro/select_i64cmp_973.wat diff --git a/scripts/repro/select_i64cmp_973.wat b/scripts/repro/select_i64cmp_973.wat new file mode 100644 index 00000000..3b7a1585 --- /dev/null +++ b/scripts/repro/select_i64cmp_973.wat @@ -0,0 +1,123 @@ +;; #973 — ARM: `select` on an i64-comparison condition with COMPUTED arms. +;; +;; The i64 comparison needs a consecutive register PAIR for each sign-extended +;; operand. `alloc_consecutive_pair` frees one by spilling the DEEPEST +;; register-resident vstack entry — which is the select's then-arm, sitting +;; under the else-arm and the condition. When `select` later pops its operands +;; the reload of that spilled then-arm allocated against `live_params` ONLY, so +;; it could pick the register still holding the LIVE else-arm (or the condition +;; itself): both `it` arms then moved the same register and the select always +;; returned the then-value. +;; +;; Every shape below is `cmp(a, b) ? a + 100 : b + 200` so the two arms are +;; DISTINCT for every argument pair, including a == b — a fixture whose arms +;; coincide cannot see this defect at all (and `i32.const` arms make it vanish +;; because nothing needs spilling). +;; +;; The bare comparisons are carried alongside as the CONTRAST: they were always +;; correct, so a run where they fail too is a different defect. +(module + ;; ── the reported shape, once per signed/unsigned i64 comparison ────────── + (func $sel_i64_lt_s (export "sel_i64_lt_s") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.lt_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) + + (func $sel_i64_lt_u (export "sel_i64_lt_u") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.lt_u (i64.extend_i32_u (local.get $a)) + (i64.extend_i32_u (local.get $b))))) + + (func $sel_i64_gt_s (export "sel_i64_gt_s") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.gt_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) + + (func $sel_i64_le_s (export "sel_i64_le_s") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.le_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) + + (func $sel_i64_ge_u (export "sel_i64_ge_u") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.ge_u (i64.extend_i32_u (local.get $a)) + (i64.extend_i32_u (local.get $b))))) + + (func $sel_i64_eq (export "sel_i64_eq") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.eq (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) + + (func $sel_i64_ne (export "sel_i64_ne") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.ne (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) + + ;; i64 comparison whose OPERANDS are themselves computed — more pressure, so + ;; the spill/reload window is wider than in the minimal repro. + (func $sel_i64_deep (export "sel_i64_deep") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.lt_s (i64.add (i64.extend_i32_s (local.get $a)) (i64.const 7)) + (i64.mul (i64.extend_i32_s (local.get $b)) (i64.const 3))))) + + ;; ── the WIDE select: i64 ARMS under an i64-comparison condition ────────── + ;; Result folds lo ^ hi so a wrong half is loud rather than invisible. + (func $sel_wide_i64cmp (export "sel_wide_i64cmp") (param $a i32) (param $b i32) (result i32) + (local $v i64) + (local.set $v + (select (i64.add (i64.extend_i32_s (local.get $a)) (i64.const 0x100000064)) + (i64.add (i64.extend_i32_s (local.get $b)) (i64.const 0x2000000C8)) + (i64.lt_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) + (i32.xor (i32.wrap_i64 (local.get $v)) + (i32.wrap_i64 (i64.shr_u (local.get $v) (i64.const 32))))) + + ;; ── contrast: the comparisons ALONE were always correct ───────────────── + (func $cmp_i64_lt_s (export "cmp_i64_lt_s") (param $a i32) (param $b i32) (result i32) + (i64.lt_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b)))) + + (func $cmp_i64_ge_u (export "cmp_i64_ge_u") (param $a i32) (param $b i32) (result i32) + (i64.ge_u (i64.extend_i32_u (local.get $a)) + (i64.extend_i32_u (local.get $b)))) + + ;; ── guards: shapes the fix must NOT change ────────────────────────────── + ;; Constant arms: nothing to spill, so this passed before the fix too. + (func $guard_const_arms (export "guard_const_arms") (param $a i32) (param $b i32) (result i32) + (select (i32.const 100) (i32.const 200) + (i64.lt_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) + + ;; i32-comparison condition with computed arms — the ordinary select path, + ;; correct before and after (and byte-frozen elsewhere). + (func $guard_i32cmp (export "guard_i32cmp") (param $a i32) (param $b i32) (result i32) + (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i32.lt_s (local.get $a) (local.get $b)))) + + ;; BOTH arms are the same value: the two conditional moves LEGITIMATELY read + ;; one register here, so "same source" is not by itself the defect signature. + (func $guard_same_arm (export "guard_same_arm") (param $a i32) (param $b i32) (result i32) + (select (local.get $a) (local.get $a) + (i64.lt_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) + + ;; Nested selects on i64 conditions: the second select's operands are live + ;; across the first one's spill window. + (func $guard_nested (export "guard_nested") (param $a i32) (param $b i32) (result i32) + (select (select (i32.add (local.get $a) (i32.const 100)) + (i32.add (local.get $b) (i32.const 200)) + (i64.lt_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b)))) + (i32.add (local.get $b) (i32.const 300)) + (i64.gt_s (i64.extend_i32_s (local.get $a)) + (i64.extend_i32_s (local.get $b))))) +) From 07bceef3868a2d8017badf78b1499c11b6c4f7e8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 18 Aug 2026 20:46:35 +0200 Subject: [PATCH 2/6] =?UTF-8?q?test(#973):=20RED-FIRST=20=E2=80=94=20ARM?= =?UTF-8?q?=20i64-cmp=20select=20execution=20differential=20(264/360)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The fixture + unicorn-vs-wasmtime differential for RQ-58-SELECT973, landed BEFORE the fix so the red is on the record. Measured on 60ab2278 (pre-fix), `--target cortex-m4`, BOTH ARM lowering legs: [relocatable] 132/180 vectors match wasmtime [self-contained] 132/180 vectors match wasmtime #973 CHECKS=264/360 96 wrong vectors, and every one returns the THEN-arm where the else-arm was due: 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(100,100): want=300 got=200 BUG sel_i64_eq(-1,1): want=201 got=99 MECHANISM RE-DERIVED HERE, not taken from the issue (capstone over the ELF .text, never `synth disasm` text): add.w r5, r1, #0xc8 ; else-arm -> r5, LIVE str.w r3, [sp] ; then-arm SPILLED to free an i64 pair ... ; the 64-bit compare ldr.w r5, [sp] ; RELOADED INTO r5 == the live else-arm movne r6, r5 moveq r6, r5 ; both `it` 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, which the i64 comparison's two sign-extended pairs guarantee. `pop_operand`'s reload then allocates against the REMAINING vstack plus `live_params`; a value already popped for this same op is on neither list, so the allocator is free to hand out exactly the register the select still needs. Two facts the issue did not have: * the SELF-CONTAINED (optimized) leg emits a BYTE-IDENTICAL body (sha256 1bef7e189ae8e090 both legs) — the i64 ops delegate this shape to `select_with_stack`, so this is one defect on two nominal paths, not two. * `sel_wide_i64cmp` (i64 ARMS under an i64 comparison) is GREEN pre-fix: the wide path already reserves its destination pair across the pops, which is the shape of the fix the narrow path needs. Guards are in the fixture for the two NON-signatures: `guard_const_arms` (constant arms spill nothing, so the bug is invisible) and `guard_same_arm` (two conditional moves reading one register is CORRECT when both arms are the same value — so "same source" is not by itself the defect). --- .../select_i64cmp_973_arm_differential.py | 256 ++++++++++++++++++ 1 file changed, 256 insertions(+) create mode 100644 scripts/repro/select_i64cmp_973_arm_differential.py diff --git a/scripts/repro/select_i64cmp_973_arm_differential.py b/scripts/repro/select_i64cmp_973_arm_differential.py new file mode 100644 index 00000000..2d779172 --- /dev/null +++ b/scripts/repro/select_i64cmp_973_arm_differential.py @@ -0,0 +1,256 @@ +#!/usr/bin/env python3 +# ci-status: wired +# ci-checks: emulations >= 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_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(" Date: Tue, 18 Aug 2026 21:04:56 +0200 Subject: [PATCH 3/6] =?UTF-8?q?fix(#973):=20ARM=20select=20=E2=80=94=20res?= =?UTF-8?q?erve=20what=20the=20op=20already=20holds=20across=20a=20reloadi?= =?UTF-8?q?ng=20pop?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RQ-58-SELECT973. `select` on an i64-comparison condition with COMPUTED arms returned the then-arm on every vector where the else-arm was due. MECHANISM (verified by execution and by the emitted bytes, not taken from the issue). `pop_operand`'s reload allocates against the REMAINING vstack plus `reserved`. A value the 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. The narrow `Select` arm passed only `live_params`, so the reload was free to hand back the register the select still needed: add.w r5, r1, #0xc8 ; else-arm -> r5, LIVE str.w r3, [sp] ; then-arm spilled: the i64 compare needs a PAIR ldr.w r5, [sp] ; reloaded INTO the live else-arm movne r6, r5 moveq r6, r5 ; both `it` 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 entry unconditionally when no free pair remains, which an i64 comparison's two sign-extended operands guarantee. That is why the bug needs an i64 CONDITION and COMPUTED arms: constant arms spill nothing. THE FIX is the reservation discipline #677 already established for bulk-memory ("every popped operand of the op"), generalized into `pop_operand_committed` so the next multi-pop site cannot forget it: the condition register is committed across both pops, and `val2` across the second. The wide (i64-arms) path gets the same treatment for `val2`'s PAIR — that path measured GREEN pre-fix because it already reserved its destination pair, so this is the identical latent shape closed rather than a second live bug. BYTES. The reservation can only change an allocation the OLD code would have answered with a committed register — which is the miscompile — so everything else is byte-identical: * 10/10 frozen anchors UNCHANGED (`cargo test -p synth-cli --test frozen_codegen_bytes`), control_step and flight_algo included. No re-freeze was needed and none was done. * full `cargo test --workspace` green (142 test binaries), clippy -D warnings clean. Where bytes DO move, they move to correct AND smaller code — `sel_i64_lt_s` 68 B -> 64 B, because with `val1 != val2` restored the #209 in-place select applies and one conditional move disappears: ldr.w r6, [sp] ; reload lands clear of the live else-arm cmp r4, #0 it ne movne r5, r6 ; single in-place move; r5 already holds the else-arm EXECUTION EVIDENCE. `scripts/repro/select_i64cmp_973_arm_differential.py` 264/360 -> 360/360 against wasmtime, on BOTH ARM lowering legs (relocatable and self-contained, whose bodies are byte-identical here). The defensive `Err` in `pop_operand_committed` is a TRIPWIRE for future edits, not a live path: with the reservation in place it is unreachable by construction. It is unit-tested directly rather than left as untested prose. --- .../src/instruction_selector.rs | 98 +++++++++++++++++-- 1 file changed, 90 insertions(+), 8 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 4d657a28..a3a8772a 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -1192,6 +1192,67 @@ 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 is not redundant with the reservation: it is the invariant +/// stated where a future edit would break it. It only fires on a RELOAD (a +/// register-resident operand legitimately aliases a live param, and `select +/// (local.get 0) (local.get 0) c` legitimately pops the same register twice), +/// and 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 mut landed = vec![reg]; + if is_i64 { + landed.push(i64_pair_hi(reg)?); + } + if let Some(clobbered) = landed.into_iter().find(|r| committed.contains(r)) { + 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) +} + /// 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 +15320,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 +15377,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 From 0119ba377a65d35aa8afed13f67bec1c770c8a47 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 18 Aug 2026 21:12:48 +0200 Subject: [PATCH 4/6] =?UTF-8?q?test(#973):=20ARM=20corpus=20sweep=20?= =?UTF-8?q?=E2=80=94=20the=20backend=20CI=20never=20compiled,=20wired=20wi?= =?UTF-8?q?th=20floors?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The second half of RQ-58-SELECT973, and the larger half. #973 was found only because a lane compiled `scripts/repro/*.wat` for ARM BY HAND. Nothing in CI did that: the `repro-sweep-*` jobs 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` has carried the #973 shape as `sel_cmp_i64` since v0.11 and no ARM build ever saw it. RED-FIRST FOR THE GATE ITSELF, not only for the fix. Run against the PRE-fix binary, this sweep reports 7 wrong vectors for `rv32_cmp_select_472.wat:sel_cmp_i64` — the already-in-tree fixture — and 55 across the #973 shapes in total. Post-fix those are gone. The leg would have caught the defect it was built for, with no new fixture required. TWO PHASES, because compiling alone would not have caught #973 (it compiled perfectly and returned the wrong number): A. COMPILE CENSUS over all 156 fixtures at `--target cortex-m4f --relocatable --all-exports`. Measured 144 compile / 12 decline / 0 hard error. The 12 are LOUD `#952` declines listed by name and reason, ratcheted BOTH ways: an undeclared failure is red, and a listed fixture that starts compiling is red too ("remove the entry"), so the list cannot rot into a permanent excuse. B. EXECUTION DIFFERENTIAL vs wasmtime over every all-i32 export of every module pure enough to emulate faithfully. Measured 43 modules, 2327 compared vectors, 2335 emulator entries. WHAT IT SURFACED — 48 pre-existing wrong vectors that have nothing to do with #973, identical on binaries built before and after the fix. Reported, not narrowed away, and both classes proven from the emitted bytes: * #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 (`mov r0,r0; movw r1,#0x64; mov r0,r1; adds r2,r0,r0`); `get_set_get_param_no_alias` never reads its argument at all. RV32 has the protection (`snapshot_aliases`) and its own fixture comment predicts this miscompile; ARM has no equivalent. 44 vectors, 4 exports. * #990 — a local written on only ONE arm of a `br_if` is never zero-inited, so the merge reads uninitialised stack (`bne` jumps past the only `str.w`, then `ldr.w` reads the slot). Provable rather than inferred: the returned values are this harness's 0xDEADBEEF poison plus/minus one, the two `select` arms at the merge. #970 closed the parameter half of this class; this is the local-on-a-br_if half. 3 vectors, information-disclosure shape. They are listed in `KNOWN_ARM_MISMATCHES` against their issue number, ratcheted in both directions — an entry that stops mismatching must be deleted, which is how each fix will record itself — and SUPPRESSED rather than skipped, so listing debt cannot buy slack in the comparison floor. FLOORS ARE MEASURED, NOT GUESSED (this hub found existing floors at half their real value). Both scripts were calibrated through the real CI invocation path, `scripts/oracle_run.py --report-only`: select_i64cmp_973_arm_differential.py emulations = 360 (floor 360) arm_corpus_sweep_973.py emulations = 2335 (floor 2335) The sweep carries a SECOND floor the driver cannot express: `emulations` counts emulator ENTRIES, and a run that entered the emulator and then discarded every result on budget grounds would still clear it. `MIN_COMPARED = 2327` is the floor on vectors actually compared against wasmtime. HONEST GAPS, all counted and printed rather than assumed away: 91 modules are excluded from phase B for declaring a memory/table/global/data/elem/import section (their images are `repro-sweep-memory-oracle`'s job — a differential that reported its own setup gaps as miscompiles would train people to ignore it); 37 vectors trap under wasmtime; 36 exceed a budget. Both engines get one — wasmtime runs on FUEL, unicorn on an instruction count — because `aarch64_ctrlflow_851.wat:countdown(-1)` is a 2^32-iteration loop that costs 1.4 s per vector in the interpreter, and a leg that takes an hour gets deleted. Ledger moved with the docs, as the #910 ritual requires: ORACLE_WIRING.md 144 -> 146 oracles and 296,059 -> 298,754 entries, feature_matrix.md.tmpl, claims.yaml (both the verbatim texts and the emulations count-min), and ci.yml's `--min-emulation-floor`. Also corrected two pre-existing drifts found in the same table: the stdout floor total read 458 against a measured 460, and the doc's `--min-emulation-floor 295621` disagreed with ci.yml's 295726. claim_check 43/43. --- .github/workflows/ci.yml | 68 ++- claims.yaml | 12 +- .../src/instruction_selector.rs | 181 +++++- docs/status/FEATURE_MATRIX.md | 2 +- scripts/repro/ORACLE_WIRING.md | 6 +- scripts/repro/arm_corpus_sweep_973.py | 517 ++++++++++++++++++ scripts/templates/feature_matrix.md.tmpl | 2 +- 7 files changed, 756 insertions(+), 32 deletions(-) create mode 100644 scripts/repro/arm_corpus_sweep_973.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 843bd958..be86362c 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,72 @@ 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" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools capstone + - name: Install wabt (wat2wasm — the whole corpus is .wat) + run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt + - 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 a3a8772a..72a3844e 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -1213,13 +1213,16 @@ fn pop_operand( /// applies in [`bulk_mutable_operand`] — "every popped operand of the op" — /// generalized so the next multi-pop site cannot forget it. /// -/// The post-check is not redundant with the reservation: it is the invariant -/// stated where a future edit would break it. It only fires on a RELOAD (a -/// register-resident operand legitimately aliases a live param, and `select -/// (local.get 0) (local.get 0) c` legitimately pops the same register twice), -/// and 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. +/// 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, @@ -1236,23 +1239,40 @@ fn pop_operand_committed( 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 mut landed = vec![reg]; - if is_i64 { - landed.push(i64_pair_hi(reg)?); - } - if let Some(clobbered) = landed.into_iter().find(|r| committed.contains(r)) { - 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." - ))); - } + 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 @@ -27734,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..f4677f79 --- /dev/null +++ b/scripts/repro/arm_corpus_sweep_973.py @@ -0,0 +1,517 @@ +#!/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 + wat2wasm): + 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, or None when the REFERENCE toolchain refuses it. + + `--enable-all` because several fixtures use post-MVP proposals synth's own + frontend accepts (multi-memory, bulk-memory). A fixture wat2wasm still + refuses is a Phase-B skip with its own counter, never a silent one: synth + compiled it in Phase A, so the gap is in the reference side, and calling + that a miscompile would be the harness blaming the compiler for its own + tooling. + """ + p = subprocess.run( + ["wat2wasm", "--enable-all", str(wat), "-o", "/dev/stdout"], + capture_output=True, + ) + return p.stdout if p.returncode == 0 else 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(" Date: Tue, 18 Aug 2026 21:22:16 +0200 Subject: [PATCH 5/6] =?UTF-8?q?test(#973):=20drop=20the=20wabt=20host=20de?= =?UTF-8?q?pendency=20=E2=80=94=20assemble=20.wat=20with=20wasmtime=20itse?= =?UTF-8?q?lf?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pre-emptive fix for the class this job would otherwise have discovered the hard way. The ARM corpus sweep shelled out to `wat2wasm --enable-all`, which makes the EXECUTED POPULATION depend on the runner's wabt build: several fixtures use post-MVP proposals (multi-memory, bulk-memory), and a wabt that rejects the flag or a proposal would have refused every fixture, collapsed the comparison count, and reported it as a coverage failure rather than as the toolchain problem it is. That is the #850/#881 host-dependency class, and a never-before-run job is exactly where it hides — this repo's own #890 job comments say so verbatim. `wasmtime.wat2wasm` is the SAME library that then instantiates the module, so what parses and what runs cannot disagree, and there is no apt package in the path at all (the step is gone; the #973 differential never used wat2wasm either, it loads the `.wat` through `Module.from_file`). MEASURED EQUIVALENT, not assumed: across all 156 fixtures wabt and wasmtime accept exactly the same set (0 refusals each), and the section-id purity classification is identical for every one of them. The sweep's numbers are unchanged — compiled 144/156, 2327 compared vectors, emulations 2335, so no floor moved. Also: a mass reference-refusal now names ITSELF. Without it, a host whose assembler cannot read the corpus reds on the comparison floor, which reads as "the sweep lost coverage" and sends the next reader to the compiler. Fail-closed either way; the difference is the diagnostic. Gates re-run after the change, each without a pipe: sweep PASS (floor 2335, measured 2335), #973 differential 360/360 (floor 360, measured 360), oracle_wiring_check --min-emulation-floor 298754 rc=0, claim_check 43/43. --- .github/workflows/ci.yml | 8 +++-- scripts/repro/arm_corpus_sweep_973.py | 45 ++++++++++++++++++--------- 2 files changed, 37 insertions(+), 16 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index be86362c..8d61aa92 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3554,10 +3554,14 @@ jobs: - 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: Install wabt (wat2wasm — the whole corpus is .wat) - run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt - 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)" diff --git a/scripts/repro/arm_corpus_sweep_973.py b/scripts/repro/arm_corpus_sweep_973.py index f4677f79..98f62236 100644 --- a/scripts/repro/arm_corpus_sweep_973.py +++ b/scripts/repro/arm_corpus_sweep_973.py @@ -69,7 +69,7 @@ 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 + wat2wasm): +Run (needs wasmtime + unicorn + pyelftools — no wabt): SYNTH=./target/debug/synth python scripts/repro/arm_corpus_sweep_973.py """ import os @@ -233,20 +233,27 @@ def impure_sections(wasm): def to_wasm(wat): - """Assemble the fixture, or None when the REFERENCE toolchain refuses it. - - `--enable-all` because several fixtures use post-MVP proposals synth's own - frontend accepts (multi-memory, bulk-memory). A fixture wat2wasm still - refuses is a Phase-B skip with its own counter, never a silent one: synth - compiled it in Phase A, so the gap is in the reference side, and calling - that a miscompile would be the harness blaming the compiler for its own - tooling. + """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. """ - p = subprocess.run( - ["wat2wasm", "--enable-all", str(wat), "-o", "/dev/stdout"], - capture_output=True, - ) - return p.stdout if p.returncode == 0 else None + try: + return wasmtime.wat2wasm(wat.read_text()) + except Exception: + return None def compile_arm(wat, out): @@ -494,6 +501,16 @@ def main(): + ", ".join(f"{f}:{e} (#{KNOWN_ARM_MISMATCHES[(f, e)]})" for f, e in sorted(known_seen))) + # Name a HOST problem as a host problem. Without this a runner whose + # wasmtime cannot assemble the corpus reds on the comparison floor, which + # reads as "the sweep lost coverage" and sends the next reader to the + # compiler. Fail-closed either way; the difference is the diagnostic. + if reference_refused: + fails.append( + f"PHASE B REFERENCE: wasmtime's assembler refused {reference_refused} " + f"fixture(s) that synth compiled. That is a toolchain/host problem, " + f"not a miscompile — measured 0 on the v0.58 tree across all 156." + ) if checks < MIN_COMPARED: fails.append( f"PHASE B FLOOR: only {checks} vectors were actually COMPARED, floor is " From 618bf851259c2593df60d212a822f8fe4e2f0dda Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 18 Aug 2026 21:25:18 +0200 Subject: [PATCH 6/6] test(#973): close two small vacuity holes in the new oracles MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both found by re-reading the checkers rather than the checked code — v0.57's lesson was that 5 of its 10 defects lived in instruments. 1. The #973 differential did not assert that the emulation REACHED the return pad. The instruction budget is ~500x what these straight-line functions need, so it cannot be hit today; the point is that if it ever were, `run()` would return whatever R0 happened to hold and the vector could COMPARE EQUAL by accident. A differential that passes on a value it never finished computing is precisely the shape being guarded against elsewhere in this lane. The corpus sweep already checked PC; now both do. 2. The sweep leaked its temp dir (`mkdtemp` with no cleanup). Re-verified after the change, each without a pipe: differential 360/360 (floor 360, measured 360), sweep PASS with compiled 144/156 and 2327 compared vectors (floor 2335 emulations, measured 2335). No number moved. --- scripts/repro/arm_corpus_sweep_973.py | 3 ++- scripts/repro/select_i64cmp_973_arm_differential.py | 8 ++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/scripts/repro/arm_corpus_sweep_973.py b/scripts/repro/arm_corpus_sweep_973.py index 98f62236..aab8c1be 100644 --- a/scripts/repro/arm_corpus_sweep_973.py +++ b/scripts/repro/arm_corpus_sweep_973.py @@ -354,7 +354,8 @@ def main(): compiled, declined, unexpected = [], {}, [] objects = {} - td = tempfile.mkdtemp() + tmp = tempfile.TemporaryDirectory() + td = tmp.name for wat in wats: out = os.path.join(td, wat.stem + ".o") rc, log = compile_arm(wat, out) diff --git a/scripts/repro/select_i64cmp_973_arm_differential.py b/scripts/repro/select_i64cmp_973_arm_differential.py index 2d779172..f293c19a 100644 --- a/scripts/repro/select_i64cmp_973_arm_differential.py +++ b/scripts/repro/select_i64cmp_973_arm_differential.py @@ -71,6 +71,7 @@ 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, @@ -209,6 +210,13 @@ def run(syms, text, base, name, args): mu.emu_start((CODE + addr) | 1, RET_PAD, count=20000) except UcError as ex: return None, str(ex) + # The instruction budget is ~500x what these straight-line functions need, + # so exhausting it cannot happen today. Check anyway: without this, a run + # that stopped early returns whatever R0 happened to hold and could COMPARE + # EQUAL by accident — a differential that passes on a value it never + # finished computing is the vacuity this repo keeps rediscovering. + if mu.reg_read(UC_ARM_REG_PC) & ~1 != RET_PAD & ~1: + return None, "did not reach the return pad (instruction budget exhausted)" return mu.reg_read(UC_ARM_REG_R0) & M32, ""