Fix FMA sign handling in float_bvt for infinity and zero results#8985
Open
tautschnig wants to merge 3 commits into
Open
Fix FMA sign handling in float_bvt for infinity and zero results#8985tautschnig wants to merge 3 commits into
tautschnig wants to merge 3 commits into
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
Fixes incorrect sign selection in float_bvt::fma results by choosing the sign based on whether the final result is infinity, zero, or a normal value, and adds a regression test focused on infinity-sign behavior.
Changes:
- Update
float_bvt::fmato select the result sign differently for infinity and zero outcomes. - Introduce a regression test (
Float-fma-sign) for infinity-result sign handling in both bitvector and SMT modes.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| src/solvers/floatbv/float_bv.cpp | Adjusts FMA result sign selection for infinity and zero outcomes. |
| regression/cbmc/Float-fma-sign/main.c | Adds regression assertions for infinity sign behavior using __CPROVER_fmaf. |
| regression/cbmc/Float-fma-sign/test.desc | Runs the new regression under --floatbv. |
| regression/cbmc/Float-fma-sign/test_smt.desc | Runs the new regression under SMT (--smt2 --z3). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8985 +/- ##
========================================
Coverage 80.60% 80.60%
========================================
Files 1711 1711
Lines 189454 189463 +9
Branches 73 73
========================================
+ Hits 152700 152717 +17
+ Misses 36754 36746 -8 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
fix-fma-sign
branch
2 times, most recently
from
96d7430 to
a8a81f4
Compare
Collaborator
|
Should the test check those floating-point status flags? |
… isinf
The fma/fmaf/fmal wrappers in src/ansi-c/library/math.c previously
raised FE_INVALID for any infinite addend, regardless of whether the
product was also infinite or not. IEEE-754 §7.2 only requires
FE_INVALID in two cases:
- the product is undefined: 0 * inf or inf * 0; and
- the product is infinite (one factor infinite, neither factor zero)
and the addend is infinite with the opposite sign -- the inf - inf
subcase.
Plain finite_nonzero * finite_nonzero + (+/-inf) is exact and raises
no flag; the previous wrapper rejected such inputs as a verification
failure, forcing tests to call __CPROVER_fma{,f,l} directly to bypass
the wrapper. Tighten the second branch to the actual inf - inf check:
the addend must be infinite, at least one factor must be infinite (so
the product is infinite, since the 0 * inf case is peeled off above),
and the product's sign (signbit(x) XOR signbit(y)) must oppose the
addend's sign.
Drive-by portability fix: switch fmaf and fmal from the typed
isinff()/isinfl() forms to the C99 type-generic isinf() macro. Some
<math.h> headers (e.g. macOS-14 arm64) only expose the generic form,
on which CBMC's library-load step otherwise warned that 'isinff' is
not declared and fell back to an implicit int(...) signature
conflicting with the actual model. fma() (double) was already using
the portable form; fmaf and fmal now match.
This lets the FMA-sign tests in the next commit go through plain fmaf
in every scenario, which gives free coverage of the wrapper's flag
handling per IEEE-754.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Collaborator
Author
Added a60aabd to make this genuinely possible. We would previously have had spurious (as far as the standard prescribes them) flag setting. |
float_bvt::fma always set the sign to the add/sub sign, ignoring
special cases. Added proper sign selection:
- Infinity: use product sign if product is inf, else addend sign
- Zero: respect ROUND_TO_MINUS_INF sign convention for signed zeros
- Normal: use the add/sub sign (unchanged)
The shape of the new sign computation mirrors float_bvt::add_sub
(rounding_mode_bitst, infinity_sign / zero_sign, the three-way
if_exprt selection on result.infinity / result.zero, and the
rederivation of result.zero from result.fraction == 0). The two
copies are now identical in shape, so a 'keep in sync' note is
added in the FMA block; extracting a shared helper covering both
add/sub and FMA is a sensible follow-up.
Regression test exercises both the infinity sign branch and the
zero sign branch using plain fmaf(): the preceding commit tightened
the library wrapper so that finite_nonzero*finite_nonzero +
(+/-inf) and inf*finite_nonzero + same-signed-inf no longer trigger
spurious FE_INVALID assertions, which means all four infinity
cases and all eight zero-cancellation cases can call fmaf directly.
Going through the wrapper additionally validates its IEEE-754 flag
handling: none of these inputs are an inf - inf, so no FE_INVALID
should be raised, and the test would fail if a regression
re-introduced the over-approximation.
Without the fix, the regression test catches three counterexamples
on develop: the (+inf)*(-3)+100 case, the 2*3+(-inf) case, and
the FE_DOWNWARD exact-cancellation zero case.
The regression test is tagged broken-cprover-smt-backend: the
cbmc-cprover-smt2 backend reproducibly aborts on this test on
macOS-14 arm64 with an INVARIANT violation in
smt2_conv.cpp::flatten2bv ("floatbv expressions should be
flattened when using FPA theory"), but the same invocation
succeeds on Linux x86_64. The abort happens in the conversion
phase before any solver call. The cprover-smt2 backend hits the
same INVARIANT class on multiple existing Float-* tests
(Float-flags-{no-,}simp1, Float-no-simp{5,9}, Float-zero-sum1),
all of which carry the same tag. Investigating the macOS arm64
specific behaviour is out of scope for this fix.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
On the cbmc-paths-lifo-CORE profile (--paths lifo), the regression test added in the previous commit times out on the macOS-14 cmake-clang CI runner: the runner uses cadical and arm64, and SAT solving on the test's formula under --paths lifo regularly exceeds the 1200 s profile budget, causing the whole profile to time out. The same invocation completes in under a second on Linux x86_64 (with both minisat and cadical), so this is a platform-specific solver-time issue rather than a CBMC regression. The conventional fix in this codebase is to tag tests in this situation 'thorough-paths', which excludes them from cbmc-paths-lifo-CORE while keeping them in the regular cbmc-CORE run. Several existing Float-* tests that share the broken-cprover-smt-backend tag already do this for the same reason, e.g. Float-flags-no-simp1 and Float-no-simp9. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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
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.
Depends-on: #9020
float_bvt::fma always set the sign to the add/sub sign, ignoring special cases. Added proper sign selection: