Merge pull request #3655 from diffblue/fix-adjust_float_expressions

Fix adjust_float_expressions

Author: tautschnig

regression/cbmc/Float-no-simp1/main.c

@@ -1,10 +1,31 @@
+#include <assert.h>
+
+struct S
+{
+  unsigned int some_bit : 7;
+};
+
 int main()
 {
   unsigned int i, j;
   double d;
 
+  // double to integer and back
   i=100.0;
   d=i;
   j=d;
   assert(j==100);
+
+  // double to bool and back
+  _Bool b;
+  b = 100.0;
+  d = b;
+  assert(d);
+
+  // double to bit-field and back
+  struct S s;
+  s.some_bit = 100.0;
+  d = s.some_bit;
+  s.some_bit = d;
+  assert(s.some_bit == 100);
 }

src/goto-programs/adjust_float_expressions.cpp

@@ -53,16 +53,15 @@ static bool have_to_adjust_float_expressions(const exprt &expr)
     if(dest_type.id()==ID_floatbv &&
        src_type.id()==ID_floatbv)
       return true;
-    else if(dest_type.id()==ID_floatbv &&
-            (src_type.id()==ID_c_bool ||
-             src_type.id()==ID_signedbv ||
-             src_type.id()==ID_unsignedbv ||
-             src_type.id()==ID_c_enum_tag))
+    else if(
+      dest_type.id() == ID_floatbv &&
+      (src_type.id() == ID_c_bit_field || src_type.id() == ID_signedbv ||
+       src_type.id() == ID_unsignedbv || src_type.id() == ID_c_enum_tag))
       return true;
-    else if((dest_type.id()==ID_signedbv ||
-             dest_type.id()==ID_unsignedbv ||
-             dest_type.id()==ID_c_enum_tag) &&
-             src_type.id()==ID_floatbv)
+    else if(
+      (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
+       dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
+      src_type.id() == ID_floatbv)
       return true;
   }
 
@@ -136,21 +135,26 @@ void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
       expr.operands().resize(2);
       expr.op1()=rounding_mode;
     }
-    else if(dest_type.id()==ID_floatbv &&
-            (src_type.id()==ID_c_bool ||
-             src_type.id()==ID_signedbv ||
-             src_type.id()==ID_unsignedbv ||
-             src_type.id()==ID_c_enum_tag))
+    else if(
+      dest_type.id() == ID_floatbv &&
+      (src_type.id() == ID_signedbv || src_type.id() == ID_unsignedbv ||
+       src_type.id() == ID_c_enum_tag || src_type.id() == ID_c_bit_field))
     {
       // casts from integer to float-type might round
       expr.id(ID_floatbv_typecast);
       expr.operands().resize(2);
       expr.op1()=rounding_mode;
     }
-    else if((dest_type.id()==ID_signedbv ||
-             dest_type.id()==ID_unsignedbv ||
-             dest_type.id()==ID_c_enum_tag) &&
-             src_type.id()==ID_floatbv)
+    else if(
+      dest_type.id() == ID_floatbv &&
+      (src_type.id() == ID_c_bool || src_type.id() == ID_bool))
+    {
+      // casts from bool or c_bool to float-type do not need rounding
+    }
+    else if(
+      (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
+       dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
+      src_type.id() == ID_floatbv)
     {
       // In C, casts from float to integer always round to zero,
       // irrespectively of the rounding mode that is currently set.

src/solvers/flattening/boolbv_floatbv_op.cpp

@@ -29,6 +29,13 @@ bvt boolbvt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
   if(src_type==dest_type) // redundant type cast?
     return bv0;
 
+  if(src_type.id() == ID_c_bit_field)
+  {
+    // go through underlying type
+    return convert_floatbv_typecast(floatbv_typecast_exprt(
+      typecast_exprt(op0, src_type.subtype()), op1, dest_type));
+  }
+
   float_utilst float_utils(prop);
 
   float_utils.set_rounding_mode(convert_bv(op1));