diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp index 162f1e8cd0a..5195eae9eef 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 13706f06bd5..3c8974fc56c 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 989c8d53377..dbaa5422bd4 100644 --- a/src/solvers/floatbv/float_utils.h +++ b/src/solvers/floatbv/float_utils.h @@ -25,6 +25,7 @@ class float_utilst literalt round_to_zero; literalt round_to_plus_inf; literalt round_to_minus_inf; + literalt round_to_away; rounding_mode_bitst(): round_to_even(const_literal(true)), @@ -36,8 +37,8 @@ class float_utilst 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 +58,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 5a876f828bf..6584655b15c 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3804,10 +3804,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 @@ -3827,10 +3829,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 451436e04a0..b5f684b57c8 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1088,8 +1088,9 @@ 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["roundTowardPositive"] = [] { diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 1fee65294a2..51dc68fcab9 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -618,6 +618,11 @@ void ieee_floatt::align() else make_fltmax(); // positive break; + + case ROUND_TO_AWAY: + // round towards + or - infinity + infinity_flag = true; + break; } return; // done @@ -693,6 +698,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 788975ba040..2f996845067 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -117,13 +117,19 @@ class ieee_floatt 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, - UNKNOWN, NONDETERMINISTIC + ROUND_TO_EVEN = 0, + ROUND_TO_MINUS_INF = 1, + ROUND_TO_PLUS_INF = 2, + ROUND_TO_ZERO = 3, + ROUND_TO_AWAY = 4, + UNKNOWN, + NONDETERMINISTIC }; // A helper to turn a rounding mode into a constant bitvector expression