Merge pull request #9297 from tautschnig/kiro/rr-41-smt2-arith-crashes

SMT2: support _Bool/enum to fixedbv and fixedbv without fraction

Author: tautschnig

regression/cbmc/smt2-fixedbv-cast/main.c

@@ -0,0 +1,33 @@
+typedef __CPROVER_fixedbv[32][16] fix32;
+typedef __CPROVER_fixedbv[16][0] fix16_nofrac;
+
+_Bool nondet_bool(void);
+enum E
+{
+  A = -1,
+  B = 1
+};
+enum E nondet_enum(void);
+fix16_nofrac nondet_fix16(void);
+
+int main(void)
+{
+  // c_bool -> fixedbv
+  _Bool b = nondet_bool();
+  fix32 d1 = b;
+  __CPROVER_assert(d1 == 0 || d1 == 1, "c_bool_to_fixedbv");
+
+  // c_enum -> fixedbv
+  enum E e = nondet_enum();
+  __CPROVER_assume(e == A || e == B);
+  fix32 d2 = e;
+  __CPROVER_assert(d2 == -1 || d2 == 1, "enum_to_fixedbv");
+
+  // fixedbv with 0 fraction bits -> int
+  fix16_nofrac d3 = nondet_fix16();
+  __CPROVER_assume(d3 < 5 && d3 > 2);
+  int i = d3;
+  __CPROVER_assert(i == 3 || i == 4, "fixedbv_no_fraction");
+
+  return 0;
+}

regression/cbmc/smt2-fixedbv-cast/test.desc

@@ -0,0 +1,11 @@
+CORE no-new-smt
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Typecasts from _Bool and enum types to fixedbv, and from fixedbv types
+without fraction bits to integers, must be supported by the SMT2 back end.

src/solvers/smt2/smt2_conv.cpp

@@ -3139,8 +3139,13 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       out << " (ite (and ";
 
       // some fraction bit is not zero
-      out << "(not (= ((_ extract " << (from_fraction_bits-1) << " 0) ?tcop) "
-             "(_ bv0 " << from_fraction_bits << ")))";
+      if(from_fraction_bits == 0)
+        out << "false";
+      else
+      {
+        out << "(not (= ((_ extract " << (from_fraction_bits - 1)
+            << " 0) ?tcop) (_ bv0 " << from_fraction_bits << ")))";
+      }
 
       // number negative
       out << " (= ((_ extract " << (from_width-1) << " " << (from_width-1)
@@ -3292,13 +3297,13 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
     std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits();
     std::size_t to_integer_bits=fixedbv_type.get_integer_bits();
 
-    if(src_type.id()==ID_unsignedbv ||
-       src_type.id()==ID_signedbv ||
-       src_type.id()==ID_c_enum)
+    if(
+      src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
+      src_type.id() == ID_c_enum || src_type.id() == ID_c_bool)
     {
       // integer to fixedbv
 
-      std::size_t from_width=to_bitvector_type(src_type).get_width();
+      std::size_t from_width = boolbv_width(src_type);
       out << "(concat ";
 
       if(from_width==to_integer_bits)
@@ -3318,7 +3323,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
           "from_width should be smaller than to_integer_bits as other case "
           "have been handled above");
         if(
-          src_type.id() == ID_unsignedbv ||
+          src_type.id() == ID_unsignedbv || src_type.id() == ID_c_bool ||
           (src_type.id() == ID_c_enum &&
            to_c_enum_type(src_type).underlying_type().id() == ID_unsignedbv))
         {