Split ieee_floatt into ieee_float_valuet and ieee_floatt

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.

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 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
       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 @@ void interval_domaint::assume_rec(
     }
     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 @@ void interval_domaint::assume_rec(
     }
     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 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
       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 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
       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 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
     // -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 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
 
     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 @@ exprt convert_float_literal(const std::string &src)
     // 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 @@ exprt interpretert::get_value(
   }
   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 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
     }
     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 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
         }
         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 @@ exprt float_bvt::is_zero(const exprt &src)
 
   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());

src/solvers/floatbv/float_utils.cpp

@@ -136,7 +136,7 @@ bvt float_utilst::to_integer(
   return result;
 }
 
-bvt float_utilst::build_constant(const ieee_floatt &src)
+bvt float_utilst::build_constant(const ieee_float_valuet &src)
 {
   unbiased_floatt result;
 
@@ -1268,14 +1268,14 @@ bvt float_utilst::pack(const biased_floatt &src)
   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);
 

src/solvers/floatbv/float_utils.h

@@ -87,7 +87,7 @@ class float_utilst
 
   ieee_float_spect spec;
 
-  bvt build_constant(const ieee_floatt &);
+  bvt build_constant(const ieee_float_valuet &);
 
   static inline literalt sign_bit(const bvt &src)
   {
@@ -139,7 +139,7 @@ class float_utilst
   literalt relation(const bvt &src1, relt rel, const bvt &src2);
 
   // constants
-  ieee_floatt get(const bvt &) const;
+  ieee_float_valuet get(const bvt &) const;
 
   // helpers
   literalt exponent_all_ones(const bvt &);

src/solvers/smt2/smt2_conv.cpp

@@ -476,23 +476,25 @@ constant_exprt smt2_convt::parse_literal(
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::plus_infinity(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::plus_infinity(ieee_float_spect(s - 1, e))
+      .to_expr();
   }
   else if(src.get_sub().size()==4 &&
           src.get_sub()[0].id()=="_" &&
           src.get_sub()[1].id()=="-oo") // (_ -oo e s)
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::minus_infinity(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::minus_infinity(ieee_float_spect(s - 1, e))
+      .to_expr();
   }
   else if(src.get_sub().size()==4 &&
           src.get_sub()[0].id()=="_" &&
           src.get_sub()[1].id()=="NaN") // (_ NaN e s)
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::NaN(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::NaN(ieee_float_spect(s - 1, e)).to_expr();
   }
 
   if(type.id()==ID_signedbv ||
@@ -3445,7 +3447,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
          significands including the hidden bit.  Thus some encoding
          is needed to get to IEEE-754 style representations. */
 
-      ieee_floatt v=ieee_floatt(expr);
+      ieee_float_valuet v = ieee_float_valuet(expr);
       size_t e=floatbv_type.get_e();
       size_t f=floatbv_type.get_f()+1;
 

src/solvers/smt2/smt2_format.cpp

@@ -93,7 +93,7 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
     }
     else if(expr_type.id() == ID_floatbv)
     {
-      const ieee_floatt v = ieee_floatt(constant_expr);
+      const ieee_float_valuet v = ieee_float_valuet(constant_expr);
       const size_t e = v.spec.e;
       const size_t f = v.spec.f + 1; // SMT-LIB counts the hidden bit
 

src/solvers/strings/string_constraint_generator_float.cpp

@@ -77,7 +77,7 @@ exprt get_significand(
 /// \return an expression representing this floating point
 exprt constant_float(const double f, const ieee_float_spect &float_spec)
 {
-  ieee_floatt fl(float_spec);
+  ieee_float_valuet fl(float_spec);
   if(float_spec == ieee_float_spect::single_precision())
     fl.from_float(f);
   else if(float_spec == ieee_float_spect::double_precision())

src/statement-list/converters/convert_real_literal.cpp

@@ -18,7 +18,7 @@ Author: Matthias Weiss, [email protected]
 
 constant_exprt convert_real_literal(const std::string &src)
 {
-  ieee_floatt real{get_real_type()};
+  ieee_float_valuet real{get_real_type()};
   real.from_float(std::stof(src));
   return real.to_expr();
 }

src/statement-list/statement_list_parse_tree_io.cpp

@@ -31,7 +31,7 @@ static void output_constant(std::ostream &os, const constant_exprt &constant)
     os << ivalue;
   else if(can_cast_type<floatbv_typet>(constant.type()))
   {
-    ieee_floatt real{get_real_type()};
+    ieee_float_valuet real{get_real_type()};
     real.from_expr(constant);
     os << real.to_float();
   }

src/util/arith_tools.cpp

@@ -171,7 +171,9 @@ constant_exprt from_integer(
   }
   else if(type_id==ID_floatbv)
   {
-    ieee_floatt ieee_float(to_floatbv_type(type));
+    ieee_floatt ieee_float(
+      to_floatbv_type(type), ieee_floatt::rounding_modet::ROUND_TO_EVEN);
+    // always rounds to zero
     ieee_float.from_integer(int_value);
     return ieee_float.to_expr();
   }