Merge pull request #5693 from tautschnig/zero-size-objects

Offset computation can handle zero-sized objects

Author: kroening

regression/cbmc/empty_compound_type2/main.c

@@ -0,0 +1,15 @@
+struct B
+{
+} b[1];
+struct c
+{
+  void *d;
+} e = {b};
+struct
+{
+  struct c f;
+} * g;
+int main()
+{
+  g->f;
+}

regression/cbmc/empty_compound_type2/test.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+Invariant check failed
+--
+Taking the address of an empty struct resulted in an invariant failure in
+address-of flattening. This test was generated using C-Reduce plus some further
+manual simplification.

regression/cbmc/empty_compound_type3/main.c

@@ -0,0 +1,13 @@
+#include <string.h>
+
+struct a
+{
+} b()
+{
+  struct a *c;
+  memcpy(c + 2, c, 1);
+}
+int main()
+{
+  b();
+}

src/solvers/flattening/boolbv_get.cpp

@@ -126,6 +126,10 @@ exprt boolbvt::bv_get_rec(
         dest.operands().swap(op);
         return dest;
       }
+      else
+      {
+        return array_exprt{{}, to_array_type(type)};
+      }
     }
     else if(type.id()==ID_struct_tag)
     {

src/solvers/flattening/bv_pointers.cpp

@@ -138,7 +138,7 @@ bool bv_pointerst::convert_address_of_rec(
 
     // get size
     auto size = pointer_offset_size(array_type.subtype(), ns);
-    CHECK_RETURN(size.has_value() && *size > 0);
+    CHECK_RETURN(size.has_value() && *size >= 0);
 
     offset_arithmetic(bv, *size, index);
     CHECK_RETURN(bv.size()==bits);
@@ -342,7 +342,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
         else
         {
           auto size_opt = pointer_offset_size(pointer_sub_type, ns);
-          CHECK_RETURN(size_opt.has_value() && *size_opt > 0);
+          CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
           size = *size_opt;
         }
       }

src/util/pointer_offset_size.cpp

@@ -670,13 +670,8 @@ optionalt<exprt> get_subexpression_at_offset(
 
     // no arrays of non-byte-aligned, zero-, or unknown-sized objects
     if(
-      !elem_size_bits.has_value() || *elem_size_bits == 0 ||
-      *elem_size_bits % 8 != 0)
-    {
-      return {};
-    }
-
-    if(*target_size_bits <= *elem_size_bits)
+      elem_size_bits.has_value() && *elem_size_bits > 0 &&
+      *elem_size_bits % 8 == 0 && *target_size_bits <= *elem_size_bits)
     {
       const mp_integer elem_size_bytes = *elem_size_bits / 8;
       const auto offset_inside_elem = offset_bytes % elem_size_bytes;