ieee_floatt: introduce NOT_SET rounding mode

This adds a new rounding mode to ieee_floatt, NOT_SET, which is the default
when constructing the object without rounding mode.

Operations that require a rounding mode fail when the rounding mode is NOT_SET.

Author: kroening

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);
+  // Compile-time rounding is implementation defined.
+  // The choice below is arbitrary.
+  ieee_floatt a(type, ieee_floatt::rounding_modet::ROUND_TO_EVEN);
 
   if(parsed_float.exponent_base==10)
     a.from_base10(parsed_float.significand, parsed_float.exponent);

src/solvers/floatbv/float_utils.h

@@ -41,6 +41,9 @@ class float_utilst
 
       switch(mode)
       {
+      case ieee_floatt::NOT_SET:
+        PRECONDITION(false);
+
       case ieee_floatt::ROUND_TO_EVEN:
         round_to_even=const_literal(true);
         break;

src/util/ieee_float.cpp

@@ -474,6 +474,8 @@ void ieee_floatt::build(
   const mp_integer &_fraction,
   const mp_integer &_exponent)
 {
+  PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
+
   sign_flag=_fraction<0;
   fraction=_fraction;
   if(sign_flag)
@@ -488,6 +490,8 @@ void ieee_floatt::from_base10(
   const mp_integer &_fraction,
   const mp_integer &_exponent)
 {
+  PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
+
   NaN_flag=infinity_flag=false;
   sign_flag=_fraction<0;
   fraction=_fraction;
@@ -584,6 +588,9 @@ void ieee_floatt::align()
     // we need to consider the rounding mode here
     switch(rounding_mode)
     {
+    case NOT_SET:
+      PRECONDITION(false);
+
     case UNKNOWN:
     case NONDETERMINISTIC:
     case ROUND_TO_EVEN:
@@ -660,6 +667,9 @@ void ieee_floatt::divide_and_round(
   {
     switch(rounding_mode)
     {
+    case NOT_SET:
+      PRECONDITION(false);
+
     case ROUND_TO_EVEN:
       {
         mp_integer divisor_middle = divisor / 2;
@@ -708,6 +718,7 @@ constant_exprt ieee_floatt::to_expr() const
 ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
 {
   PRECONDITION(other.spec.f == spec.f);
+  PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
 
   // NaN/x = NaN
   if(NaN_flag)
@@ -782,6 +793,7 @@ ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
 ieee_floatt &ieee_floatt::operator*=(const ieee_floatt &other)
 {
   PRECONDITION(other.spec.f == spec.f);
+  PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
 
   if(other.NaN_flag)
     make_NaN();
@@ -818,6 +830,8 @@ ieee_floatt &ieee_floatt::operator*=(const ieee_floatt &other)
 ieee_floatt &ieee_floatt::operator+=(const ieee_floatt &other)
 {
   PRECONDITION(other.spec == spec);
+  PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
+
   ieee_floatt _other=other;
 
   if(other.NaN_flag)
@@ -1058,6 +1072,8 @@ bool ieee_floatt::ieee_not_equal(const ieee_floatt &other) const
 
 void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
 {
+  PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
+
   mp_integer _exponent=exponent-spec.f;
   mp_integer _fraction=fraction;
 

src/util/ieee_float.h

@@ -121,22 +121,29 @@ class ieee_floatt
   // what is recommended 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,
+    UNKNOWN,
+    NONDETERMINISTIC,
+    NOT_SET
   };
 
   // A helper to turn a rounding mode into a constant bitvector expression
   static constant_exprt rounding_mode_expr(rounding_modet);
 
-  rounding_modet rounding_mode;
+  rounding_modet rounding_mode = rounding_modet::NOT_SET;
 
   ieee_float_spect spec;
 
-  explicit ieee_floatt(const ieee_float_spect &_spec):
-    rounding_mode(ROUND_TO_EVEN),
-    spec(_spec), sign_flag(false), exponent(0), fraction(0),
-    NaN_flag(false), infinity_flag(false)
+  explicit ieee_floatt(const ieee_float_spect &_spec)
+    : spec(_spec),
+      sign_flag(false),
+      exponent(0),
+      fraction(0),
+      NaN_flag(false),
+      infinity_flag(false)
   {
   }
 
@@ -151,26 +158,47 @@ class ieee_floatt
   {
   }
 
-  explicit ieee_floatt(const floatbv_typet &type):
-    rounding_mode(ROUND_TO_EVEN),
-    spec(ieee_float_spect(type)),
-    sign_flag(false),
-    exponent(0),
-    fraction(0),
-    NaN_flag(false),
-    infinity_flag(false)
+  explicit ieee_floatt(const floatbv_typet &type)
+    : spec(ieee_float_spect(type)),
+      sign_flag(false),
+      exponent(0),
+      fraction(0),
+      NaN_flag(false),
+      infinity_flag(false)
   {
   }
 
-  ieee_floatt():
-    rounding_mode(ROUND_TO_EVEN),
-    sign_flag(false), exponent(0), fraction(0),
-    NaN_flag(false), infinity_flag(false)
+  explicit ieee_floatt(
+    const floatbv_typet &type,
+    rounding_modet __rounding_mode)
+    : rounding_mode(__rounding_mode),
+      spec(ieee_float_spect(type)),
+      sign_flag(false),
+      exponent(0),
+      fraction(0),
+      NaN_flag(false),
+      infinity_flag(false)
   {
   }
 
-  explicit ieee_floatt(const constant_exprt &expr):
-    rounding_mode(ROUND_TO_EVEN)
+  ieee_floatt()
+    : sign_flag(false),
+      exponent(0),
+      fraction(0),
+      NaN_flag(false),
+      infinity_flag(false)
+  {
+  }
+
+  explicit ieee_floatt(const constant_exprt &expr)
+  {
+    from_expr(expr);
+  }
+
+  explicit ieee_floatt(
+    const constant_exprt &expr,
+    rounding_modet __rounding_mode)
+    : rounding_mode(__rounding_mode)
   {
     from_expr(expr);
   }

src/util/simplify_expr.cpp

@@ -70,6 +70,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
 
     if(type.id()==ID_floatbv)
     {
+      // Does not need rounding
       ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
       value.set_sign(false);
       return value.to_expr();
@@ -104,6 +105,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
 
     if(type.id()==ID_floatbv)
     {
+      // Does not need rounding
       ieee_floatt value(to_constant_expr(expr.op()));
       return make_boolean_expr(value.get_sign());
     }
@@ -1179,7 +1181,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
         const floatbv_typet &f_expr_type=
           to_floatbv_type(expr_type);
 
-        ieee_floatt f(f_expr_type);
+        ieee_floatt f(f_expr_type, ieee_floatt::rounding_modet::ROUND_TO_EVEN);
         f.from_integer(int_value);
 
         return f.to_expr();
@@ -1215,7 +1217,9 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     }
     else if(op_type_id==ID_floatbv)
     {
-      ieee_floatt f(to_constant_expr(expr.op()));
+      ieee_floatt f{
+        to_constant_expr(expr.op()),
+        ieee_floatt::rounding_modet::ROUND_TO_EVEN};
 
       if(expr_type_id==ID_unsignedbv ||
          expr_type_id==ID_signedbv)
@@ -1233,7 +1237,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       {
         fixedbvt fixedbv;
         fixedbv.spec=fixedbv_spect(to_fixedbv_type(expr_type));
-        ieee_floatt factor(f.spec);
+        ieee_floatt factor(f.spec, ieee_floatt::rounding_modet::ROUND_TO_EVEN);
         factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
         f*=factor;
         fixedbv.set_value(f.to_integer());
@@ -1267,6 +1271,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       {
         const auto width = to_bv_type(op_type).get_width();
         const auto int_value = bvrep2integer(value, width, false);
+        // Does not need rounding.
         ieee_floatt ieee_float{to_floatbv_type(expr_type)};
         ieee_float.unpack(int_value);
         return ieee_float.to_expr();

src/util/simplify_expr_int.cpp

@@ -1889,7 +1889,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
     expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
     to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
   {
-    ieee_floatt const_val(to_constant_expr(expr.op1()));
+    ieee_floatt const_val{
+      to_constant_expr(expr.op1()), ieee_floatt::rounding_modet::ROUND_TO_EVEN};
     ieee_floatt const_val_converted=const_val;
     const_val_converted.change_spec(ieee_float_spect(
       to_floatbv_type(to_typecast_expr(expr.op0()).op().type())));