Fix division exponent overflow and overflow-to-inf ROUND_TO_AWAY#8984
Open
tautschnig wants to merge 1 commit into
Open
Fix division exponent overflow and overflow-to-inf ROUND_TO_AWAY#8984tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit 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 float division/rounding overflow behavior to match IEEE-style expectations, preventing exponent wraparound and ensuring overflow-to-infinity occurs under all round-to-nearest modes.
Changes:
- Widen exponent arithmetic in
float_bvt::divfromspec.e+1tospec.e+2to prevent wraparound on large quotients. - Treat
ROUND_TO_AWAYas overflow-to-infinity inround_exponent(bothfloat_utilstandfloat_bvt). - Add a regression test covering division overflow behavior under directed rounding (including SMT path).
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
| src/solvers/floatbv/float_utils.cpp | Updates overflow-to-inf condition to include round_to_away. |
| src/solvers/floatbv/float_bv.cpp | Widens exponent casts for division and updates overflow-to-inf condition for round_to_away. |
| regression/cbmc/Float-div-overflow/test.desc | Adds a FloatBV regression test driver for division overflow rounding behavior. |
| regression/cbmc/Float-div-overflow/test_smt.desc | Adds an SMT2/Z3 variant of the same regression. |
| regression/cbmc/Float-div-overflow/main.c | Implements the regression assertions for overflow behavior under multiple rounding modes. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+21
to
+39
| // ROUND_TO_EVEN: overflow -> +inf | ||
| __CPROVER_rounding_mode = 0; | ||
| float r0 = a / b; | ||
| assert(isinf(r0) && r0 > 0); | ||
|
|
||
| // ROUND_TO_ZERO: overflow, directed toward zero -> FLT_MAX | ||
| __CPROVER_rounding_mode = 3; | ||
| float r3 = a / b; | ||
| assert(r3 == FLT_MAX); | ||
|
|
||
| // ROUND_TO_PLUS_INF: positive overflow, directed toward +inf -> +inf | ||
| __CPROVER_rounding_mode = 2; | ||
| float r2 = a / b; | ||
| assert(isinf(r2) && r2 > 0); | ||
|
|
||
| // ROUND_TO_MINUS_INF: positive overflow, directed toward -inf -> FLT_MAX | ||
| __CPROVER_rounding_mode = 1; | ||
| float r1 = a / b; | ||
| assert(r1 == FLT_MAX); |
Comment on lines
+1287
to
+1295
| // Directed rounding modes round overflow to the maximum normal | ||
| // depending on the particular mode and the sign | ||
| literalt overflow_to_inf= | ||
| prop.lor(rounding_mode_bits.round_to_even, | ||
| prop.lor(prop.land(rounding_mode_bits.round_to_plus_inf, | ||
| !result.sign), | ||
| prop.land(rounding_mode_bits.round_to_minus_inf, | ||
| result.sign))); | ||
| literalt overflow_to_inf = prop.lor( | ||
| rounding_mode_bits.round_to_even, | ||
| prop.lor( | ||
| rounding_mode_bits.round_to_away, | ||
| prop.lor( | ||
| prop.land(rounding_mode_bits.round_to_plus_inf, !result.sign), | ||
| prop.land(rounding_mode_bits.round_to_minus_inf, result.sign)))); |
|
|
||
| // We will subtract the exponents; | ||
| // to account for overflow, we add a bit. | ||
| // we add a second bit for the adjust by extra fraction bits |
Comment on lines
+21
to
+22
| // ROUND_TO_EVEN: overflow -> +inf | ||
| __CPROVER_rounding_mode = 0; |
Comment on lines
+26
to
+27
| // ROUND_TO_ZERO: overflow, directed toward zero -> FLT_MAX | ||
| __CPROVER_rounding_mode = 3; |
Comment on lines
+31
to
+32
| // ROUND_TO_PLUS_INF: positive overflow, directed toward +inf -> +inf | ||
| __CPROVER_rounding_mode = 2; |
Comment on lines
+36
to
+37
| // ROUND_TO_MINUS_INF: positive overflow, directed toward -inf -> FLT_MAX | ||
| __CPROVER_rounding_mode = 1; |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8984 +/- ##
===========================================
+ Coverage 80.59% 80.62% +0.03%
===========================================
Files 1711 1711
Lines 189454 189456 +2
Branches 73 73
===========================================
+ Hits 152697 152757 +60
+ Misses 36757 36699 -58 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Two fixes: 1. float_bvt::div: exponent extended by only 1 bit (spec.e+1) instead of 2 (spec.e+2), so the post-+spec.f adjustment was vulnerable to silent wraparound on large quotients. The fix brings float_bvt::div into agreement with float_utilst::div (which has used +2 since 2017) and with float_bvt::mul. 2. round_exponent in both float_utilst and float_bvt: overflow_to_inf did not include ROUND_TO_AWAY. Since ROUND_TO_AWAY is a round-to-nearest mode, overflow must produce ±inf — matching the behaviour of ieee_floatt::align(). This is a clear miss from commit 5c62ecc ("Add IEEE 754 TiesToAway rounding mode") where every other site that branches on rounding mode was updated but round_exponent was not. The regression test exercises positive and negative overflow under all five rounding modes, plus FLT_MAX/FLT_MIN and DBL_MAX/DBL_MIN cases that exercise the wider exponent type. The ROUND_TO_AWAY cases pin fix 2 — reverting the round_to_away disjunct in either encoder leaves them failing. The FLT_MAX/FLT_MIN cases happen to saturate correctly to ±inf even on the pre-fix encoder via downstream denormalization-shift handling, so they don't pin fix 1 as a strict regression test, but they remain useful coverage of the corrected exponent-extension path. Drive-by: rewrite the now-stale comment above overflow_to_inf in both encoders (it claimed to introduce 'directed rounding modes round overflow to the maximum normal' but the disjunction now includes round-to-nearest); rewrite the cryptic '+1 to absorb overflow / +1 for adjust' comment in float_bvt::div and float_utilst::div; and fix the long-standing 'thown'/'thowing' typo at four sites in the two files. Maintainability follow-up (out of scope here): float_bvt and float_utilst implement essentially the same algorithm twice, and each of the patches in this area (cd9d007 in 2017, 5c62ecc later, this PR) has had to be applied in both places. A common rounding-mode policy or single source of truth would make this class of bug structurally impossible. 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.
Two fixes:
float_bvt::div: exponent extended by only 1 bit (spec.e+1) instead of 2 (spec.e+2), causing wraparound for large quotients.
round_exponent in both float_utilst and float_bvt: overflow_to_inf did not include ROUND_TO_AWAY. Since ROUND_TO_AWAY is a round-to-nearest mode, overflow should produce infinity.