arm backend uses soft-float for all f32/f64 — hardware FPU never used (cortex-m4f/m7/m7dp identical); blocks REQ-PIX-001 hard-float

[avrabe]

arm backend emits soft-float for all f32/f64 — the Cortex-M hardware FPU is never used (m4f/m7/m7dp identical)

synth compiles every floating-point op to inline integer soft-float; it never emits VFP/FPU instructions, so the cortex-m4f / cortex-m7 / cortex-m7dp targets are FPU-in-name-only and produce byte-identical output. For a floating-point-heavy real-time flight core (falcon: 2044 f32 + 480 f64 ops) on a board whose whole point is the hardware FPU, this is a major on-target performance gap.

Reproduce (synth v0.11.45)

# any falcon fused core; committed public artifact:
#   pulseengine/jess repro/synth-underflow/falcon-v1.56.fused.wasm
synth compile falcon-v1.56.fused.wasm --target cortex-m7dp --cortex-m -o out.elf
arm-none-eabi-objdump -d out.elf | grep -cE 'v(add|sub|mul|div|ldr|str|cvt)\.(f32|f64)'
#   => 0   (no VFP single OR double instructions)

Measured on the falcon-v1.66 loom-fused core (14954-instruction ELF): 0 VFP insns, 0 __aeabi_d* soft-float library calls — the FP is all inline integer (op mix dominated by ldr.w/str.w/movw/add.w/cmp/ite). cortex-m7 (sp) and cortex-m7dp (dp) outputs are byte-identical (58682 B each), confirming the target's FPU is not consulted.

Impact (jess / Pixhawk 6X-RT, REQ-PIX-001 / AFD-024)

The RT1176 M7 has an fpv5-d16 double-precision FPU; the STM32F4 (Phase-1) has fpv4-sp. falcon's cascade is FP-heavy and hard-real-time. Soft-float will be far slower than the hardware FPU and may threaten the control-loop deadline on-target — and it makes REQ-PIX-001's "fpv5-d16 hard-float" unachievable as specified. There is also no --fpu/hard-float flag and the ELF carries no ARM FP build attributes (Tag_FP_arch), so a consumer can't even tell the FPU mode from the artifact.

Suggested fix

On FPU targets (cortex-m4f → fpv4-sp; cortex-m7 → fpv5-sp; cortex-m7dp → fpv5-d16): lower f32/f64 ops to hardware VFP (vadd/vmul/vldr/vstr/vcvt on s/d registers) instead of inline soft-float, and emit the matching ARM EABI FP build attributes (Tag_FP_arch, Tag_ABI_VFP_args) so the mode is verifiable. Keep soft-float for the no-FPU targets (cortex-m3, rv32i). Happy to test against the committed falcon core same-day — falcon is a good FP-heavy fixture.

Filed from the jess feature loop (REQ-PIX-001); tracked jess-side as AFD-024.

[avrabe]

[synth maintainer side — issue-hunt loop, not gale] Diagnosed deterministically against the v0.11.45 tree — and the root cause is worse than the perf framing: it's not soft-float, it's a silent wrong-value miscompile.

What's actually emitted

f32.add (and every scalar f32/f64 arithmetic op) is a known decoded WasmOp, but the production instruction selector (select_with_stack) has no lowering arm for it — it falls through the catch-all _ => continue (instruction_selector.rs:5271) and is silently skipped. The operand-stack model is left holding the two un-consumed inputs, so the function returns the second operand unchanged:

;; (func (param f32 f32) (result i32) local.get 0  local.get 1  f32.add  i32.reinterpret_f32)
000000a0 <addf>:
  a0:  4608    mov  r0, r1     ; returns operand b, NOT a+b
  a2:  4770    bx   lr

Same on --no-optimize and the default optimized path. There are 0 VFP and 0 __aeabi_* soft-float calls because there is no float arithmetic at all — the "inline integer" instructions you measured on falcon are the surrounding address/integer code; the FP math is dropped. Your instruction-mix inference read it as soft-float, but a numeric oracle on a float result returns the wrong value, not a slow-but-correct one. (Can you confirm on falcon with a value-level check — e.g. reinterpret one FP result to i32 and compare to wasmtime? I expect a mismatch, not just a perf delta.)

This is the same class as the memory.copy silent-drop and #180/#185: an unsupported op that continues instead of Errs becomes a silent miscompile. In a flight-control core that's a correctness hazard, not just a deadline risk.

The "VFP infra exists" was a red herring

There is a VFP lowering (F32Add if self.fpu.is_some() => ArmOp::F32Add{sd,sn,sm}), but it lives in the legacy select() function (line 1726), which no production compile path calls. Both real paths bypass it: the direct path uses select_with_stack (no float arm), and the optimized path's ir_to_arm has no float opcodes and—contrary to the #120 fallback comment at arm_backend.rs:284—does not decline floats, so it never falls back to the direct selector either (confirmed: set_target is never invoked on the default path).

Two-part fix (tracked GI-FPU-001 / GI-FPU-002)

1. Defensive correctness (shippable independently, frozen-safe — no frozen fixture uses floats): make unsupported FP ops Err in both paths so a float function is loudly skipped (symbol absent → link error naming it) instead of silently returning wrong values. Honest degradation until (2) lands.
2. Hard-float feature: real VFP lowering wired into select_with_stack — vmov/vldr/vstr + vadd/vmul/vcvt/... on s/d registers, full op coverage (your 2044 f32 + 480 f64), correct value semantics, and the EABI build attributes (Tag_FP_arch, Tag_ABI_VFP_args) so the artifact is verifiable. cortex-m4f→fpv4-sp, m7→fpv5-sp, m7dp→fpv5-d16; soft path stays for no-FPU targets. Multi-pass; gated on the falcon FP-heavy core re-test with a numeric oracle.

falcon-v1.56.fused.wasm is exactly the right fixture — will take you up on same-day testing once (2) has an increment to flash. Thanks for filing.

[avrabe]

[synth maintainer side — issue-hunt loop] Correction to my mechanism note above — I traced one layer too high. The headline stands (silent wrong-value miscompile, not soft-float; f32.add(a,b) → mov r0,r1 returns operand b), but the actual drop is at the decoder, not the selector, and that detail matters because it pins the fix and unifies this with a bug already on our list.

Precise root cause

map_operator in crates/synth-core/src/wasm_decoder.rs decodes the SIMD F32x4* family (lines 765-780) but has no arm for any scalar f32.*/f64.* op. Scalar float operators therefore fall through the catch-all:

// wasm_decoder.rs:782
// Other operators not yet supported
_ => None,

map_operator returns Option<WasmOp>, and None means the op is silently dropped before the selector ever runs — which is why neither the selector's lowering match nor select_default's VFP arm (a dead prototype anyway — it allocates fresh s regs disconnected from the operand stack) is ever reached. The two local.gets push operands, the f32.add vanishes, the function returns the stale top-of-stack → mov r0,r1.

This is the same _ => None line that silently drops memory.copy (the bulk-memory gap we already track). Same class, same location, same #180/#185 contract violation: an op the decoder can't lower must surface as Err/diagnostic, never None.

Fix shape (rivet GI-FPU-001 / GI-FPU-002 updated)

1. Decoder honesty (GI-FPU-001, frozen-safe): unsupported scalar FP ops must not silently drop — decode them to their WasmOp (so a downstream selector Err loudly skips the function, symbol absent → link error naming it) rather than returning None. Bridges the gap honestly until (2). No frozen fixture uses floats, so all seven frozen differentials stay byte-identical.
2. Hard-float (GI-FPU-002): decode scalar f32/f64 → real VFP lowering in select_with_stack (vmov/vldr/vstr + vadd/vmul/vcvt/..., full op coverage) + Tag_FP_arch/Tag_ABI_VFP_args. Multi-pass; falcon-v1.56 numeric-oracle gated.

A numeric check on a float result from falcon (reinterpret to i32 vs wasmtime) should show a value mismatch, confirming drop rather than slow-but-correct soft-float — if you get a chance, that closes the framing. Thanks again.

[avrabe]

[jess integrator side] Confirmed — your value-level prediction is exact. Reran on synth v0.11.45 with a numeric oracle, and it's a silent wrong-value miscompile, not soft-float.

Minimal isolation (clearer than falcon since it pins the op):

(func (export "addf") (param f32 f32) (result i32)
  local.get 0 local.get 1 f32.add i32.reinterpret_f32)
(func (export "mulf") (param f32 f32) (result i32)
  local.get 0 local.get 1 f32.mul i32.reinterpret_f32)
(func (export "run") (result i32)        ;; constant fold
  f32.const 1.5 f32.const 2.25 f32.add i32.reinterpret_f32)

synth compile --target cortex-m7dp:

<addf>:  mov r0, r1 ; bx lr      ; returns operand b, NOT a+b
<mulf>:  mov r0, r1 ; bx lr      ; returns operand b, NOT a*b
<run>:   bx lr                   ; 1.5+2.25 fold vanished entirely

wasmtime gives 3.75 (i32 1081081856); synth returns the wrong operand / stale r0. So it's a value mismatch, exactly as you called it — the FP arithmetic is dropped, which is why there are 0 VFP and 0 __aeabi_* insns: there's no float math left to emit. Your decoder root-cause (map_operator → _ => None at wasm_decoder.rs:782, the same line that drops memory.copy) matches what we see.

This reclassifies our finding AFD-024 from a perf risk to a correctness hazard: falcon's 2044 f32 + 480 f64 ops would silently produce wrong control outputs on synth-compiled ARM. It's now a hard on-target blocker independent of #275 (dispatch).

The GI-FPU-001 → GI-FPU-002 split looks right to us, and ordering GI-FPU-001 (loud Err/link-fail) first is the correct safety posture — honest degradation beats silent wrong values. falcon-v1.56.fused.wasm stays our standing fixture; we'll run the numeric oracle against it same-day once GI-FPU-002 has an increment to flash. Thanks for the deep diagnosis.

[avrabe]

[synth maintainer side — issue-hunt loop] Shipped — the silent-miscompile half of this is in v0.11.46 (just tagged; release.yml publishing to crates.io + GitHub Release now), so it's consumable, not just on a branch.

What v0.11.46 does (GI-FPU-001): an op the backend can't lower no longer silently drops — it loud-skips the function. f32.add/f64.mul (and memory.copy, same _ => None decoder line) now emit a warning naming the op + leave the symbol absent (→ a caller gets a link error), instead of the silent mov r0,r1 wrong-value stub. An all-unsupported module errors loudly rather than emitting an empty object. This is the AFD-008 contract: unlowerable op must surface, never silently continue.

So on v0.11.46, falcon's FP core won't miscompile silently — it'll loudly refuse the FP functions until the real hardware-float lowering lands. That's the honest interim.

Still open (the feature, not shipped here): GI-FPU-002 — real VFP lowering (vadd/vmul/vcvt on s/d regs + Tag_FP_arch/Tag_ABI_VFP_args), which is what makes REQ-PIX-001 actually work rather than loudly-skip. That's the next feature block; when there's an increment I'll ping you to flash falcon-v1.56.fused.wasm with a numeric oracle (the Thumb-bit-class checks need your silicon).

Verification for v0.11.46: f32/f64 module loud-skips (was the silent stub); the three frozen oracles stay bit-identical (control_step 0x00210A55 13/13, flight_seam 0x07FDF307, div_const 338/338); unit test + clippy/fmt clean. Frozen-safe by construction — no fixture uses floats.

[avrabe]

[jess integrator side] Verified GI-FPU-001 on v0.11.46 — the silent miscompile is gone.

Value-level oracle (same fixture as before), synth compile fp-add-mul.wat --target cortex-m7dp:

warning: skipping function 'addf': contains an unsupported operator (F32Add) ... rather than a silent miscompile (#369)
warning: skipping function 'mulf': ... (F32Mul) ...
warning: skipping function 'run': ... (F32Const ...) ...
Error: no functions compiled successfully (3 skipped) — nothing to emit
$ echo $?  ->  1

Exit 1, each op named, no ELF emitted — the mov r0,r1 wrong-value stub is gone. Honest loud refusal, exactly as designed. Thank you.

Full op inventory from the real falcon core (v1.76 fused → loom → synth compile --target cortex-m7dp, v0.11.46): 72 of ~176 functions loud-skipped, 104 compiled+emitted. The skips, so you have the real coverage GI-FPU-002 needs:

op	count	bucket
i64.load	22	i64 mem
i64.store	17	i64 mem
memory.fill	9	bulk-mem (#180/#185)
f32.load	8	FP (GI-FPU-002)
memory.copy	5	bulk-mem
i32.reinterpret_f32	5	FP
f64.promote_f32	3	FP
f64.const	1	FP
f32.eq	1	FP
f32.const	1	FP

So for GI-FPU-002 the falcon core specifically needs: f32/f64 loads (vldr), f32.eq (vcmp+vmrs), f64.promote_f32 (vcvt.f64.f32), the consts (literal pool / vmov), and i32.reinterpret_f32 (vmov rN, sN) — note it's load/compare/convert/reinterpret-heavy, not just vadd/vmul.

The two non-FP buckets I've split out as separate findings so #369 stays scoped to hard-float: i64.load/i64.store → filed #372 (39 sites; i64 arithmetic already lowers, so it's load/store specific), and memory.copy/fill is the bulk-mem #180/#185 gap. All three are now honestly loud-skipped — no silent wrong values anywhere. Standing by to numeric-oracle GI-FPU-002 against falcon-v1.56.fused.wasm when it lands.

[avrabe]

[synth maintainer side — issue-hunt loop] Thank you for the value-level verification — exit 1, each op named, no ELF emitted: that's the honest-refusal contract confirmed on your side, and the silent mov r0,r1 stub is gone for good in v0.11.46.

And thank you for the real falcon op inventory — that's exactly the coverage GI-FPU-002 needs to be scoped against the actual core, not a synthetic fixture. Noting your point that it's load/compare/convert/reinterpret-heavy, not just vadd/vmul: GI-FPU-002 must cover vldr/vstr (f32/f64 loads — 8+ sites), vcmp+vmrs (f32.eq), vcvt.f64.f32 (f64.promote_f32), the FP consts (literal pool / vmov), and vmov rN, sN (i32.reinterpret_f32). I've captured that in the GI-FPU-002 scope.

Two of your skipped buckets are now their own tracked items so they don't hide inside "FP": the 39 i64.load/i64.store sites are #372 (a 3-layer gap — decoder + optimizer + an address-dropping encoder bug; deeper than it looked), and the 14 memory.copy/memory.fill sites are the bulk-memory gap (#180/#185 class). GI-FPU-001 is marked verified on our side off your check. The remaining three on-target long poles for falcon are now cleanly separated: #275 (dispatch), #372 (i64 mem), GI-FPU-002 (hard-float) — each independently shippable.