Merge pull request #7303 from tautschnig/bugfixes/float-z3

SMT back-end: support floatbv to raw bitvector cast

Author: kroening

regression/cbmc/Float-no-simp2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$

regression/cbmc/Float-no-simp3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$

regression/cbmc/Float-no-simp5/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$

regression/cbmc/Float-zero-sum1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$

regression/cbmc/Float12/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc/Float22/test.desc

@@ -1,8 +1,11 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Fixing this test for the CPROVER SMT2 solver (or any other SMT2 solver
+supporting FPA) requires addressing the TODO "bit-wise floatbv to bv".

regression/cbmc/Float3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE
 main.c
 --floatbv
 ^EXIT=0$

src/solvers/floatbv/float_bv.cpp

@@ -78,6 +78,23 @@ exprt float_bvt::convert(const exprt &expr) const
   {
     return not_exprt(is_zero(to_typecast_expr(expr).op()));
   }
+  else if(
+    expr.id() == ID_typecast && expr.type().id() == ID_bv &&
+    to_typecast_expr(expr).op().type().id() == ID_floatbv) // float -> raw bv
+  {
+    const typecast_exprt &tc = to_typecast_expr(expr);
+    const bitvector_typet &dest_type = to_bitvector_type(expr.type());
+    const floatbv_typet &src_type = to_floatbv_type(tc.op().type());
+    if(
+      dest_type.get_width() != src_type.get_width() ||
+      dest_type.get_width() == 0)
+    {
+      return nil_exprt{};
+    }
+
+    return extractbits_exprt{
+      to_typecast_expr(expr).op(), dest_type.get_width() - 1, 0, dest_type};
+  }
   else if(expr.id()==ID_floatbv_plus)
   {
     const auto &float_expr = to_ieee_float_op_expr(expr);

src/solvers/smt2/smt2_conv.cpp

@@ -987,6 +987,10 @@ std::string smt2_convt::type2id(const typet &type) const
     ieee_float_spect spec(to_floatbv_type(type));
     return "f"+std::to_string(spec.width())+"_"+std::to_string(spec.f);
   }
+  else if(type.id() == ID_bv)
+  {
+    return "B" + std::to_string(to_bitvector_type(type).get_width());
+  }
   else if(type.id()==ID_unsignedbv)
   {
     return "u"+std::to_string(to_unsignedbv_type(type).get_width());