Introduce `floatbv_round_to_integral_exprt` #8538

kroening · 2024-12-21T14:33:04Z

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.

Each commit message has a non-empty body, explaining why the change was made.
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.

codecov · 2024-12-21T22:52:02Z

Codecov Report

Attention: Patch coverage is 91.16719% with 28 lines in your changes missing coverage. Please review.

Project coverage is 79.63%. Comparing base (b712143) to head (49850ea).
Report is 2 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/solvers/smt2/smt2_conv.cpp	8.33%	11 Missing ⚠️
src/solvers/smt2/smt2_parser.cpp	12.50%	7 Missing ⚠️
src/util/ieee_float.cpp	85.29%	5 Missing ⚠️
src/ansi-c/c_typecheck_expr.cpp	75.00%	3 Missing ⚠️
src/solvers/flattening/boolbv_floatbv_op.cpp	87.50%	1 Missing ⚠️
unit/util/ieee_float.cpp	98.94%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8538      +/-   ##
===========================================
+ Coverage    79.60%   79.63%   +0.02%     
===========================================
  Files         1733     1733              
  Lines       197377   197686     +309     
  Branches     18169    18226      +57     
===========================================
+ Hits        157118   157418     +300     
- Misses       40259    40268       +9

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

src/ansi-c/library/math.c

tautschnig · 2025-01-03T13:32:06Z

src/solvers/floatbv/float_utils.cpp

  return result;
 }

+bvt float_utilst::round_to_integral(const bvt &src)


Where does this actually consider the rounding mode?

It calls add_sub.

tautschnig · 2025-01-03T13:32:27Z

src/solvers/floatbv/float_utils.cpp

+
+  auto tmp1 = add_sub(src, magic_number_bv, false);
+
+  auto tmp2 = add_sub(tmp1, magic_number_bv, true);


If ieee_floatt::round_to_integral is to be trusted, shouldn't the sign bit be used instead of hard-coding false and true?

Note line 153 -- this variant tweaks the sign bit of the magic constant instead.

remi-delmas-3000

looks good but could use some comments to explain how fractional bits get cleared due to the exponent alignment with the magic constant, and tests for halfway values and different tie breaking modes

unit/util/ieee_float.cpp

peterschrammel · 2025-02-15T15:46:50Z

src/solvers/floatbv/float_utils.cpp

+
+  magic_number_bv.back() = src.back(); // copy sign bit
+
+  auto tmp1 = add_sub(src, magic_number_bv, false);


Can this overflow when the number of exponent bits is small?

In that case, ge_magic_number will be true.

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.

This fixes the rounding modes used for the floor and trunc C library functions.

fixup #8538 -- correct rounding modes for `floor`, `trunc`

This release addresses both soundness (via diffblue#8562) and performance issues (via diffblue#8574, diffblue#8576) in our code contracts instrumentation, and includes a collection of bit-operator cleanup (such as diffblue#8524, diffblue#8531) and floating-point support improvements (TiesToAway rounding via diffblue#8515, native rounding to integer via diffblue#8538) that aid EBMC/HW-CBMC.

kroening added the SMT Backend Interface label Dec 21, 2024

kroening force-pushed the round_to_integral branch 2 times, most recently from 84b83ec to b52d32e Compare December 21, 2024 14:45

kroening changed the title ~~Introduce round_to_integral_exprt~~ Introduce floatbv_round_to_integral_exprt Dec 21, 2024

kroening force-pushed the round_to_integral branch 9 times, most recently from 9c6589a to e189f1c Compare December 21, 2024 21:49

kroening marked this pull request as ready for review December 21, 2024 22:07

kroening requested review from TGWDB, martin-cs, peterschrammel, remi-delmas-3000 and tautschnig as code owners December 21, 2024 22:07

kroening assigned tautschnig, peterschrammel and martin-cs Dec 27, 2024

kroening force-pushed the round_to_integral branch 4 times, most recently from f59ad70 to 151d627 Compare January 2, 2025 13:28

tautschnig reviewed Jan 3, 2025

View reviewed changes

kroening force-pushed the round_to_integral branch 2 times, most recently from ec1cfc6 to 643372e Compare January 9, 2025 23:10

kroening force-pushed the round_to_integral branch 4 times, most recently from b6b25aa to ddeedbc Compare January 10, 2025 14:47

kroening force-pushed the round_to_integral branch from ddeedbc to 8b80200 Compare February 5, 2025 10:47

remi-delmas-3000 reviewed Feb 5, 2025

View reviewed changes

unit/util/ieee_float.cpp Show resolved Hide resolved

kroening force-pushed the round_to_integral branch 5 times, most recently from 90018fc to 5e40ab0 Compare February 11, 2025 16:15

remi-delmas-3000 approved these changes Feb 11, 2025

View reviewed changes

kroening force-pushed the round_to_integral branch 2 times, most recently from 7f1be0e to a6d1ba4 Compare February 11, 2025 19:28

peterschrammel approved these changes Feb 15, 2025

View reviewed changes

kroening force-pushed the round_to_integral branch from a6d1ba4 to 6c7c09e Compare February 15, 2025 17:21

Introduce floatbv_round_to_integral_exprt

49850ea

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 6c7c09e to 49850ea Compare February 15, 2025 17:26

kroening enabled auto-merge February 15, 2025 17:32

kroening merged commit 0fc8a49 into develop Feb 15, 2025
38 of 39 checks passed

kroening added a commit that referenced this pull request Feb 19, 2025

fixup #8538 -- correct rounding modes for floor, trunc

38093d7

This fixes the rounding modes used for the floor and trunc C library functions.

kroening added a commit that referenced this pull request Feb 20, 2025

fixup #8538 -- correct rounding modes for floor, trunc

177f33b

This fixes the rounding modes used for the floor and trunc C library functions.

kroening added a commit that referenced this pull request Feb 20, 2025

fixup #8538 -- correct rounding modes for floor, trunc

2bf5ced

This fixes the rounding modes used for the floor and trunc C library functions.

kroening added a commit that referenced this pull request Feb 20, 2025

fixup #8538 -- correct rounding modes for floor, trunc

43662c2

This fixes the rounding modes used for the floor and trunc C library functions.

kroening added a commit that referenced this pull request Feb 20, 2025

fixup #8538 -- correct rounding modes for floor, trunc

15bddab

This fixes the rounding modes used for the floor and trunc C library functions.

kroening added a commit that referenced this pull request Feb 20, 2025

fixup #8538 -- correct rounding modes for floor, trunc

968c28f

This fixes the rounding modes used for the floor and trunc C library functions.

kroening added a commit that referenced this pull request Mar 2, 2025

Merge pull request #8597 from diffblue/fixup-8538

f55f636

fixup #8538 -- correct rounding modes for `floor`, `trunc`

tautschnig mentioned this pull request Mar 13, 2025

Release CBMC 6.5.0 #8607

Merged

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Introduce `floatbv_round_to_integral_exprt` #8538

Introduce `floatbv_round_to_integral_exprt` #8538

Uh oh!

kroening commented Dec 21, 2024 •

edited

Loading

Uh oh!

codecov bot commented Dec 21, 2024 •

edited

Loading

Uh oh!

Uh oh!

tautschnig Jan 3, 2025

Uh oh!

kroening Jan 3, 2025

Uh oh!

tautschnig Jan 3, 2025

Uh oh!

kroening Jan 3, 2025

Uh oh!

remi-delmas-3000 left a comment

Uh oh!

Uh oh!

peterschrammel Feb 15, 2025

Uh oh!

kroening Feb 15, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants


		auto tmp1 = add_sub(src, magic_number_bv, false);

		auto tmp2 = add_sub(tmp1, magic_number_bv, true);


		magic_number_bv.back() = src.back(); // copy sign bit

		auto tmp1 = add_sub(src, magic_number_bv, false);

Introduce floatbv_round_to_integral_exprt #8538

Introduce floatbv_round_to_integral_exprt #8538

Uh oh!

Conversation

kroening commented Dec 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Dec 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Uh oh!

tautschnig Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

kroening Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

kroening Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

peterschrammel Feb 15, 2025

Choose a reason for hiding this comment

Uh oh!

kroening Feb 15, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Introduce `floatbv_round_to_integral_exprt` #8538

Introduce `floatbv_round_to_integral_exprt` #8538

kroening commented Dec 21, 2024 •

edited

Loading

codecov bot commented Dec 21, 2024 •

edited

Loading