Skip to content
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.

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

Add IEEE 754 TiesToAway rounding mode #8515

Open
wants to merge 2 commits into
base: develop
Choose a base branch
from
Open

Add IEEE 754 TiesToAway rounding mode #8515

wants to merge 2 commits into from

Conversation

kroening
Copy link
Member

This adds IEEE 754 TiesToAway rounding mode, which rounds away from zero in case of a tie.

  • 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.
  • 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.

Sorry, something went wrong.

@kroening kroening force-pushed the TiesToAway branch 3 times, most recently from 278c8af to 5e5f9ee Compare December 6, 2024 15:23
Copy link

codecov bot commented Dec 6, 2024

Codecov Report

Attention: Patch coverage is 61.85286% with 140 lines in your changes missing coverage. Please review.

Project coverage is 77.73%. Comparing base (3d79560) to head (b6dd050).

Files with missing lines Patch % Lines
src/util/ieee_float.cpp 51.45% 100 Missing ⚠️
src/solvers/smt2/smt2_conv.cpp 28.57% 10 Missing ⚠️
src/ansi-c/goto-conversion/goto_check_c.cpp 40.00% 6 Missing ⚠️
src/goto-programs/interpreter_evaluate.cpp 0.00% 4 Missing ⚠️
src/solvers/smt2/smt2_parser.cpp 33.33% 4 Missing ⚠️
src/solvers/floatbv/float_bv.cpp 70.00% 3 Missing ⚠️
src/solvers/floatbv/float_utils.h 72.72% 3 Missing ⚠️
src/util/ieee_float.h 90.90% 3 Missing ⚠️
src/analyses/interval_domain.cpp 0.00% 2 Missing ⚠️
...src/java_bytecode/java_bytecode_convert_method.cpp 75.00% 1 Missing ⚠️
... and 4 more
Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8515      +/-   ##
===========================================
- Coverage    78.92%   77.73%   -1.19%     
===========================================
  Files         1732     1732              
  Lines       198953   202018    +3065     
  Branches     18560    18570      +10     
===========================================
+ Hits        157021   157039      +18     
- Misses       41932    44979    +3047     

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

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.
This adds IEEE 754 TiesToAway rounding mode, which rounds away from zero in
case of a tie.

The rounding mode is added to three distinct implementations:

1. The implementation for constants, in util/ieee_float.h

2. The implementation that creates a bit-level encoding, in
src/solvers/floatbv/float_utils.h.

3. The implementation that creates a word-level encoding, in
solvers/floatbv/float_bv.cpp.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants