diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 48340c11..099b2787 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -474,6 +474,12 @@ jobs: run: SYNTH=./target/debug/synth python scripts/repro/aarch64_ctrlflow_851_differential.py - name: Run #865 linear-memory BOUNDS oracle (OOB traps + modes differ + mask/mpu hard-error) run: SYNTH=./target/debug/synth python scripts/repro/aarch64_bounds_865_differential.py + - name: Run #851 v0.53 op-surface oracle (select x4 types + wrap/extends + drop/nop + memory.size/grow) + # The VCR-SEL-005 third-backend closes: select (CSEL/FCSEL) incl. + # NaN/-0 carry, wrap/extends with POISONED upper argument bits (the + # AAPCS64 x-view hazard), drop/nop, fixed-memory size/grow parity + # against a min=max module (growth failure is spec-forced there). + run: SYNTH=./target/debug/synth python scripts/repro/aarch64_surface_851_differential.py - name: Run decline-matrix honesty oracle run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_decline_538.py diff --git a/Cargo.lock b/Cargo.lock index 421c4d54..30562be0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1160,6 +1160,7 @@ version = "0.52.0" dependencies = [ "anyhow", "proptest", + "synth-backend-aarch64", "synth-core", "synth-synthesis", "thiserror", diff --git a/artifacts/status.json b/artifacts/status.json index 9f4dc4e2..b32b20ec 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -1,5 +1,5 @@ { - "aarch64_selector_ops": 148, + "aarch64_selector_ops": 161, "arm_refinement_assumed_connection": 5, "arm_semantics_axioms": 72, "backends": [ diff --git a/claims.yaml b/claims.yaml index 6d2b3d03..aed028d5 100644 --- a/claims.yaml +++ b/claims.yaml @@ -803,7 +803,12 @@ claims: - id: SYNTH-MATRIX-AARCH64-DIVREM-POPCNT doc: scripts/templates/feature_matrix.md.tmpl - text: "`div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards) and `popcnt` (#851)" + # v0.53: the op list this sentence heads grew (select/CSEL, drop/nop, wrap, + # extends), so the trailing " and `popcnt` (#851)" no longer reads verbatim. + # Re-pinned to the capability-bearing span — the trap-guard parenthetical is + # the load-bearing soundness claim and stays inside the pin, so a silent + # removal of the ÷0 / INT_MIN÷−1 guards still reddens this gate. + text: "`div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`" evidence: - kind: file-exists path: scripts/repro/aarch64_divrem_851_differential.py diff --git a/crates/synth-backend-aarch64/src/backend.rs b/crates/synth-backend-aarch64/src/backend.rs index 2751ceef..2b580526 100644 --- a/crates/synth-backend-aarch64/src/backend.rs +++ b/crates/synth-backend-aarch64/src/backend.rs @@ -196,6 +196,31 @@ impl Backend for AArch64Backend { // non-exported helper containing an unsupported op now FAILS the compile // instead of being silently ignored — the loud-skip contract, applied to // the whole reachable local set. + // #851: active data segments are NOT materialized by this backend — + // there is no data section, no startup, and no x28-establishing code + // (the base is an embedder precondition). Compiling a data-carrying + // module would ship its initialized region reading ZEROS where WASM + // guarantees segment bytes: the silent-miscompile class (#757/#758/ + // #798 on the other backends). Decline loudly; data-segment init is a + // documented follow-on. + if !module.data_segments.is_empty() { + return Err(BackendError::CompilationFailed(format!( + "module carries {} active data segment(s), but the aarch64 \ + backend does not materialize data segments — a load from the \ + initialized region would silently read zeros; refusing \ + (#851). Data-segment init is a documented follow-on.", + module.data_segments.len() + ))); + } + // A memory-0 segment with a NON-CONST offset is legacy-dropped at + // decode (absent from data_segments) — the recorded reason is the only + // trace. Same silent-miscompile class; same loud refusal. + if let Some(reason) = &module.default_memory_nonconst_data { + return Err(BackendError::CompilationFailed(format!( + "aarch64: {reason} — refusing to ship the region uninitialized \ + (#851)" + ))); + } let locals: Vec<&_> = module .functions .iter() diff --git a/crates/synth-backend-aarch64/src/encoder.rs b/crates/synth-backend-aarch64/src/encoder.rs index 9980a0bb..12fdc597 100644 --- a/crates/synth-backend-aarch64/src/encoder.rs +++ b/crates/synth-backend-aarch64/src/encoder.rs @@ -282,6 +282,66 @@ pub fn cset(rd: Reg, cond: Cond) -> u32 { 0x1A9F_07E0 | (cond.cset_field() << 12) | (rd as u32) } +/// `csel wd, wn, wm, ` — conditional select: `wd = cond ? wn : wm`. +/// The cond field is the ARCHITECTURAL (non-inverted) encoding, same as +/// `b.`. Clang ground truth: `csel w9, w10, w11, ne` = 0x1A8B1149. +pub fn csel(rd: Reg, rn: Reg, rm: Reg, cond: Cond) -> u32 { + 0x1A80_0000 + | ((rm as u32) << 16) + | (cond.bcond_field() << 12) + | ((rn as u32) << 5) + | (rd as u32) +} +/// `csel xd, xn, xm, ` — 64-bit form. Clang: `csel x9, x10, x11, ne` = +/// 0x9A8B1149. Width-agnostic for the wasm `select` lowering: an i32 result is +/// consumed through its low 32 bits (w-form readers), so carrying the full X +/// register is correct for both i32 and i64 operands. +pub fn csel64(rd: Reg, rn: Reg, rm: Reg, cond: Cond) -> u32 { + csel(rd, rn, rm, cond) | SF64 +} +/// `fcsel sd, sn, sm, ` — FP conditional select, single precision. +/// Clang ground truth: `fcsel s16, s17, s18, ne` = 0x1E321E30. +pub fn fcsel_s(rd: FReg, rn: FReg, rm: FReg, cond: Cond) -> u32 { + 0x1E20_0C00 + | ((rm as u32) << 16) + | (cond.bcond_field() << 12) + | ((rn as u32) << 5) + | (rd as u32) +} +/// `fcsel dd, dn, dm, ` — double-precision form. Clang: `fcsel d16, d17, +/// d18, ne` = 0x1E721E30. Used width-agnostically for the wasm `select` on FP +/// operands (an f32 lives in the low 32 bits of the D view; consumers read the +/// S view — the same convention as the epilogue's `fmov d0, dN`). +pub fn fcsel_d(rd: FReg, rn: FReg, rm: FReg, cond: Cond) -> u32 { + fcsel_s(rd, rn, rm, cond) | 0x0040_0000 +} + +/// `sxtb wd, wn` — sign-extend byte to 32 bits (`SBFM` alias). Clang ground +/// truth: `sxtb w9, w10` = 0x13001D49. +pub fn sxtb(rd: Reg, rn: Reg) -> u32 { + 0x1300_1C00 | ((rn as u32) << 5) | (rd as u32) +} +/// `sxth wd, wn` — sign-extend halfword to 32 bits. Clang: `sxth w9, w10` = +/// 0x13003D49. +pub fn sxth(rd: Reg, rn: Reg) -> u32 { + 0x1300_3C00 | ((rn as u32) << 5) | (rd as u32) +} +/// `sxtb xd, wn` — sign-extend byte to 64 bits. Clang: `sxtb x9, w10` = +/// 0x93401D49. +pub fn sxtb64(rd: Reg, rn: Reg) -> u32 { + 0x9340_1C00 | ((rn as u32) << 5) | (rd as u32) +} +/// `sxth xd, wn` — sign-extend halfword to 64 bits. Clang: `sxth x9, w10` = +/// 0x93403D49. +pub fn sxth64(rd: Reg, rn: Reg) -> u32 { + 0x9340_3C00 | ((rn as u32) << 5) | (rd as u32) +} +/// `sxtw xd, wn` — sign-extend word to 64 bits (i64.extend_i32_s / +/// i64.extend32_s). Clang: `sxtw x9, w10` = 0x93407D49. +pub fn sxtw(rd: Reg, rn: Reg) -> u32 { + 0x9340_7C00 | ((rn as u32) << 5) | (rd as u32) +} + /// `mov wd, wn` — architectural alias `orr wd, wzr, wn`. pub fn mov_reg(rd: Reg, rn: Reg) -> u32 { orr(rd, WZR, rn) @@ -905,6 +965,27 @@ mod tests { assert_eq!(mov_reg64(0, 9), 0xAA09_03E0); } + #[test] + fn csel_fcsel_encodings_match_clang() { + // clang -arch arm64 ground truth (see doc comments). + assert_eq!(csel(9, 10, 11, Cond::Ne), 0x1A8B_1149); + assert_eq!(csel64(9, 10, 11, Cond::Ne), 0x9A8B_1149); + assert_eq!(csel64(0, 1, 2, Cond::Eq), 0x9A82_0020); + assert_eq!(fcsel_s(16, 17, 18, Cond::Ne), 0x1E32_1E30); + assert_eq!(fcsel_d(16, 17, 18, Cond::Ne), 0x1E72_1E30); + assert_eq!(fcsel_d(0, 1, 2, Cond::Eq), 0x1E62_0C20); + } + + #[test] + fn sign_extend_encodings_match_clang() { + // clang -arch arm64 ground truth (see doc comments). + assert_eq!(sxtb(9, 10), 0x1300_1D49); + assert_eq!(sxth(9, 10), 0x1300_3D49); + assert_eq!(sxtb64(9, 10), 0x9340_1D49); + assert_eq!(sxth64(9, 10), 0x9340_3D49); + assert_eq!(sxtw(9, 10), 0x9340_7D49); + } + #[test] fn variable_shift_encodings_match_clang() { // 32-bit forms diff --git a/crates/synth-backend-aarch64/src/selector.rs b/crates/synth-backend-aarch64/src/selector.rs index f4d00924..ba44c444 100644 --- a/crates/synth-backend-aarch64/src/selector.rs +++ b/crates/synth-backend-aarch64/src/selector.rs @@ -24,12 +24,28 @@ //! "more-total-than-WASM" class is guarded, not naive), `popcnt` (SIMD //! `CNT`+`ADDV`), f64↔i64 reinterpret, linear-memory load/store, non-param //! locals, direct `call`, and full control flow (`if`/`else`/`loop`/`return`). +//! The VCR-SEL-005 third-backend enumeration (#851, v0.53) then closed: +//! `select` (branchless `CSEL`/`FCSEL`, both register files), `drop`/`nop`, +//! `i32.wrap_i64`, `i64.extend_i32_{s,u}`, the five in-place sign extensions +//! (`i32/i64.extend8/16/32_s` — `SXTB`/`SXTH`/`SXTW`), and fixed-memory +//! `memory.size`/`memory.grow` (declared-min page count / branchless +//! `grow(0)≡size`, `grow(n>0)`→−1, the #539 rule — growth failure is +//! §-permitted and keeps the #865 static bounds limit sound). //! -//! **Deliberately still declined (loud-skip, never wrong code):** +//! **Deliberately still declined (loud-skip, never wrong code) — the +//! mechanically-derived complement lives in the cross-backend op-parity oracle +//! (`crates/synth-backend-riscv/tests/cross_backend_op_parity.rs`, aarch64 +//! leg):** //! - `call_indirect`, import calls, `>8` integer args, multi-result or //! float-result callees (returned in v0/d0, not x0), a caller reading its own -//! params across a call (param-homing is a later increment). -//! - `br_table`, value-carrying `block`/`loop`/`if`, and register spilling. +//! params across a call (param-homing is a later increment), and WRITING a +//! parameter (`local.set`/`tee` on a param index). +//! - `br_table`, value-carrying `block`/`loop`/`if`, register spilling, +//! `global.get`/`global.set` (no globals substrate), and bulk memory +//! (`memory.copy`/`memory.fill`). +//! - Float rounding (`ceil`/`floor`/`trunc`/`nearest`), f32/f64 linear-memory +//! load/store, i64→float converts, and the TRAPPING i64-target truncations +//! (the saturating forms do lower). //! - Data-segment init and the startup that establishes the `x28` linear-memory //! base (the load/store lowering is correct given the base precondition; //! wiring it at runtime is a follow-on). OOB accesses TRAP since #865 under @@ -1706,6 +1722,146 @@ pub fn select_typed_cf_calls( stack.push(Val::gp(dst)); } } + // --- #851 / VCR-SEL-005 third-backend op-surface closes --- + // + // `nop` executes nothing (WASM §4.4.1); no code, no stack effect. + WasmOp::Nop => {} + // `drop` pops and discards the top value (either register file); + // purely a value-stack bookkeeping op, no code emitted. + WasmOp::Drop => { + stack + .pop() + .ok_or_else(|| SelectError("drop underflow".into()))?; + } + // `select`: [v1 v2 c] → c != 0 ? v1 : v2 (WASM §4.4.1) — the + // branchless conditional gale flagged in #851. Lowered to + // `cmp w_c, wzr` + `csel`/`fcsel` on NE (c nonzero picks v1). + // Width-agnostic X/D forms carry both i32/i64 (resp. f32/f64) + // correctly: consumers read the low half through w/s views, the + // same convention the epilogue and `fmov d0, dN` already use. + // Both operands must live in the SAME register file (validated + // wasm guarantees same type; a mismatch here is loud, not silent). + WasmOp::Select => { + let cond = pop_gp(&mut stack, "select")?; + let v2 = stack + .pop() + .ok_or_else(|| SelectError("select underflow".into()))?; + let v1 = stack + .pop() + .ok_or_else(|| SelectError("select underflow".into()))?; + if v1.file != v2.file { + return Err(SelectError( + "select: operand register-file mismatch (GP vs FP)".into(), + )); + } + // cmp reads only `cond`; csel/fcsel read v1/v2 before writing + // dst (single instruction), so dst may safely reuse any of the + // three just-popped registers. + words.push(enc::cmp(cond, enc::WZR)); + match v1.file { + File::Gp => { + let dst = alloc_temp(&stack)?; + words.push(enc::csel64(dst, v1.reg, v2.reg, Cond::Ne)); + stack.push(Val::gp(dst)); + } + File::Fp => { + let dst = alloc_ftemp(&stack)?; + words.push(enc::fcsel_d(dst, v1.reg, v2.reg, Cond::Ne)); + stack.push(Val::fp(dst)); + } + } + } + // `i32.wrap_i64` — take the low 32 bits. `mov wd, wn` (w-form orr) + // reads the low half and ZEROES the upper half, so the result is a + // clean i32 regardless of the source's upper bits. + WasmOp::I32WrapI64 => unop(&mut words, &mut stack, enc::mov_reg)?, + // `i64.extend_i32_u` — zero-extend: the same `mov wd, wn` (w-form + // writes zero-extend to 64 bits by architecture). + WasmOp::I64ExtendI32U => unop(&mut words, &mut stack, enc::mov_reg)?, + // `i64.extend_i32_s` / `i64.extend32_s` — sign-extend the low word + // (SXTW). Reads only the low 32 bits, so garbage upper source bits + // (e.g. an i32 param's) never leak. + WasmOp::I64ExtendI32S => unop(&mut words, &mut stack, enc::sxtw)?, + WasmOp::I64Extend32S => unop(&mut words, &mut stack, enc::sxtw)?, + // in-place sign extensions (sign-extension operators proposal) + WasmOp::I32Extend8S => unop(&mut words, &mut stack, enc::sxtb)?, + WasmOp::I32Extend16S => unop(&mut words, &mut stack, enc::sxth)?, + WasmOp::I64Extend8S => unop(&mut words, &mut stack, enc::sxtb64)?, + WasmOp::I64Extend16S => unop(&mut words, &mut stack, enc::sxth64)?, + // `memory.size` (#851): this backend never lowers a real grow (see + // MemoryGrow below), so the module's declared minimum IS the + // runtime size — the same static argument that makes the #865 + // bounds limit sound — and memory.size is the compile-time page + // count. Needs the limit, so it declines honestly under + // `--safety-bounds none` (no limit is threaded there). + WasmOp::MemorySize(mem) => { + if *mem != 0 { + return Err(SelectError(format!( + "memory.size on memory {mem}: multi-memory is not \ + supported for aarch64 (#406) — loud-declining" + ))); + } + let MemBounds::Software { limit_bytes } = bounds else { + return Err(SelectError( + "memory.size needs the module's memory limit, which is \ + not threaded under --safety-bounds none — \ + loud-declining (#851)" + .into(), + )); + }; + let dst = alloc_temp(&stack)?; + for w in enc::mov_imm32(dst, (limit_bytes / 65536) as u32) { + words.push(w); + } + stack.push(Val::gp(dst)); + } + // `memory.grow` (#851): the linear memory is a FIXED host buffer of + // the declared minimum size, so growth always fails — which WASM + // explicitly permits (§4.4.7: grow MAY fail, returning −1). + // `grow(0)` trivially succeeds and returns the current page count + // (grow(0) ≡ size, the #539 rule). Lowered branchless: + // mov t0, #pages ; mov t1, #-1 ; cmp delta, wzr ; csel t0 eq + // Keeping the failure static means the #865 bounds limit stays + // sound (the limit can never move at runtime). + WasmOp::MemoryGrow(mem) => { + if *mem != 0 { + return Err(SelectError(format!( + "memory.grow on memory {mem}: multi-memory is not \ + supported for aarch64 (#406) — loud-declining" + ))); + } + let MemBounds::Software { limit_bytes } = bounds else { + return Err(SelectError( + "memory.grow needs the module's memory limit, which is \ + not threaded under --safety-bounds none — \ + loud-declining (#851)" + .into(), + )); + }; + let delta = pop_gp(&mut stack, "memory.grow")?; + // Reserve `delta` so the two scratch temps are distinct from it. + stack.push(Val::gp(delta)); + let mut free = TEMPS + .iter() + .copied() + .filter(|t| !stack.iter().any(|v| v.file == File::Gp && v.reg == *t)); + let (Some(t0), Some(t1)) = (free.next(), free.next()) else { + stack.pop(); + return Err(SelectError( + "value-stack too deep (memory.grow needs 2 GP temps)".into(), + )); + }; + stack.pop(); + for w in enc::mov_imm32(t0, (limit_bytes / 65536) as u32) { + words.push(w); + } + for w in enc::mov_imm32(t1, u32::MAX) { + words.push(w); + } + words.push(enc::cmp(delta, enc::WZR)); + words.push(enc::csel(t0, t0, t1, Cond::Eq)); + stack.push(Val::gp(t0)); + } other => { return Err(SelectError(format!( "unsupported wasm op for aarch64 subset: {other:?}" @@ -3170,6 +3326,156 @@ mod tests { assert_eq!(w[w.len() - 2], enc::add_imm64(enc::SP, enc::SP, 16)); } + // --- #851 / VCR-SEL-005 third-backend op-surface closes --- + + #[test] + fn select_gp_lowers_to_cmp_csel() { + // (param i32 i32 i32) select(v1=p0, v2=p1, c=p2): + // cmp w2, wzr ; csel x9, x0, x1, ne ; mov x0, x9 ; ret + let ops = vec![ + WasmOp::LocalGet(0), + WasmOp::LocalGet(1), + WasmOp::LocalGet(2), + WasmOp::Select, + WasmOp::End, + ]; + let w = select(&ops, 3).unwrap(); + assert_eq!( + w, + vec![ + enc::cmp(2, enc::WZR), + enc::csel64(9, 0, 1, Cond::Ne), + enc::mov_reg64(0, 9), + enc::ret(), + ] + ); + } + + #[test] + fn select_fp_lowers_to_cmp_fcsel() { + // (param f32 f32 i32): FP operands (s0, s1 under the independent NSRN + // counter), GP condition (w0). fcsel on NE picks v1. + let ops = vec![ + WasmOp::LocalGet(0), + WasmOp::LocalGet(1), + WasmOp::LocalGet(2), + WasmOp::Select, + WasmOp::End, + ]; + let w = select_typed(&ops, 3, &[true, true, false], &[]).unwrap(); + assert_eq!( + w, + vec![ + enc::cmp(0, enc::WZR), + enc::fcsel_d(16, 0, 1, Cond::Ne), + enc::fmov_d(0, 16), + enc::ret(), + ] + ); + } + + #[test] + fn select_mixed_files_loud_declines() { + // v1 GP, v2 FP — a register-file mismatch must be loud, never silent. + let ops = vec![ + WasmOp::I32Const(1), + WasmOp::F32Const(1.0), + WasmOp::I32Const(1), + WasmOp::Select, + WasmOp::End, + ]; + assert!(select(&ops, 0).is_err()); + } + + #[test] + fn drop_pops_and_emits_nothing() { + // const 7 (movz) is dropped; result is p0 already in x0 → just ret. + let ops = vec![ + WasmOp::LocalGet(0), + WasmOp::I32Const(7), + WasmOp::Drop, + WasmOp::End, + ]; + let w = select(&ops, 1).unwrap(); + assert_eq!(w, vec![enc::movz(9, 7), enc::ret()]); + } + + #[test] + fn nop_emits_nothing() { + let ops = vec![WasmOp::Nop, WasmOp::LocalGet(0), WasmOp::Nop, WasmOp::End]; + let w = select(&ops, 1).unwrap(); + assert_eq!(w, vec![enc::ret()]); + } + + #[test] + fn wrap_and_extends_lower_to_mov_sxt() { + for (op, want) in [ + (WasmOp::I32WrapI64, enc::mov_reg(9, 0)), + (WasmOp::I64ExtendI32U, enc::mov_reg(9, 0)), + (WasmOp::I64ExtendI32S, enc::sxtw(9, 0)), + (WasmOp::I64Extend32S, enc::sxtw(9, 0)), + (WasmOp::I32Extend8S, enc::sxtb(9, 0)), + (WasmOp::I32Extend16S, enc::sxth(9, 0)), + (WasmOp::I64Extend8S, enc::sxtb64(9, 0)), + (WasmOp::I64Extend16S, enc::sxth64(9, 0)), + ] { + let ops = vec![WasmOp::LocalGet(0), op.clone(), WasmOp::End]; + let w = select(&ops, 1).unwrap(); + assert_eq!( + w, + vec![want, enc::mov_reg64(0, 9), enc::ret()], + "lowering mismatch for {op:?}" + ); + } + } + + #[test] + fn memory_size_is_page_count_constant() { + // (memory 2) → 131072 bytes → memory.size = 2. + let ops = vec![WasmOp::MemorySize(0), WasmOp::End]; + let w = sel_mem( + &ops, + 0, + MemBounds::Software { + limit_bytes: 131072, + }, + ); + assert_eq!(w, vec![enc::movz(9, 2), enc::mov_reg64(0, 9), enc::ret()]); + } + + #[test] + fn memory_grow_zero_is_size_nonzero_is_minus_one() { + // grow(delta): mov t0,#pages ; mov t1,#-1 ; cmp delta,wzr ; csel eq. + let ops = vec![WasmOp::LocalGet(0), WasmOp::MemoryGrow(0), WasmOp::End]; + let w = sel_mem(&ops, 1, MemBounds::Software { limit_bytes: 65536 }); + let mut expect = vec![enc::movz(9, 1)]; + expect.extend(enc::mov_imm32(10, u32::MAX)); + expect.push(enc::cmp(0, enc::WZR)); + expect.push(enc::csel(9, 9, 10, Cond::Eq)); + expect.push(enc::mov_reg64(0, 9)); + expect.push(enc::ret()); + assert_eq!(w, expect); + } + + #[test] + fn memory_size_declines_without_limit() { + // Under --safety-bounds none no limit is threaded — decline loudly. + let ops = vec![WasmOp::MemorySize(0), WasmOp::End]; + let r = select_typed_cf_calls( + &ops, + 0, + &[], + &[], + &[], + 0, + &[], + &[], + &[], + MemBounds::Unchecked, + ); + assert!(r.is_err()); + } + #[test] fn three_locals_frame_rounds_to_32() { // 0 params, 3 non-param locals → 3*8 = 24 rounds up to 32. diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index 16820324..fce99ef9 100644 --- a/crates/synth-backend-riscv/Cargo.toml +++ b/crates/synth-backend-riscv/Cargo.toml @@ -19,3 +19,6 @@ tracing.workspace = true [dev-dependencies] proptest.workspace = true +# VCR-SEL-005 (#851): the cross-backend op-parity oracle probes the AArch64 +# selector as the THIRD backend (tests/cross_backend_op_parity.rs only). +synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.52.0" } diff --git a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs index 4833a31e..d00c4e58 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -80,6 +80,32 @@ fn riscv_lowers(ops: &[WasmOp], num_params: u32) -> bool { riscv_select(ops, num_params).is_ok() } +/// Does the AArch64 (A64 host-native) selector lower this sequence? (#851 — +/// the THIRD backend in the VCR-SEL-005 enumeration.) +/// +/// Construction mirrors the real call site (`synth-backend-aarch64/backend.rs`): +/// no imports, a single void 0-arg local function `func_0` as call metadata (so +/// the `call` probe resolves), and the SHIPPING default bounds mode +/// (`MemBounds::Software` with a 1-page limit — the `--safety-bounds software` +/// CLI default). Unlike ARM, the aarch64 float lowering is NOT +/// target-parameterized (one fixed host profile), so the float surface is +/// probe-able here too — see [`a64_extended_surface`]. +fn aarch64_lowers(ops: &[WasmOp], num_params: u32) -> bool { + synth_backend_aarch64::selector::select_typed_cf_calls( + ops, + num_params, + &[], + &[], + &[], + 0, + &[0], + &[0], + &[false], + synth_backend_aarch64::selector::MemBounds::Software { limit_bytes: 65536 }, + ) + .is_ok() +} + /// The parity class of a `WasmOp` — assigned by the no-wildcard [`classify`] /// match so the WASM-op universe is compiler-enforced complete. enum ParityClass { @@ -836,6 +862,785 @@ fn known_divergences() -> &'static [(&'static str, &'static str)] { ] } +/// Ledger of KNOWN AArch64-vs-ARM divergences among the INTEGER-CORE ops (#851 +/// — the third-backend leg of VCR-SEL-005). ARM (the most complete backend) is +/// the reference: an entry means "ARM lowers this, the aarch64 selector +/// loud-declines it" (or, exceptionally, the reverse — the reason must say so). +/// Same contract as [`known_divergences`]: every entry carries a concrete +/// reason; when the aarch64 lowering lands the stale-entry check FAILS until +/// the line is deleted, so a deferral cannot quietly outlive its fix. +/// +/// MEASURED 2026-07-29 (this file's aarch64 leg, probing the real selector): +/// the initial enumeration surfaced TWENTY ARM-lowers/aarch64-declines gaps. +/// Thirteen were closed in the same change (v0.53 #851: `select` via +/// CSEL/FCSEL, `drop`, `nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, the five +/// `extend8/16/32_s` forms, fixed-memory `memory.size`/`memory.grow`), leaving +/// the SEVEN below. This ledger — the COMPLEMENT of what aarch64 lowers — is +/// the mechanically-derived answer to "what is missing on armv8?" (#851); the +/// float-surface complement lives in [`a64_extended_surface`]. +fn aarch64_known_divergences() -> &'static [(&'static str, &'static str)] { + &[ + ( + "br_table", + "aarch64 selector has no BrTable arm (loud decline); the jump-table \ + dispatch is not yet lowered — deferred, VCR-SEL-005/#851", + ), + ( + "local.set+get(param)", + "aarch64 declines WRITING a parameter: params live in arg registers \ + by reference on the value stack, so a param write could alias a \ + stacked value; param HOMING (to callee-saved regs or slots) is the \ + prerequisite — deferred, #851", + ), + ( + "local.tee(param)", + "aarch64 declines writing a parameter (same homing prerequisite as \ + local.set) — deferred, #851", + ), + ( + "global.get", + "aarch64 has no globals substrate (no data section / global-region \ + addressing convention beyond the x28 linear-memory base); the \ + RV32 ledger entry above documents the same #798-class stack needed \ + — deferred, #851", + ), + ( + "global.set", + "aarch64 has no globals substrate (see global.get) — deferred, #851", + ), + ( + "memory.copy", + "aarch64 selector has no MemoryCopy arm (loud decline); bulk-memory \ + (#374) not yet lowered on aarch64 — deferred, #851", + ), + ( + "memory.fill", + "aarch64 selector has no MemoryFill arm (loud decline); bulk-memory \ + (#374) not yet lowered on aarch64 — deferred, #851", + ), + ] +} + +/// The aarch64 leg of the parity gate: probe every INTEGER-CORE op on the +/// AArch64 selector against the ARM reference. Same both-direction contract as +/// [`run_parity`]: an unledgered divergence is a #223-class gap (red); a +/// ledgered entry whose gap has closed is stale (red until deleted). +fn run_a64_parity( + ledger: &std::collections::HashMap<&str, &str>, +) -> (usize, Vec, Vec) { + let mut unexpected: Vec = Vec::new(); + let mut stale: Vec = Vec::new(); + let mut at_parity = 0usize; + + for op in all_wasm_op_representatives() { + let (label, num_params, ops) = match classify(&op) { + ParityClass::IntegerCore { + label, + num_params, + ops, + } => (label, num_params, ops), + ParityClass::StructurallyExcluded(_) => continue, + }; + + let arm = arm_lowers(&ops, num_params); + let a64 = aarch64_lowers(&ops, num_params); + let ledgered = ledger.get(label); + + match (arm == a64, ledgered) { + (true, None) => at_parity += 1, + (true, Some(_reason)) => stale.push(format!( + " {label} — ledgered as an ARM/aarch64 divergence but both now \ + agree (arm_ok={arm}, aarch64_ok={a64}); delete the entry" + )), + (false, Some(_reason)) => { /* known, explained divergence — OK */ } + (false, None) => unexpected.push(format!( + " {label} — arm_lowers={arm}, aarch64_lowers={a64} (cross-backend \ + op-gap; the #223 class, third backend). Either implement the \ + missing aarch64 lowering or ledger it with a reason." + )), + } + } + (at_parity, unexpected, stale) +} + +/// The aarch64 surface for the ops [`classify`] marks `StructurallyExcluded` +/// (#851). Those exclusions exist because the ARM float lowering is +/// TARGET-PARAMETERIZED and RV32 has no FPU — but the aarch64 backend has ONE +/// fixed host profile, so its float surface IS probe-able and deserves the same +/// no-gap-can-hide treatment. NO wildcard arm: a new `WasmOp` variant fails to +/// compile here too until placed. +/// +/// Returns `None` for ops handled by the IntegerCore parity leg +/// ([`run_a64_parity`]), `Some((label, num_params, probe, expect))` otherwise, +/// where `expect` is `Ok(())` when the aarch64 selector MUST lower the probe +/// and `Err(reason)` when it MUST decline (the reason documents the gap — the +/// valuable complement). Both directions are asserted: a decline where lowering +/// is expected is a regression; a lowering where a decline is recorded is a +/// stale entry that must be flipped (a gap claim must not outlive the gap). +#[allow(clippy::type_complexity)] +fn a64_extended_surface( + op: &WasmOp, +) -> Option<(&'static str, u32, Vec, Result<(), &'static str>)> { + // Gap reasons, shared per class. + const ROUNDING: &str = "aarch64 selector has no ceil/floor/trunc/nearest arm (A64 FRINTP/FRINTM/\ + FRINTZ/FRINTN exist; encoder support not yet landed) — deferred, #851"; + const FP_MEM: &str = "aarch64 selector has no f32/f64 load/store arm (linear-memory FP access \ + needs LDR/STR (SIMD&FP) forms) — deferred, #851"; + const I64_TO_FP: &str = "aarch64 selector has no i64→float convert arm (SCVTF/UCVTF x-forms not \ + yet landed; only the i32-source forms are) — deferred, #851"; + const TRAP_TRUNC_I64: &str = "aarch64 selector has no TRAPPING i64-target truncation arm (needs the \ + #709-class i64 domain guard; the SATURATING i64 forms do lower) — \ + deferred, #851"; + const SIMD: &str = "v128/SIMD is not lowered on aarch64 (Advanced-SIMD lowering is a separate \ + lane, mirroring the ARM Helium/MVE exclusion) — deferred, #851"; + const MULTI_MEM: &str = "multi-memory wrapper (#406): the aarch64 backend has no per-memory base \ + lowering (single x28 base only) — declines, #851"; + const CALL_INDIRECT: &str = "call_indirect needs a function table + type/null/OOB trap guards \ + (§4.4.8); no aarch64 table substrate yet — loud-declined, #851"; + + let some = + |label: &'static str, + num_params: u32, + ops: Vec, + expect: Result<(), &'static str>| Some((label, num_params, ops, expect)); + + match op { + // ─── handled by the IntegerCore parity leg ─────────────────────── + I32Add + | I32Sub + | I32Mul + | I32DivS + | I32DivU + | I32RemS + | I32RemU + | I32And + | I32Or + | I32Xor + | I32Shl + | I32ShrS + | I32ShrU + | I32Rotl + | I32Rotr + | I32Clz + | I32Ctz + | I32Popcnt + | I32Extend8S + | I32Extend16S + | I32Eqz + | I32Eq + | I32Ne + | I32LtS + | I32LtU + | I32LeS + | I32LeU + | I32GtS + | I32GtU + | I32GeS + | I32GeU + | I32Const(_) + | I32Load { .. } + | I32Store { .. } + | I32Load8S { .. } + | I32Load8U { .. } + | I32Load16S { .. } + | I32Load16U { .. } + | I32Store8 { .. } + | I32Store16 { .. } + | Block + | Loop + | Br(_) + | BrIf(_) + | BrTable { .. } + | Return + | If + | Else + | End + | Call(_) + | LocalGet(_) + | LocalSet(_) + | LocalTee(_) + | GlobalGet(_) + | GlobalSet(_) + | MemorySize(_) + | MemoryGrow(_) + | MemoryCopy + | MemoryFill + | Drop + | Select + | Unreachable + | Nop + | I64Add + | I64Sub + | I64Mul + | I64DivS + | I64DivU + | I64RemS + | I64RemU + | I64And + | I64Or + | I64Xor + | I64Shl + | I64ShrS + | I64ShrU + | I64Rotl + | I64Rotr + | I64Clz + | I64Ctz + | I64Popcnt + | I64Eqz + | I64Eq + | I64Ne + | I64LtS + | I64LtU + | I64LeS + | I64LeU + | I64GtS + | I64GtU + | I64GeS + | I64GeU + | I64Const(_) + | I64Load { .. } + | I64Store { .. } + | I64Load8S { .. } + | I64Load8U { .. } + | I64Load16S { .. } + | I64Load16U { .. } + | I64Load32S { .. } + | I64Load32U { .. } + | I64Store8 { .. } + | I64Store16 { .. } + | I64Store32 { .. } + | I64ExtendI32S + | I64ExtendI32U + | I32WrapI64 + | I64Extend8S + | I64Extend16S + | I64Extend32S => None, + + // ─── f32 arithmetic / compares — lower (m3/m4, #538) ───────────── + F32Add => some( + "f32.add", + 0, + vec![F32Const(1.5), F32Const(2.5), F32Add], + Ok(()), + ), + F32Sub => some( + "f32.sub", + 0, + vec![F32Const(1.5), F32Const(2.5), F32Sub], + Ok(()), + ), + F32Mul => some( + "f32.mul", + 0, + vec![F32Const(1.5), F32Const(2.5), F32Mul], + Ok(()), + ), + F32Div => some( + "f32.div", + 0, + vec![F32Const(1.5), F32Const(2.5), F32Div], + Ok(()), + ), + F32Eq => some( + "f32.eq", + 0, + vec![F32Const(1.0), F32Const(2.0), F32Eq], + Ok(()), + ), + F32Ne => some( + "f32.ne", + 0, + vec![F32Const(1.0), F32Const(2.0), F32Ne], + Ok(()), + ), + F32Lt => some( + "f32.lt", + 0, + vec![F32Const(1.0), F32Const(2.0), F32Lt], + Ok(()), + ), + F32Le => some( + "f32.le", + 0, + vec![F32Const(1.0), F32Const(2.0), F32Le], + Ok(()), + ), + F32Gt => some( + "f32.gt", + 0, + vec![F32Const(1.0), F32Const(2.0), F32Gt], + Ok(()), + ), + F32Ge => some( + "f32.ge", + 0, + vec![F32Const(1.0), F32Const(2.0), F32Ge], + Ok(()), + ), + F32Abs => some("f32.abs", 0, vec![F32Const(-1.5), F32Abs], Ok(())), + F32Neg => some("f32.neg", 0, vec![F32Const(1.5), F32Neg], Ok(())), + F32Sqrt => some("f32.sqrt", 0, vec![F32Const(2.0), F32Sqrt], Ok(())), + F32Min => some( + "f32.min", + 0, + vec![F32Const(1.0), F32Const(2.0), F32Min], + Ok(()), + ), + F32Max => some( + "f32.max", + 0, + vec![F32Const(1.0), F32Const(2.0), F32Max], + Ok(()), + ), + F32Copysign => some( + "f32.copysign", + 0, + vec![F32Const(1.0), F32Const(-2.0), F32Copysign], + Ok(()), + ), + F32Const(_) => some("f32.const", 0, vec![F32Const(1.0)], Ok(())), + // ─── f32 rounding — GAP ────────────────────────────────────────── + F32Ceil => some("f32.ceil", 0, vec![F32Const(1.5), F32Ceil], Err(ROUNDING)), + F32Floor => some("f32.floor", 0, vec![F32Const(1.5), F32Floor], Err(ROUNDING)), + F32Trunc => some("f32.trunc", 0, vec![F32Const(1.5), F32Trunc], Err(ROUNDING)), + F32Nearest => some( + "f32.nearest", + 0, + vec![F32Const(1.5), F32Nearest], + Err(ROUNDING), + ), + // ─── f32 memory — GAP ──────────────────────────────────────────── + F32Load { .. } => some( + "f32.load", + 0, + vec![ + I32Const(0), + F32Load { + offset: 0, + align: 2, + }, + ], + Err(FP_MEM), + ), + F32Store { .. } => some( + "f32.store", + 0, + vec![ + I32Const(0), + F32Const(1.0), + F32Store { + offset: 0, + align: 2, + }, + ], + Err(FP_MEM), + ), + // ─── f32 conversions ───────────────────────────────────────────── + F32ConvertI32S => some( + "f32.convert_i32_s", + 0, + vec![I32Const(5), F32ConvertI32S], + Ok(()), + ), + F32ConvertI32U => some( + "f32.convert_i32_u", + 0, + vec![I32Const(5), F32ConvertI32U], + Ok(()), + ), + F32ConvertI64S => some( + "f32.convert_i64_s", + 0, + vec![I64Const(5), F32ConvertI64S], + Err(I64_TO_FP), + ), + F32ConvertI64U => some( + "f32.convert_i64_u", + 0, + vec![I64Const(5), F32ConvertI64U], + Err(I64_TO_FP), + ), + F32DemoteF64 => some( + "f32.demote_f64", + 0, + vec![F64Const(1.5), F32DemoteF64], + Ok(()), + ), + F32ReinterpretI32 => some( + "f32.reinterpret_i32", + 0, + vec![I32Const(1), F32ReinterpretI32], + Ok(()), + ), + I32ReinterpretF32 => some( + "i32.reinterpret_f32", + 0, + vec![F32Const(1.0), I32ReinterpretF32], + Ok(()), + ), + I32TruncF32S => some( + "i32.trunc_f32_s", + 0, + vec![F32Const(1.5), I32TruncF32S], + Ok(()), + ), + I32TruncF32U => some( + "i32.trunc_f32_u", + 0, + vec![F32Const(1.5), I32TruncF32U], + Ok(()), + ), + I32TruncSatF32S => some( + "i32.trunc_sat_f32_s", + 0, + vec![F32Const(1.5), I32TruncSatF32S], + Ok(()), + ), + I32TruncSatF32U => some( + "i32.trunc_sat_f32_u", + 0, + vec![F32Const(1.5), I32TruncSatF32U], + Ok(()), + ), + I64TruncSatF32S => some( + "i64.trunc_sat_f32_s", + 0, + vec![F32Const(1.5), I64TruncSatF32S], + Ok(()), + ), + I64TruncSatF32U => some( + "i64.trunc_sat_f32_u", + 0, + vec![F32Const(1.5), I64TruncSatF32U], + Ok(()), + ), + I64TruncF32S => some( + "i64.trunc_f32_s", + 0, + vec![F32Const(1.5), I64TruncF32S], + Err(TRAP_TRUNC_I64), + ), + I64TruncF32U => some( + "i64.trunc_f32_u", + 0, + vec![F32Const(1.5), I64TruncF32U], + Err(TRAP_TRUNC_I64), + ), + + // ─── f64 arithmetic / compares — lower (m3/m4, #538) ───────────── + F64Add => some( + "f64.add", + 0, + vec![F64Const(1.5), F64Const(2.5), F64Add], + Ok(()), + ), + F64Sub => some( + "f64.sub", + 0, + vec![F64Const(1.5), F64Const(2.5), F64Sub], + Ok(()), + ), + F64Mul => some( + "f64.mul", + 0, + vec![F64Const(1.5), F64Const(2.5), F64Mul], + Ok(()), + ), + F64Div => some( + "f64.div", + 0, + vec![F64Const(1.5), F64Const(2.5), F64Div], + Ok(()), + ), + F64Eq => some( + "f64.eq", + 0, + vec![F64Const(1.0), F64Const(2.0), F64Eq], + Ok(()), + ), + F64Ne => some( + "f64.ne", + 0, + vec![F64Const(1.0), F64Const(2.0), F64Ne], + Ok(()), + ), + F64Lt => some( + "f64.lt", + 0, + vec![F64Const(1.0), F64Const(2.0), F64Lt], + Ok(()), + ), + F64Le => some( + "f64.le", + 0, + vec![F64Const(1.0), F64Const(2.0), F64Le], + Ok(()), + ), + F64Gt => some( + "f64.gt", + 0, + vec![F64Const(1.0), F64Const(2.0), F64Gt], + Ok(()), + ), + F64Ge => some( + "f64.ge", + 0, + vec![F64Const(1.0), F64Const(2.0), F64Ge], + Ok(()), + ), + F64Abs => some("f64.abs", 0, vec![F64Const(-1.5), F64Abs], Ok(())), + F64Neg => some("f64.neg", 0, vec![F64Const(1.5), F64Neg], Ok(())), + F64Sqrt => some("f64.sqrt", 0, vec![F64Const(2.0), F64Sqrt], Ok(())), + F64Min => some( + "f64.min", + 0, + vec![F64Const(1.0), F64Const(2.0), F64Min], + Ok(()), + ), + F64Max => some( + "f64.max", + 0, + vec![F64Const(1.0), F64Const(2.0), F64Max], + Ok(()), + ), + F64Copysign => some( + "f64.copysign", + 0, + vec![F64Const(1.0), F64Const(-2.0), F64Copysign], + Ok(()), + ), + F64Const(_) => some("f64.const", 0, vec![F64Const(1.0)], Ok(())), + // ─── f64 rounding — GAP ────────────────────────────────────────── + F64Ceil => some("f64.ceil", 0, vec![F64Const(1.5), F64Ceil], Err(ROUNDING)), + F64Floor => some("f64.floor", 0, vec![F64Const(1.5), F64Floor], Err(ROUNDING)), + F64Trunc => some("f64.trunc", 0, vec![F64Const(1.5), F64Trunc], Err(ROUNDING)), + F64Nearest => some( + "f64.nearest", + 0, + vec![F64Const(1.5), F64Nearest], + Err(ROUNDING), + ), + // ─── f64 memory — GAP ──────────────────────────────────────────── + F64Load { .. } => some( + "f64.load", + 0, + vec![ + I32Const(0), + F64Load { + offset: 0, + align: 3, + }, + ], + Err(FP_MEM), + ), + F64Store { .. } => some( + "f64.store", + 0, + vec![ + I32Const(0), + F64Const(1.0), + F64Store { + offset: 0, + align: 3, + }, + ], + Err(FP_MEM), + ), + // ─── f64 conversions ───────────────────────────────────────────── + F64ConvertI32S => some( + "f64.convert_i32_s", + 0, + vec![I32Const(5), F64ConvertI32S], + Ok(()), + ), + F64ConvertI32U => some( + "f64.convert_i32_u", + 0, + vec![I32Const(5), F64ConvertI32U], + Ok(()), + ), + F64ConvertI64S => some( + "f64.convert_i64_s", + 0, + vec![I64Const(5), F64ConvertI64S], + Err(I64_TO_FP), + ), + F64ConvertI64U => some( + "f64.convert_i64_u", + 0, + vec![I64Const(5), F64ConvertI64U], + Err(I64_TO_FP), + ), + F64PromoteF32 => some( + "f64.promote_f32", + 0, + vec![F32Const(1.5), F64PromoteF32], + Ok(()), + ), + F64ReinterpretI64 => some( + "f64.reinterpret_i64", + 0, + vec![I64Const(1), F64ReinterpretI64], + Ok(()), + ), + I64ReinterpretF64 => some( + "i64.reinterpret_f64", + 0, + vec![F64Const(1.0), I64ReinterpretF64], + Ok(()), + ), + I32TruncF64S => some( + "i32.trunc_f64_s", + 0, + vec![F64Const(1.5), I32TruncF64S], + Ok(()), + ), + I32TruncF64U => some( + "i32.trunc_f64_u", + 0, + vec![F64Const(1.5), I32TruncF64U], + Ok(()), + ), + I32TruncSatF64S => some( + "i32.trunc_sat_f64_s", + 0, + vec![F64Const(1.5), I32TruncSatF64S], + Ok(()), + ), + I32TruncSatF64U => some( + "i32.trunc_sat_f64_u", + 0, + vec![F64Const(1.5), I32TruncSatF64U], + Ok(()), + ), + I64TruncSatF64S => some( + "i64.trunc_sat_f64_s", + 0, + vec![F64Const(1.5), I64TruncSatF64S], + Ok(()), + ), + I64TruncSatF64U => some( + "i64.trunc_sat_f64_u", + 0, + vec![F64Const(1.5), I64TruncSatF64U], + Ok(()), + ), + I64TruncF64S => some( + "i64.trunc_f64_s", + 0, + vec![F64Const(1.5), I64TruncF64S], + Err(TRAP_TRUNC_I64), + ), + I64TruncF64U => some( + "i64.trunc_f64_u", + 0, + vec![F64Const(1.5), I64TruncF64U], + Err(TRAP_TRUNC_I64), + ), + + // ─── module-context ops — declines with named reasons ──────────── + MultiMemory { .. } => some( + "multi-memory wrapper", + 0, + vec![ + I32Const(0), + MultiMemory { + memory: 1, + op: Box::new(I32Load { + offset: 0, + align: 2, + }), + }, + ], + Err(MULTI_MEM), + ), + CallIndirect { .. } => some( + "call_indirect", + 0, + vec![ + I32Const(0), + CallIndirect { + type_index: 0, + table_index: 0, + }, + ], + Err(CALL_INDIRECT), + ), + + // ─── v128 / SIMD — GAP (all decline) ───────────────────────────── + V128Const(_) => some("v128.const", 0, vec![V128Const([0; 16])], Err(SIMD)), + V128Load { .. } => some( + "v128.load", + 0, + vec![ + I32Const(0), + V128Load { + offset: 0, + align: 4, + }, + ], + Err(SIMD), + ), + V128Store { .. } => some( + "v128.store", + 0, + vec![ + I32Const(0), + V128Const([0; 16]), + V128Store { + offset: 0, + align: 4, + }, + ], + Err(SIMD), + ), + V128And => some( + "v128.and", + 0, + vec![V128Const([0; 16]), V128Const([0; 16]), V128And], + Err(SIMD), + ), + V128Or => some( + "v128.or", + 0, + vec![V128Const([0; 16]), V128Const([0; 16]), V128Or], + Err(SIMD), + ), + V128Xor => some( + "v128.xor", + 0, + vec![V128Const([0; 16]), V128Const([0; 16]), V128Xor], + Err(SIMD), + ), + V128Not => some("v128.not", 0, vec![V128Const([0; 16]), V128Not], Err(SIMD)), + V128AndNot => some( + "v128.andnot", + 0, + vec![V128Const([0; 16]), V128Const([0; 16]), V128AndNot], + Err(SIMD), + ), + I8x16Add | I8x16Sub | I8x16Neg | I8x16Eq | I8x16Ne | I8x16LtS | I8x16LtU | I8x16GtS + | I8x16GtU | I8x16LeS | I8x16LeU | I8x16GeS | I8x16GeU | I8x16Splat + | I8x16ExtractLaneS(_) | I8x16ExtractLaneU(_) | I8x16ReplaceLane(_) | I8x16Shuffle(_) + | I8x16Swizzle | I16x8Add | I16x8Sub | I16x8Mul | I16x8Neg | I16x8Eq | I16x8Ne + | I16x8LtS | I16x8LtU | I16x8GtS | I16x8GtU | I16x8LeS | I16x8LeU | I16x8GeS | I16x8GeU + | I16x8Splat | I16x8ExtractLaneS(_) | I16x8ExtractLaneU(_) | I16x8ReplaceLane(_) + | I32x4Add | I32x4Sub | I32x4Mul | I32x4Neg | I32x4Eq | I32x4Ne | I32x4LtS | I32x4LtU + | I32x4GtS | I32x4GtU | I32x4LeS | I32x4LeU | I32x4GeS | I32x4GeU | I32x4Splat + | I32x4ExtractLane(_) | I32x4ReplaceLane(_) | I64x2Add | I64x2Sub | I64x2Mul | I64x2Neg + | I64x2Eq | I64x2Ne | I64x2LtS | I64x2GtS | I64x2LeS | I64x2GeS | I64x2Splat + | I64x2ExtractLane(_) | I64x2ReplaceLane(_) | F32x4Add | F32x4Sub | F32x4Mul | F32x4Div + | F32x4Abs | F32x4Neg | F32x4Sqrt | F32x4Eq | F32x4Ne | F32x4Lt | F32x4Le | F32x4Gt + | F32x4Ge | F32x4Splat | F32x4ExtractLane(_) | F32x4ReplaceLane(_) => some( + "simd (grouped)", + 0, + vec![V128Const([0; 16]), V128Const([0; 16]), op.clone()], + Err(SIMD), + ), + } +} + /// The classification core, factored out so the red-first companion test can /// drive it with a mutated ledger. Returns (at_parity_count, unexpected, stale). /// @@ -941,6 +1746,138 @@ fn red_first_unledgered_one_sided_gap_is_caught() { ); } +/// #851 — the aarch64 (third-backend) integer-core parity gate. Same shape as +/// [`cross_backend_integer_op_parity_242`]: an unledgered ARM/aarch64 +/// divergence is red (the #223 class on the third backend); a ledgered entry +/// whose gap closed is red until deleted. +#[test] +fn aarch64_integer_op_parity_851() { + let ledger: std::collections::HashMap<&str, &str> = + aarch64_known_divergences().iter().copied().collect(); + + let (at_parity, unexpected, stale) = run_a64_parity(&ledger); + + // Non-vacuity floor: the probe must actually exercise the aarch64 selector + // across the shared integer core. + assert!( + at_parity >= 60, + "aarch64 parity leg exercised too few common-core ops ({at_parity}); \ + the classifier or the aarch64 probe construction regressed" + ); + + assert!( + unexpected.is_empty() && stale.is_empty(), + "ARM/aarch64 op-parity ledger is out of date:\n\ + NEW UNEXPLAINED DIVERGENCES (the #223 op-gap class, third backend):\n{}\n\ + STALE LEDGER ENTRIES (close them):\n{}", + if unexpected.is_empty() { + " (none)".into() + } else { + unexpected.join("\n") + }, + if stale.is_empty() { + " (none)".into() + } else { + stale.join("\n") + }, + ); +} + +/// #851 — the aarch64 EXTENDED surface (the ops the ARM/RV32 integer oracle +/// structurally excludes: floats, SIMD, module-context wrappers). Asserts, for +/// every such op, that the aarch64 selector's probe outcome MATCHES the +/// recorded expectation in BOTH directions: +/// * expected-Lowers but declines → capability regression (red); +/// * expected-Declines but lowers → stale gap entry (red until the entry is +/// flipped to `Ok(())` — a gap claim must not outlive the gap). +/// +/// The `Err(reason)` entries of [`a64_extended_surface`], together with the +/// [`aarch64_known_divergences`] ledger, ARE the definitive mechanically- +/// derived "what aarch64 does not lower" list. +#[test] +fn aarch64_extended_surface_851() { + let mut mismatches: Vec = Vec::new(); + let mut probed = 0usize; + + for op in all_wasm_op_representatives() { + let Some((label, num_params, ops, expect)) = a64_extended_surface(&op) else { + continue; + }; + probed += 1; + let lowered = aarch64_lowers(&ops, num_params); + match (lowered, expect) { + (true, Ok(())) | (false, Err(_)) => {} + (false, Ok(())) => mismatches.push(format!( + " {label} — expected the aarch64 selector to LOWER this probe, \ + but it declined (capability regression)" + )), + (true, Err(reason)) => mismatches.push(format!( + " {label} — recorded as an aarch64 gap ({reason}) but the \ + selector now LOWERS the probe; flip the entry to Ok(())" + )), + } + } + + // Non-vacuity floor: the extended surface spans the float + SIMD universe. + assert!( + probed >= 100, + "aarch64 extended-surface probe exercised too few ops ({probed})" + ); + assert!( + mismatches.is_empty(), + "aarch64 extended-surface expectations are out of date:\n{}", + mismatches.join("\n") + ); +} + +/// RED-FIRST non-vacuity proof for the aarch64 leg: drop a KNOWN, REAL +/// ARM-lowers/aarch64-declines entry from the ledger and assert the gate goes +/// red — proving [`run_a64_parity`] genuinely detects a one-sided gap on the +/// real selectors. +#[test] +fn red_first_unledgered_aarch64_gap_is_caught() { + let (probe_label, _) = aarch64_known_divergences()[0]; + let ledger: std::collections::HashMap<&str, &str> = aarch64_known_divergences() + .iter() + .copied() + .filter(|(label, _)| *label != probe_label) + .collect(); + + let (_at_parity, unexpected, _stale) = run_a64_parity(&ledger); + + assert!( + unexpected.iter().any(|line| line.contains(probe_label)), + "RED-FIRST vacuity check FAILED: dropping the '{probe_label}' ledger \ + entry did NOT surface it as an unexpected ARM/aarch64 divergence. \ + unexpected = {unexpected:?}" + ); +} + +/// Every aarch64-ledgered divergence must name a live `IntegerCore` label +/// (same anti-drift rule as [`ledger_labels_are_live_integer_core_ops`]). +#[test] +fn aarch64_ledger_labels_are_live_integer_core_ops() { + let live: std::collections::HashSet<&str> = all_wasm_op_representatives() + .iter() + .filter_map(|op| match classify(op) { + ParityClass::IntegerCore { label, .. } => Some(label), + ParityClass::StructurallyExcluded(_) => None, + }) + .collect(); + + let dangling: Vec<&str> = aarch64_known_divergences() + .iter() + .map(|(label, _)| *label) + .filter(|label| !live.contains(label)) + .collect(); + + assert!( + dangling.is_empty(), + "aarch64 known-divergence ledger references labels that are not live \ + IntegerCore ops: {dangling:?}" + ); +} + /// Every ledgered divergence must name a REAL integer-core op (a live /// `IntegerCore` label), so the ledger cannot drift to reference an op that no /// longer exists or was reclassified as StructurallyExcluded. diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index d09cd0a0..365457b7 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -1562,7 +1562,10 @@ fn compile_command( let mut startup_globals_words: Vec = Vec::new(); // #758: set when the single-function compile path decodes a module carrying // active data segments — the single-func cortex-m builder can't ship them. + // #851: the aarch64 single-function path declines on them too (it ships no + // data at all), including the non-const-offset segment decode legacy-drops. let mut single_func_has_data_segments = false; + let mut single_func_nonconst_data: Option = None; // #865: the module's declared minimum linear-memory size (memory 0, bytes). // The single-function path previously never threaded memory context into // the config; the aarch64 software bounds check needs the real limit (a 0 @@ -1629,6 +1632,7 @@ fn compile_command( // this path would silently read zeros. Record so the cortex-m call // below loud-declines rather than emit that silent miscompile. single_func_has_data_segments = !module.data_segments.is_empty(); + single_func_nonconst_data = module.default_memory_nonconst_data.clone(); // #865: capture memory 0's declared minimum size for the aarch64 // software bounds check (pages × 64 KiB). single_func_linear_memory_bytes = module @@ -1880,6 +1884,21 @@ fn compile_command( info!("Encoded {} bytes of machine code", code.len()); let elf_data = if backend.name() == "aarch64" { + // #851: the aarch64 object ships no data segments — a data-carrying + // module's initialized region would silently read zeros (the + // #757/#758/#798 class). Decline loudly, mirroring the cortex-m + // single-function guard below. + if single_func_has_data_segments { + anyhow::bail!( + "module carries active data segment(s), but the aarch64 \ + backend does not materialize data segments — a load from the \ + initialized region would silently read zeros; refusing \ + (#851). Data-segment init is a documented follow-on." + ); + } + if let Some(reason) = &single_func_nonconst_data { + anyhow::bail!("aarch64: {reason} — refusing to ship the region uninitialized (#851)"); + } // #546: emit the AArch64 backend's own EM_AARCH64 ELF64 object, not the // ARM (EM_ARM/ELF32) wrapper. The A64 codegen is correct; only the // container differs. Discriminate on backend name, not target family: @@ -2667,7 +2686,8 @@ fn compile_all_exports( all_wsc_facts, // VCR-PERF-002 Phase 1 (#494): loom wsc.facts premises all_extra_memory_segments, // #406: (mem_idx>0, offset, bytes) init segments on non-default memories multi_memory_decline, // #406: decode-level reason multi-memory must decline (if any) - all_call_indirect_guards, // #642: table size + closed-world type verdicts + default_memory_nonconst_data, // #851: memory-0 segment with a non-const offset (legacy-dropped at decode) + all_call_indirect_guards, // #642: table size + closed-world type verdicts all_funcref_slots, // #275: static funcref-region image (slot -> func index; None = null) ) = if path.extension().is_some_and(|ext| ext == "wast") { info!("Parsing WAST (extracting all modules)..."); @@ -2779,6 +2799,7 @@ fn compile_all_exports( Vec::new(), // #494: facts are a loom-emitted-.wasm channel; WAST fixtures carry none Vec::new(), // #406: non-default-memory data segments are single-module .wasm only None, // #406: the WAST fixture suite is single-memory — no decline reason + None, // #851: WAST fixtures carry no data segments (see #237 above) // #642: the multi-module WAST merge has no single table image to // verify — the default guards DECLINE any call_indirect (the WAST // fixture suite carries none), never an unchecked branch. @@ -2972,8 +2993,9 @@ fn compile_all_exports( // decline reason (e.g. a non-const segment offset on memory k). module.extra_memory_data_segments, module.multi_memory_decline, - guards, // #642 - funcref_slots, // #275 + module.default_memory_nonconst_data, // #851 + guards, // #642 + funcref_slots, // #275 ) }; @@ -3596,6 +3618,28 @@ fn compile_all_exports( } let elf_data = if is_aarch64 { + // #851: the aarch64 object ships NO data segments (no data section, + // no startup — the x28 base itself is an embedder precondition). A + // data-carrying module would have its initialized region silently + // read ZEROS where WASM guarantees segment bytes — the #757/#758/#798 + // silent-miscompile class. Decline loudly; data-segment init is a + // documented follow-on. + if !all_data_segments.is_empty() { + anyhow::bail!( + "module carries {} active data segment(s), but the aarch64 \ + backend does not materialize data segments (no data section \ + or startup) — a load from the initialized region would \ + silently read zeros; refusing (#851). Data-segment init is a \ + documented follow-on.", + all_data_segments.len() + ); + } + // A memory-0 segment with a NON-CONST offset was legacy-dropped at + // decode (absent from all_data_segments); the recorded reason is its + // only trace. Same class, same refusal. + if let Some(reason) = &default_memory_nonconst_data { + anyhow::bail!("aarch64: {reason} — refusing to ship the region uninitialized (#851)"); + } // #546: the AArch64 backend emits its own EM_AARCH64 ELF64 (ET_REL) // object. This must precede the `has_external_relocations || relocatable` // arm so `-b aarch64 --relocatable` isn't stolen into the ARM builder. diff --git a/crates/synth-core/src/wasm_decoder.rs b/crates/synth-core/src/wasm_decoder.rs index 34429fd3..2de42b4b 100644 --- a/crates/synth-core/src/wasm_decoder.rs +++ b/crates/synth-core/src/wasm_decoder.rs @@ -296,6 +296,14 @@ pub struct DecodedModule { /// must decline LOUDLY with this reason; single-memory modules never set /// it. pub multi_memory_decline: Option, + /// #851 — `Some(reason)` when an active data segment on MEMORY 0 has a + /// NON-CONSTANT offset expression: such a segment cannot be placed at + /// compile time and is absent from [`Self::data_segments`] (the legacy + /// drop, kept frozen for the ARM/RV32 paths). Recording it lets a backend + /// with no runtime-offset placement (aarch64) decline LOUDLY instead of + /// shipping the region uninitialized — the segment would otherwise be + /// INVISIBLE to any post-decode honesty check. + pub default_memory_nonconst_data: Option, /// Import entries (module name, field name, kind) pub imports: Vec, /// Number of imported functions (for distinguishing import calls from local calls) @@ -687,6 +695,8 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { // reason multi-memory lowering must be declined (if any). let mut extra_memory_data_segments: Vec<(u32, u32, Vec)> = Vec::new(); let mut multi_memory_decline: Option = None; + // #851: memory-0 active segment with a non-const offset (legacy-dropped). + let mut default_memory_nonconst_data: Option = None; let mut globals: Vec = Vec::new(); let mut imports = Vec::new(); let mut func_index = 0u32; @@ -1107,9 +1117,21 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { if memory_index == 0 { // Memory-0 behavior unchanged (frozen): a const- // offset segment is captured, anything else keeps - // the legacy drop. + // the legacy drop — but #851 RECORDS the drop so a + // backend without runtime-offset placement can + // decline loudly instead of shipping the region + // uninitialized (the segment is otherwise + // invisible post-decode). if let Some(off) = const_off { data_segments.push((off, data.data.to_vec())); + } else { + default_memory_nonconst_data.get_or_insert( + "active data segment on memory 0 has a \ + non-constant offset expression — it cannot \ + be placed at compile time and is NOT in \ + data_segments (#851)" + .to_string(), + ); } } else if let Some(off) = const_off { // VCR-MEM-002 phase 1 (#406): capture non-default- @@ -1299,6 +1321,7 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { data_segments, extra_memory_data_segments, multi_memory_decline, + default_memory_nonconst_data, imports, num_imported_funcs, func_arg_counts, diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 390d6890..64a2b814 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -33,7 +33,7 @@ soundness feature, not an absence. | ARM Thumb-2 (primary) | `synth-backend` | `cortex-m3`, `cortex-m4`, `cortex-m4f`, `cortex-m7`, `cortex-m7dp` (+ `cortex-m55` experimental MVE) | i32 + i64 (register pairs) complete; scalar f32/f64 via VFP on FPU targets; control flow (block/loop/if/br/br_table); memory incl. sub-word; direct calls; `call_indirect` in both relocatable and self-contained `--cortex-m` images (v0.47, #275) | | ARM A32 | `synth-backend` | `cortex-r5` | i32 + i64 integer family (221-variant no-wildcard tripwire, #615); self-contained `call_indirect` declines loudly (no flash-table builder) | | RISC-V RV32IMAC | `synth-backend-riscv` | `rv32imac`, `rv32imc`, `rv32im`, `rv32i`, `rv32gc`, `esp32c3` | i32 + i64 integer ops, control flow, calls incl. `call_indirect`, memory loads/stores; relocatable ELF; import/external calls emit `R_RISCV_CALL_PLT` relocations (`.rela.text`, undefined import symbols — #871) with exact-arity marshalling from the module signature tables; >8-arg / i64-arg / multi-value calls decline loudly; floats decline loudly | -| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | 148 distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards) and `popcnt` (#851); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms against the `x28` base, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table; data-segment init and the startup that establishes the base remain follow-ons); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851) — `call_indirect`, import calls, value-carrying blocks/loops, `br_table`, `>8` args, and float-result callees decline loudly | +| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | 161 distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851). **PRECONDITION, not emitted code:** memory-using functions expect `x28` = linear-memory base on entry — synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). Declines (loud, mechanically enumerated by the VCR-SEL-005 third-backend oracle): `call_indirect`, import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local, globals, `memory.copy`/`fill`, float `ceil`/`floor`/`trunc`/`nearest`, f32/f64 load/store, i64→float converts, trapping i64-target truncations, `>8` args, float-result callees | --- diff --git a/scripts/repro/aarch64_matrix.sh b/scripts/repro/aarch64_matrix.sh index b1de1d85..b5a95890 100755 --- a/scripts/repro/aarch64_matrix.sh +++ b/scripts/repro/aarch64_matrix.sh @@ -94,6 +94,19 @@ fop2 f32.add "f32.add" 1069547520 1077936128 fop2 f32.min "f32.min" 0 2147483648 2143289344 1065353216 fop2 f32.max "f32.max" 0 2147483648 2143289344 1065353216 fop2 f32.copysign "f32.copysign" 1065353216 2147483648 +# --- #851 v0.53 op-surface closes (select / extends / wrap / drop / nop) --- +# select with a COMPUTED condition exercises both arms across the case list. +op2 select "(select (local.get 0)(local.get 1)(i32.gt_s (local.get 0)(local.get 1)))" 3 5 5 3 -7 -9 -2147483648 2147483647 +op1 select_c "(select (i32.const 7)(i32.const 9)(local.get 0))" 0 1 -1 +op1 extend8_s "(i32.extend8_s (local.get 0))" 128 127 255 -1 +op1 extend16_s "(i32.extend16_s (local.get 0))" 32768 32767 65535 0 +op1 nop_drop "(nop)(drop (i32.const 9))(i32.add (local.get 0)(i32.const 1))" 41 -1 +lop2 select "(select (local.get 0)(local.get 1)(i64.gt_s (local.get 0)(local.get 1)))" 4000000000 5000000000 -1 1 +lop2 extend32_s "(i64.extend32_s (local.get 0))" 4294967295 0 2147483647 0 +lop2 extend8_s "(i64.extend8_s (local.get 0))" 128 0 255 0 +lop2 extend16_s "(i64.extend16_s (local.get 0))" 40000 0 32767 0 +# f32 select through the reinterpret wrapper: NaN vs 1.0 both directions. +op2 f32.select "(i32.reinterpret_f32 (select (f32.reinterpret_i32 (local.get 0))(f32.reinterpret_i32 (local.get 1))(i32.lt_u (local.get 0)(local.get 1))))" 2143289344 1065353216 1065353216 2143289344 0 2147483648 echo "aarch64: $acc ops accepted, $n native checks. Declined frontier:$dec" if [ -z "$bad" ]; then echo "PASS: all accepted aarch64 ops match wasmtime"; exit 0 diff --git a/scripts/repro/aarch64_surface_851.wat b/scripts/repro/aarch64_surface_851.wat new file mode 100644 index 00000000..46836830 --- /dev/null +++ b/scripts/repro/aarch64_surface_851.wat @@ -0,0 +1,40 @@ +(module + ;; #851 v0.53 op-surface differential module. Memory pinned min=max so + ;; memory.grow(n>0) MUST fail (-1) in wasmtime too — bit-identical to the + ;; aarch64 fixed-buffer lowering (growth failure is spec-permitted; pinning + ;; max makes it spec-forced, so the differential asserts real parity). + (memory 2 2) + + ;; select — all four value types, condition as a runtime param so both arms + ;; are exercised by the case list. + (func (export "sel32") (param i32 i32 i32) (result i32) + (select (local.get 0) (local.get 1) (local.get 2))) + (func (export "sel64") (param i64 i64 i32) (result i64) + (select (local.get 0) (local.get 1) (local.get 2))) + (func (export "self32") (param f32 f32 i32) (result f32) + (select (local.get 0) (local.get 1) (local.get 2))) + (func (export "self64") (param f64 f64 i32) (result f64) + (select (local.get 0) (local.get 1) (local.get 2))) + + ;; width conversions / in-place sign extensions + (func (export "wrap") (param i64) (result i32) (i32.wrap_i64 (local.get 0))) + (func (export "ext32s") (param i32) (result i64) (i64.extend_i32_s (local.get 0))) + (func (export "ext32u") (param i32) (result i64) (i64.extend_i32_u (local.get 0))) + (func (export "e8") (param i32) (result i32) (i32.extend8_s (local.get 0))) + (func (export "e16") (param i32) (result i32) (i32.extend16_s (local.get 0))) + (func (export "e648") (param i64) (result i64) (i64.extend8_s (local.get 0))) + (func (export "e6416") (param i64) (result i64) (i64.extend16_s (local.get 0))) + (func (export "e6432") (param i64) (result i64) (i64.extend32_s (local.get 0))) + + ;; nop + drop (no code / stack bookkeeping only) + (func (export "dn") (param i32) (result i32) + (nop) (drop (i32.const 9)) (i32.add (local.get 0) (i32.const 1))) + + ;; fixed-memory memory.size / memory.grow (grow(0) == size; grow(n>0) == -1) + (func (export "msize") (result i32) (memory.size)) + (func (export "mgrow") (param i32) (result i32) (memory.grow (local.get 0))) + ;; grow-then-size on one instance: a failed grow must NOT change the size. + (func (export "growsize") (param i32) (result i32) + (drop (memory.grow (local.get 0))) + (memory.size)) +) diff --git a/scripts/repro/aarch64_surface_851_differential.py b/scripts/repro/aarch64_surface_851_differential.py new file mode 100644 index 00000000..647af007 --- /dev/null +++ b/scripts/repro/aarch64_surface_851_differential.py @@ -0,0 +1,250 @@ +#!/usr/bin/env python3 +"""#851 v0.53 — execution-differential for the aarch64 op-surface closes. + +The VCR-SEL-005 third-backend enumeration (cross_backend_op_parity.rs, aarch64 +leg) measured 20 integer-core ops ARM lowers that aarch64 loud-declined; +thirteen were closed in v0.53: `select` (CSEL/FCSEL, all four value types), +`drop`, `nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, the five in-place sign +extensions, and fixed-memory `memory.size`/`memory.grow`. This harness +execution-verifies each of them: compiles `aarch64_surface_851.wat` with +`synth compile -b aarch64 --all-exports`, runs every exported probe under +unicorn (A64 emulation), and diffs bit-exact against wasmtime. + +Adversarial detail (AAPCS64): a caller may leave GARBAGE in the upper 32 bits +of an i32 argument register. Every i32 argument here is written with poisoned +upper bits (0x5A5A5A5A_xxxxxxxx), so a lowering that reads the X view of an +i32 (the wrap/extend hazard class) diverges from wasmtime and fails this gate. + +The module pins `(memory 2 2)` (min = max) so `memory.grow(n>0)` must fail +(-1) in wasmtime as well — the aarch64 fixed-buffer lowering's growth failure +is spec-permitted in general, but pinning max makes it spec-forced, so the +differential asserts REAL parity rather than an always-allowed divergence. + +RED-first: before the v0.53 lowerings `synth compile` fails on the first +declined op (`select`), so this gate is RED; after them it is GREEN. + +Runs on any host (unicorn emulates A64). Needs wasmtime + unicorn + pyelftools: + SYNTH=/debug/synth python scripts/repro/aarch64_surface_851_differential.py +""" + +import os +import struct +import subprocess +import sys +from pathlib import Path + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_ARM64, UC_MODE_ARM, Uc, UcError +from unicorn.arm64_const import ( + UC_ARM64_REG_D0, + UC_ARM64_REG_D1, + UC_ARM64_REG_LR, + UC_ARM64_REG_S0, + UC_ARM64_REG_S1, + UC_ARM64_REG_SP, + UC_ARM64_REG_X0, + UC_ARM64_REG_X1, + UC_ARM64_REG_X2, + UC_ARM64_REG_X28, +) + +WAT = Path(__file__).with_name("aarch64_surface_851.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") + +CODE, STK, RET = 0x100000, 0x400000, 0x500000 +LINMEM = 0x1000000 +LINMEM_SIZE = 0x20000 # 128 KiB = the (memory 2) declared minimum + +M32 = (1 << 32) - 1 +M64 = (1 << 64) - 1 +POISON = 0x5A5A_5A5A << 32 # garbage upper bits for i32 args (AAPCS-legal) + +NAN32 = 0x7FC00000 +NAN64 = 0x7FF8000000000000 + +# (fn, [param kinds], result kind, [arg case lists]) — kinds: i32/i64/f32/f64. +# f32/f64 args are given as BIT PATTERNS (ints); results compared bit-exact. +CASES = [ + # select: both arms, boundary values, cond 0/1/nonzero. + ("sel32", ["i32", "i32", "i32"], "i32", + [(10, 20, 1), (10, 20, 0), (0x80000000, 0x7FFFFFFF, 2), + (0xFFFFFFFF, 0, 0), (7, 9, 0xFFFFFFFF)]), + ("sel64", ["i64", "i64", "i32"], "i64", + [(0x0123456789ABCDEF, 0xFEDCBA9876543210, 1), + (0x0123456789ABCDEF, 0xFEDCBA9876543210, 0), + (M64, 0, 1), (M64, 0, 0)]), + ("self32", ["f32", "f32", "i32"], "f32", + [(0x3F800000, 0x40000000, 1), (0x3F800000, 0x40000000, 0), + (NAN32, 0x3F800000, 1), (NAN32, 0x3F800000, 0), + (0x80000000, 0x00000000, 1)]), # -0.0 vs +0.0: bit-exact carry + ("self64", ["f64", "f64", "i32"], "f64", + [(0x3FF0000000000000, 0x4000000000000000, 1), + (0x3FF0000000000000, 0x4000000000000000, 0), + (NAN64, 0x3FF0000000000000, 0), + (0x8000000000000000, 0, 1)]), + # wrap / extends — poisoned upper bits on every i32 arg (see POISON). + ("wrap", ["i64"], "i32", + [(0x1_00000001,), (M64,), (0x7FFFFFFF,), (0xDEADBEEF_80000000,)]), + ("ext32s", ["i32"], "i64", [(0x80000000,), (0x7FFFFFFF,), (0,), (M32,)]), + ("ext32u", ["i32"], "i64", [(0x80000000,), (0x7FFFFFFF,), (0,), (M32,)]), + ("e8", ["i32"], "i32", [(0x80,), (0x7F,), (0x1234AB80,), (M32,)]), + ("e16", ["i32"], "i32", [(0x8000,), (0x7FFF,), (0x1234_8000,), (M32,)]), + ("e648", ["i64"], "i64", [(0x80,), (0x7F,), (0xFFFF_FF80,), (M64,)]), + ("e6416", ["i64"], "i64", [(0x8000,), (0x7FFF,), (0xFFFF_8000,), (M64,)]), + ("e6432", ["i64"], "i64", + [(0x80000000,), (0x7FFFFFFF,), (0x1_00000000,), (M64,)]), + # nop + drop + ("dn", ["i32"], "i32", [(41,), (M32,)]), + # fixed-memory size/grow: size=2 pages; grow(0)=2, grow(n>0)=-1; a failed + # grow must not change the observed size. + ("msize", [], "i32", [()]), + ("mgrow", ["i32"], "i32", [(0,), (1,), (100,)]), + ("growsize", ["i32"], "i32", [(0,), (1,)]), +] + + +def sx(v, bits): + v &= (1 << bits) - 1 + return v - (1 << bits) if v & (1 << (bits - 1)) else v + + +def bits_to_float(bits, kind): + if kind == "f32": + return struct.unpack("8-arg / i64-arg / multi-value calls decline loudly; floats decline loudly | -| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | {{aarch64_selector_ops}} distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards) and `popcnt` (#851); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms against the `x28` base, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table; data-segment init and the startup that establishes the base remain follow-ons); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851) — `call_indirect`, import calls, value-carrying blocks/loops, `br_table`, `>8` args, and float-result callees decline loudly | +| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | {{aarch64_selector_ops}} distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851). **PRECONDITION, not emitted code:** memory-using functions expect `x28` = linear-memory base on entry — synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). Declines (loud, mechanically enumerated by the VCR-SEL-005 third-backend oracle): `call_indirect`, import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local, globals, `memory.copy`/`fill`, float `ceil`/`floor`/`trunc`/`nearest`, f32/f64 load/store, i64→float converts, trapping i64-target truncations, `>8` args, float-result callees | ---