feat(f32): op-completeness for falcon — store/abs/neg/copysign + AAPCS-VFP mixed params (#719)#721
Merged
Conversation
…umb-2 VFP) Lands the falcon f32 residual left after #708 (load + reinterpret) — the ops on which falcon's float functions were skipping next (#369/#242 GI-FPU-002 phase 1b): * f32.store — decoded + lowered as the VFP-store twin of f32.load: VMOV the S-register value into a core register (reinterpret) and reuse the PROVEN i32.store address path (generate_store_with_bounds_ check). Symmetric #359/#237 static-data honest-declines. * f32.abs / f32.neg — VABS.F32 / VNEG.F32 (sign-bit edits, bit-exact on ±0.0/NaN/±inf). * f32.copysign — the sign-bit splice, sn=magnitude / sm=sign (wasm operand order [a,b], b on top). * f32 local.set/tee — VFP home write-back: copy the top-of-stack f32 into the local's stable, pinned home S-register (bit-exact via the core reinterpret round-trip; the phase-1 ArmOp set has no VMOV.F32). Also fixes a latent Thumb-2 copysign encoder bug: the sign-mask AND/BIC emitted the modified immediate #0x00020002 instead of #0x80000000 (wrong imm3/imm8), so copysign spliced bits 17+1 instead of the sign bit. Never execution- differentiated until now; the A32 encoder (different immediate scheme) was correct. All four ops honest-reject on cortex-m3 (no FPU) and on -b riscv/ -b aarch64 (no panic). Refs #719 #369 #242 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Generalizes the pure-f32 param homing to interleaved signatures. Under the AAPCS-VFP (hard-float) convention f32 args are passed in the INDEPENDENT VFP argument pool (S0,S1,…) and consume no core register or NSAA stack slot, so the core-register walk must skip them: `aapcs_param_layout` (and, through it, `compute_local_layout`'s param_slots/incoming_params) gains a `params_f32` arg and `continue`s past each f32 param. `(f32, i32)` therefore maps the i32 to R0, not R1. The f32-home seed already assigned S(k) from the VFP pool independently, so removing the mixed-param decline is all that remains. Empty `params_f32` (every integer module + all existing callers) ⇒ no skips ⇒ byte-identical layout — frozen anchors 10/10 and the #619/#708/#709 pure-f32 differentials stay green. f32-across-a-call is still declined loudly this round (S0..S15 caller-saved spill/rehome is the next increment). Refs #719 #369 #242 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…tests
Adds scripts/repro/f32_ops_719{.wat,_differential.py}: a symtab-based unicorn
(cortex-m4f) vs wasmtime bit-exact oracle over the whole #719 residual —
f32.store, abs/neg/copysign (with the ±0.0/NaN-sign/±inf sign edges),
local.set/tee, and mixed f32/int AAPCS-VFP params (incl. the `(f32,i32)`
i32-in-R0 discriminator, R1 poisoned). 156/156 bit-exact; cortex-m3 honest-reject
confirmed. Wired into the ci.yml trap-semantics-oracle job, alongside a
now-wired #708/#709 step (the load/reinterpret/trunc-trap oracle was previously
unwired).
Selector unit tests: test_719_aapcs_vfp_mixed_param_pools pins the independent
core/VFP argument pools (the `(f32,i32)`→R0 discriminator), and
test_719_f32_with_call_declines_loudly pins the honest f32-across-call decline.
Refs #719 #369 #242
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Closes most of #719 — the falcon f32 op residual after v0.40.0's #708 (f32.load + reinterpret). Falcon's float functions now skip on the next unsupported f32 op; this lands the scalar + calling-convention set.
Landed (all bit-exact vs wasmtime)
f32.storeVMOV Rn,Sn+ proven i32.store address pathf32.absVABS.F32f32.negVNEG.F32f32.copysignf32.local.set/teef32/intparams(param i32 f32)→ i32 in R0, f32 in S0; both orderingsDeclined (loud, never silent)
S0..S15caller-saved): declines with"f32 in a function with a call is not yet lowered (S0..S15 are caller-saved) — declining"; the function is skipped, absent from the ELF — not a silent miscompile. This is the ~2-function residual; the spill/rehome-across-bllane is a clean follow-up.Gate
scripts/repro/f32_ops_719_differential.py+f32_ops_719.wat: 156/156 bit-exact vs wasmtime on cortex-m4f (store incl. sign edge cases, abs/neg/copysign, local.set/tee, mixed params both orderings, mix_store, mix_add). Wired into CI (trap-semantics-oraclejob).-b riscv/-b aarch64honest-reject the newly-decoded ops.Note: this branch and #720 both touch
ci.yml(each adds an f32 oracle step) — expect a trivial union merge; keep both steps.🤖 Generated with Claude Code