Add round_to_integral to float_bvt, rewrite in float_utilst#8989
Open
tautschnig wants to merge 2 commits into
Open
Add round_to_integral to float_bvt, rewrite in float_utilst#8989tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 commits into
Conversation
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
This PR replaces the prior “add-magic-subtract-magic” float round-to-integral lowering with a direct packed-bitvector masking + conditional increment approach, and wires the new lowering into the SMT2 converter for the non-FPA (bitvector) SMT path.
Changes:
- Reimplemented
round_to_integralin the floatbv bit-blaster (float_utilst) using exponent-based masking and rounding. - Added
float_bvt::round_to_integralexpression-rewrite and integrated it intosmt2_convtwhenuse_FPA_theoryis false. - Added cbmc regression coverage for
rintfunder multiple rounding modes (floatbv path + SMT2/Z3 path).
Reviewed changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| src/solvers/smt2/smt2_conv.cpp | Lowers floatbv_round_to_integral via float_bvt for non-FPA SMT output. |
| src/solvers/floatbv/float_utils.cpp | Rewrites bit-blasted round_to_integral to a mask+round scheme (avoids overflow from magic-number trick). |
| src/solvers/floatbv/float_bv.h | Declares new float_bvt::round_to_integral helper. |
| src/solvers/floatbv/float_bv.cpp | Implements float_bvt::round_to_integral and hooks it into float_bvt::convert. |
| regression/cbmc/Float-round-to-integral/test.desc | Adds regression for rintf under floatbv encoding. |
| regression/cbmc/Float-round-to-integral/test_smt.desc | Adds regression for rintf via SMT2/Z3 path. |
| regression/cbmc/Float-round-to-integral/main.c | Test program exercising rounding modes and integral cases. |
💡 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 #8989 +/- ##
===========================================
+ Coverage 80.58% 80.63% +0.04%
===========================================
Files 1712 1712
Lines 189328 189463 +135
Branches 73 73
===========================================
+ Hits 152578 152774 +196
+ Misses 36750 36689 -61 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
add-rewrite-round_to_integral
branch
from
cca2b7f to
a8aad2f
Compare
Collaborator
|
What are the "rounding tables"? |
Add float_bvt::round_to_integral (a new expression-rewrite for
floatbv_round_to_integral_exprt) and rewrite float_utilst::round_to_integral
in the same shape. Both encodings replace the previous
add-magic-subtract-magic algorithm with a direct bitvector approach:
for each possible biased exponent E in [bias, bias+f-1], mask off the
trailing fractional bits of the packed representation and apply the
rounding-mode-specific increment. Values with |x| < 1 are handled
separately; special values and values already integer short-circuit
to src.
User-visible fix: round_to_integral now works on the SMT non-FPA
path. Previously, 'cbmc --smt2 --z3' on any rintf/rint program
tripped UNEXPECTEDCASE("TODO floatbv_round_to_integral without
FPA") in smt2_conv.cpp. The new dispatch routes through the
existing bvfp_set / convert_floatbv define-fun cache, so multiple
call sites share a single SMT model definition rather than
duplicating the float_bvt rewrite at each call site.
The new encoding uses an O(f^2) expression-tree (an f-deep ITE
cascade where each branch contains an f-bit adder), versus O(f)
for the magic-number formulation. For double (f=52) that is
roughly a 25x growth in node count. The two-place duplication
between float_bv.cpp and float_utils.cpp is intentional and
matches the rest of these files' structure; comments mark them
as needing to be kept in lockstep. A loop-free barrel-shifter
formulation is plausible as a follow-up.
The regression test exercises rintf and rint across all five
rounding modes, special values (NaN, +/-Inf, +/-0), denormals,
negative ties, and an already-integer input above the loop bound
(exp_ge_f early-out). The SMT variant fails on develop with
EXIT=134 (UNEXPECTEDCASE) and passes here.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…utilst Replace the f-deep ITE cascade introduced in the previous commit with a single barrel-shifter pass: drop = f - max(0, unbiased_exp) (0..f) masked = (src >> drop) << drop rbit = bit (drop - 1) of src lsb = bit (drop) of src sticky = (src << (width + 1 - drop)) != 0 inc_val = 1 << drop result = masked + (inc ? inc_val : 0) The per-rounding-mode increment decision (round_to_even / _away / _plus_inf / _minus_inf / _zero) is unchanged from the loop version. The |x| < 1 and exp_ge_f / is_special branches are likewise unchanged. The fraction-bit carry into the exponent at the largest relevant biased exponent is also unchanged and remains intentional and bounded. This brings the round_to_integral encoding from O(f^2) expression nodes (an f-deep ITE cascade where each branch contains an f-bit adder) down to O(1) at the float_bvt / float_utilst level — a constant number of variable-amount shifts plus a single adder, all at width spec.width(). The bit-blasting / SMT layer expands the variable-amount shifts into O(log f)-depth circuits, so the asymptotic gate count is O(width * log f) rather than O(f^2). float_bvt::round_to_integral and float_utilst::round_to_integral are mirror translations of the same algorithm between the exprt and literalt/bvt APIs; comments mark them as needing to be kept in lockstep, as before. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
add-rewrite-round_to_integral
branch
from
a8aad2f to
b44ec4f
Compare
Collaborator
Author
Wording fixed in code comments and commit messages. This was an ill-advised shorthand for rounding decisions. |
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.
Replace the add-magic-subtract-magic algorithm in both encodings with a direct bitvector approach: mask off fractional bits per exponent value, apply rounding. O(f) if-then-else branches, each simple.
Fixes overflow bug when |x| + 2^f exceeds the representable range. Works with the SMT non-FPA path (Z3 can handle the expression tree). Wire into smt2_conv for the non-FPA case.