Merge pull request #8551 from diffblue/ieee_floatt-protect-rounding_mode

protect `ieee_floatt::rounding_mode`

Author: kroening

src/solvers/refinement/refine_arithmetic.cpp

@@ -171,12 +171,6 @@ void bv_refinementt::check_SAT(approximationt &a)
     if(a.over_state==MAX_STATE)
       return;
 
-    ieee_float_spect spec(to_floatbv_type(type));
-    ieee_floatt o0(spec), o1(spec);
-
-    o0.unpack(a.op0_value);
-    o1.unpack(a.op1_value);
-
     // get actual rounding mode
     constant_exprt rounding_mode_expr =
       to_constant_expr(get(float_op.rounding_mode()));
@@ -185,10 +179,13 @@ void bv_refinementt::check_SAT(approximationt &a)
     ieee_floatt::rounding_modet rounding_mode =
       (ieee_floatt::rounding_modet)rounding_mode_int;
 
-    ieee_floatt result=o0;
-    o0.rounding_mode=rounding_mode;
-    o1.rounding_mode=rounding_mode;
-    result.rounding_mode=rounding_mode;
+    ieee_float_spect spec(to_floatbv_type(type));
+    ieee_floatt o0(spec, rounding_mode), o1(spec, rounding_mode);
+
+    o0.unpack(a.op0_value);
+    o1.unpack(a.op1_value);
+
+    ieee_floatt result = o0;
 
     if(a.expr.id()==ID_floatbv_plus)
       result+=o1;

src/util/ieee_float.h

@@ -129,20 +129,22 @@ class ieee_floatt
   // A helper to turn a rounding mode into a constant bitvector expression
   static constant_exprt rounding_mode_expr(rounding_modet);
 
-  rounding_modet rounding_mode;
-
   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),
+      rounding_mode(ROUND_TO_EVEN),
+      sign_flag(false),
+      exponent(0),
+      fraction(0),
+      NaN_flag(false),
+      infinity_flag(false)
   {
   }
 
-  explicit ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
-    : rounding_mode(__rounding_mode),
-      spec(std::move(__spec)),
+  ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
+    : spec(std::move(__spec)),
+      rounding_mode(__rounding_mode),
       sign_flag(false),
       exponent(0),
       fraction(0),
@@ -151,14 +153,27 @@ 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)),
+      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)
+    : spec(ieee_float_spect(type)),
+      rounding_mode(__rounding_mode),
+      sign_flag(false),
+      exponent(0),
+      fraction(0),
+      NaN_flag(false),
+      infinity_flag(false)
   {
   }
 
@@ -175,6 +190,12 @@ class ieee_floatt
     from_expr(expr);
   }
 
+  ieee_floatt(const constant_exprt &expr, rounding_modet __rounding_mode)
+    : rounding_mode(__rounding_mode)
+  {
+    from_expr(expr);
+  }
+
   void negate()
   {
     sign_flag=!sign_flag;
@@ -316,6 +337,8 @@ class ieee_floatt
   void align();
   void next_representable(bool greater);
 
+  rounding_modet rounding_mode;
+
   // we store the number unpacked
   bool sign_flag;
   mp_integer exponent; // this is unbiased

src/util/simplify_expr_floatbv.cpp

@@ -190,10 +190,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
       {
         if(dest_type.id()==ID_floatbv) // float to float
         {
-          ieee_floatt result(to_constant_expr(casted_expr));
-          result.rounding_mode =
+          auto rounding_mode =
             (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
               *rounding_mode_index);
+          ieee_floatt result(to_constant_expr(casted_expr), rounding_mode);
           result.change_spec(
             ieee_float_spect(to_floatbv_type(dest_type)));
           return result.to_expr();
@@ -203,10 +203,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
         {
           if(*rounding_mode_index == ieee_floatt::ROUND_TO_ZERO)
           {
-            ieee_floatt result(to_constant_expr(casted_expr));
-            result.rounding_mode =
+            auto rounding_mode =
               (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
                 *rounding_mode_index);
+            ieee_floatt result(to_constant_expr(casted_expr), rounding_mode);
             mp_integer value=result.to_integer();
             return from_integer(value, dest_type);
           }
@@ -220,10 +220,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
         {
           if(dest_type.id()==ID_floatbv) // int to float
           {
-            ieee_floatt result(to_floatbv_type(dest_type));
-            result.rounding_mode =
+            auto rounding_mode =
               (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
                 *rounding_mode_index);
+            ieee_floatt result(to_floatbv_type(dest_type), rounding_mode);
             result.from_integer(*value);
             return result.to_expr();
           }
@@ -296,16 +296,16 @@ simplify_exprt::simplify_floatbv_op(const ieee_float_op_exprt &expr)
 
   if(op0.is_constant() && op1.is_constant() && op2.is_constant())
   {
-    ieee_floatt v0(to_constant_expr(op0));
-    ieee_floatt v1(to_constant_expr(op1));
+    const auto rounding_mode_opt = numeric_cast<mp_integer>(op2);
 
-    const auto rounding_mode = numeric_cast<mp_integer>(op2);
-    if(rounding_mode.has_value())
+    if(rounding_mode_opt.has_value())
     {
-      v0.rounding_mode =
+      const auto rounding_mode =
         (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
-          *rounding_mode);
-      v1.rounding_mode=v0.rounding_mode;
+          *rounding_mode_opt);
+
+      ieee_floatt v0(to_constant_expr(op0), rounding_mode);
+      ieee_floatt v1(to_constant_expr(op1), rounding_mode);
 
       ieee_floatt result=v0;