Introduce floatbv_round_to_integral_exprt
#8538
Open
Conversation
This file contains 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
kroening
force-pushed
the
round_to_integral
branch
2 times, most recently
from
84b83ec to
b52d32e
Compare
kroening
changed the title
round_to_integral_exprtfloatbv_round_to_integral_exprt
kroening
force-pushed
the
round_to_integral
branch
9 times, most recently
from
9c6589a to
e189f1c
Compare
kroening
requested review from
martin-cs,
peterschrammel,
TGWDB,
tautschnig and
remi-delmas-3000
as code owners
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8538 +/- ##
===========================================
- Coverage 78.79% 78.19% -0.61%
===========================================
Files 1730 1730
Lines 199160 201007 +1847
Branches 18320 18331 +11
===========================================
+ Hits 156938 157179 +241
- Misses 42222 43828 +1606 ☔ View full report in Codecov by Sentry. |
kroening
force-pushed
the
round_to_integral
branch
4 times, most recently
from
f59ad70 to
151d627
Compare
tautschnig
reviewed
Jan 3, 2025
| double ceil(double x) | ||
| { | ||
| return __sort_of_CPROVER_round_to_integral(FE_UPWARD, x); | ||
| return __CPROVER_round_to_integrald(x, 2); // FE_UPWARD |
There was a problem hiding this comment.
Why did you choose not to use the named constant FE_UPWARD?
There was a problem hiding this comment.
__CPROVER_round_to_integrald uses our own numbering, which may or may not match FE_UPWARD on the target platform.
| @@ -136,6 +136,32 @@ bvt float_utilst::to_integer( | |||
| return result; | |||
| } | |||
|
|
|||
| bvt float_utilst::round_to_integral(const bvt &src) | |||
There was a problem hiding this comment.
Where does this actually consider the rounding mode?
Comment on lines
+154
to
+174
|
|
||
| auto tmp1 = add_sub(src, magic_number_bv, false); | ||
|
|
||
| auto tmp2 = add_sub(tmp1, magic_number_bv, true); |
There was a problem hiding this comment.
If ieee_floatt::round_to_integral is to be trusted, shouldn't the sign bit be used instead of hard-coding false and true?
There was a problem hiding this comment.
Note line 153 -- this variant tweaks the sign bit of the magic constant instead.
kroening
force-pushed
the
round_to_integral
branch
2 times, most recently
from
ec1cfc6 to
643372e
Compare
kroening
force-pushed
the
round_to_integral
branch
from
643372e to
ce96ec2
Compare
This splits ieee_floatt into two parts: 1) ieee_float_valuet stores an IEEE 754 floating-point value. It offers no operations that require rounding, and hence, does not require a rounding mode. 2) ieee_floatt extends ieee_float_valuet with a rounding mode, and hence, offers operators that require rounding.
kroening
force-pushed
the
round_to_integral
branch
2 times, most recently
from
dcf0732 to
b6b25aa
Compare
This adds a new expression, floatbv_round_to_integral, which rounds an IEEE 754 floating-point number given as bit-vector to the nearest integer, considering the explicitly given rounding mode.
kroening
force-pushed
the
round_to_integral
branch
from
b6b25aa to
ddeedbc
Compare
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.
This adds a new expression,
floatbv_round_to_integral, which rounds an IEEE 754 floating-point number given as bit-vector to the nearest integer, considering the explicitly given rounding mode.