test(f32): gate all six f32 comparisons + CI-wire f32 soundness oracles (#712)#720
Merged
Merged
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
… f32 oracles (#712) #712 reported all six f32 comparisons returning value-independent wrong results on cortex-m4f — the MOVS-after-VMRS flag clobber. Already FIXED in v0.40.0 (#716), but #712 exposed a gate gap: the #619 harness only exercised flt/fgt, so eq/ne/le/ge were fixed-but-ungated (the same vacuous-harness pattern that let the bug ship). Verified on v0.40.0: disasm shows movs #0 precedes vcmp/vmrs for all six (correct condition codes), extended harness 84/84 bit-exact vs wasmtime. Also CI-wired the f32 soundness oracles (619 compares + 708/709 trunc/load/ reinterpret) in the trap-semantics-oracle job — dev-only before, the exact gap that let #709 + #712 ship. Unioned with #719's f32_ops oracle (all three run). CI surfaced (and this fixes) a pre-existing harness fragility the dev run missed: f32.div(-0.0,0.0) is NaN, and WASM leaves a NaN result's sign/payload NON-DETERMINISTIC (§4.3.3) — ARM's DefaultNaN 0x7fc00000 vs a wasmtime build's 0xffc00000, both valid qNaNs. A bit-exact NaN compare is over-specified and version-dependent. f32_bits_eq now treats NaN==NaN regardless of bits while keeping every non-NaN result bit-exact (signed zero / ±inf still can't slip). Closes #712. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
avrabe
force-pushed
the
fix/712-f32-compare-oracle-all-six
branch
from
eec46f1 to
e4a498e
Compare
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
#712 reported all six f32 comparisons returning value-independent wrong results (the
MOVS-after-VMRSflag clobber). That bug was already fixed in v0.40.0 (#716) — but #712 exposed a gate gap: the #619 harness only exercisedflt/fgt, soeq/ne/le/gewere fixed-but-ungated. This is the same vacuous-harness pattern that let the bug ship in v0.39.0.Verification (v0.40.0)
movs #0now precedesvcmp/vmrs, correct condition codes (eq→EQ, ne→NE, lt→MI, gt→GT, le→LS, ge→GE).Change
f32_vfp_619.wat: addfeq/fne/fle/fge.f32_vfp_619_differential.py:CMP_F32= all six.ci.yml: CI-gate the f32 soundness oracles (619 compares + 708/709 trunc/load/reinterpret) in thetrap-semantics-oraclejob. They were dev-only before — the exact gap that let thumb-2 f32: i32.trunc_f32_s/u silently saturate instead of trapping on NaN/Inf/out-of-range (bare VCVT, no guard) — WASM Core §4.3.3 soundness bug #709 + thumb-2 f32: all six f32 comparisons (eq/ne/lt/gt/le/ge) return value-independent wrong results on cortex-m4f — flag-setting MOVS clobbers N/Z after VMRS (silent miscompile) #712 ship. f32 soundness is now enforced on every PR.No production code changed (test/oracle + CI only); frozen anchors untouched. Closes #712.
🤖 Generated with Claude Code