Fix FMA sign handling in float_bvt for infinity and zero results#8985
Fix FMA sign handling in float_bvt for infinity and zero results#8985tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
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) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.
| // Zero: result is zero when fraction is zero and not inf/NaN | ||
| result.zero = and_exprt( | ||
| not_exprt(or_exprt(result.infinity, result.NaN)), | ||
| equal_exprt(result.fraction, from_integer(0, result.fraction.type()))); |
There was a problem hiding this comment.
result.zero is being (re)derived solely from result.fraction == 0. If result.fraction is not a complete “value is zero” indicator at this stage (e.g., if the representation allows non-zero values with a zero fraction field, or if rounder/packing logic expects result.zero to be computed differently), this can misclassify non-zero values as zero and affect both sign selection and downstream handling in rounder. Consider: (1) using the existing zero classification already maintained by the unpacking/addition pipeline (if available), or (2) computing a local is_zero_result predicate for sign selection without assigning to result.zero, leaving result.zero to be set by the established canonical logic.
| // Sign for zero: under round-to-minus-inf, +0 + (-0) = -0 | ||
| const rounding_mode_bitst rounding_mode_bits(rm); | ||
| exprt zero_sign = if_exprt( | ||
| rounding_mode_bits.round_to_minus_inf, | ||
| or_exprt(prod_sign, unpacked_add.sign), | ||
| and_exprt(prod_sign, unpacked_add.sign)); |
There was a problem hiding this comment.
The PR description mentions zero-sign handling (round-to-minus-inf signed-zero convention), but the added regression test only covers infinity-result sign selection. Please add a regression case that forces an exact-zero FMA result and checks the sign across rounding modes—at minimum ROUND_TO_MINUS_INF vs a non-minus-inf mode—to ensure this new branch is exercised in both --floatbv and SMT runs.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8985 +/- ##
===========================================
+ Coverage 80.50% 80.51% +0.01%
===========================================
Files 1704 1704
Lines 188796 188805 +9
Branches 73 73
===========================================
+ Hits 151993 152024 +31
+ Misses 36803 36781 -22 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
float_bvt::fma always set the sign to the add/sub sign, ignoring special cases. Added proper sign selection: