Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
27 changes: 27 additions & 0 deletions crates/synth-backend/src/arm_backend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading
Loading