diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 077fd805..d18acab5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -626,6 +626,16 @@ jobs: # This gate caught the optimized-path silent-NOP drop at land time. - name: Run trunc_sat boundary oracle (#782a, m7dp+m4f+aarch64) run: SYNTH=./target/debug/synth python scripts/repro/trunc_sat_782_differential.py + # #869: the 64-bit integer<->float conversion family (gale's six + + # the #756 i64.trunc_f64 pair) on cortex-m7dp — converts bit-exact + # (incl. the round-to-odd double-rounding killers), the TRAPPING trunc + # forms EXECUTED on every NaN/±inf/2^63/-2^63/2^64 boundary row (a + # wasmtime trap must be an ARM UDF stop — the #709-class silent- + # miscompile gate), m4f loud-decline honesty, falcon-flags symbol + # presence, and >=10k fixed-seed fuzz per direction. This gate caught + # the range-realloc cross-barrier live-in miscompile at land time. + - name: Run i64<->float conversion family oracle (#869, m7dp+m4f) + run: SYNTH=./target/debug/synth python scripts/repro/i64_float_conv_869_differential.py # #782(b): float `select` + explicit float `return` — the dominant class # on the real falcon fused core (12/26 skips incl. run-stabilization was # "an integer operation popped an f32"): select over two f32/f64 values diff --git a/CHANGELOG.md b/CHANGELOG.md index 47b4604a..0b5f5a67 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,37 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Added +- **ARM 64-bit integer↔float conversion family lowered (#869, + the #756 + `i64.trunc_f64` pair)** — all eight ops that previously loud-skipped their + function with `GI-FPU-001` now compile on `cortex-m7dp` (the falcon target), + unblocking `falcon:cascade/rate#tick`, `position#tick`, and `ekf#estimate` + at their public entry points. ARMv7E-M VFP has no 64-bit-integer `VCVT`, so + the lowerings are **self-contained multi-step expansions** (no `__aeabi` + runtime dependency, unicorn-executable): + - `f64.convert_i64_{s,u}`: exact two-word build — `VCVT` each 32-bit half, + scale the high word by 2^32 (exact), one `VADD.F64` = the single correct + round-to-nearest-even. + - `f32.convert_i64_{s,u}`: the same build plus a Fast2Sum exact residual and + a branch-free **round-to-odd** integer fixup before the `VCVT.F32.F64` + demote — the naive demote double-rounds (e.g. `0x8000_0080_0000_0001` + must round UP to 2^63+2^40 in f32; the f64 intermediate erases the sticky + bit). Round-to-odd at 53 bits makes the two-step rounding exactly equal + the direct 64→24 RNE (Boldo–Melquiond). + - `i64.trunc_f32_{s,u}` / `i64.trunc_f64_{s,u}` (**TRAPPING**, WASM §4.3.3): + the #709-class i64 domain guard (`-2^63 <= x < 2^63` signed / + `-1 < x < 2^64` unsigned, ordered compares + `UDF`; NaN fails the first + compare) in front of the #782 word-decompose, which for a guarded operand + provably never saturates. A bare decompose — or a bare `__aeabi_f2lz` + call — would saturate where WASM requires a trap: the + #633/#666/#709/#665/#642 silent-miscompile class. + + CI gate: `scripts/repro/i64_float_conv_869_differential.py` — bit-exact vs + wasmtime under unicorn on every boundary row **with the trap rows executed + on both sides** (NaN, ±inf, 2^63, −2^63, 2^64, the largest-below-bound + f32/f64 values), the double-rounding killer patterns, and ≥10k fixed-seed + random patterns per direction (96k checks). Frozen fixtures 10/10 + byte-identical (byte-changing only for modules using these ops). + - **ISA-model adequacy (#867): "proved against a simplified model" is now an explicit, counted, CI-pinned trusted-base entry.** #682's shape — a green Qed while shipped code silently miscompiled, because the SIMPLIFIED @@ -50,6 +81,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 model (differential suites exercise compiler OUTPUT); the artifact records that explicitly instead of implying test coverage. +### Fixed + +- **Single-precision targets (m4f/m7) now loud-decline the whole #869 family + by name at the selector preamble** (listed in the f64 capability scope): + every member's lowering runs on double-precision machinery, and the + pre-existing `i64.trunc_sat_f32_{s,u}` promote-to-f64 path previously slid + past the capability gate to be caught only later at ISA validation. Same + honest-skip outcome, one gate earlier and named. + ## [0.51.0] - 2026-07-23 **"aarch64 runs real WASM modules."** The `-b aarch64` host-native backend crosses diff --git a/claims.yaml b/claims.yaml index 315e2462..581e09ea 100644 --- a/claims.yaml +++ b/claims.yaml @@ -430,8 +430,10 @@ claims: # in-progress, not implemented. LIVE (derived-ARM-trap-term) classes now: # i32 div/rem, i64 div/rem (#756, field-derived), unreachable, i32 # load/store (all widths), call_indirect, i32.trunc_f32_s/u, i32.trunc_f64_s/u - # (#756, D-register guard). i64.trunc_f64 has no shipped lowering (selector - # declines it) — its classifier is unit-gated only. + # (#756, D-register guard). i64.trunc_f32/f64 SHIP a guarded lowering since + # #869, but their symbolic ARM-side wiring (F64 compare/decompose chain) is + # the named residual — classifier unit-gated + EXECUTION-gated (the #869 + # differential runs every trap row under unicorn), not yet derived-term VC. # Phase B (ordeal 0.9.1, ordeal#59/TR-020): float→int trunc trap class # covered — trunc_op/trap_trunc wrapper + #709 boundary-table eval gate. - id: SYNTH-VCR-VER-002-STATUS 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 e9945b9e..4833a31e 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -525,7 +525,12 @@ fn classify(op: &WasmOp) -> ParityClass { | I32TruncSatF32S | I32TruncSatF32U | I64TruncSatF32S - | I64TruncSatF32U => StructurallyExcluded(FLOAT), + | I64TruncSatF32U + // #869: the f32-source i64-target TRAPPING truncations (ARM32 m7dp + // lowers them via the i64 domain guard + #782 decompose; RV32 has no + // floats — target-parameterized like the rest of the float surface). + | I64TruncF32S + | I64TruncF32U => StructurallyExcluded(FLOAT), // ─── f64 (StructurallyExcluded — target-parameterized) ─────────── F64Add | F64Sub @@ -648,7 +653,7 @@ fn all_wasm_op_representatives() -> Vec { F32Load { offset: 0, align: 2 }, F32Store { offset: 0, align: 2 }, F32ConvertI32S, F32ConvertI32U, F32ConvertI64S, F32ConvertI64U, F32DemoteF64, F32ReinterpretI32, I32ReinterpretF32, I32TruncF32S, I32TruncF32U, I32TruncSatF32S, - I32TruncSatF32U, I64TruncSatF32S, I64TruncSatF32U, + I32TruncSatF32U, I64TruncSatF32S, I64TruncSatF32U, I64TruncF32S, I64TruncF32U, // f64 F64Add, F64Sub, F64Mul, F64Div, F64Eq, F64Ne, F64Lt, F64Le, F64Gt, F64Ge, F64Abs, F64Neg, F64Ceil, F64Floor, F64Trunc, F64Nearest, F64Sqrt, F64Min, F64Max, diff --git a/crates/synth-core/src/wasm_decoder.rs b/crates/synth-core/src/wasm_decoder.rs index 1c408ea5..34429fd3 100644 --- a/crates/synth-core/src/wasm_decoder.rs +++ b/crates/synth-core/src/wasm_decoder.rs @@ -2258,6 +2258,21 @@ fn convert_operator(op: &wasmparser::Operator) -> Option { F32ConvertI32U => Some(WasmOp::F32ConvertI32U), I32TruncF32S => Some(WasmOp::I32TruncF32S), I32TruncF32U => Some(WasmOp::I32TruncF32U), + // #869: the 64-bit integer<->float conversion family — previously all + // dropped here (`_ => None`), which loud-skipped every function using + // them (3 of 5 falcon cascade stages at their public entry points). + // ARMv7E-M VFP has no 64-bit-integer<->float instruction (VCVT on + // FPv4-SP/FPv5-D16 encodes only S32/U32 <-> F32/F64), so the ARM32 + // lowering is a self-contained multi-step expansion on cortex-m7dp + // (see `try_lower_f32`/`try_lower_f64`); the TRAPPING trunc forms + // carry the #709-class i64 domain guard (WASM §4.3.3 requires a trap + // on NaN/out-of-range — the saturating decompose alone would be a + // silent miscompile). Backends without the machinery (RV32, aarch64's + // current subset, single-precision ARM) still loud-decline downstream. + F32ConvertI64S => Some(WasmOp::F32ConvertI64S), + F32ConvertI64U => Some(WasmOp::F32ConvertI64U), + I64TruncF32S => Some(WasmOp::I64TruncF32S), + I64TruncF32U => Some(WasmOp::I64TruncF32U), // #782a: the nontrapping trunc_sat family (0xFC-prefixed, // saturating-float-to-int proposal) — TOTAL ops (§4.3.2: NaN → 0, // out-of-range saturates to INT_MIN/INT_MAX, no traps). Un-dropped so @@ -2309,8 +2324,8 @@ fn convert_operator(op: &wasmparser::Operator) -> Option { // splice, f32.demote_f64 / i32<->f64 conversions via VCVT // (i32.trunc_f64_* carries the #709 trap-on-out-of-range domain // guard). Still m7dp-only (the selector preamble honest-rejects any - // f64 op elsewhere). Remaining dropped f64 surface: the i64<->f64 - // conversions and reinterprets (need lowered i64 pair plumbing). + // f64 op elsewhere). The i64<->f64 reinterprets were un-dropped by + // #851 and the i64<->f64 conversions by #869 (below). F64Ceil => Some(WasmOp::F64Ceil), F64Floor => Some(WasmOp::F64Floor), F64Trunc => Some(WasmOp::F64Trunc), @@ -2323,6 +2338,14 @@ fn convert_operator(op: &wasmparser::Operator) -> Option { F64ConvertI32U => Some(WasmOp::F64ConvertI32U), I32TruncF64S => Some(WasmOp::I32TruncF64S), I32TruncF64U => Some(WasmOp::I32TruncF64U), + // #869 (+#756): the f64 half of the 64-bit integer<->float family — + // i64->f64 exact two-word VCVT+scale+add, i64.trunc_f64_* via the + // #709-class i64 domain guard + the #782 word-decompose. See the f32 + // group above for the family story. + F64ConvertI64S => Some(WasmOp::F64ConvertI64S), + F64ConvertI64U => Some(WasmOp::F64ConvertI64U), + I64TruncF64S => Some(WasmOp::I64TruncF64S), + I64TruncF64U => Some(WasmOp::I64TruncF64U), // #782a: f64-source trunc_sat twins (see the f32 group above). falcon // v1.123 carries 7× i32.trunc_sat_f64_s — the m7dp double-precision // VCVT twins lower the i32-target forms; i64 targets loud-decline. @@ -3011,11 +3034,12 @@ mod tests { // is no longer flagged — and since phase 2 (#369) so is the lowered // f64 subset (`f64.add` here; the m7dp-only capability gate lives in // the selector). Since phase 3 the f64 op TAIL (`f64.min` here) is - // decoded too; an out-of-scope scalar float op (`i64.trunc_f64_s` — - // the i64<->f64 conversions need lowered pair plumbing) is STILL - // flagged (loud-skip), never silently dropped — the #369 honesty - // contract holds for the not-yet-lowered surface. A pure-integer - // function stays clean. + // decoded too; and since #869 the 64-bit integer<->float conversion + // family (`i64.trunc_f64_s` here) decodes as well — the scalar float + // decode surface is complete, with capability gating (m7dp-only) + // living in the selector. The flag-never-drop honesty contract for + // the remaining undecoded float surface is pinned by the + // float-global test below. A pure-integer function stays clean. let wat = r#" (module (func (export "fadd") (param f32 f32) (result f32) @@ -3084,12 +3108,18 @@ mod tests { "f64.min must decode to WasmOp::F64Min: {:?}", dmin.ops ); - // Out-of-scope scalar double op: still flagged, never dropped. + // #869: the i64<->f64 conversions are now IN scope — decoded, not + // flagged (the m7dp capability gate lives in the selector preamble). assert!( - dtrunc64.unsupported.is_some(), - "i64.trunc_f64_s must still flag the function unsupported (out of scope), got {:?}", + dtrunc64.unsupported.is_none(), + "#869: i64.trunc_f64_s must now decode (not be flagged), got {:?}", dtrunc64.unsupported ); + assert!( + dtrunc64.ops.contains(&WasmOp::I64TruncF64S), + "i64.trunc_f64_s must decode to WasmOp::I64TruncF64S: {:?}", + dtrunc64.ops + ); assert!( iadd.unsupported.is_none(), "a pure-integer function must NOT be flagged: {:?}", diff --git a/crates/synth-core/src/wasm_op.rs b/crates/synth-core/src/wasm_op.rs index 56acc9c6..c8a3eadd 100644 --- a/crates/synth-core/src/wasm_op.rs +++ b/crates/synth-core/src/wasm_op.rs @@ -365,6 +365,11 @@ pub enum WasmOp { I64TruncF64U, // Truncate f64 to unsigned i64 I32TruncF64S, // Truncate f64 to signed i32 I32TruncF64U, // Truncate f64 to unsigned i32 + // #869: the f32-source i64-target TRAPPING truncations — the only two + // members of the 64-bit integer<->float conversion family that had no + // WasmOp variant at all (the rest existed but were dropped at decode). + I64TruncF32S, // Truncate f32 to signed i64 (traps on NaN/out-of-range) + I64TruncF32U, // Truncate f32 to unsigned i64 (traps on NaN/out-of-range) // Nontrapping f64→int (saturating-float-to-int, §4.3.2 trunc_sat — see // the f32 group above for the semantics). diff --git a/crates/synth-core/src/wasm_stack_check.rs b/crates/synth-core/src/wasm_stack_check.rs index 22362570..b8371863 100644 --- a/crates/synth-core/src/wasm_stack_check.rs +++ b/crates/synth-core/src/wasm_stack_check.rs @@ -163,8 +163,9 @@ fn stack_effect_or_bail(op: &WasmOp) -> StackEffect { | F32ReinterpretI32 | I32ReinterpretF32 | I32TruncF32S | I32TruncF32U | F64ConvertI32S | F64ConvertI32U | F64ConvertI64S | F64ConvertI64U | F64PromoteF32 | F64ReinterpretI64 | I64ReinterpretF64 | I64TruncF64S | I64TruncF64U | I32TruncF64S | I32TruncF64U - | I32TruncSatF32S | I32TruncSatF32U | I32TruncSatF64S | I32TruncSatF64U - | I64TruncSatF32S | I64TruncSatF32U | I64TruncSatF64S | I64TruncSatF64U => modeled(1, 1), + | I64TruncF32S | I64TruncF32U | I32TruncSatF32S | I32TruncSatF32U | I32TruncSatF64S + | I32TruncSatF64U | I64TruncSatF32S | I64TruncSatF32U | I64TruncSatF64S + | I64TruncSatF64U => modeled(1, 1), // ---- pop-only ---------------------------------------------------- LocalSet(_) | GlobalSet(_) | Drop => modeled(1, 0), diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 206f47c4..bb02a173 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -2019,9 +2019,10 @@ fn wasm_stack_effect(op: &WasmOp) -> (usize, usize) { F32ConvertI32S | F32ConvertI32U | F32ConvertI64S | F32ConvertI64U | F32DemoteF64 | F64ConvertI32S | F64ConvertI32U | F64ConvertI64S | F64ConvertI64U | F64PromoteF32 | I32TruncF32S | I32TruncF32U | I32TruncF64S | I32TruncF64U | I64TruncF64S - | I64TruncF64U | I32TruncSatF32S | I32TruncSatF32U | I32TruncSatF64S | I32TruncSatF64U - | I64TruncSatF32S | I64TruncSatF32U | I64TruncSatF64S | I64TruncSatF64U - | F32ReinterpretI32 | I32ReinterpretF32 | F64ReinterpretI64 | I64ReinterpretF64 => (1, 1), + | I64TruncF64U | I64TruncF32S | I64TruncF32U | I32TruncSatF32S | I32TruncSatF32U + | I32TruncSatF64S | I32TruncSatF64U | I64TruncSatF32S | I64TruncSatF32U + | I64TruncSatF64S | I64TruncSatF64U | F32ReinterpretI32 | I32ReinterpretF32 + | F64ReinterpretI64 | I64ReinterpretF64 => (1, 1), // Constants: push 1 I32Const(_) | I64Const(_) | F32Const(_) | F64Const(_) => (0, 1), @@ -2309,6 +2310,16 @@ fn is_scope_f32_op(op: &WasmOp) -> bool { | I32TruncSatF32U | I64TruncSatF32S | I64TruncSatF32U + // #869: the f32 half of the 64-bit integer<->float family — the + // TRAPPING i64<-f32 truncations (i64 domain guard + promote + + // #782 decompose) and the i64->f32 converts (exact two-word f64 + // build + round-to-odd fixup + demote). All four also appear in + // `is_scope_f64_op` — their lowerings run on f64 machinery, so + // the DP capability gate must fire for them. + | I64TruncF32S + | I64TruncF32U + | F32ConvertI64S + | F32ConvertI64U // #708 (phase 1b): un-dropped f32 memory-load + f32<->i32 bitcasts. // `F32Load` itself is lowered in the main `select_with_stack` match // (it needs `self`'s bounds/base-rewrite machinery); listing it here @@ -2730,6 +2741,65 @@ fn try_lower_f32( reserved, ) } + op @ (I64TruncF32S | I64TruncF32U) => { + // #869: the TRAPPING `i64.trunc_f32_{s,u}` — promote to f64 + // (EXACT: sign/NaN/±inf preserved), run the #709-class i64 domain + // guard (§4.3.3: TRAP on NaN/out-of-range — the bounds are exact + // on the promoted value, see `emit_i64_trunc_f64_domain_guard`), + // then the #782 word-decompose, which for a guarded in-range + // operand computes the exact truncation (it can no longer + // saturate). DP-only like every f64-machinery op (preamble gate). + let signed = matches!(op, I64TruncF32S); + let sm = pop_float(stack)?; + let dd = alloc_vfp_dtemp(vfp_used)?; + instructions.push(ArmInstruction { + op: ArmOp::F64PromoteF32 { dd, sm }, + source_line: Some(idx), + }); + free_vfp_temp(vfp_used, vfp_home, sm); + emit_i64_trunc_f64_domain_guard( + dd, + signed, + idx, + vfp_used, + vfp_home, + stack, + next_temp, + spill, + instructions, + reserved, + )?; + lower_i64_trunc_sat_from_f64( + dd, + signed, + idx, + vfp_used, + vfp_home, + stack, + next_temp, + spill, + instructions, + reserved, + ) + } + op @ (F32ConvertI64S | F32ConvertI64U) => { + // #869: `f32.convert_i64_{s,u}` — exact two-word f64 build + + // round-to-odd fixup + single demote rounding (see + // `lower_f32_convert_i64` for why the naive promote-then-demote + // double-rounds). DP-only (preamble gate). + let signed = matches!(op, F32ConvertI64S); + lower_f32_convert_i64( + signed, + idx, + vfp_used, + vfp_home, + stack, + next_temp, + spill, + instructions, + reserved, + ) + } F32ReinterpretI32 => { // #708: i32 bits → f32 (VMOV Sd, Rm). Pure bit-cast, no conversion. let rm = pop_operand(stack, next_temp, instructions, spill, reserved, idx)?; @@ -2888,6 +2958,25 @@ fn is_scope_f64_op(op: &WasmOp) -> bool { | I32TruncSatF64U | I64TruncSatF64S | I64TruncSatF64U + // #869 (+#756): the 64-bit integer<->float conversion family. + // The f64-source/-target members are f64 ops outright; the + // f32-source/-target members (and the pre-existing f32-source + // i64-target trunc_sat pair, whose promote-to-f64 lowering + // predates this entry) are listed here because their lowerings + // run on DOUBLE-precision machinery (F64PromoteF32 / the #782 + // word-decompose / the exact two-word f64 build) — a + // single-precision target (m4f/m7) must loud-decline them via + // the preamble DP gate, never emit undefined VCVT.F64 encodings. + | F64ConvertI64S + | F64ConvertI64U + | I64TruncF64S + | I64TruncF64U + | F32ConvertI64S + | F32ConvertI64U + | I64TruncF32S + | I64TruncF32U + | I64TruncSatF32S + | I64TruncSatF32U ) } @@ -3294,6 +3383,476 @@ fn blend_word( Ok(()) } +/// #869 (SOUNDNESS): the i64-target domain guard for the TRAPPING +/// `i64.trunc_f32_{s,u}` / `i64.trunc_f64_{s,u}` — the 64-bit twin of the +/// #709 f32 guard and the #369 `i32.trunc_f64_*` guard. WASM §4.3.3 requires +/// a TRAP on NaN or an out-of-i64-range operand; the #782 word-decompose this +/// guard precedes SATURATES instead (NaN → 0), so running it bare would be a +/// silent miscompile (the #633/#666/#709/#665/#642 "ARM more-total-than-WASM" +/// class). Emitting the guard first makes the decompose provably exact. +/// +/// Valid domain, checked on the (exactly promoted) f64 operand — every bound +/// exactly representable in f64, and for the f32-source twins the SAME bounds +/// are exact after the lossless `VCVT.F64.F32` promote: +/// trunc_*_s: -2^63 <= x < 2^63 (inclusive lower: -2^63 is a valid input +/// truncating to INT64_MIN, and no f32/f64 value exists strictly +/// between -2^63-1 and -2^63, so `>=` captures the exact set) +/// trunc_*_u: -1.0 < x < 2^64 (strict lower: (-1,0) truncates to 0) +/// All compares are ORDERED (false on NaN), so a NaN fails the first guard +/// and falls to the UDF — same idiom as every existing trunc guard +/// (`F64 compare; CMP #0; B.NE +0 skip; UDF`). +#[allow(clippy::too_many_arguments)] +fn emit_i64_trunc_f64_domain_guard( + work: VfpReg, + signed: bool, + idx: usize, + vfp_used: &mut [bool; 16], + vfp_home: &[bool; 16], + stack: &mut Vec, + next_temp: &mut u8, + spill: &mut SpillState, + instructions: &mut Vec, + reserved: &[Reg], +) -> Result<()> { + // 2^63 / -2^63 / 2^64 / -1.0 as exact f64 bit patterns. + const POW2_63: u64 = 0x43E0_0000_0000_0000; + const NEG_POW2_63: u64 = 0xC3E0_0000_0000_0000; + const POW2_64: u64 = 0x43F0_0000_0000_0000; + const NEG_ONE: u64 = 0xBFF0_0000_0000_0000; + let (hi, lo) = if signed { + (POW2_63, NEG_POW2_63) + } else { + (POW2_64, NEG_ONE) + }; + let rd = alloc_temp_or_spill(next_temp, stack, instructions, spill, reserved, idx)?; + let mut emit_guard = |bound: u64, upper: bool| -> Result<()> { + let d_bound = materialize_f64_const( + bound, + idx, + vfp_used, + stack, + next_temp, + spill, + instructions, + reserved, + )?; + // Upper: x < hi (F64Lt). Lower: x >= -2^63 (F64Ge, signed) or + // x > -1.0 (F64Gt, unsigned). All yield rd=0 on NaN. + let cmp = if upper { + ArmOp::F64Lt { + rd, + dn: work, + dm: d_bound, + } + } else if signed { + ArmOp::F64Ge { + rd, + dn: work, + dm: d_bound, + } + } else { + ArmOp::F64Gt { + rd, + dn: work, + dm: d_bound, + } + }; + instructions.push(ArmInstruction { + op: cmp, + source_line: Some(idx), + }); + instructions.push(ArmInstruction { + op: ArmOp::Cmp { + rn: rd, + op2: Operand2::Imm(0), + }, + source_line: Some(idx), + }); + // Skip the UDF when in-range (rd != 0); else fall through to trap. + instructions.push(ArmInstruction { + op: ArmOp::BCondOffset { + cond: Condition::NE, + offset: 0, + }, + source_line: Some(idx), + }); + instructions.push(ArmInstruction { + op: ArmOp::Udf { imm: 0 }, + source_line: Some(idx), + }); + free_vfp_dtemp(vfp_used, vfp_home, d_bound); + Ok(()) + }; + emit_guard(hi, true)?; // upper: x < hi (also traps NaN) + emit_guard(lo, false)?; // lower: x >= -2^63 (s) / x > -1.0 (u) + Ok(()) +} + +/// #869: build the CORRECTLY-ROUNDED f64 value of an i64 register pair — +/// the `f64.convert_i64_{s,u}` lowering, and (with `want_residual`) the +/// double-rounding-safe front half of `f32.convert_i64_{s,u}`. ARMv7 VFP has +/// no 64-bit-integer VCVT, so the value is assembled from two exact 32-bit +/// conversions: +/// +/// ```text +/// a = (f64)(hi as u32/s32) * 2^32 ; both steps EXACT (32-bit value into +/// ; 53-bit mantissa; power-of-two scale) +/// b = (f64)(lo as u32) ; EXACT +/// s = a + b ; IEEE add = ONE correct RNE rounding +/// ; of the exact sum hi*2^32 + lo +/// ``` +/// +/// For an f64 target `s` IS the answer. For an f32 target, demoting `s` +/// would DOUBLE-ROUND (64 -> 53 RNE -> 24 RNE loses the sticky information; +/// e.g. u64 0x8000_0080_0000_0001 must round UP to 2^63+2^40 in f32 but the +/// f64 intermediate erases the `..0001`). So the caller also needs the EXACT +/// residual `t = (hi:lo) - s`, computed error-free by Fast2Sum — valid +/// because `a` is a multiple of 2^32 with `|a| >= 2^32 > |b|` whenever +/// `hi != 0`, and when `hi == 0` the add was exact so `t` computes to +0: +/// +/// ```text +/// z = s - a ; exact (Sterbenz/Fast2Sum step) +/// t = b - z ; exact residual, == 0 iff s is exact +/// ``` +/// +/// Returns `(s, Some(t))` with both D-temps live (caller frees), or +/// `(s, None)` without the residual computation. +#[allow(clippy::too_many_arguments)] +fn lower_f64_from_i64_pair( + lo: Reg, + hi: Reg, + signed: bool, + want_residual: bool, + idx: usize, + vfp_used: &mut [bool; 16], + vfp_home: &mut [bool; 16], + stack: &mut Vec, + next_temp: &mut u8, + spill: &mut SpillState, + instructions: &mut Vec, + reserved: &[Reg], +) -> Result<(VfpReg, Option)> { + const POW2_32: u64 = 0x41F0_0000_0000_0000; // 2^32, exact + // b = (f64)(u32)lo — exact. Convert BOTH words before any core-temp + // allocation (materialize_f64_const grabs two core scratches, which must + // not collide with a just-popped pair). + let d_b = alloc_vfp_dtemp(vfp_used)?; + instructions.push(ArmInstruction { + op: ArmOp::F64ConvertI32U { dd: d_b, rm: lo }, + source_line: Some(idx), + }); + // a = (f64)(hi as s32/u32) — exact; sign of the whole i64 lives here. + let d_a = alloc_vfp_dtemp(vfp_used)?; + let cvt_hi = if signed { + ArmOp::F64ConvertI32S { dd: d_a, rm: hi } + } else { + ArmOp::F64ConvertI32U { dd: d_a, rm: hi } + }; + instructions.push(ArmInstruction { + op: cvt_hi, + source_line: Some(idx), + }); + // a *= 2^32 — exact power-of-two scale. + let d_scale = materialize_f64_const( + POW2_32, + idx, + vfp_used, + stack, + next_temp, + spill, + instructions, + reserved, + )?; + instructions.push(ArmInstruction { + op: ArmOp::F64Mul { + dd: d_a, + dn: d_a, + dm: d_scale, + }, + source_line: Some(idx), + }); + free_vfp_dtemp(vfp_used, vfp_home, d_scale); + // s = a + b — the single correct rounding. + let d_s = alloc_vfp_dtemp(vfp_used)?; + instructions.push(ArmInstruction { + op: ArmOp::F64Add { + dd: d_s, + dn: d_a, + dm: d_b, + }, + source_line: Some(idx), + }); + if !want_residual { + free_vfp_dtemp(vfp_used, vfp_home, d_a); + free_vfp_dtemp(vfp_used, vfp_home, d_b); + return Ok((d_s, None)); + } + // Fast2Sum: z = s - a (exact); t = b - z (exact residual). + let d_z = alloc_vfp_dtemp(vfp_used)?; + instructions.push(ArmInstruction { + op: ArmOp::F64Sub { + dd: d_z, + dn: d_s, + dm: d_a, + }, + source_line: Some(idx), + }); + free_vfp_dtemp(vfp_used, vfp_home, d_a); + instructions.push(ArmInstruction { + op: ArmOp::F64Sub { + dd: d_z, + dn: d_b, + dm: d_z, + }, + source_line: Some(idx), + }); + free_vfp_dtemp(vfp_used, vfp_home, d_b); + Ok((d_s, Some(d_z))) +} + +/// #869: lower `f32.convert_i64_{s,u}` — pop the i64 pair, build the exact +/// f64 sum + residual ([`lower_f64_from_i64_pair`]), force the 53-bit +/// intermediate to ROUND-TO-ODD with a branch-free integer fixup, then demote. +/// Round-to-odd with >= 2 guard bits (53 >= 24+2) makes the double rounding +/// exact (Boldo–Melquiond): `RN_24(RO_53(x)) == RN_24(x)` for every real x, +/// so the emitted f32 is the correctly-rounded conversion WASM §4.3.3 +/// requires. The fixup: +/// +/// ```text +/// inexact = (t != 0) ; t is the EXACT residual, +0 iff exact +/// if inexact && LSB(s) == 0: ; s must become its ODD neighbor +/// s(bits) += sign(t)==sign(s) ? +1 : -1 +/// ; IEEE bit patterns are monotone in +/// ; magnitude: ±1 on the 64-bit pattern +/// ; IS nextafter toward/away from zero, +/// ; correct across binade boundaries, +/// ; and always flips mantissa parity +/// ``` +/// realised branch-free over the register pairs (adj ∈ {0,1}, d = sign-diff +/// mask ∈ {0,-1}, delta = (adj ^ d) - d ∈ {-1,0,+1}). `s` can never be ±0 +/// when inexact (|s| > 2^31), and never overflows to ±inf (|s| <= 2^64). +#[allow(clippy::too_many_arguments)] +fn lower_f32_convert_i64( + signed: bool, + idx: usize, + vfp_used: &mut [bool; 16], + vfp_home: &mut [bool; 16], + stack: &mut Vec, + next_temp: &mut u8, + spill: &mut SpillState, + instructions: &mut Vec, + reserved: &[Reg], +) -> Result { + // Pop the i64 operand (reloads a spilled pair; `lo` names the pair). + let lo = pop_operand(stack, next_temp, instructions, spill, reserved, idx)?; + let hi = i64_pair_hi(lo)?; + let (d_s, d_t) = lower_f64_from_i64_pair( + lo, + hi, + signed, + true, + idx, + vfp_used, + vfp_home, + stack, + next_temp, + spill, + instructions, + reserved, + )?; + let d_t = d_t.expect("want_residual returns Some"); + // Five core scratches, kept mutually distinct via the reserved list + // (grown as each is handed out — the alloc_temp discipline used by the + // #782 decompose). + let mut resv: Vec = reserved.to_vec(); + let grab = |resv: &mut Vec, + stack: &mut Vec, + next_temp: &mut u8, + instructions: &mut Vec, + spill: &mut SpillState| + -> Result { + let r = alloc_temp_or_spill(next_temp, stack, instructions, spill, resv, idx)?; + resv.push(r); + Ok(r) + }; + let slo = grab(&mut resv, stack, next_temp, instructions, spill)?; + let shi = grab(&mut resv, stack, next_temp, instructions, spill)?; + let tlo = grab(&mut resv, stack, next_temp, instructions, spill)?; + let thi = grab(&mut resv, stack, next_temp, instructions, spill)?; + let tmp = grab(&mut resv, stack, next_temp, instructions, spill)?; + let emit = |op: ArmOp, instructions: &mut Vec| { + instructions.push(ArmInstruction { + op, + source_line: Some(idx), + }); + }; + emit( + ArmOp::I64ReinterpretF64 { + rdlo: slo, + rdhi: shi, + dm: d_s, + }, + instructions, + ); + emit( + ArmOp::I64ReinterpretF64 { + rdlo: tlo, + rdhi: thi, + dm: d_t, + }, + instructions, + ); + free_vfp_dtemp(vfp_used, vfp_home, d_t); + // Combined zero test over BOTH of t's words FIRST (the residual is often + // a power of two whose LOW word is all-zero, so testing tlo alone would + // miss real inexactness — the fatal under-round). Fast2Sum's residual of + // an exact sum is +0 under RNE (never -0), so all-zero-bits iff exact. + emit( + ArmOp::Orr { + rd: tmp, + rn: tlo, + op2: Operand2::Reg(thi), + }, + instructions, + ); + // d = ASR(shi ^ thi, 31) ∈ {0,-1}: 0 when sign(s) == sign(t) (odd + // neighbor lies away from zero: bits+1), -1 when they differ (toward + // zero: bits-1). Reads the ORIGINAL thi (the Orr above only wrote tmp). + emit( + ArmOp::Eor { + rd: thi, + rn: shi, + op2: Operand2::Reg(thi), + }, + instructions, + ); + emit( + ArmOp::Asr { + rd: thi, + rn: thi, + shift: 31, + }, + instructions, + ); + // inexact = (tmp | -tmp) >> 31 ∈ {0,1} (t's words are dead; reuse tlo). + emit( + ArmOp::Rsb { + rd: tlo, + rn: tmp, + imm: 0, + }, + instructions, + ); + emit( + ArmOp::Orr { + rd: tlo, + rn: tlo, + op2: Operand2::Reg(tmp), + }, + instructions, + ); + emit( + ArmOp::Lsr { + rd: tlo, + rn: tlo, + shift: 31, + }, + instructions, + ); + // adj = inexact & ~LSB(s) & 1 — flip to the odd neighbor only when the + // sum was inexact AND s's mantissa LSB is even (an odd s already IS the + // round-to-odd result). + emit( + ArmOp::Mvn { + rd: tmp, + op2: Operand2::Reg(slo), + }, + instructions, + ); + emit( + ArmOp::And { + rd: tmp, + rn: tmp, + op2: Operand2::Reg(tlo), + }, + instructions, + ); + emit( + ArmOp::And { + rd: tmp, + rn: tmp, + op2: Operand2::Imm(1), + }, + instructions, + ); + // delta = (adj ^ d) - d ∈ {-1, 0, +1}; sign-extend into a pair and add. + emit( + ArmOp::Eor { + rd: tmp, + rn: tmp, + op2: Operand2::Reg(thi), + }, + instructions, + ); + emit( + ArmOp::Sub { + rd: tmp, + rn: tmp, + op2: Operand2::Reg(thi), + }, + instructions, + ); + emit( + ArmOp::Asr { + rd: tlo, + rn: tmp, + shift: 31, + }, + instructions, + ); + // 64-bit `s += delta` as MODELED Adds/Adc — deliberately NOT the + // `ArmOp::I64Add` pseudo-op (same bytes): `reg_effect` returns None for + // the i64-pair family, which makes it a range-realloc SEGMENT BARRIER + // whose reads of slo/shi are INVISIBLE to the segment-local liveness — + // the colorer then reuses slo/shi for intermediates after their last + // in-segment use and the pair reaching the final VMOV is garbage (caught + // by the #869 differential at land time; the segment validator shares + // the same last-use assumption, so it accepted the wrong rewrite). With + // Adds/Adc the uses sit INSIDE the segment at its end: the live-in + // ranges of slo/shi span the whole segment and the defs are the pinned + // exit ranges — sound under reallocation by construction. + emit( + ArmOp::Adds { + rd: slo, + rn: slo, + op2: Operand2::Reg(tmp), + }, + instructions, + ); + emit( + ArmOp::Adc { + rd: shi, + rn: shi, + op2: Operand2::Reg(tlo), + }, + instructions, + ); + // Back to the FP file: s' (round-to-odd) then the single 24-bit rounding. + emit( + ArmOp::F64ReinterpretI64 { + dd: d_s, + rmlo: slo, + rmhi: shi, + }, + instructions, + ); + let sd = alloc_vfp_temp(vfp_used)?; + emit(ArmOp::F32DemoteF64 { sd, dm: d_s }, instructions); + free_vfp_dtemp(vfp_used, vfp_home, d_s); + stack.push(StackVal::Float { sreg: sd }); + Ok(true) +} + /// Lower an in-scope scalar f64 op onto the caller-saved D-register file. /// Returns `Ok(true)` when handled, `Ok(false)` when `op` is not an f64 op /// (fall through), `Err` on an honest decline. Gated by the caller on @@ -3788,6 +4347,84 @@ fn try_lower_f64( reserved, ) } + op @ (I64TruncF64S | I64TruncF64U) => { + // #869 (+#756): the TRAPPING `i64.trunc_f64_{s,u}` — the #709-class + // i64 domain guard (§4.3.3: TRAP on NaN/out-of-range) followed by + // the #782 word-decompose, which for a guarded in-range operand + // computes the exact truncation (it provably never saturates). + let signed = matches!(op, I64TruncF64S); + let dm = pop_double(stack)?; + // The decompose consumes its operand (frees it internally, and the + // signed path VABSes through it). A pinned param/local HOME must + // survive — hand it a fresh copy (same hazard as the sat twin). + let dm_is_home = vfp_d_index(dm).is_some_and(|d| vfp_home[2 * d]); + let work = if dm_is_home { + let copy = alloc_vfp_dtemp(vfp_used)?; + emit_d_copy( + copy, + dm, + idx, + stack, + next_temp, + spill, + instructions, + reserved, + )?; + copy + } else { + dm + }; + emit_i64_trunc_f64_domain_guard( + work, + signed, + idx, + vfp_used, + vfp_home, + stack, + next_temp, + spill, + instructions, + reserved, + )?; + lower_i64_trunc_sat_from_f64( + work, + signed, + idx, + vfp_used, + vfp_home, + stack, + next_temp, + spill, + instructions, + reserved, + ) + } + op @ (F64ConvertI64S | F64ConvertI64U) => { + // #869: `f64.convert_i64_{s,u}` — the exact two-word build: + // (f64)(hi as s32/u32) * 2^32 + (f64)(u32)lo. Every step but the + // final VADD is exact, and IEEE VADD delivers the one correct + // round-to-nearest-even of the exact sum — bit-identical to a + // native 64-bit conversion (§4.3.3). + let signed = matches!(op, F64ConvertI64S); + let lo = pop_operand(stack, next_temp, instructions, spill, reserved, idx)?; + let hi = i64_pair_hi(lo)?; + let (dd, _) = lower_f64_from_i64_pair( + lo, + hi, + signed, + false, + idx, + vfp_used, + vfp_home, + stack, + next_temp, + spill, + instructions, + reserved, + )?; + stack.push(StackVal::Double { dreg: dd }); + Ok(true) + } _ => Ok(false), } } @@ -6530,6 +7167,16 @@ impl InstructionSelector { shipping select_with_stack selector lowers it (#782)" ))); } + // #869: same selector asymmetry for the TRAPPING f32->i64 + // truncations — `select_with_stack` lowers them (i64 domain guard + // + promote + #782 decompose); this register-blind fallback + // loud-declines (decline > wrong). + op @ (I64TruncF32S | I64TruncF32U) if self.fpu.is_some() => { + return Err(synth_core::Error::synthesis(format!( + "{op:?}: select_default has no i64 register-pair path — the \ + shipping select_with_stack selector lowers it (#869)" + ))); + } // F32 rounding pseudo-ops — emit ArmOp variants, encoder expands to // multi-instruction sequences using FPSCR rounding-mode manipulation @@ -6578,9 +7225,13 @@ impl InstructionSelector { vec![ArmOp::F32Copysign { sd, sn, sm }] } + // #869: lowered by the shipping `select_with_stack` (exact + // two-word f64 build + round-to-odd fixup + demote); this + // register-blind fallback keeps the honest decline. op @ (F32ConvertI64S | F32ConvertI64U) if self.fpu.is_some() => { return Err(synth_core::Error::synthesis(format!( - "{op:?} not supported (requires i64 register pairs on 32-bit ARM)" + "{op:?}: select_default has no i64 register-pair path — the \ + shipping select_with_stack selector lowers it (#869)" ))); } @@ -6627,7 +7278,9 @@ impl InstructionSelector { | I32TruncSatF32S | I32TruncSatF32U | I64TruncSatF32S - | I64TruncSatF32U) => { + | I64TruncSatF32U + | I64TruncF32S + | I64TruncF32U) => { return Err(synth_core::Error::synthesis(format!( "target {} has no FPU; cannot compile {op:?}", self.target_name @@ -6832,20 +7485,22 @@ impl InstructionSelector { vec![ArmOp::F64Copysign { dd, dn, dm }] } - // F64 i64 conversions: VCVT.{F64,S32}.{S32,F64} with i64 register - // pairs is not implemented in this register-blind `select_default` - // fallback. Surface a typed error. NOTE (#782): the two - // `I64TruncSatF64*` forms ARE lowered on the shipping - // `select_with_stack` path (v0.49 finale); they decline here only - // because select_default lacks the pair machinery, and a normal - // compile never routes them through this arm. The trapping - // `I64TruncF64*` and `F64ConvertI64*` remain genuinely unimplemented. + // F64 i64 conversions: i64 register pairs are not implemented in + // this register-blind `select_default` fallback. Surface a typed + // error. NOTE (#782/#869): ALL of these forms ARE lowered on the + // shipping `select_with_stack` path (trunc_sat via the v0.49 + // word-decompose; the trapping `I64TruncF64*` via the i64 domain + // guard + decompose and `F64ConvertI64*` via the exact two-word + // build, both #869). They decline here only because + // select_default lacks the pair machinery, and a normal compile + // never routes them through this arm. op @ (F64ConvertI64S | F64ConvertI64U | I64TruncF64S | I64TruncF64U | I64TruncSatF64S | I64TruncSatF64U) if self.has_double_fpu() => { return Err(synth_core::Error::synthesis(format!( - "{op:?} not supported (requires i64 register pairs on 32-bit ARM)" + "{op:?}: select_default has no i64 register-pair path — the \ + shipping select_with_stack selector lowers it (#869)" ))); } diff --git a/crates/synth-synthesis/src/optimizer_bridge.rs b/crates/synth-synthesis/src/optimizer_bridge.rs index b082ba3b..d0bbad14 100644 --- a/crates/synth-synthesis/src/optimizer_bridge.rs +++ b/crates/synth-synthesis/src/optimizer_bridge.rs @@ -1055,6 +1055,13 @@ impl OptimizerBridge { | WasmOp::I32TruncSatF32U | WasmOp::I64TruncSatF32S | WasmOp::I64TruncSatF32U + // #869: the TRAPPING f32->i64 truncations — same reasoning as + // the trunc_sat group above (a float-typed operand the + // optimized path cannot map; omitting them would be the #615 + // silent-drop class). Their convert twins F32ConvertI64S/U + // are already listed with the f32 conversions. + | WasmOp::I64TruncF32S + | WasmOp::I64TruncF32U // f64 arithmetic | WasmOp::F64Add | WasmOp::F64Sub diff --git a/crates/synth-synthesis/tests/i64_float_conv_869.rs b/crates/synth-synthesis/tests/i64_float_conv_869.rs new file mode 100644 index 00000000..e443ea02 --- /dev/null +++ b/crates/synth-synthesis/tests/i64_float_conv_869.rs @@ -0,0 +1,177 @@ +//! #869 — the ARM 64-bit integer<->float conversion family lowering contracts +//! on the shipping path (`select_with_stack`, the path falcon's +//! `--relocatable` cortex-m7dp compile takes). +//! +//! * the four CONVERTS (`f32/f64.convert_i64_{s,u}`) are TOTAL — they lower +//! on m7dp with NO `Udf` (a guard would be a spurious trap); +//! * the four TRAPPING truncations (`i64.trunc_f32/f64_{s,u}`) carry the +//! #709-class i64 domain guard: exactly two `Udf` trap sites (upper + +//! lower bound; NaN falls out of the first ordered compare) in front of +//! the #782 word-decompose; +//! * the nontrapping `i64.trunc_sat_*` twins still emit NO `Udf` (the new +//! guard must not leak into the saturating forms); +//! * every family member LOUD-declines on a single-precision target +//! (m4f/m7 — the lowerings run on f64 machinery, undefined on FPv4-SP) +//! and on a no-FPU target (m3). +//! +//! The execution truth (boundary + trap rows + double-rounding killers + +//! fuzz vs wasmtime under unicorn) lives in +//! `scripts/repro/i64_float_conv_869_differential.py`. + +use synth_core::target::FPUPrecision; +use synth_synthesis::rules::ArmOp; +use synth_synthesis::{InstructionSelector, RuleDatabase, WasmOp}; + +fn selector(fpu: Option, name: &str) -> InstructionSelector { + let db = RuleDatabase::with_standard_rules(); + let mut sel = InstructionSelector::new(db.rules().to_vec()); + sel.set_target(fpu, name); + sel +} + +/// Lower `(param ) (result _) op(local.get 0)` on the given target. +fn lower( + fpu: Option, + name: &str, + op: WasmOp, + param: Param, +) -> Result, String> { + let mut sel = selector(fpu, name); + match param { + Param::I64 => sel.set_params_i64(vec![true]), + Param::F32 => sel.set_params_f32(vec![true]), + Param::F64 => sel.set_params_f64(vec![true]), + } + let ops = vec![WasmOp::LocalGet(0), op, WasmOp::End]; + sel.select_with_stack(&ops, 1) + .map(|instrs| instrs.into_iter().map(|i| i.op).collect()) + .map_err(|e| e.to_string()) +} + +#[derive(Clone, Copy)] +enum Param { + I64, + F32, + F64, +} + +fn udf_count(ops: &[ArmOp]) -> usize { + ops.iter() + .filter(|o| matches!(o, ArmOp::Udf { .. })) + .count() +} + +fn family() -> Vec<(WasmOp, Param, bool)> { + // (op, param type, is_trapping_trunc) + vec![ + (WasmOp::F32ConvertI64S, Param::I64, false), + (WasmOp::F32ConvertI64U, Param::I64, false), + (WasmOp::F64ConvertI64S, Param::I64, false), + (WasmOp::F64ConvertI64U, Param::I64, false), + (WasmOp::I64TruncF32S, Param::F32, true), + (WasmOp::I64TruncF32U, Param::F32, true), + (WasmOp::I64TruncF64S, Param::F64, true), + (WasmOp::I64TruncF64U, Param::F64, true), + ] +} + +// --------------------------------------------------------------------------- +// m7dp (double-precision): all eight lower; guard geometry pinned +// --------------------------------------------------------------------------- + +#[test] +fn m7dp_lowers_all_eight_converts_guardfree_truncs_double_guarded() { + for (op, param, trapping) in family() { + let ops = lower(Some(FPUPrecision::Double), "cortex-m7dp", op.clone(), param) + .unwrap_or_else(|e| panic!("{op:?} must lower on cortex-m7dp, got decline: {e}")); + let udfs = udf_count(&ops); + if trapping { + assert_eq!( + udfs, 2, + "{op:?}: the trapping trunc must carry exactly the two-bound \ + #709-class domain guard (upper + lower UDF), found {udfs}" + ); + } else { + assert_eq!( + udfs, 0, + "{op:?}: converts are TOTAL — a Udf is a spurious trap" + ); + } + } +} + +#[test] +fn m7dp_trunc_sat_twins_stay_guard_free() { + // The #869 guard must not leak into the NONTRAPPING saturating forms. + for (op, param) in [ + (WasmOp::I64TruncSatF32S, Param::F32), + (WasmOp::I64TruncSatF32U, Param::F32), + (WasmOp::I64TruncSatF64S, Param::F64), + (WasmOp::I64TruncSatF64U, Param::F64), + ] { + let ops = lower(Some(FPUPrecision::Double), "cortex-m7dp", op.clone(), param) + .unwrap_or_else(|e| panic!("{op:?} must lower on cortex-m7dp: {e}")); + assert_eq!( + udf_count(&ops), + 0, + "{op:?}: trunc_sat NEVER traps (§4.3.2) — a Udf is a miscompile" + ); + } +} + +#[test] +fn m7dp_f32_convert_carries_round_to_odd_fixup_and_single_demote() { + // The f32 converts must go through the f64 build + demote (one + // VCVT.F32.F64) — and the fixup's 64-bit increment must be the MODELED + // Adds/Adc pair, never the reg_effect-None I64Add pseudo-op (the + // range-realloc segment-liveness hazard caught at land time). + for op in [WasmOp::F32ConvertI64S, WasmOp::F32ConvertI64U] { + let ops = lower( + Some(FPUPrecision::Double), + "cortex-m7dp", + op.clone(), + Param::I64, + ) + .unwrap(); + let demotes = ops + .iter() + .filter(|o| matches!(o, ArmOp::F32DemoteF64 { .. })) + .count(); + assert_eq!(demotes, 1, "{op:?}: exactly one final demote rounding"); + assert!( + !ops.iter().any(|o| matches!(o, ArmOp::I64Add { .. })), + "{op:?}: the fixup increment must be modeled Adds/Adc, not the \ + I64Add pseudo-op (realloc segment-liveness hazard)" + ); + assert!( + ops.iter().any(|o| matches!(o, ArmOp::Adds { .. })) + && ops.iter().any(|o| matches!(o, ArmOp::Adc { .. })), + "{op:?}: missing the Adds/Adc round-to-odd increment" + ); + } +} + +// --------------------------------------------------------------------------- +// capability honesty: single-precision and no-FPU targets decline loudly +// --------------------------------------------------------------------------- + +#[test] +fn single_precision_m4f_declines_every_family_member() { + for (op, param, _) in family() { + let err = lower(Some(FPUPrecision::Single), "cortex-m4f", op.clone(), param).expect_err( + &format!("{op:?} must LOUD-decline on single-precision m4f (f64 machinery)"), + ); + assert!( + err.contains("double-precision"), + "{op:?}: decline must name the missing capability, got: {err}" + ); + } +} + +#[test] +fn no_fpu_m3_declines_every_family_member() { + for (op, param, _) in family() { + lower(None, "cortex-m3", op.clone(), param) + .expect_err(&format!("{op:?} must LOUD-decline on no-FPU cortex-m3")); + } +} diff --git a/crates/synth-verify/src/translation_validator.rs b/crates/synth-verify/src/translation_validator.rs index 7cd3cf9c..62b5837c 100644 --- a/crates/synth-verify/src/translation_validator.rs +++ b/crates/synth-verify/src/translation_validator.rs @@ -176,9 +176,16 @@ impl TranslationValidator { | WasmOp::I32TruncF32S | WasmOp::I32TruncF32U // f64→i32 trunc (#756): D-register domain guard, condition-only - // VC. NOT `I64TruncF64S/U`: the selector loud-declines those - // (no i64 register-pair lowering on 32-bit ARM), so there is no - // shipped guard to validate — a gate entry would be dead. + // VC. NOT `I64TruncF64S/U` / `I64TruncF32S/U`: since #869 the + // shipping `select_with_stack` DOES lower them (i64 domain + // guard + #782 decompose), but they are never expressed as a + // `SynthesisRule` (this gate's input), and the symbolic ARM + // exec model does not yet interpret the F64 compare/decompose + // chain their guard rides on — a gate entry here would + // false-red, not protect. Their trap behavior is + // EXECUTION-gated instead (the #869 differential runs every + // NaN/±inf/2^63/-2^63/2^64 trap row on both sides); the + // symbolic wiring is the named #756-class residual. | WasmOp::I32TruncF64S | WasmOp::I32TruncF64U ) diff --git a/crates/synth-verify/src/trap.rs b/crates/synth-verify/src/trap.rs index 37ce6a2d..38869c00 100644 --- a/crates/synth-verify/src/trap.rs +++ b/crates/synth-verify/src/trap.rs @@ -161,9 +161,8 @@ pub fn trap_div(op: DivOp, dividend: &BV, divisor: &BV) -> Bool { /// Map a float→int truncation [`WasmOp`] to its /// `(float format, integer target, signedness)` triple; `None` for any -/// non-trunc op. Covers all six trunc variants synth's decoder produces -/// (`i64.trunc_f32_s/u` are not `WasmOp` variants; the raw [`trap_trunc`] -/// builder still covers those shapes if they ever land). +/// non-trunc op. Covers all eight trunc variants synth's decoder produces +/// (`i64.trunc_f32_s/u` gained `WasmOp` variants + an ARM lowering in #869). pub fn trunc_op(op: &WasmOp) -> Option<(FpFmt, IntTarget, bool)> { Some(match op { WasmOp::I32TruncF32S => (FpFmt::F32, IntTarget::I32, true), @@ -172,6 +171,10 @@ pub fn trunc_op(op: &WasmOp) -> Option<(FpFmt, IntTarget, bool)> { WasmOp::I32TruncF64U => (FpFmt::F64, IntTarget::I32, false), WasmOp::I64TruncF64S => (FpFmt::F64, IntTarget::I64, true), WasmOp::I64TruncF64U => (FpFmt::F64, IntTarget::I64, false), + // #869: the f32-source i64-target pair — WasmOp variants (and an ARM + // lowering) exist now; the raw builder always covered the shape. + WasmOp::I64TruncF32S => (FpFmt::F32, IntTarget::I64, true), + WasmOp::I64TruncF32U => (FpFmt::F32, IntTarget::I64, false), _ => return None, }) } diff --git a/crates/synth-verify/src/wasm_semantics.rs b/crates/synth-verify/src/wasm_semantics.rs index 83a86e42..0bb5eaee 100644 --- a/crates/synth-verify/src/wasm_semantics.rs +++ b/crates/synth-verify/src/wasm_semantics.rs @@ -931,6 +931,21 @@ impl WasmSemantics { BV::new_const("i64_trunc_f64u_result", 64) } + // #869: the f32-source i64-target trapping truncations — modeled + // like their f64 twins (uninterpreted 64-bit result; the TRAP + // side is carried by `trap::trunc_op` + `trap_trunc`). Without + // these arms the wildcard would hand back a 32-BIT symbolic const + // for a 64-bit-typed op. + WasmOp::I64TruncF32S => { + assert_eq!(inputs.len(), 1, "I64TruncF32S requires 1 input"); + BV::new_const("i64_trunc_f32s_result", 64) + } + + WasmOp::I64TruncF32U => { + assert_eq!(inputs.len(), 1, "I64TruncF32U requires 1 input"); + BV::new_const("i64_trunc_f32u_result", 64) + } + WasmOp::I32TruncF64S => { assert_eq!(inputs.len(), 1, "I32TruncF64S requires 1 input"); // Truncate f64 to signed i32 diff --git a/scripts/repro/i64_float_conv_869.wat b/scripts/repro/i64_float_conv_869.wat new file mode 100644 index 00000000..2d5ce507 --- /dev/null +++ b/scripts/repro/i64_float_conv_869.wat @@ -0,0 +1,19 @@ +;; #869 — gale's self-contained repro: the ARM 64-bit integer<->float +;; conversion family. RED before the fix: the six i64<->float exports are +;; skipped (absent from `nm`); the four i32 rows lower and prove the 32-bit +;; family was never the gap. GREEN after: all ten exports reach `nm` -> T on +;; cortex-m7dp. +(module + (func (export "i64u_to_f32") (param i64) (result f32) local.get 0 f32.convert_i64_u) + (func (export "i64s_to_f32") (param i64) (result f32) local.get 0 f32.convert_i64_s) + (func (export "i64u_to_f64") (param i64) (result f64) local.get 0 f64.convert_i64_u) + (func (export "i64s_to_f64") (param i64) (result f64) local.get 0 f64.convert_i64_s) + (func (export "f32_to_i64s") (param f32) (result i64) local.get 0 i64.trunc_f32_s) + (func (export "f32_to_i64u") (param f32) (result i64) local.get 0 i64.trunc_f32_u) + ;; #756 completeness rows — the f64-source trunc twins. + (func (export "f64_to_i64s") (param f64) (result i64) local.get 0 i64.trunc_f64_s) + (func (export "f64_to_i64u") (param f64) (result i64) local.get 0 i64.trunc_f64_u) + (func (export "i32u_to_f32") (param i32) (result f32) local.get 0 f32.convert_i32_u) + (func (export "i32s_to_f32") (param i32) (result f32) local.get 0 f32.convert_i32_s) + (func (export "f32_to_i32s") (param f32) (result i32) local.get 0 i32.trunc_f32_s) + (func (export "wrap_then_i32u")(param i64) (result f32) local.get 0 i32.wrap_i64 f32.convert_i32_u)) diff --git a/scripts/repro/i64_float_conv_869_differential.py b/scripts/repro/i64_float_conv_869_differential.py new file mode 100644 index 00000000..88ca680f --- /dev/null +++ b/scripts/repro/i64_float_conv_869_differential.py @@ -0,0 +1,454 @@ +#!/usr/bin/env python3 +"""#869 — the ARM 64-bit integer<->float conversion family EXECUTION +differential (cortex-m7dp, Thumb-2, unicorn) vs wasmtime. + +Eight ops under test (gale's six + the #756 i64.trunc_f64 pair): + + f32.convert_i64_{s,u} / f64.convert_i64_{s,u} + ARMv7E-M VFP has no 64-bit-integer VCVT, so the lowering assembles the + value from two exact 32-bit conversions: a = (f64)hi * 2^32 (exact), + b = (f64)lo (exact), s = a + b (ONE correct RNE rounding). The f32 + targets additionally carry a Fast2Sum residual + branch-free + ROUND-TO-ODD fixup before the demote — a bare demote of s would + DOUBLE-ROUND (the 0x8000008000000001 row below is the killer case). + Converts are TOTAL: any trap on our side fails the run. + + i64.trunc_f32_{s,u} / i64.trunc_f64_{s,u} + The TRAPPING truncations (WASM §4.3.3): NaN and out-of-i64-range MUST + trap. The lowering is the #709-class i64 domain guard (compare + UDF) + in front of the #782 saturating word-decompose — a bare decompose (or a + bare AEABI __aeabi_f2lz call) would saturate instead of trapping: the + "ARM more-total-than-WASM" silent-miscompile class + (#633/#666/#709/#665/#642). Every trap row is EXECUTED here: wasmtime + must trap AND the ARM side must stop at a UDF; a value where wasmtime + traps (or vice versa) fails the run. + +Also gated: + * falcon's exact flags (-t cortex-m7dp --relocatable): all family exports + must reach the symbol table (the #869 skip class, RED before the fix). + * decline-honesty on the single-precision cortex-m4f: every family member + runs on f64 machinery, so all eight must be LOUD-declined there (absent + from the symbol table) — never undefined VCVT.F64 encodings on FPv4-SP. + * >=10k fixed-seed random patterns per direction (bit-exact, trap-aware). + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=/debug/synth python scripts/repro/i64_float_conv_869_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_ARM, UC_MODE_THUMB, Uc, UcError +from unicorn.arm_const import ( + UC_ARM_REG_D0, + UC_ARM_REG_LR, + UC_ARM_REG_PC, + UC_ARM_REG_R0, + UC_ARM_REG_R1, + UC_ARM_REG_R11, + UC_ARM_REG_S0, + UC_ARM_REG_SP, +) + +try: + from unicorn.arm_const import UC_ARM_REG_C1_C0_2, UC_ARM_REG_FPEXC +except ImportError: # older unicorn naming + UC_ARM_REG_C1_C0_2 = None + UC_ARM_REG_FPEXC = None + +WAT = Path(__file__).with_name("i64_float_conv_869.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") +MEMBASE = 0x20000000 # ARM32 R11/fp linear-memory base at reset (cortex_m.rs) + +M32 = (1 << 32) - 1 +M64 = (1 << 64) - 1 +INF = float("inf") +NAN = float("nan") + +# fn -> (arg type, result type) +CONVERTS = { + "i64u_to_f32": ("i64u", "f32"), + "i64s_to_f32": ("i64s", "f32"), + "i64u_to_f64": ("i64u", "f64"), + "i64s_to_f64": ("i64s", "f64"), +} +TRUNCS = { + "f32_to_i64s": ("f32", "i64"), + "f32_to_i64u": ("f32", "i64"), + "f64_to_i64s": ("f64", "i64"), + "f64_to_i64u": ("f64", "i64"), +} +FAMILY = {**CONVERTS, **TRUNCS} + +# --------------------------------------------------------------------------- +# Convert boundary table: u64 bit patterns (the _s forms reinterpret them as +# two's-complement i64). Rows pin: zero/small exact values, hi==0 (the +# Fast2Sum a==0 edge), INT64/UINT64 extremes, round-to-nearest-even TIES at +# both f32 (24-bit) and f64 (53-bit) granularity — including the +# double-rounding killers where RN53-then-RN24 differs from direct RN24 — and +# plain mid-range patterns exercising the borrow/carry of the fixup. +CONVERT_PATTERNS = [ + 0x0000000000000000, + 0x0000000000000001, + 0x0000000000000002, + 0x000000000000002A, + 0x00000000FFFFFFFF, # hi == 0: the exact single-word path + 0x0000000100000000, # lo == 0 + 0x0000000100000001, + 0x0000001000000001, # small hi, sticky in lo + 0x0000000001000001, # 2^24 + 1: first f32 rounding (tie -> even) + 0x0000000001000003, + 0x0000000002000002, + 0x0000000002000006, + 0x0020000000000001, # 2^53 + 1: first f64 rounding (tie -> even) + 0x0020000000000003, + 0x0040000000000004, + 0x123456789ABCDEF0, + 0x7FFFFFFFFFFFFFFF, # INT64_MAX + 0x7FFFFFFFFFFFFC00, + 0x8000000000000000, # INT64_MIN as _s; 2^63 as _u + 0x8000000000000001, + 0x8000000000000200, # 2^63 + 512: f64 tie -> even (down) + 0x8000000000000201, # 2^63 + 513: f64 rounds up + 0x8000000000000600, # 2^63 + 3*512: f64 tie -> even (up) + 0x8000008000000000, # 2^63 + 2^39: exact f32 tie -> even (down) + 0x8000008000000001, # DOUBLE-ROUNDING KILLER: f64 hides the +1 sticky + 0x8000018000000001, # odd-mantissa neighbor of the above + 0xFFFFFF7FFFFFFFFF, # just below the top f32 tie + 0xFFFFFF8000000000, # top f32 tie (rounds to 2^64, even) + 0xFFFFFF8000000001, # KILLER at the very top: must round UP to 2^64 + 0xFFFFFFFFFFFFF800, + 0xFFFFFFFFFFFFFBFF, + 0xFFFFFFFFFFFFFC00, # top f64 tie + 0xFFFFFFFFFFFFFC01, + 0xFFFFFFFFFFFFFFFF, # UINT64_MAX / -1 + 0xFFFFFFFF00000000, + 0xC000000000000000, + 0x8000000180000001, +] + +# Trunc boundary table per source type: every i64-range edge on BOTH sides, +# NaN/±inf, the exact 2^63 / -2^63 / 2^64 boundaries, fraction rows, and the +# unsigned (-1, 0) truncate-to-zero window. wasmtime decides trap-vs-value; +# the ARM side must agree row by row. +TRUNC_VALUES = { + "f32": [ + 0.0, -0.0, 0.5, -0.5, 0.9, -0.9, 1.5, -1.5, 42.0, -42.0, 100.75, + -0.99609375, # in (-1,0): _u truncates to 0 (no trap) + 2147483648.0, -2147483648.0, 4294967296.0, + 1e10, -1e10, 3e18, -3e18, + 9223371487098961920.0, # largest f32 < 2^63: _s in-range max + 9223372036854775808.0, # 2^63 exactly: _s TRAPS + -9223372036854775808.0, # -2^63 exactly: _s in-range minimum + -9223373136366403584.0, # first f32 below -2^63: _s TRAPS + 18446742974197923840.0, # largest f32 < 2^64: _u in-range max + 18446744073709551616.0, # 2^64 exactly: _u TRAPS + -1.0, # _u TRAPS (strict lower bound) + -1.5, 1e30, -1e30, INF, -INF, NAN, + ], + "f64": [ + 0.0, -0.0, 0.5, -0.5, 0.9, -0.9, 1.5, -1.5, 42.0, -42.0, 100.75, + -0.9999999999999999, # in (-1,0): _u truncates to 0 (no trap) + 2147483648.5, -2147483649.5, 4294967296.5, + 1e10, -1e10, 3e18, -3e18, + 9223372036854774784.0, # largest f64 < 2^63: _s in-range max + 9223372036854775808.0, # 2^63 exactly: _s TRAPS + -9223372036854775808.0, # -2^63 exactly: _s in-range minimum + -9223372036854777856.0, # first f64 below -2^63: _s TRAPS + 18446744073709549568.0, # largest f64 < 2^64: _u in-range max + 18446744073709551616.0, # 2^64 exactly: _u TRAPS + -1.0, # _u TRAPS (strict lower bound) + -1.5, 1e300, -1e300, INF, -INF, NAN, + ], +} + +FUZZ_PER_DIR = int(os.environ.get("I64_FLOAT_FUZZ", "12000")) + + +def f32_bits(x): + return struct.unpack("= (1 << 63) else b + + +# --------------------------------------------------------------------------- +def wasmtime_instance(): + engine = wasmtime.Engine() + module = wasmtime.Module.from_file(engine, str(WAT)) + store = wasmtime.Store(engine) + return store, wasmtime.Instance(store, module, []).exports(store) + + +def compile_or_die(out, extra, what): + cmd = [SYNTH, "compile", str(WAT), "-o", out, *extra] + r = subprocess.run(cmd, capture_output=True, text=True, + env={"PATH": "/usr/bin:/bin"}) + if r.returncode != 0: + sys.exit(f"{what} compile failed: {r.stderr}") + return r.stderr + r.stdout + + +def load(elf): + f = ELFFile(open(elf, "rb")) + text = f.get_section_by_name(".text") + code, base = text.data(), text["sh_addr"] + syms = {} + for sec in f.iter_sections(): + if sec.header.sh_type == "SHT_SYMTAB": # #489: symtab, not disasm text + for sy in sec.iter_symbols(): + if sy.name: + syms[sy.name] = sy["st_value"] + return code, base, syms + + +# --------------------------------------------------------------------------- +# ARM32 Thumb-2 unicorn execution. AAPCS-VFP: i64 args in R0:R1, f32/f64 args +# in S0/D0; f32/f64 results in S0/D0, i64 results in R0:R1 (reading only R0 +# would blind every hi-word bug). Returns ('ok', bits) / ('trap-udf', info) / +# ('fault', info). +def arm32_run(text, base, addr, aty, rty, arg_bits_val): + uc = Uc(UC_ARCH_ARM, UC_MODE_THUMB) + map_base = base & ~0xFFF + size = ((len(text) + (base - map_base)) + 0xFFF) & ~0xFFF + uc.mem_map(map_base, max(size, 0x1000)) + uc.mem_write(base, text) + uc.mem_map(0x30000, 0x10000) # stack + uc.mem_map(MEMBASE, 0x10000) # linear-memory window (R11 base) + uc.reg_write(UC_ARM_REG_SP, 0x38000) + uc.reg_write(UC_ARM_REG_R11, MEMBASE) + if UC_ARM_REG_C1_C0_2 is not None: + uc.reg_write(UC_ARM_REG_C1_C0_2, 0x00F00000) # CPACR CP10/CP11 + if UC_ARM_REG_FPEXC is not None: + uc.reg_write(UC_ARM_REG_FPEXC, 0x40000000) # FPEXC.EN + if aty in ("i64u", "i64s"): + uc.reg_write(UC_ARM_REG_R0, arg_bits_val & M32) + uc.reg_write(UC_ARM_REG_R1, (arg_bits_val >> 32) & M32) + elif aty == "f32": + uc.reg_write(UC_ARM_REG_S0, arg_bits_val) + else: + uc.reg_write(UC_ARM_REG_D0, arg_bits_val) + ret = 0x38000 + uc.reg_write(UC_ARM_REG_LR, ret | 1) + try: + uc.emu_start(addr | 1, ret & ~1, count=2000) + except UcError as e: + pc = uc.reg_read(UC_ARM_REG_PC) + kind = "fault" + if base <= pc < base + len(text): + hw = struct.unpack(" {kind}: {got} — converts " + f"are TOTAL (wasmtime bits {want:#x})") + return fails + 1 + if got != want: + print(f"BUG [{what}] {fn}({pattern:#x}) = {got:#x} != wasmtime " + f"{want:#x} (round-to-nearest-even violation)") + return fails + 1 + return fails + + +def check_trunc(store, wexp, text, base, syms, fn, v, fails, what): + aty, _ = TRUNCS[fn] + bits = f32_bits(v) if aty == "f32" else f64_bits(v) + wkind, want = wasmtime_trunc(store, wexp, fn, v) + kind, got = arm32_run(text, base, syms[fn], aty, "i64", bits) + if wkind == "trap": + if kind != "trap-udf": + print(f"BUG [{what}] {fn}({v!r}): wasmtime TRAPS but ARM " + f"{'returned ' + hex(got) if kind == 'ok' else kind} — the " + f"#709-class silent-miscompile (missing domain guard)") + return fails + 1 + return fails + if kind != "ok": + print(f"BUG [{what}] {fn}({v!r}) -> {kind}: {got} — wasmtime returns " + f"{want:#x} (guard over-traps)") + return fails + 1 + if got != want: + print(f"BUG [{what}] {fn}({v!r}) = {got:#x} != wasmtime {want:#x}") + return fails + 1 + return fails + + +# --------------------------------------------------------------------------- +def _rand_u64(rng): + """u64 patterns biased toward tie-prone shapes: a short mantissa shifted + high (exactly the round/sticky geometry of the 24- and 53-bit roundings) + alongside uniform patterns and small/word-edge values.""" + r = rng.random() + if r < 0.40: + return rng.getrandbits(64) + if r < 0.70: # short significand << k, then poison low bits sometimes + v = rng.getrandbits(rng.randint(20, 30)) << rng.randint(0, 40) + if rng.random() < 0.5: + v |= rng.getrandbits(rng.randint(1, 10)) + return v & M64 + if r < 0.85: # dense high bits (top-of-range rounding, carry-out shapes) + return (M64 ^ rng.getrandbits(rng.randint(1, 41))) & M64 + return rng.getrandbits(rng.randint(1, 64)) + + +def _rand_f32_bits(rng): + r = rng.random() + if r < 0.5: + return rng.getrandbits(32) + if r < 0.85: # exponents around the i64 boundary (2^62..2^65) + exp = rng.randint(180, 195) + return (rng.getrandbits(1) << 31) | (exp << 23) | rng.getrandbits(23) + return (rng.getrandbits(1) << 31) | (0xFF << 23) | rng.getrandbits(23) + + +def _rand_f64_bits(rng): + r = rng.random() + if r < 0.5: + return rng.getrandbits(64) + if r < 0.85: + exp = rng.randint(1084, 1091) # 2^61..2^68 + return (rng.getrandbits(1) << 63) | (exp << 52) | rng.getrandbits(52) + return (rng.getrandbits(1) << 63) | (0x7FF << 52) | rng.getrandbits(52) + + +# --------------------------------------------------------------------------- +def main(): + store, wexp = wasmtime_instance() + fails = 0 + total = 0 + + # ==== gale's exact flags: -t cortex-m7dp --relocatable ================= + # RED before #869: all eight family exports skipped. GREEN: all present + # (plus the four 32-bit control rows that always lowered). + compile_or_die("/tmp/i64_float_conv_869_reloc.o", + ["-b", "arm", "--target", "cortex-m7dp", "--relocatable"], + "ARM32 --relocatable (falcon flags)") + _, _, reloc_syms = load("/tmp/i64_float_conv_869_reloc.o") + for fn in [*FAMILY, "i32u_to_f32", "i32s_to_f32", "f32_to_i32s", + "wrap_then_i32u"]: + total += 1 + if fn not in reloc_syms: + fails += 1 + print(f"FAIL [falcon-flags] {fn}: SKIPPED under -t cortex-m7dp " + f"--relocatable (the #869 skip class)") + + # ==== decline-honesty: single-precision m4f must LOUD-decline ========== + # Every family member's lowering runs on f64 machinery (promote/decompose/ + # two-word build) — undefined encodings on FPv4-SP. Absent symbol = the + # honest decline; present = the capability gate regressed. + compile_or_die("/tmp/i64_float_conv_869_m4f.o", + ["-b", "arm", "--target", "cortex-m4f", "--all-exports"], + "ARM32 cortex-m4f") + _, _, m4f_syms = load("/tmp/i64_float_conv_869_m4f.o") + for fn in FAMILY: + total += 1 + if fn in m4f_syms: + fails += 1 + print(f"FAIL [m4f] {fn}: compiled on a single-precision target — " + f"expected a LOUD decline (f64 machinery on FPv4-SP)") + + # ==== execute the boundary tables (cortex-m7dp self-contained) ========= + compile_or_die("/tmp/i64_float_conv_869_arm.elf", + ["-b", "arm", "--target", "cortex-m7dp", "--all-exports"], + "ARM32 cortex-m7dp") + text, base, syms = load("/tmp/i64_float_conv_869_arm.elf") + for fn in FAMILY: + if fn not in syms: + sys.exit(f"FATAL [m7dp] {fn}: symbol missing from the execution " + f"build — cannot gate") + + for fn in CONVERTS: + for pattern in CONVERT_PATTERNS: + total += 1 + fails = check_convert(store, wexp, text, base, syms, fn, pattern, + fails, "boundary") + for fn, (aty, _) in TRUNCS.items(): + for v in TRUNC_VALUES[aty]: + total += 1 + fails = check_trunc(store, wexp, text, base, syms, fn, v, fails, + "boundary") + + # ==== fixed-seed fuzz: converts (u64 patterns) and truncs (float bits) == + import random + rng = random.Random(0x869F17E) + for _ in range(FUZZ_PER_DIR): + pattern = _rand_u64(rng) + for fn in CONVERTS: + total += 1 + f = fails + fails = check_convert(store, wexp, text, base, syms, fn, pattern, + fails, "fuzz") + if fails > f and fails > 25: + sys.exit(f"FAIL (aborted early at {fails} failures)") + for src, gen in (("f32", _rand_f32_bits), ("f64", _rand_f64_bits)): + fns = [fn for fn, (aty, _) in TRUNCS.items() if aty == src] + for _ in range(FUZZ_PER_DIR): + b = gen(rng) + if src == "f32": + v = struct.unpack(" f and fails > 25: + sys.exit(f"FAIL (aborted early at {fails} failures)") + + print(f"\n{total} checks (boundary + {FUZZ_PER_DIR}/direction fixed-seed " + f"fuzz), trap rows executed on both sides") + print("RESULT:", "PASS — i64<->float family matches wasmtime bit-exactly " + "on cortex-m7dp (incl. executed NaN/±inf/2^63/-2^63/2^64 trap rows " + "and the double-rounding killers); m4f loud-declines; falcon flags " + "lower all exports" if not fails else f"FAIL ({fails})") + sys.exit(1 if fails else 0) + + +if __name__ == "__main__": + main()