Fix subnormal division precision loss in float_utilst and float_bvt#8987
Fix subnormal division precision loss in float_utilst and float_bvt#8987tautschnig wants to merge 2 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 precision loss when dividing a subnormal float by a normal float by widening the intermediate division bit-width to preserve enough significant bits for correct rounding.
Changes:
- Increase division intermediate width in
float_utilst::divandfloat_bvt::divbyspec.fbits to account for leading zeros in subnormal fractions. - Add CBMC regression tests covering subnormal/normal division for both
--floatbvand SMT2 (--smt2 --z3) paths.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| src/solvers/floatbv/float_utils.cpp | Widen internal division width to avoid 1-ULP rounding errors for subnormal dividends. |
| src/solvers/floatbv/float_bv.cpp | Mirror the widened division width change in the bitvector expression implementation. |
| regression/cbmc/Float-div-subnormal/test.desc | Add regression test driver for the --floatbv backend. |
| regression/cbmc/Float-div-subnormal/test_smt.desc | Add regression test driver for the SMT2 backend. |
| regression/cbmc/Float-div-subnormal/main.c | Add concrete subnormal-division assertions that previously triggered 1-ULP errors. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // full precision even when the dividend is subnormal. A subnormal | ||
| // has up to f leading zeros in the fraction, so we add f extra bits. | ||
| std::size_t div_width = fraction_width * 2 + 1 + spec.f; |
There was a problem hiding this comment.
This computes fraction_width from unpacked1.fraction.type() but then uses spec.f for the extra bits. That mixes two sources of truth and can become inconsistent if the unpacked fraction width ever differs from spec.f (e.g., hidden-bit inclusion changes). Prefer deriving the extra width from fraction_width (e.g., fraction_width - 1) or add an invariant/assertion tying fraction_width to spec.f.
| // full precision even when the dividend is subnormal. A subnormal | |
| // has up to f leading zeros in the fraction, so we add f extra bits. | |
| std::size_t div_width = fraction_width * 2 + 1 + spec.f; | |
| // full precision even when the dividend is subnormal. A subnormal | |
| // has up to f leading zeros in the fraction, so we add that many | |
| // extra bits; derive this from the unpacked fraction width, which | |
| // includes the hidden bit. | |
| const std::size_t extra_precision_bits = fraction_width - 1; | |
| std::size_t div_width = | |
| fraction_width * 2 + 1 + extra_precision_bits; |
| // full precision even when the dividend is subnormal. A subnormal | ||
| // has up to f leading zeros in the fraction, so we add f extra bits. | ||
| std::size_t div_width = fraction_width * 2 + 1 + spec.f; |
There was a problem hiding this comment.
This computes fraction_width from unpacked1.fraction.type() but then uses spec.f for the extra bits. That mixes two sources of truth and can become inconsistent if the unpacked fraction width ever differs from spec.f (e.g., hidden-bit inclusion changes). Prefer deriving the extra width from fraction_width (e.g., fraction_width - 1) or add an invariant/assertion tying fraction_width to spec.f.
| // full precision even when the dividend is subnormal. A subnormal | |
| // has up to f leading zeros in the fraction, so we add f extra bits. | |
| std::size_t div_width = fraction_width * 2 + 1 + spec.f; | |
| // full precision even when the dividend is subnormal. A subnormal | |
| // has up to f leading zeros in the fraction; derive those extra | |
| // bits from the unpacked fraction width to keep sizing consistent. | |
| std::size_t extra_div_bits = fraction_width - 1; | |
| std::size_t div_width = fraction_width * 2 + 1 + extra_div_bits; |
| // Division width: we need enough bits for the quotient to have | ||
| // full precision even when the dividend is subnormal. A subnormal | ||
| // has up to f leading zeros in the fraction, so we add f extra bits. | ||
| std::size_t div_width = unpacked1.fraction.size() * 2 + 1 + spec.f; |
There was a problem hiding this comment.
This increases the division width for all divisions, even when src1 is normal, which can increase solver bit-width and cost. If the intent is specifically to cover the subnormal-dividend case, consider conditionally adding the extra spec.f bits only when the dividend is subnormal (keeping the current *2+1 width for normal numbers).
| int main() | ||
| { | ||
| // A subnormal divided by a normal. | ||
| // FLT_MIN / 2 is the smallest normal; values below are subnormal. |
There was a problem hiding this comment.
This comment is incorrect: FLT_MIN is the smallest normal float; FLT_MIN / 2 is already subnormal. Consider updating it to something like 'FLT_MIN is the smallest normal; values below it (e.g., FLT_MIN/2) are subnormal' to avoid misleading future readers.
| // FLT_MIN / 2 is the smallest normal; values below are subnormal. | |
| // FLT_MIN is the smallest normal float; smaller positive values | |
| // such as FLT_MIN * 0.5f are subnormal. |
|
|
||
| #include <assert.h> | ||
| #include <float.h> | ||
| #include <math.h> |
There was a problem hiding this comment.
<math.h> isn't used in this test file. Removing unused includes helps keep test inputs minimal and avoids accidental reliance on headers.
| #include <math.h> |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8987 +/- ##
===========================================
+ Coverage 80.58% 80.61% +0.02%
===========================================
Files 1712 1712
Lines 189328 189333 +5
Branches 73 73
===========================================
+ Hits 152578 152628 +50
+ Misses 36750 36705 -45 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
When the dividend of a floating-point division is subnormal, its unpacked fraction has leading zeros (the hidden bit is 0). The rounder's normalization step then left-shifts the quotient by a correspondingly larger amount to bring the leading 1 to the top of the buffer, which moves the `have_remainder` sticky bit up into the round position with all-zero bits below it. A genuine round-up (round=1, sticky=1) is thereby mistaken for a tie (round=1, sticky=0) and broken to even, yielding a 1-ULP error. This only surfaces when the quotient lands back in the normal range and so needs rounding -- in practice subnormal/subnormal division. For example 0x1p-149f / 0x3p-149f (mathematically 1/3) returned 0x1.555554p-2f instead of the correct round-to-nearest-even 0x1.555556p-2f. A subnormal divided by a normal yields an (exact) subnormal or zero and does not trigger it. Fix: widen div_width by spec.f extra bits (the worst-case number of leading zeros in a subnormal fraction) so the sticky bit has room below the round position and survives the normalization shift. The same change is applied to both float_utilst::div and float_bvt::div. Add a regression test (regression/cbmc/Float-div-subnormal) covering the subnormal/subnormal case on both the bit-flattening and the SMT (z3) back ends; it fails on the unpatched solver and passes with this change. This widening is paid by every float division: div_width grows from 49 to 72 bits for float and from 105 to 157 for double. Measured end-to-end with the default flattening back end: - single double division: ~0.10s -> ~0.13s - four chained double divisions: ~0.39s -> ~6.5s A follow-up commit reduces this cost by pre-normalizing the (subnormal) dividend instead of widening the divider unconditionally. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…vider The previous commit fixes the subnormal-dividend precision loss by widening div_width by spec.f bits. That widening is paid by every float division, including normal/normal, and roughly squares the bit-blasted divider's cost (measured ~17x on a chained double division). Instead, normalize the dividend before dividing: left-align its fraction and decrease the exponent by the same amount (value-preserving) using the existing normalization_shift helper. A normalized dividend has no leading zeros, so the original minimal div_width (fraction*2+1) is sufficient and the quotient keeps full precision. The exponent arithmetic is widened to accommodate the more negative exponent of a freshly normalized (formerly subnormal) dividend. Applied to both float_utilst::div and float_bvt::div. The regression test from the previous commit still fails on the unpatched solver and passes here, on both the flattening and SMT (z3) back ends; the regression/cbmc/Float* suite (CORE and THOROUGH) passes unchanged. Performance, measured end-to-end with the default flattening back end (base = unpatched develop, (a) = previous commit's widening, (b) = this): - single double division: base ~0.10s (a) ~0.13s (b) ~0.10s - four chained double divisions: base ~0.39s (a) ~6.5s (b) ~3.2s Pre-normalization removes the regression for isolated divisions and roughly halves it for chained divisions; the residual cost is the per-division normalization shifter, which is far cheaper than the wider divider. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-subnormal
branch
from
f9ab381 to
7104852
Compare
When the dividend of a floating-point division is subnormal, its unpacked fraction has leading zeros (the hidden bit is 0). The rounder's normalization step then left-shifts the quotient to bring the leading 1 to the top of the buffer, which moves the
have_remaindersticky bit into the round position with all-zero bits below it. A genuine round-up (round=1, sticky=1) is thereby mistaken for a tie (round=1, sticky=0) and broken to even, giving a 1-ULP error.This only surfaces when the quotient lands back in the normal range and so needs rounding — in practice subnormal/subnormal division. For example
0x1p-149f / 0x3p-149f(mathematically 1/3) returned0x1.555554p-2finstead of the correct round-to-nearest-even0x1.555556p-2f. (A subnormal divided by a normal yields an exact subnormal or zero and does not trigger it; the original "subnormal by a normal" framing has been corrected.)The fix is applied to both
float_utilst::div(bit-flattening back end) andfloat_bvt::div(used by the non-FPA SMT back end, e.g. Z3).Commits
1. Fix subnormal division precision loss — widen
div_widthbyspec.fextra bits so the sticky bit has room below the round position and survives the normalization shift. Includes the regression test. This widening is paid by every float division.2. Pre-normalize the dividend instead of widening the divider — normalize the dividend before dividing (left-align its fraction, decrease the exponent by the same amount; value-preserving) via the existing
normalization_shift. A normalized dividend has no leading zeros, so the minimaldiv_widthsuffices, avoiding the unconditional widening.The two commits are kept separate on purpose: commit 1 is the minimal, self-contained fix; commit 2 is an optional optimization that explains and justifies the extra machinery. Reverting to commit 1 alone remains a valid, simpler option.
Regression test
regression/cbmc/Float-div-subnormalexercises the subnormal/subnormal case (and an exact subnormal/normal sanity check) on both back ends (test.desc→ flattening;test_smt.desc→--smt2 --z3). Verified to fail on an unpatchedcbmcand pass with either fix. The fullregression/cbmc/Float*suite (CORE and THOROUGH) passes unchanged.Performance
Measured end-to-end with the default flattening back end (base = unpatched develop):
Commit 1's unconditional widening grows
div_widthfrom 49→72 bits (float) and 105→157 (double); the bit-blasted divider's cost grows roughly with the square of its width. Commit 2 removes the regression for isolated divisions and roughly halves it for chained divisions; the residual cost is the per-division normalization shifter, which is far cheaper than the wider divider.