Merge pull request #1211 from tautschnig/fix-1209

Enable extractbits over arbitrary types, fix byte extract omission

Author: Daniel Kroening

regression/cbmc/union9/main.c

@@ -0,0 +1,35 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+typedef union {
+  struct {
+    uint8_t x;
+    uint8_t z;
+  } b;
+} union_t;
+
+typedef struct {
+    uint32_t magic;
+    union_t unions[];
+} flex;
+
+int flex_init(flex * flex, size_t num)
+{
+    if (num == 0 || num >= 200) {
+        return -1;
+    }
+    flex->unions[num - 1].b.z = 255;
+    return 0;
+}
+
+int main() {
+    uint8_t num = nondet_size();
+    flex * pool = (flex *) malloc(sizeof(flex) + num * sizeof(union_t));
+    int ret = flex_init(pool, num);
+    if (num > 0 && num < 200) {
+        __CPROVER_assert(ret == 0, "Accept inside range");
+    } else {
+        __CPROVER_assert(ret != 0, "Reject outside range");
+    }
+}
+

regression/cbmc/union9/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/flattening/boolbv_extractbits.cpp

@@ -17,15 +17,6 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  const irep_idt &type_id=expr.type().id();
-
-  if(type_id!=ID_signedbv &&
-     type_id!=ID_unsignedbv &&
-     type_id!=ID_c_enum &&
-     type_id!=ID_c_enum_tag &&
-     type_id!=ID_bv)
-    return conversion_failed(expr);
-
   if(expr.operands().size()!=3)
   {
     error().source_location=expr.find_source_location();

src/solvers/flattening/flatten_byte_operators.cpp

@@ -109,8 +109,8 @@ static exprt unpack_rec(
   }
   else if(type.id()!=ID_empty)
   {
-    // a basic type; we turn that into logical right shift and
-    // extractbits while considering endianness
+    // a basic type; we turn that into extractbits while considering
+    // endianness
     mp_integer bits=pointer_offset_bits(type, ns);
     if(bits<0)
     {
@@ -121,17 +121,12 @@ static exprt unpack_rec(
         bits*=8;
     }
 
-    // cast to generic bit-vector
-    typecast_exprt src_tc(src, unsignedbv_typet(integer2size_t(bits)));
-
     for(mp_integer i=0; i<bits; i+=8)
     {
-      lshr_exprt right_shift(src_tc, from_integer(i, index_type()));
-
       extractbits_exprt extractbits(
-        right_shift,
-        from_integer(7, index_type()),
-        from_integer(0, index_type()),
+        src,
+        from_integer(i+7, index_type()),
+        from_integer(i, index_type()),
         unsignedbv_typet(8));
 
       if(little_endian)
@@ -283,6 +278,8 @@ exprt flatten_byte_extract(
       byte_extract_exprt tmp(unpacked);
       tmp.type()=comp.type();
       tmp.offset()=simplify_expr(new_offset, ns);
+
+      s.move_to_operands(tmp);
     }
 
     if(!failed)