Add IEEE 754 TiesToAway rounding mode

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -358,13 +358,13 @@ assign_primitive_from_json(const exprt &expr, const jsont &json)
   }
   else if(expr.type() == java_double_type())
   {
-    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
+    ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_double(std::stod(json.value));
     result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }
   else if(expr.type() == java_float_type())
   {
-    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
+    ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_float(std::stof(json.value));
     result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }

jbmc/src/java_bytecode/expr2java.cpp

@@ -230,7 +230,7 @@ std::string expr2javat::convert_constant(
           (src.type()==java_double_type()))
   {
     // This converts NaNs to the canonical NaN
-    const ieee_floatt ieee_repr(to_constant_expr(src));
+    const ieee_float_valuet ieee_repr(to_constant_expr(src));
     if(ieee_repr.is_double())
       return floating_point_to_java_string(ieee_repr.to_double());
     return floating_point_to_java_string(ieee_repr.to_float());

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2181,16 +2181,19 @@
       is_float ? ieee_float_spect::single_precision()
                : ieee_float_spect::double_precision());
 
-    ieee_floatt value(spec);
     if(arg0.type().id() != ID_floatbv)
     {
+      // conversion from integer to float may need rounding
+      auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
       const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      ieee_floatt value(spec, rm);
       value.from_integer(number);
+      results[0] = value.to_expr();
     }
     else
-      value.from_expr(arg0);
-
-    results[0] = value.to_expr();
+    {
+      results[0] = ieee_float_valuet{arg0}.to_expr();
+    }
   }
   else
   {

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -782,7 +782,7 @@ void java_bytecode_parsert::rconstant_pool()
 
       case CONSTANT_Float:
       {
-        ieee_floatt value(ieee_float_spect::single_precision());
+        ieee_float_valuet value(ieee_float_spect::single_precision());
         value.unpack(entry.number);
         entry.expr = value.to_expr();
       }
@@ -794,7 +794,7 @@ void java_bytecode_parsert::rconstant_pool()
 
       case CONSTANT_Double:
       {
-        ieee_floatt value(ieee_float_spect::double_precision());
+        ieee_float_valuet value(ieee_float_spect::double_precision());
         value.unpack(entry.number);
         entry.expr = value.to_expr();
       }

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -938,7 +938,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Expression representing 0.0
   const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
-  ieee_floatt zero_float(float_spec);
+  ieee_float_valuet zero_float(float_spec);
   zero_float.from_float(0.0);
   const constant_exprt zero = zero_float.to_expr();
 
@@ -996,16 +996,17 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   string_expr_list.push_back(zero_string);
 
   // Case of -0.0
-  ieee_floatt minus_zero_float(float_spec);
+  ieee_float_valuet minus_zero_float(float_spec);
   minus_zero_float.from_float(-0.0f);
   condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
   const refined_string_exprt minus_zero_string =
     string_literal_to_string_expr("-0.0", loc, symbol_table, code);
   string_expr_list.push_back(minus_zero_string);
 
   // Case of simple notation
-  ieee_floatt bound_inf_float(float_spec);
-  ieee_floatt bound_sup_float(float_spec);
+  auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+  ieee_floatt bound_inf_float(float_spec, rm);
+  ieee_floatt bound_sup_float(float_spec, rm);
   bound_inf_float.from_float(1e-3f);
   bound_sup_float.from_float(1e7f);
   bound_inf_float.change_spec(float_spec);

src/analyses/interval_domain.cpp

@@ -288,7 +288,7 @@
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {
-      ieee_floatt tmp(to_constant_expr(rhs));
+      ieee_float_valuet tmp(to_constant_expr(rhs));
       if(id==ID_lt)
         tmp.decrement();
       ieee_float_intervalt &fi=float_map[lhs_identifier];
@@ -313,7 +313,7 @@
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {
-      ieee_floatt tmp(to_constant_expr(lhs));
+      ieee_float_valuet tmp(to_constant_expr(lhs));
       if(id==ID_lt)
         tmp.increment();
       ieee_float_intervalt &fi=float_map[rhs_identifier];

src/analyses/interval_domain.h

@@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ai_domain.h"
 
-typedef interval_templatet<ieee_floatt> ieee_float_intervalt;
+typedef interval_templatet<ieee_float_valuet> ieee_float_intervalt;
 
 class interval_domaint:public ai_domain_baset
 {

src/ansi-c/expr2c.cpp

@@ -1912,7 +1912,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_floatbv)
   {
-    dest=ieee_floatt(to_constant_expr(src)).to_ansi_c_string();
+    dest = ieee_float_valuet(to_constant_expr(src)).to_ansi_c_string();
 
     if(!dest.empty() && isdigit(dest[dest.size() - 1]))
     {

src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -761,12 +761,13 @@
       else if(old_type.id() == ID_floatbv) // float -> signed
       {
         // Note that the fractional part is truncated!
-        ieee_floatt upper(to_floatbv_type(old_type));
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt upper(to_floatbv_type(old_type), rm);
         upper.from_integer(power(2, new_width - 1));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());
 
-        ieee_floatt lower(to_floatbv_type(old_type));
+        ieee_floatt lower(to_floatbv_type(old_type), rm);
         lower.from_integer(-power(2, new_width - 1) - 1);
         const binary_relation_exprt no_overflow_lower(
           op, ID_gt, lower.to_expr());
@@ -844,12 +845,13 @@
       else if(old_type.id() == ID_floatbv) // float -> unsigned
       {
         // Note that the fractional part is truncated!
-        ieee_floatt upper(to_floatbv_type(old_type));
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt upper(to_floatbv_type(old_type), rm);
         upper.from_integer(power(2, new_width));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());
 
-        ieee_floatt lower(to_floatbv_type(old_type));
+        ieee_floatt lower(to_floatbv_type(old_type), rm);
         lower.from_integer(-1);
         const binary_relation_exprt no_overflow_lower(
           op, ID_gt, lower.to_expr());
@@ -1295,8 +1297,8 @@
     // -inf + +inf = NaN and +inf + -inf = NaN,
     // i.e., signs differ
     ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
-    exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
-    exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
+    exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
+    exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
 
     isnan = or_exprt(
       and_exprt(
@@ -1315,8 +1317,8 @@
 
     ieee_float_spect spec =
       ieee_float_spect(to_floatbv_type(minus_expr.type()));
-    exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
-    exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
+    exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
+    exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
 
     isnan = or_exprt(
       and_exprt(

src/ansi-c/literals/convert_float_literal.cpp

@@ -71,7 +71,9 @@
     // but these aren't handled anywhere
   }
 
-  ieee_floatt a(type);
+  // This may require rounding.
+  auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+  ieee_floatt a(type, rm);
 
   if(parsed_float.exponent_base==10)
     a.from_base10(parsed_float.significand, parsed_float.exponent);

src/goto-instrument/goto_program2code.cpp

@@ -1923,7 +1923,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
   {
     if(expr.type().id()==ID_floatbv)
     {
-      const ieee_floatt f(to_constant_expr(expr));
+      const ieee_float_valuet f(to_constant_expr(expr));
       if(f.is_NaN() || f.is_infinity())
         system_headers.insert("math.h");
     }

src/goto-programs/interpreter.cpp

@@ -576,7 +576,7 @@
   }
   else if(type.id() == ID_floatbv)
   {
-    ieee_floatt f(to_floatbv_type(type));
+    ieee_float_valuet f(to_floatbv_type(type));
     f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
     return f.to_expr();
   }

src/goto-programs/interpreter_evaluate.cpp

@@ -364,7 +364,7 @@
     }
     else if(expr.type().id()==ID_floatbv)
     {
-      ieee_floatt f;
+      ieee_float_valuet f;
       f.from_expr(to_constant_expr(expr));
       return {f.pack()};
     }
@@ -731,8 +731,9 @@
         }
         else if(expr.type().id()==ID_floatbv)
         {
-          ieee_floatt f1(to_floatbv_type(expr.type()));
-          ieee_floatt f2(to_floatbv_type(op.type()));
+          auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+          ieee_floatt f1(to_floatbv_type(expr.type()), rm);
+          ieee_floatt f2(to_floatbv_type(op.type()), rm);
           f1.unpack(result);
           f2.unpack(tmp.front());
           f1*=f2;

src/goto-programs/json_expr.cpp

@@ -276,7 +276,7 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
         json_numbert(std::to_string(to_bitvector_type(type).get_width()));
       result["binary"] = json_stringt(binary(constant_expr));
       result["data"] =
-        json_stringt(ieee_floatt(constant_expr).to_ansi_c_string());
+        json_stringt(ieee_float_valuet(constant_expr).to_ansi_c_string());
     }
     else if(type.id() == ID_pointer)
     {

src/goto-programs/xml_expr.cpp

@@ -212,7 +212,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)
       result.set_attribute("width", width);
       result.set_attribute(
         "binary", integer2binary(bvrep2integer(value, width, false), width));
-      result.data = ieee_floatt(constant_expr).to_ansi_c_string();
+      result.data = ieee_float_valuet(constant_expr).to_ansi_c_string();
     }
     else if(type.id() == ID_pointer)
     {

src/solvers/floatbv/float_bv.cpp

@@ -240,7 +240,7 @@
 
   constant_exprt mask(integer2bvrep(v, width), src.type());
 
-  ieee_floatt z(type);
+  ieee_float_valuet z(type);
   z.make_zero();
 
   return equal_exprt(bitand_exprt(src, mask), z.to_expr());
@@ -282,11 +282,14 @@
   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 @@
   // 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 @@
     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)
@@ -136,7 +139,7 @@
   return result;
 }
 
-bvt float_utilst::build_constant(const ieee_floatt &src)
+bvt float_utilst::build_constant(const ieee_float_valuet &src)
 {
   unbiased_floatt result;
 
@@ -990,12 +993,18 @@
   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)
@@ -1268,14 +1277,14 @@
   return result;
 }
 
-ieee_floatt float_utilst::get(const bvt &src) const
+ieee_float_valuet float_utilst::get(const bvt &src) const
 {
   mp_integer int_value=0;
 
   for(std::size_t i=0; i<src.size(); i++)
     int_value+=power(2, i)*prop.l_get(src[i]).is_true();
 
-  ieee_floatt result;
+  ieee_float_valuet result;
   result.spec=spec;
   result.unpack(int_value);