Fix float-to-integer conversion for wide destination types#8986
Open
tautschnig wants to merge 1 commit into
Open
Fix float-to-integer conversion for wide destination types#8986tautschnig 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 incorrect float-to-integer conversion when the destination integer width exceeds the float fraction width by extending the fraction before shifting and adding a regression test.
Changes:
- Extend
unpacked.fractiontodest_width(when needed) before computing the shift for integer conversion. - Adjust the shift offset computation to use the effective fraction width.
- Add regression tests covering wide float-to-int conversions (bitvector + SMT paths).
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| src/solvers/floatbv/float_bv.cpp | Extends fraction width before shifting to avoid negative/incorrect shift distances for wide integer targets. |
| regression/cbmc/Float-to-int-wide/main.c | Adds a regression program exercising float-to-(wide)int conversions. |
| regression/cbmc/Float-to-int-wide/test.desc | Adds a FloatBV regression test harness entry. |
| regression/cbmc/Float-to-int-wide/test_smt.desc | Adds an SMT regression test harness entry for the same scenario. |
💡 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 #8986 +/- ##
===========================================
+ Coverage 80.59% 80.61% +0.02%
===========================================
Files 1713 1713
Lines 189403 189417 +14
Branches 73 73
===========================================
+ Hits 152647 152700 +53
+ Misses 36756 36717 -39 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
fix-float-to-integer
branch
from
1195e13 to
e14b54d
Compare
tautschnig
force-pushed
the
fix-float-to-integer
branch
from
e14b54d to
065d7dc
Compare
float_bvt::to_integer did not extend the fraction to dest_width before shifting, causing incorrect results when dest_width exceeds the fraction width (the shift distance went negative for large exponents). The fix mirrors the extend-then-shift pattern already used by float_utilst::to_integer. Both encodings previously built the shift distance in a bit-vector of width spec.e, so dest_width - 1 had to be representable there. That held for float/double to the integer types C supports, but not for a narrow source such as _Float16 (spec.e = 5) converted to a 64-bit or wider integer, where the distance silently wrapped (and, before this change, was guarded by a PRECONDITION that turned the legal conversion into an invariant failure). The shift distance is now built in a type wide enough to hold both effective_width - 1 and the sign-extended exponent, i.e. max(spec.e, address_bits(effective_width) + 1), so narrow-source/wide- destination conversions are handled correctly in both encoders. Matching 'keep in sync' comments are retained. The float_bvt fix affects the SMT back-end, which lowers float operations through float_bvt; test_smt.desc (--z3) is therefore the descriptor that pins it -- eight of the float/double assertions fail there on the unfixed encoder. The SAT path (test.desc, --floatbv) exercises float_utilst, which already extended the fraction. The regression test exercises the parameter space: int (at and above 2^24), unsigned int (including a 2^31 case where unsigned-vs-signed semantics matter), long long and __int128 from float and double sources, and _Float16 to int / long long / __int128 -- the narrow-source case the distance widening repairs (a fixed-width distance gets the 64-bit-and-wider destinations wrong). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-float-to-integer
branch
from
065d7dc to
6befe03
Compare
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.
float_bvt::to_integer did not extend the fraction to dest_width before shifting, causing incorrect results when dest_width exceeds the fraction width (the shift distance went negative for large exponents).