From 5de7b26e88582f2fba54c30390d04e7200aa2b8a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 20 Nov 2024 05:57:18 -0800 Subject: [PATCH] Add IEEE 754 TiesToAway rounding mode 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. --- src/solvers/floatbv/float_bv.cpp | 11 ++++++++++- src/solvers/floatbv/float_bv.h | 1 + src/solvers/floatbv/float_utils.cpp | 11 ++++++++++- src/solvers/floatbv/float_utils.h | 22 ++++++++++++++-------- src/solvers/smt2/smt2_conv.cpp | 12 +++++++++--- src/solvers/smt2/smt2_parser.cpp | 10 ++++++---- src/util/ieee_float.cpp | 9 +++++++++ src/util/ieee_float.h | 5 ++++- 8 files changed, 63 insertions(+), 18 deletions(-) diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp index 9450694fb43..6f8b8dc5fb0 100644 --- a/src/solvers/floatbv/float_bv.cpp +++ b/src/solvers/floatbv/float_bv.cpp @@ -282,11 +282,14 @@ void float_bvt::rounding_mode_bitst::get(const exprt &rm) exprt round_to_minus_inf_const= from_integer(ieee_floatt::ROUND_TO_MINUS_INF, rm.type()); exprt round_to_zero_const=from_integer(ieee_floatt::ROUND_TO_ZERO, rm.type()); + exprt round_to_away_const = + from_integer(ieee_floatt::ROUND_TO_AWAY, rm.type()); round_to_even=equal_exprt(rm, round_to_even_const); round_to_plus_inf=equal_exprt(rm, round_to_plus_inf_const); round_to_minus_inf=equal_exprt(rm, round_to_minus_inf_const); round_to_zero=equal_exprt(rm, round_to_zero_const); + round_to_away = equal_exprt(rm, round_to_away_const); } exprt float_bvt::sign_bit(const exprt &op) @@ -1166,12 +1169,18 @@ exprt float_bvt::fraction_rounding_decision( // round to zero false_exprt round_to_zero; + // round to away + const auto round_to_away = or_exprt(rounding_bit, sticky_bit); + // now select appropriate one + // clang-format off return if_exprt(rounding_mode_bits.round_to_even, round_to_even, if_exprt(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf, if_exprt(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf, if_exprt(rounding_mode_bits.round_to_zero, round_to_zero, - false_exprt())))); // otherwise zero + if_exprt(rounding_mode_bits.round_to_away, round_to_away, + false_exprt()))))); // otherwise zero + // clang-format off } void float_bvt::round_fraction( diff --git a/src/solvers/floatbv/float_bv.h b/src/solvers/floatbv/float_bv.h index 7c4ff63b84d..5fe0378d825 100644 --- a/src/solvers/floatbv/float_bv.h +++ b/src/solvers/floatbv/float_bv.h @@ -104,6 +104,7 @@ class float_bvt exprt round_to_zero; exprt round_to_plus_inf; exprt round_to_minus_inf; + exprt round_to_away; void get(const exprt &rm); explicit rounding_mode_bitst(const exprt &rm) { get(rm); } diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp index dc94a842226..1fa414656ed 100644 --- a/src/solvers/floatbv/float_utils.cpp +++ b/src/solvers/floatbv/float_utils.cpp @@ -22,11 +22,14 @@ void float_utilst::set_rounding_mode(const bvt &src) bv_utils.build_constant(ieee_floatt::ROUND_TO_MINUS_INF, src.size()); bvt round_to_zero= bv_utils.build_constant(ieee_floatt::ROUND_TO_ZERO, src.size()); + bvt round_to_away = + bv_utils.build_constant(ieee_floatt::ROUND_TO_AWAY, src.size()); rounding_mode_bits.round_to_even=bv_utils.equal(src, round_to_even); rounding_mode_bits.round_to_plus_inf=bv_utils.equal(src, round_to_plus_inf); rounding_mode_bits.round_to_minus_inf=bv_utils.equal(src, round_to_minus_inf); rounding_mode_bits.round_to_zero=bv_utils.equal(src, round_to_zero); + rounding_mode_bits.round_to_away = bv_utils.equal(src, round_to_away); } bvt float_utilst::from_signed_integer(const bvt &src) @@ -990,12 +993,18 @@ literalt float_utilst::fraction_rounding_decision( literalt round_to_zero= const_literal(false); + // round to away + literalt round_to_away = prop.lor(rounding_least, sticky_bit); + // now select appropriate one + // clang-format off return prop.lselect(rounding_mode_bits.round_to_even, round_to_even, prop.lselect(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf, prop.lselect(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf, prop.lselect(rounding_mode_bits.round_to_zero, round_to_zero, - prop.new_variable())))); // otherwise non-det + prop.lselect(rounding_mode_bits.round_to_away, round_to_away, + prop.new_variable()))))); // otherwise non-det + // clang-format on } void float_utilst::round_fraction(unbiased_floatt &result) diff --git a/src/solvers/floatbv/float_utils.h b/src/solvers/floatbv/float_utils.h index 875555c9120..4bc275ec4df 100644 --- a/src/solvers/floatbv/float_utils.h +++ b/src/solvers/floatbv/float_utils.h @@ -25,19 +25,21 @@ class float_utilst literalt round_to_zero; literalt round_to_plus_inf; literalt round_to_minus_inf; - - rounding_mode_bitst(): - round_to_even(const_literal(true)), - round_to_zero(const_literal(false)), - round_to_plus_inf(const_literal(false)), - round_to_minus_inf(const_literal(false)) + literalt round_to_away; + + rounding_mode_bitst() + : round_to_even(const_literal(true)), + round_to_zero(const_literal(false)), + round_to_plus_inf(const_literal(false)), + round_to_minus_inf(const_literal(false)), + round_to_away(const_literal(false)) { } void set(const ieee_floatt::rounding_modet mode) { - round_to_even=round_to_zero=round_to_plus_inf=round_to_minus_inf= - const_literal(false); + round_to_even = round_to_zero = round_to_plus_inf = round_to_minus_inf = + round_to_away = const_literal(false); switch(mode) { @@ -57,6 +59,10 @@ class float_utilst round_to_zero=const_literal(true); break; + case ieee_floatt::ROUND_TO_AWAY: + round_to_away = const_literal(true); + break; + case ieee_floatt::NONDETERMINISTIC: case ieee_floatt::UNKNOWN: UNREACHABLE; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 3aeb9598181..8d94f4a3a4e 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3880,10 +3880,12 @@ void smt2_convt::convert_rounding_mode_FPA(const exprt &expr) out << "roundTowardPositive"; else if(value==3) out << "roundTowardZero"; + else if(value == 4) + out << "roundNearestTiesToAway"; else INVARIANT_WITH_DIAGNOSTICS( false, - "Rounding mode should have value 0, 1, 2, or 3", + "Rounding mode should have value 0, 1, 2, 3, or 4", id2string(cexpr.get_value())); } else @@ -3903,10 +3905,14 @@ void smt2_convt::convert_rounding_mode_FPA(const exprt &expr) convert_expr(expr); out << ") roundTowardPositive "; + out << "(ite (= (_ bv3 " << width << ") "; + convert_expr(expr); + out << ") roundTowardZero "; + // TODO: add some kind of error checking here - out << "roundTowardZero"; + out << "roundTowardAway"; - out << ")))"; + out << "))))"; } } diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index c952506111f..e6854cfb2dc 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1093,12 +1093,14 @@ void smt2_parsert::setup_expressions() return from_integer(ieee_floatt::ROUND_TO_EVEN, unsignedbv_typet(32)); }; - expressions["roundNearestTiesToAway"] = [this]() -> exprt { - throw error("unsupported rounding mode"); + expressions["roundNearestTiesToAway"] = [] { + // we encode as 32-bit unsignedbv + return from_integer(ieee_floatt::ROUND_TO_AWAY, unsignedbv_typet(32)); }; - expressions["RNA"] = [this]() -> exprt { - throw error("unsupported rounding mode"); + expressions["RNA"] = [] { + // we encode as 32-bit unsignedbv + return from_integer(ieee_floatt::ROUND_TO_AWAY, unsignedbv_typet(32)); }; expressions["roundTowardPositive"] = [] { diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index dccd2cda819..6ff7ee4522a 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -894,6 +894,11 @@ void ieee_floatt::align() else make_fltmax(); // positive break; + + case ROUND_TO_AWAY: + // round towards + or - infinity + infinity_flag = true; + break; } return; // done @@ -969,6 +974,10 @@ void ieee_floatt::divide_and_round( ++dividend; break; + case ROUND_TO_AWAY: + ++dividend; + break; + case NONDETERMINISTIC: case UNKNOWN: UNREACHABLE; diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index 5eb2f04e979..4cd1da6b5a3 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -331,14 +331,17 @@ class ieee_floatt : public ieee_float_valuet public: // ROUND_TO_EVEN is also known as "round to nearest, ties to even", and // is the IEEE default. + // ROUND_TO_AWAY is also known as "round to infinity". // The numbering below is what x86 uses in the control word and - // what is recommended in C11 5.2.4.2.2 + // what is recommended in C11 5.2.4.2.2. + // The numbering of ROUND_TO_AWAY is not specified in C11 5.2.4.2.2. enum rounding_modet { ROUND_TO_EVEN = 0, ROUND_TO_MINUS_INF = 1, ROUND_TO_PLUS_INF = 2, ROUND_TO_ZERO = 3, + ROUND_TO_AWAY = 4, UNKNOWN, NONDETERMINISTIC };