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

@@ -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(

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); }

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)

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;

src/solvers/smt2/smt2_conv.cpp

@@ -3897,10 +3897,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
@@ -3920,10 +3922,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 << "))))";
   }
 }
 

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"] = [] {

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;

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