Skip to content

Floating-point normalization must not overflow #7617

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Jun 30, 2023
Merged

Floating-point normalization must not overflow #7617

merged 1 commit into from
Jun 30, 2023

Conversation

tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Mar 24, 2023 •
edited
Loading

We need to extend the exponent to compute a new exponent without
overflow; subsequent denormalization and rounding will ensure the
exponent fits into the target format.

Fixes: #7616

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig self-assigned this Mar 24, 2023
@tautschnig tautschnig mentioned this pull request Mar 24, 2023
Closed
@tautschnig tautschnig force-pushed the bugfixes/7616-float-conversion branch from 41c6266 to 8f848b6 Compare April 18, 2023 13:46
@tautschnig tautschnig changed the title Floating-point rounding must not extend the exponent Floating-point normalization must not overflow Apr 18, 2023
@tautschnig tautschnig force-pushed the bugfixes/7616-float-conversion branch from 8f848b6 to 9bb815e Compare April 18, 2023 13:59
@tautschnig tautschnig marked this pull request as ready for review April 18, 2023 14:09
@tautschnig tautschnig removed their assignment Apr 18, 2023
@tautschnig tautschnig force-pushed the bugfixes/7616-float-conversion branch from 9bb815e to 4991a69 Compare April 18, 2023 14:09
@codecov
Copy link

codecov bot commented Apr 18, 2023 •
edited
Loading

Codecov Report

Patch coverage: 71.42% and project coverage change: -0.10 ⚠️

Comparison is base (793801c) 78.52% compared to head (5c7c154) 78.42%.

Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #7617      +/-   ##
===========================================
- Coverage    78.52%   78.42%   -0.10%     
===========================================
  Files         1674     1674              
  Lines       191971   191974       +3     
===========================================
- Hits        150738   150554     -184     
- Misses       41233    41420     +187
Impacted Files Coverage Δ
src/solvers/floatbv/float_bv.cpp 53.44% <50.00%> (-0.01%) ⬇️
src/solvers/floatbv/float_utils.cpp 96.11% <100.00%> (+0.18%) ⬆️

... and 14 files with indirect coverage changes

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

kroening
kroening reviewed Apr 18, 2023
View reviewed changes
src/solvers/floatbv/float_utils.cpp
@@ -195,6 +195,7 @@ bvt float_utilst::conversion(
if(dest_spec.e > spec.e)
{
normalization_shift(result.fraction, result.exponent);
result.exponent.resize(dest_spec.e);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you explain that one?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Comment added.

@kroening
Copy link
Member

May I ask you to check whether the world-level flattening implementation in solvers/floatbv/float_bv.cpp does the same mistake?

@tautschnig
Floating-point normalization must not overflow
5c7c154 
We need to extend the exponent to compute a new exponent without
overflow; subsequent denormalization and rounding will ensure the
exponent fits into the target format.

Fixes: diffblue#7616
@tautschnig tautschnig force-pushed the bugfixes/7616-float-conversion branch from 4991a69 to 5c7c154 Compare April 20, 2023 19:52
@tautschnig
Copy link
Collaborator Author

tautschnig commented Apr 20, 2023 •
edited
Loading

May I ask you to check whether the world-level flattening implementation in solvers/floatbv/float_bv.cpp does the same mistake?

Oh, thank you, indeed! Having put the fix in place makes the regression test pass when using Z3 (or any other SMT back-end that doesn't support FPA).

@kroening kroening merged commit 6066b34 into diffblue:develop Jun 30, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kroening kroening kroening approved these changes

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

Assignees

@kroening kroening

@martin-cs martin-cs

Labels
bugfix
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Converting a positive subnormal double to float yields +infinity
3 participants
@tautschnig @kroening @martin-cs