Merge pull request #3552 from diffblue/smt2_floatbv_model_fix

smt2 backend: fix floating-point values

Author: Daniel Kroening

regression/cbmc/hex_trace/main.c

@@ -1,12 +1,15 @@
 int main()
 {
-	int a;
-	unsigned int b;
-	a = 0;
-	a = -100;
-	a = 2147483647;
-	b = a*2;
-	a = -2147483647;
-	__CPROVER_assert(0,"");
+  int a;
+  unsigned int b;
+  float f;
 
+  a = 0;
+  a = -100;
+  a = 2147483647;
+  b = a * 2;
+  a = -2147483647;
+  f = 0.1f;
+
+  __CPROVER_assert(0, "");
 }

regression/cbmc/hex_trace/test.desc

@@ -9,6 +9,7 @@ a=-100 \s*\(0xFFFFFF9C\)
 a=2147483647 \s*\(0x7FFFFFFF\)
 b=4294967294ul? \s*\(0xFFFFFFFE\)
 a=-2147483647 \s*\(0x80000001\)
+f=0\.1f \s*\(0x3DCCCCCD\)
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

scripts/delete_failing_smt2_solver_tests

@@ -29,7 +29,6 @@ rm Float13/test.desc
 rm Float20/test.desc
 rm Float22/test.desc
 rm Float23/test.desc
-rm Float24/test.desc
 rm Float3/test.desc
 rm Float4/test.desc
 rm Float5/test.desc

src/solvers/floatbv/float_bv.cpp

@@ -103,21 +103,19 @@ ieee_float_spect float_bvt::get_spec(const exprt &expr)
 exprt float_bvt::abs(const exprt &op, const ieee_float_spect &spec)
 {
   // we mask away the sign bit, which is the most significant bit
-  std::string mask_str(spec.width(), '1');
-  mask_str[0]='0';
+  const mp_integer v = power(2, spec.width() - 1) - 1;
 
-  constant_exprt mask(mask_str, op.type());
+  const constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
 
   return bitand_exprt(op, mask);
 }
 
 exprt float_bvt::negation(const exprt &op, const ieee_float_spect &spec)
 {
   // we flip the sign bit with an xor
-  std::string mask_str(spec.width(), '0');
-  mask_str[0]='1';
+  const mp_integer v = power(2, spec.width() - 1);
 
-  constant_exprt mask(mask_str, op.type());
+  constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
 
   return bitxor_exprt(op, mask);
 }
@@ -150,10 +148,9 @@ exprt float_bvt::is_zero(const exprt &src)
   const floatbv_typet &type=to_floatbv_type(src.type());
   std::size_t width=type.get_width();
 
-  std::string mask_str(width, '1');
-  mask_str[0]='0';
+  const mp_integer v = power(2, width - 1) - 1;
 
-  constant_exprt mask(mask_str, src.type());
+  constant_exprt mask(integer2bvrep(v, width), src.type());
 
   ieee_floatt z(type);
   z.make_zero();

src/solvers/smt2/smt2_conv.cpp

@@ -325,7 +325,7 @@ constant_exprt smt2_convt::parse_literal(
           type.id()==ID_floatbv)
   {
     std::size_t width=boolbv_width(type);
-    return constant_exprt(integer2binary(value, width), type);
+    return constant_exprt(integer2bvrep(value, width), type);
   }
   else if(type.id()==ID_integer ||
           type.id()==ID_range)
@@ -2776,11 +2776,8 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
     else
     {
       // produce corresponding bit-vector
-      ieee_float_spect spec(floatbv_type);
-
-      mp_integer v=binary2integer(
-        id2string(expr.get_value()), false);
-
+      const ieee_float_spect spec(floatbv_type);
+      const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false);
       out << "(_ bv" << v << " " << spec.width() << ")";
     }
   }