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

@@ -136,6 +136,32 @@ bvt float_utilst::to_integer(
  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.

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 martin-cs, peterschrammel, TGWDB, tautschnig and remi-delmas-3000 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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

tautschnig Jan 3, 2025

kroening Jan 3, 2025

tautschnig Jan 3, 2025

kroening Jan 3, 2025

remi-delmas-3000 left a comment

peterschrammel Feb 15, 2025

kroening Feb 15, 2025


		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

Conversation

kroening commented Dec 21, 2024 • edited Loading

codecov bot commented Dec 21, 2024 • edited Loading

Codecov Report

tautschnig Jan 3, 2025

Choose a reason for hiding this comment

kroening Jan 3, 2025

Choose a reason for hiding this comment

tautschnig Jan 3, 2025

Choose a reason for hiding this comment

kroening Jan 3, 2025

Choose a reason for hiding this comment

remi-delmas-3000 left a comment

Choose a reason for hiding this comment

peterschrammel Feb 15, 2025

Choose a reason for hiding this comment

kroening Feb 15, 2025

Choose a reason for hiding this comment

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