Handle empty structs in the back-end (and a number of induced fixes)

regression/cbmc/Empty_struct2/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+struct empty
+{
+};
+
+#pragma pack(1)
+struct S
+{
+  char x;
+  struct empty e;
+  char y;
+};
+#pragma pack()
+
+int main()
+{
+  struct S s;
+  assert(sizeof(struct S) == 2);
+
+  struct empty *p = &s.e;
+
+  assert(p == (char *)&s + 1);
+
+  return 0;
+}

regression/cbmc/Empty_struct2/test.desc

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

src/pointer-analysis/value_set_dereference.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
 // global data, horrible
@@ -471,6 +472,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       // try to build a member/index expression - do not use byte_extract
       exprt subexpr = get_subexpression_at_offset(
         root_object_subexpression, o.offset(), dereference_type, ns);
+      if(subexpr.is_not_nil())
+        simplify(subexpr, ns);
       if(subexpr.is_not_nil() && subexpr.id() != byte_extract_id())
       {
         // Successfully found a member, array index, or combination thereof

src/solvers/flattening/pointer_logic.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "pointer_logic.h"
 
 #include <util/arith_tools.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
@@ -98,76 +99,35 @@ exprt pointer_logict::pointer_expr(
 
   const exprt &object_expr=objects[pointer.object];
 
-  exprt deep_object=object_rec(pointer.offset, type, object_expr);
-
-  return address_of_exprt(deep_object, type);
-}
-
-exprt pointer_logict::object_rec(
-  const mp_integer &offset,
-  const typet &pointer_type,
-  const exprt &src) const
-{
-  if(src.type().id()==ID_array)
+  typet subtype = type.subtype();
+  // This is a gcc extension.
+  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+  if(subtype.id() == ID_empty)
+    subtype = char_type();
+  const exprt deep_object =
+    get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns);
+  CHECK_RETURN(deep_object.is_not_nil());
+  if(deep_object.id() != byte_extract_id())
+    return address_of_exprt(deep_object, type);
+
+  const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
+  if(be.offset().is_zero())
+    return address_of_exprt(be.op(), type);
+
+  const auto subtype_bytes = pointer_offset_size(subtype, ns);
+  CHECK_RETURN(subtype_bytes.has_value() && *subtype_bytes > 0);
+  if(*subtype_bytes > pointer.offset)
   {
-    auto size = pointer_offset_size(src.type().subtype(), ns);
-
-    if(!size.has_value() || *size == 0)
-      return src;
-
-    mp_integer index = offset / (*size);
-    mp_integer rest = offset % (*size);
-    if(rest<0)
-      rest=-rest;
-
-    index_exprt tmp(src.type().subtype());
-    tmp.index()=from_integer(index, typet(ID_integer));
-    tmp.array()=src;
-
-    return object_rec(rest, pointer_type, tmp);
+    return plus_exprt(
+      address_of_exprt(be.op(), pointer_type(char_type())),
+      from_integer(pointer.offset, index_type()));
   }
-  else if(src.type().id()==ID_struct)
+  else
   {
-    const struct_typet::componentst &components=
-      to_struct_type(src.type()).components();
-
-    if(offset<0)
-      return src;
-
-    mp_integer current_offset=0;
-
-    for(const auto &c : components)
-    {
-      INVARIANT(
-        offset >= current_offset,
-        "when the object has not been found yet its offset must not be smaller"
-        "than the offset of the current struct component");
-
-      const typet &subtype=c.type();
-
-      const auto sub_size = pointer_offset_size(subtype, ns);
-      CHECK_RETURN(sub_size.has_value() && *sub_size != 0);
-
-      mp_integer new_offset = current_offset + *sub_size;
-
-      if(new_offset>offset)
-      {
-        // found it
-        member_exprt tmp(src, c);
-
-        return object_rec(
-          offset-current_offset, pointer_type, tmp);
-      }
-
-      current_offset=new_offset;
-    }
-
-    return src;
+    return plus_exprt(
+      address_of_exprt(be.op(), pointer_type(char_type())),
+      from_integer(pointer.offset / *subtype_bytes, index_type()));
   }
-  else if(src.type().id()==ID_union)
-    return src;
-
-  return src;
 }
 
 pointer_logict::pointer_logict(const namespacet &_ns):ns(_ns)

src/solvers/flattening/pointer_logic.h

@@ -78,11 +78,6 @@ class pointer_logict
   exprt pointer_expr(
     const mp_integer &offset,
     const exprt &object) const;
-
-  exprt object_rec(
-    const mp_integer &offset,
-    const typet &pointer_type,
-    const exprt &src) const;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H

src/util/pointer_offset_size.cpp

@@ -722,12 +722,11 @@ exprt get_subexpression_at_offset(
     }
   }
 
-  const byte_extract_exprt be(
+  return byte_extract_exprt(
     byte_extract_id(),
     expr,
     from_integer(offset_bytes, index_type()),
     target_type_raw);
-  return simplify_expr(be, ns);
 }
 
 exprt get_subexpression_at_offset(

src/util/simplify_expr.cpp

@@ -1781,112 +1781,15 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     }
   }
 
-  // rethink the remaining code to correctly handle big endian
-  if(expr.id()!=ID_byte_extract_little_endian)
+  // try to refine it down to extracting from a member or an index in an array
+  exprt subexpr =
+    get_subexpression_at_offset(expr.op(), offset, expr.type(), ns);
+  if(subexpr.is_nil() || subexpr == expr)
     return true;
 
-  // get type of object
-  const typet &op_type=ns.follow(expr.op().type());
-
-  if(op_type.id()==ID_array)
-  {
-    exprt result=expr.op();
-
-    // try proper array or string constant
-    for(const typet *op_type_ptr=&op_type;
-        op_type_ptr->id()==ID_array;
-        op_type_ptr=&(ns.follow(*op_type_ptr).subtype()))
-    {
-      DATA_INVARIANT(*el_size > 0, "arrays must not have zero-sized objects");
-      DATA_INVARIANT(
-        (*el_size) % 8 == 0,
-        "array elements have a size in bits which is a multiple of bytes");
-
-      mp_integer el_bytes = (*el_size) / 8;
-
-      if(base_type_eq(expr.type(), op_type_ptr->subtype(), ns) ||
-         (expr.type().id()==ID_pointer &&
-          op_type_ptr->subtype().id()==ID_pointer))
-      {
-        if(offset%el_bytes==0)
-        {
-          offset/=el_bytes;
-
-          result=
-            index_exprt(
-              result,
-              from_integer(offset, expr.offset().type()));
-          result.make_typecast(expr.type());
-
-          if(!base_type_eq(expr.type(), op_type_ptr->subtype(), ns))
-             result.make_typecast(expr.type());
-
-          expr.swap(result);
-          simplify_rec(expr);
-          return false;
-        }
-      }
-      else
-      {
-        auto sub_size = pointer_offset_size(op_type_ptr->subtype(), ns);
-
-        if(sub_size.has_value() && *sub_size > 0)
-        {
-          mp_integer index = offset / (*sub_size);
-          offset %= (*sub_size);
-
-          result=
-            index_exprt(
-              result,
-              from_integer(index, expr.offset().type()));
-        }
-      }
-    }
-  }
-  else if(op_type.id()==ID_struct)
-  {
-    const struct_typet &struct_type=
-      to_struct_type(op_type);
-    const struct_typet::componentst &components=
-      struct_type.components();
-
-    mp_integer m_offset_bits=0;
-    for(const auto &component : components)
-    {
-      auto m_size = pointer_offset_bits(component.type(), ns);
-      if(!m_size.has_value() || *m_size <= 0)
-        break;
-
-      if(
-        offset * 8 == m_offset_bits && *el_size == *m_size &&
-        base_type_eq(expr.type(), component.type(), ns))
-      {
-        member_exprt member(expr.op(), component.get_name(), component.type());
-        simplify_member(member);
-        expr.swap(member);
-
-        return false;
-      }
-      else if(
-        offset * 8 >= m_offset_bits &&
-        offset * 8 + *el_size <= m_offset_bits + *m_size &&
-        m_offset_bits % 8 == 0)
-      {
-        expr.op()=
-          member_exprt(expr.op(), component.get_name(), component.type());
-        simplify_member(expr.op());
-        expr.offset()=
-          from_integer(offset-m_offset_bits/8, expr.offset().type());
-        simplify_rec(expr);
-
-        return false;
-      }
-
-      m_offset_bits += *m_size;
-    }
-  }
-
-  return true;
+  simplify_rec(subexpr);
+  expr.swap(subexpr);
+  return false;
 }
 
 bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)