From d45b860a02b367a8e949018b7a2008a298e068c5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 07:44:02 +0200 Subject: [PATCH 1/3] =?UTF-8?q?fix(#782b):=20float=20select=20+=20explicit?= =?UTF-8?q?=20float=20return=20=E2=80=94=20clear=20the=20'integer=20popped?= =?UTF-8?q?=20f32'=20class?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 12-function 'GI-FPU-002: an integer operation popped an f32' class on falcon's real fused core (incl. run-stabilization) is NOT register-pressure: it is (a) untyped `select` over f32/f64 values (falcon's clamp idiom) and (b) an EXPLICIT `return` of an f32 result — both routed the VFP-resident value into the integer pop, which loud-declines. * Select: when both value operands are VFP-resident, move the bit patterns into core registers (VMOV reinterpret, bit-exact), run the same flag-safe CMP + IT;MOV select on the patterns, and home the winner in a fresh S/D register. NaN-safe by construction (select picks, never computes). * Return: home an f32/f64 result to S0/D0 (AAPCS-VFP) exactly like the fall-through epilogue, with the same #719 soundness guard (an integer- tagged float result still declines loudly — never an R0 return a hard- float caller would misread). Byte-identical for every previously-compiling function: both new paths are reachable only from stack states that previously ERRORED (function skipped). falcon-flight-v1.123 fused core, cortex-m7dp --relocatable --native-pointer-abi: 26 -> 15 skips; 'integer popped f32' 12 -> 0; run-stabilization compiles. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 265 ++++++++++++++++++ 1 file changed, 265 insertions(+) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index b6a646c1..b7fbf13e 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -12556,6 +12556,94 @@ impl InstructionSelector { } Return => { + // GI-FPU-002 (#782): a float result reaches an EXPLICIT + // `return` in the VFP file — home it to S0 (f32) / D0 + // (f64) per AAPCS-VFP, exactly like the fall-through + // epilogue below the op loop (which already does this), + // instead of loud-declining in the integer pop. Same + // soundness guard as the epilogue (#719): a hard-float + // function whose f32/f64 result shows up integer-tagged + // (e.g. a call's R0 result) must NOT emit the integer R0 + // return — the AAPCS-VFP caller reads S0/D0. + let ret_top_f32 = stack.last().and_then(|v| v.as_float()); + let ret_top_f64 = stack.last().and_then(|v| v.as_double()); + if (self.ret_f32 || self.ret_f64) && fpu.is_some() { + let top_matches = if self.ret_f64 { + ret_top_f64.is_some() + } else { + ret_top_f32.is_some() + }; + if !top_matches { + return Err(synth_core::Error::synthesis(format!( + "GI-FPU-002 phase 2: function returns {} but an \ + explicit `return`'s result is in a core register \ + — refusing to emit an integer R0 return where an \ + AAPCS-VFP caller reads {} (declining, #719/#369)", + if self.ret_f64 { "f64" } else { "f32" }, + if self.ret_f64 { "D0" } else { "S0" }, + ))); + } + } + if self.ret_f64 && let Some(dreg) = ret_top_f64 { + // Home to D0 via the core round-trip (bit-exact; no + // D→D move in the ArmOp set). R0/R1 are dead at the + // return of an f64-returning function. + if vfp_d_index(dreg) != Some(0) { + instructions.push(ArmInstruction { + op: ArmOp::I64ReinterpretF64 { + rdlo: Reg::R0, + rdhi: Reg::R1, + dm: dreg, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + instructions.push(ArmInstruction { + op: ArmOp::F64ReinterpretI64 { + dd: VfpReg::D0, + rmlo: Reg::R0, + rmhi: Reg::R1, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + } + stack.pop(); + free_vfp_dtemp(&mut vfp_used, &vfp_home, dreg); + } else if self.ret_f32 && let Some(sreg) = ret_top_f32 { + // Home to S0 via the R12 (IP scratch) round-trip. + if vfp_s_index(sreg) != Some(0) { + instructions.push(ArmInstruction { + op: ArmOp::I32ReinterpretF32 { + rd: Reg::R12, + sm: sreg, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + instructions.push(ArmInstruction { + op: ArmOp::F32ReinterpretI32 { + sd: VfpReg::S0, + rm: Reg::R12, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + } + stack.pop(); + free_vfp_temp(&mut vfp_used, &vfp_home, sreg); + } else if ret_top_f32.is_some() || ret_top_f64.is_some() { + // A float on top of the stack at the `return` of a + // function that does not return that float type — + // invalid wasm (or an unlowered shape). Loud, as ever. + return Err(synth_core::Error::synthesis( + "GI-FPU-002: a VFP stack value reached an explicit \ + `return` of a non-float-returning function — \ + invalid wasm or an unlowered float op reached the \ + integer path" + .to_string(), + )); + } else // Move top-of-stack to R0 for return value (AAPCS). Pop is // reload-aware (#171): a spilled return value is reloaded // from its frame slot first. @@ -13147,6 +13235,183 @@ impl InstructionSelector { &live_params, idx, )?; + // GI-FPU-002 (#782): FLOAT select — both value operands + // live in the VFP register file (`select` over f32/f64 is + // the clamp idiom `(x>k)?k:x` falcon emits throughout its + // stabilization math). The integer pop below loud-declines + // on a Float/Double entry, so route the float shapes + // through a VFP-aware lowering FIRST: move both operands' + // bit patterns into core registers (VMOV — bit-exact, no + // conversion), run the SAME flag-safe CMP + IT;MOV select + // on the patterns, and move the winner back into a fresh + // VFP register. NaN-safe by construction: `select` picks a + // value, never computes one, and the round-trip preserves + // the exact bits. Only reachable when an operand is + // VFP-resident (fpu-gated paths pushed it), so integer + // modules are byte-identical. + let top2_f32 = stack.len() >= 2 + && matches!(stack[stack.len() - 1], StackVal::Float { .. }) + && matches!(stack[stack.len() - 2], StackVal::Float { .. }); + let top2_f64 = stack.len() >= 2 + && matches!(stack[stack.len() - 1], StackVal::Double { .. }) + && matches!(stack[stack.len() - 2], StackVal::Double { .. }); + if top2_f32 { + let s2 = pop_float(&mut stack)?; // val2 (cond == 0) + let s1 = pop_float(&mut stack)?; // val1 (cond != 0) + // `cond_reg` is off the vstack but must survive until + // the CMP — reserve it (and the first pattern temp) + // through the core-register allocations. + let mut resv = live_params.clone(); + resv.push(cond_reg); + let ra = alloc_temp_or_spill( + &mut next_temp, + &mut stack, + &mut instructions, + &mut spill, + &resv, + idx, + )?; + instructions.push(ArmInstruction { + op: ArmOp::I32ReinterpretF32 { rd: ra, sm: s1 }, + source_line: Some(idx), + }); + cf.add_instruction(); + resv.push(ra); + let rb = alloc_temp_or_spill( + &mut next_temp, + &mut stack, + &mut instructions, + &mut spill, + &resv, + idx, + )?; + instructions.push(ArmInstruction { + op: ArmOp::I32ReinterpretF32 { rd: rb, sm: s2 }, + source_line: Some(idx), + }); + cf.add_instruction(); + // CMP first, then the single flag-preserving IT;MOV — + // `rb` already holds val2's pattern (the EQ result), so + // only the NE override is needed (in-place form). + instructions.push(ArmInstruction { + op: ArmOp::Cmp { + rn: cond_reg, + op2: Operand2::Imm(0), + }, + source_line: Some(idx), + }); + cf.add_instruction(); + instructions.push(ArmInstruction { + op: ArmOp::SelectMove { + rd: rb, + rm: ra, + cond: Condition::NE, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + // Free the two consumed S-registers (home-aware), then + // home the selected pattern in a fresh S-register. + free_vfp_temp(&mut vfp_used, &vfp_home, s1); + free_vfp_temp(&mut vfp_used, &vfp_home, s2); + let sd = alloc_vfp_temp(&mut vfp_used)?; + instructions.push(ArmInstruction { + op: ArmOp::F32ReinterpretI32 { sd, rm: rb }, + source_line: Some(idx), + }); + cf.add_instruction(); + stack.push(StackVal::Float { sreg: sd }); + continue; + } + if top2_f64 { + // Same bit-pattern select, one register PAIR per f64 + // (I64ReinterpretF64/F64ReinterpretI64 are the shipped + // core round-trip — no D→D move in the ArmOp set). + let d2 = pop_double(&mut stack)?; // val2 (cond == 0) + let d1 = pop_double(&mut stack)?; // val1 (cond != 0) + let mut resv = live_params.clone(); + resv.push(cond_reg); + let (alo, ahi) = alloc_consecutive_pair( + &mut next_temp, + &mut stack, + &mut instructions, + &mut spill, + &[], + &resv, + idx, + )?; + instructions.push(ArmInstruction { + op: ArmOp::I64ReinterpretF64 { + rdlo: alo, + rdhi: ahi, + dm: d1, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + resv.push(alo); + resv.push(ahi); + let (blo, bhi) = alloc_consecutive_pair( + &mut next_temp, + &mut stack, + &mut instructions, + &mut spill, + &[], + &resv, + idx, + )?; + instructions.push(ArmInstruction { + op: ArmOp::I64ReinterpretF64 { + rdlo: blo, + rdhi: bhi, + dm: d2, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + instructions.push(ArmInstruction { + op: ArmOp::Cmp { + rn: cond_reg, + op2: Operand2::Imm(0), + }, + source_line: Some(idx), + }); + cf.add_instruction(); + // Two IT;MOVs — each is the flag-preserving 0x46xx + // MOV, so the second still sees the CMP's flags. + instructions.push(ArmInstruction { + op: ArmOp::SelectMove { + rd: blo, + rm: alo, + cond: Condition::NE, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + instructions.push(ArmInstruction { + op: ArmOp::SelectMove { + rd: bhi, + rm: ahi, + cond: Condition::NE, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + free_vfp_dtemp(&mut vfp_used, &vfp_home, d1); + free_vfp_dtemp(&mut vfp_used, &vfp_home, d2); + let dd = alloc_vfp_dtemp(&mut vfp_used)?; + instructions.push(ArmInstruction { + op: ArmOp::F64ReinterpretI64 { + dd, + rmlo: blo, + rmhi: bhi, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + stack.push(StackVal::Double { dreg: dd }); + continue; + } let val2 = pop_operand( &mut stack, &mut next_temp, From 7b6810e286535d2faac4f2ad16a579d7d7295fec Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 07:55:07 +0200 Subject: [PATCH 2/3] =?UTF-8?q?fix(#782b):=20i64-select=20hi-half=20+=20ha?= =?UTF-8?q?rd-float-signature=20optimized-path=20ABI=20=E2=80=94=20two=20a?= =?UTF-8?q?dversarial=20finds=20+=20red-first=20harness?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Found while gating the float-select fix with the #782 differential harness: 1. WIDE (i64) select SILENT miscompile (every target): the integer select moved only the LO register and pushed the result as i32 — cond==0 returned val2's lo paired with val1's HI. Soft-float f64 select rode the same path. Fixed: width read before the pops, dst PAIR allocated while the operands are stack-live, both halves conditionally moved (4 flag- preserving IT;MOVs), result pushed wide. 2. Hard-float SIGNATURE-only ABI miscompile: a function whose ops all lower on the OPTIMIZED path but whose signature carries a float (pure value- pick '(param f32 f32 i32) (result f32) select' — no float op to trip the #120 ir_to_arm fallback) silently compiled with the integer ABI: callers marshal S0/S1 per AAPCS-VFP, the body read R0/R1. New pre-gate routes float-signature functions to the direct selector on FPU targets only — soft-float keeps the optimized path (integer treatment IS the ABI there, byte-identical). scripts/repro/float_select_return_782_differential.py: 702 execution cases vs wasmtime (unicorn cortex-m7dp + m3), NaN-payload-strict for selects, honest capability gates pinned on m3/m4f. GREEN. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend/src/arm_backend.rs | 27 ++ .../src/instruction_selector.rs | 80 ++++ scripts/repro/float_select_return_782.wat | 58 +++ .../float_select_return_782_differential.py | 418 ++++++++++++++++++ 4 files changed, 583 insertions(+) create mode 100644 scripts/repro/float_select_return_782.wat create mode 100644 scripts/repro/float_select_return_782_differential.py diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs index fe61fc7f..50e16a6f 100644 --- a/crates/synth-backend/src/arm_backend.rs +++ b/crates/synth-backend/src/arm_backend.rs @@ -707,6 +707,32 @@ fn compile_wasm_to_arm( .iter() .take(num_params as usize) .any(|&w| w); + // #782(b): a HARD-float (FPU) target passes f32 args in VFP S-registers + // and returns floats in S0/D0 (AAPCS-VFP) — but the optimized path's + // param/return homing is float-naive (integer R0..R3 args, R0 return). A + // function whose ops ALL lower on the optimized path but whose SIGNATURE + // carries a float — e.g. the pure value-pick + // `(param f32 f32 i32) (result f32) select`, no float OP to trip the + // issue-#120 ir_to_arm fallback — was silently compiled with the integer + // ABI: callers marshal S0/S1, the body reads R0/R1. Route every + // float-signature function to the direct selector (AAPCS-VFP homing, or + // an honest decline). Soft-float targets (no FPU) keep the optimized + // path: the integer treatment IS the ABI there — byte-identical. (f64 + // params already route direct via `has_wide_param`; this adds f32 params + // and f32/f64 returns.) + let has_float_sig = config.target.fpu.is_some() + && (config.current_func_ret_f32 + || config.current_func_ret_f64 + || config + .current_func_params_f32 + .iter() + .take(num_params as usize) + .any(|&f| f) + || config + .current_func_params_f64 + .iter() + .take(num_params as usize) + .any(|&f| f)); // #494 phase 2b: div/rem guard-elision marks are consumed by the DIRECT // selector only — the optimized path's IR passes (const-fold/CSE/DCE) // renumber instructions, so an op-index-keyed mark cannot soundly survive @@ -741,6 +767,7 @@ fn compile_wasm_to_arm( || has_br_table || has_value_carry || has_wide_param + || has_float_sig || has_global_access || has_fact_div_elide // #457: route read-before-write non-param locals to the direct diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index b7fbf13e..b4a36f26 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -13412,6 +13412,86 @@ impl InstructionSelector { stack.push(StackVal::Double { dreg: dd }); continue; } + // #782(b): WIDE (i64) select — BOTH halves must be picked. + // The narrow path below moves only the lo register and + // pushed the result as i32, silently keeping the WRONG hi + // half whenever cond == 0 (found adversarially while + // clearing the float-select class; also covers a soft-float + // f64 select, which rides the i64-pair treatment). Width is + // read BEFORE the pops (pop_operand returns only the lo). + let v2_wide = stack.last().is_some_and(|v| v.is_i64()); + let v1_wide = stack.len() >= 2 && stack[stack.len() - 2].is_i64(); + if v2_wide || v1_wide { + if v2_wide != v1_wide { + return Err(synth_core::Error::synthesis( + "select value operands disagree on width \ + (i32 vs i64) — invalid wasm" + .to_string(), + )); + } + // Destination pair FIRST, while both values are still + // stack-live (the allocator cannot hand out their + // registers; a pressure spill of them reloads on pop). + let mut resv = live_params.clone(); + resv.push(cond_reg); + let (dlo, dhi) = alloc_consecutive_pair( + &mut next_temp, + &mut stack, + &mut instructions, + &mut spill, + &[], + &resv, + idx, + )?; + // Reserve the dst pair through the (possibly reloading) + // pops so a spilled operand cannot reload into it. + resv.push(dlo); + resv.push(dhi); + let val2 = pop_operand( + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &resv, + idx, + )?; + let hi2 = i64_pair_hi(val2)?; + let val1 = pop_operand( + &mut stack, + &mut next_temp, + &mut instructions, + &mut spill, + &resv, + idx, + )?; + let hi1 = i64_pair_hi(val1)?; + instructions.push(ArmInstruction { + op: ArmOp::Cmp { + rn: cond_reg, + op2: Operand2::Imm(0), + }, + source_line: Some(idx), + }); + cf.add_instruction(); + // Four IT;MOVs (the flag-preserving 0x46xx MOV — the + // CMP flags survive all four). dst is disjoint from + // both source pairs by construction, so the NE/EQ + // moves never clobber a source half they still need. + for (rd, rm, cond) in [ + (dlo, val1, Condition::NE), + (dhi, hi1, Condition::NE), + (dlo, val2, Condition::EQ), + (dhi, hi2, Condition::EQ), + ] { + instructions.push(ArmInstruction { + op: ArmOp::SelectMove { rd, rm, cond }, + source_line: Some(idx), + }); + cf.add_instruction(); + } + stack.push(StackVal::i64(dlo)); + continue; + } let val2 = pop_operand( &mut stack, &mut next_temp, diff --git a/scripts/repro/float_select_return_782.wat b/scripts/repro/float_select_return_782.wat new file mode 100644 index 00000000..14803233 --- /dev/null +++ b/scripts/repro/float_select_return_782.wat @@ -0,0 +1,58 @@ +;; #782(b) — the falcon "integer popped f32" class, minimized. +;; +;; The 12-function GI-FPU-002 decline class on the real falcon-flight-v1.123 +;; fused core (incl. run-stabilization) is NOT register pressure: it is +;; (a) untyped `select` over two f32/f64 values (falcon's clamp idiom +;; `(x>k) ? k : x` — run-stabilization op 202, func_50 op 6, ...), and +;; (b) an EXPLICIT `return` of an f32 result (func_35/42/43/92) +;; — both routed a VFP-resident value into the integer pop, which +;; loud-declined the whole function. +(module + ;; (a) select over two f32 values — direct AAPCS-VFP params (S0, S1) + i32 + ;; cond (R0), result in S0. + (func (export "sel32") (param f32 f32 i32) (result f32) + (select (local.get 0) (local.get 1) (local.get 2))) + + ;; (a) bit-pattern variant: values enter as i32 bits and cross into the VFP + ;; file via reinterpret (falcon's real dataflow) — exercises NaN payload + ;; preservation exactly (select PICKS, never computes: strict bit compare). + (func (export "sel32b") (param i32 i32 i32) (result i32) + (i32.reinterpret_f32 + (select + (f32.reinterpret_i32 (local.get 0)) + (f32.reinterpret_i32 (local.get 1)) + (local.get 2)))) + + ;; (a) run-stabilization's exact clamp shape: cond computed by an f32 + ;; compare, val1 a const, val2 the live value. + (func (export "clamp32") (param f32) (result f32) + (select + (f32.const 0x1.99999ap-4) ;; 0.1 (picked when x > 0.1) + (local.get 0) + (f32.gt (local.get 0) (f32.const 0x1.99999ap-4)))) + + ;; (a) select over two f64 values (D0, D1 + cond R0 -> D0). + (func (export "sel64") (param f64 f64 i32) (result f64) + (select (local.get 0) (local.get 1) (local.get 2))) + + ;; (b) explicit `return` of an f32 result from inside a block — previously + ;; the integer Return pop loud-declined on the Float entry. + (func (export "ret32") (param f32 i32) (result f32) + (block + (br_if 0 (i32.eqz (local.get 1))) + (return (f32.add (local.get 0) (f32.const 1.0)))) + (f32.const 2.5)) + + ;; (b) explicit `return` of an f64 result. + (func (export "ret64") (param f64 i32) (result f64) + (block + (br_if 0 (i32.eqz (local.get 1))) + (return (f64.add (local.get 0) (f64.const 1.0)))) + (f64.const 2.5)) + + ;; (c) i64 select — found adversarially while clearing (a): the narrow + ;; integer select moved only the LO register and pushed the result as i32, + ;; silently keeping the WRONG hi half whenever cond == 0. Every target + ;; (this one is not float-gated; soft-float f64 select rides this path too). + (func (export "seli64") (param i64 i64 i32) (result i64) + (select (local.get 0) (local.get 1) (local.get 2)))) diff --git a/scripts/repro/float_select_return_782_differential.py b/scripts/repro/float_select_return_782_differential.py new file mode 100644 index 00000000..f1f55343 --- /dev/null +++ b/scripts/repro/float_select_return_782_differential.py @@ -0,0 +1,418 @@ +#!/usr/bin/env python3 +"""#782(b) — EXECUTION-validate float `select` + explicit float `return`. + +The dominant decline class on the real falcon-flight-v1.123 fused core +(12/26 skipped functions, incl. run-stabilization) was +"GI-FPU-002: an integer operation popped an f32 (VFP) stack value". It is not +register pressure: untyped `select` over two f32/f64 values (falcon's clamp +idiom) and an explicit `return` of an f32 result both routed a VFP-resident +value into the integer pop, which loud-declined the whole function. + +The fix lowers float `select` as a bit-pattern select through core registers +(VMOV reinterpret + the same flag-safe CMP + IT;MOV — bit-exact, select PICKS +a value and never computes one) and homes an explicit float return in S0/D0 +exactly like the fall-through epilogue. + +Also covered (found adversarially while clearing the float class): the WIDE +(i64) select hi-half SILENT miscompile — the narrow integer select moved only +the lo register, so `select` over i64 (or soft-float f64) values returned +val2's lo paired with val1's hi whenever cond == 0. `seli64` pins both halves +on cortex-m3 (soft-float) AND cortex-m7dp. + +Differential, unicorn (cortex-m7dp) vs wasmtime: + * sel32 / sel32b / clamp32 — strict BIT-exact compare (a select must + preserve NaN payloads exactly; no NaN leniency). + * sel64 / seli64 — strict bit-exact compare (both halves). + * ret32 / ret64 — NaN-lenient (they contain an fadd), non-NaN + bit-exact. +Honest capability gates pinned: on cortex-m3 (no FPU) the fns containing f32 +arithmetic (sel32b/clamp32/ret32/ret64) honest-skip while the pure value-pick +fns (sel32/sel64/seli64) lower soft-float and execute correctly; on +cortex-m4f (single-precision) the f64 fns honest-skip, the f32 fns lower. + +RED on origin/main: every function containing the float select / float +explicit return DECLINES (symbol missing) AND seli64 returns the wrong hi +half -> exit 1. GREEN after the fix. + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=/path/to/synth python scripts/repro/float_select_return_782_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 +from unicorn.arm_const import ( + UC_ARM_REG_D0, + UC_ARM_REG_D1, + UC_ARM_REG_LR, + UC_ARM_REG_R0, + UC_ARM_REG_R11, + UC_ARM_REG_S0, + UC_ARM_REG_S1, + 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("float_select_return_782.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") +MEMBASE = 0x20000000 # R11/fp linear-memory base at reset (cortex_m.rs) + + +def compile_elf(out, target): + r = subprocess.run( + [SYNTH, "compile", str(WAT), "-o", out, "-b", "arm", + "--target", target, "--all-exports"], + capture_output=True, text=True, env={"PATH": "/usr/bin:/bin"}, + ) + return r.returncode == 0, (r.stderr + r.stdout) + + +def load(elf): + f = ELFFile(open(elf, "rb")) + text = f.get_section_by_name(".text") + data, base = text.data(), text["sh_addr"] + syms = {} + for s in f.iter_sections(): + if s.header.sh_type == "SHT_SYMTAB": # #489: symtab, not disasm text + for sym in s.iter_symbols(): + if sym.name: + syms[sym.name] = sym["st_value"] + return data, base, syms + + +def f32_bits(x): + return struct.unpack("float32 +# exactly through the Python/wasmtime double boundary (no NaN payloads here; +# sel32b covers those via the i32-bits path). +F32_VALS = [0.0, -0.0, 1.5, -1.5, float("inf"), float("-inf"), 123.0, 0.25] + +F64_VALS = [0.0, -0.0, 1.5, -1.5, float("inf"), float("-inf"), 1e300, + 2.2250738585072014e-308] + +CONDS = [0, 1, 2, 0x80000000] + + +def run_seli64(text, base, addr, cond, a=0x2222222211111111, b=0x4444444433333333): + """i64 select: a in r0:r1, b in r2:r3, cond on the caller stack (AAPCS + 5th argument word). Returns the r1:r0 result as one 64-bit value.""" + from unicorn.arm_const import UC_ARM_REG_R1, UC_ARM_REG_R2, UC_ARM_REG_R3 + uc = new_uc(text, base) + uc.reg_write(UC_ARM_REG_SP, 0x38000 - 8) + uc.mem_write(0x38000 - 8, struct.pack("> 32) & 0xFFFFFFFF) + uc.reg_write(UC_ARM_REG_R2, b & 0xFFFFFFFF) + uc.reg_write(UC_ARM_REG_R3, (b >> 32) & 0xFFFFFFFF) + uc.reg_write(UC_ARM_REG_LR, 0x38000 | 1) + uc.emu_start(addr | 1, 0x38000, count=400) + from unicorn.arm_const import UC_ARM_REG_R1 as _R1 + return (uc.reg_read(_R1) << 32) | uc.reg_read(UC_ARM_REG_R0) + + +def main(): + elf = "/tmp/float_select_return_782_m7dp.elf" + + ok, log = compile_elf(elf, "cortex-m7dp") + if not ok: + print("RED: `synth compile -t cortex-m7dp` REJECTED the #782 fixture.") + print(log.strip()[:900]) + sys.exit(1) + + text, base, syms = load(elf) + store = wasmtime.Store(wasmtime.Engine()) + inst = wasmtime.Instance( + store, wasmtime.Module(store.engine, WAT.read_bytes()), []) + exp = inst.exports(store) + + fails = 0 + checked = 0 + + def fail(msg): + nonlocal fails + fails += 1 + print(" MISMATCH " + msg) + + def need(name): + if name not in syms: + fail(f"symbol '{name}' MISSING — function was skipped, not lowered") + return False + return True + + def to_i32(v): + return v - (1 << 32) if v >= 1 << 31 else v + + # ---- sel32: f32 params in S0/S1, cond in R0, result S0. STRICT bits. ---- + if need("sel32"): + for a in F32_VALS: + for b in F32_VALS[::-1]: + for c in CONDS: + uc = run(text, base, syms["sel32"], + s0=f32_bits(a), s1=f32_bits(b), r0=c) + got = uc.reg_read(UC_ARM_REG_S0) & 0xFFFFFFFF + want = f32_bits(exp["sel32"](store, a, b, to_i32(c))) + checked += 1 + if got != want: + fail(f"sel32({a}, {b}, {c:#x}) -> 0x{got:08x} != " + f"wasmtime 0x{want:08x}") + print(f"[sel32] {len(F32_VALS)**2 * len(CONDS)} cases bit-exact OK" + if fails == 0 else "[sel32] FAILURES above") + + # ---- sel32b: bit patterns through reinterpret — NaN payloads STRICT. ---- + pre = fails + if need("sel32b"): + from unicorn.arm_const import UC_ARM_REG_R1, UC_ARM_REG_R2 + for a in F32_EDGES: + for b in F32_EDGES[::-1]: + for c in (0, 1): + uc = new_uc(text, base) + uc.reg_write(UC_ARM_REG_R0, a) + uc.reg_write(UC_ARM_REG_R1, b) + uc.reg_write(UC_ARM_REG_R2, c) + uc.reg_write(UC_ARM_REG_LR, 0x38000 | 1) + uc.emu_start(syms["sel32b"] | 1, 0x38000, count=400) + got = uc.reg_read(UC_ARM_REG_R0) & 0xFFFFFFFF + want = exp["sel32b"](store, to_i32(a), to_i32(b), c) \ + & 0xFFFFFFFF + checked += 1 + if got != want: + fail(f"sel32b(0x{a:08x}, 0x{b:08x}, {c}) -> " + f"0x{got:08x} != wasmtime 0x{want:08x}") + if fails == pre: + print(f"[sel32b] {len(F32_EDGES)**2 * 2} NaN-payload-strict cases OK") + + # ---- clamp32: run-stabilization's clamp shape. ---- + pre = fails + if need("clamp32"): + for a in F32_VALS + [0.05, 0.1, 0.2]: + uc = run(text, base, syms["clamp32"], s0=f32_bits(a)) + got = uc.reg_read(UC_ARM_REG_S0) & 0xFFFFFFFF + want = f32_bits(exp["clamp32"](store, a)) + checked += 1 + if got != want: + fail(f"clamp32({a}) -> 0x{got:08x} != wasmtime 0x{want:08x}") + if fails == pre: + print(f"[clamp32] {len(F32_VALS) + 3} cases bit-exact OK") + + # ---- sel64: f64 params in D0/D1, cond R0, result D0. STRICT bits. ---- + pre = fails + if need("sel64"): + for a in F64_VALS: + for b in F64_VALS[::-1]: + for c in (0, 1, 2): + uc = run(text, base, syms["sel64"], + d0=f64_bits(a), d1=f64_bits(b), r0=c) + got = uc.reg_read(UC_ARM_REG_D0) & 0xFFFFFFFFFFFFFFFF + want = f64_bits(exp["sel64"](store, a, b, c)) + checked += 1 + if got != want: + fail(f"sel64({a}, {b}, {c}) -> 0x{got:016x} != " + f"wasmtime 0x{want:016x}") + if fails == pre: + print(f"[sel64] {len(F64_VALS)**2 * 3} cases bit-exact OK") + + # ---- ret32/ret64: explicit float return (NaN-lenient — contains fadd). -- + pre = fails + if need("ret32"): + for a in F32_VALS + [float("nan")]: + for c in (0, 1): + uc = run(text, base, syms["ret32"], s0=f32_bits(a), r0=c) + got = uc.reg_read(UC_ARM_REG_S0) & 0xFFFFFFFF + want = f32_bits(exp["ret32"](store, a, c)) + checked += 1 + if not f32_bits_eq_lenient(got, want): + fail(f"ret32({a}, {c}) -> 0x{got:08x} != " + f"wasmtime 0x{want:08x}") + if fails == pre: + print(f"[ret32] {(len(F32_VALS) + 1) * 2} cases OK") + + pre = fails + if need("ret64"): + for a in F64_VALS + [float("nan")]: + for c in (0, 1): + uc = run(text, base, syms["ret64"], d0=f64_bits(a), r0=c) + got = uc.reg_read(UC_ARM_REG_D0) & 0xFFFFFFFFFFFFFFFF + want = f64_bits(exp["ret64"](store, a, c)) + checked += 1 + if not f64_bits_eq_lenient(got, want): + fail(f"ret64({a}, {c}) -> 0x{got:016x} != " + f"wasmtime 0x{want:016x}") + if fails == pre: + print(f"[ret64] {(len(F64_VALS) + 1) * 2} cases OK") + + # ---- seli64 on m7dp: BOTH halves, both cond outcomes. STRICT. ---- + pre = fails + if need("seli64"): + for c in (0, 1, 7, 0x80000000): + got = run_seli64(text, base, syms["seli64"], c) + want = exp["seli64"](store, 0x2222222211111111, + 0x4444444433333333, to_i32(c)) \ + & 0xFFFFFFFFFFFFFFFF + checked += 1 + if got != want: + fail(f"seli64(cond={c:#x}) -> 0x{got:016x} != " + f"wasmtime 0x{want:016x} (hi-half drop?)") + if fails == pre: + print("[seli64/m7dp] both halves correct for all conds OK") + + # ---- m4f (single-precision): f32 fns compile, f64 fns honest-skip. ---- + elf_m4 = "/tmp/float_select_return_782_m4f.elf" + ok_m4, _ = compile_elf(elf_m4, "cortex-m4f") + if not ok_m4: + fail("cortex-m4f compile failed outright — f32 fns must still lower") + else: + _, _, syms_m4 = load(elf_m4) + for name in ("sel32", "sel32b", "clamp32", "ret32", "seli64"): + if name not in syms_m4: + fail(f"'{name}' missing on cortex-m4f — f32 select/return " + f"must lower on a single-precision FPU") + for name in ("sel64", "ret64"): + if name in syms_m4: + fail(f"'{name}' EMITTED on cortex-m4f — f64 must honest-skip " + f"on a single-precision FPU, never silently lower") + print("[m4f] f32 fns lower, f64 fns honest-skip OK") + + # ---- m3 (no FPU): f32-arithmetic fns honest-skip; the pure value-pick + # fns lower SOFT-float; seli64 executes with both halves correct (the + # pre-fix silent hi-half miscompile was live on every target). ---- + elf_m3 = "/tmp/float_select_return_782_m3.elf" + ok_m3, _ = compile_elf(elf_m3, "cortex-m3") + if not ok_m3: + fail("cortex-m3 compile failed outright — integer/soft-float value-" + "pick fns must still lower") + else: + text3, base3, syms_m3 = load(elf_m3) + for name in ("sel32b", "clamp32", "ret32", "ret64"): + if name in syms_m3: + fail(f"'{name}' EMITTED on cortex-m3 — f32/f64 arithmetic " + f"must honest-skip on a no-FPU target") + pre = fails + if "seli64" not in syms_m3: + fail("'seli64' missing on cortex-m3") + else: + for c in (0, 1, 7): + got = run_seli64(text3, base3, syms_m3["seli64"], c) + want = exp["seli64"](store, 0x2222222211111111, + 0x4444444433333333, c) \ + & 0xFFFFFFFFFFFFFFFF + checked += 1 + if got != want: + fail(f"seli64/m3(cond={c}) -> 0x{got:016x} != " + f"wasmtime 0x{want:016x} (hi-half drop?)") + if fails == pre: + print("[m3] f32 fns honest-skip; seli64 soft-float both halves OK") + + print(f"\n{checked} differential cases, {fails} failures") + if fails: + sys.exit(1) + print("GREEN: float select + explicit float return execute bit-identically " + "to wasmtime on cortex-m7dp; m3/m4f capability gates honest (#782b)") + + +if __name__ == "__main__": + main() From c0f508e38a4a419f82ca617322628bd5269b5991 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 08:04:38 +0200 Subject: [PATCH 3/3] ci(#782b): gate the float-select/return + wide-select oracle; fmt Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 13 +++++++++++++ crates/synth-synthesis/src/instruction_selector.rs | 8 ++++++-- 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c843f0e1..92a71de0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -479,6 +479,19 @@ jobs: # calls). - name: Run f64 const/promote/arith/compare/mem + across-call oracle (#369, m7dp) run: SYNTH=./target/debug/synth python scripts/repro/f64_369_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 + # (the clamp idiom) and `return` of an f32 result. Bit-exact (selects + # NaN-payload-STRICT — a select picks, never computes) vs wasmtime on + # m7dp; m3/m4f capability gates pinned. Also pins the WIDE (i64) select + # hi-half SILENT miscompile found adversarially (cond==0 returned val2's + # lo paired with val1's hi — soft-float f64 select rode the same path) + # and the hard-float SIGNATURE-only ABI hole (a float-signature function + # with no float op stayed on the float-naive optimized path: callers + # marshal S0/S1, the body read R0/R1). + - name: Run float select + explicit float return oracle (#782b, m7dp+m3) + run: SYNTH=./target/debug/synth python scripts/repro/float_select_return_782_differential.py # #739: static ABOVE sp_init under --shadow-stack-size — the sub-word # load/store arms previously BAKED the linmem offset as an un-relocated # MOVW/MOVT immediate (invisible to the #678 reloc-walking rebase AND to diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index b4a36f26..a225ca25 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -12584,7 +12584,9 @@ impl InstructionSelector { ))); } } - if self.ret_f64 && let Some(dreg) = ret_top_f64 { + if self.ret_f64 + && let Some(dreg) = ret_top_f64 + { // Home to D0 via the core round-trip (bit-exact; no // D→D move in the ArmOp set). R0/R1 are dead at the // return of an f64-returning function. @@ -12610,7 +12612,9 @@ impl InstructionSelector { } stack.pop(); free_vfp_dtemp(&mut vfp_used, &vfp_home, dreg); - } else if self.ret_f32 && let Some(sreg) = ret_top_f32 { + } else if self.ret_f32 + && let Some(sreg) = ret_top_f32 + { // Home to S0 via the R12 (IP scratch) round-trip. if vfp_s_index(sreg) != Some(0) { instructions.push(ArmInstruction {