Use get_subexpression_at_offset in pointer_logict

We now support pointers into structs with zero-sized members, which is a GCC
extension that we otherwise do support.

Author: tautschnig

regression/cbmc/Empty_struct2/main.c

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

regression/cbmc/Empty_struct2/test.desc

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

src/solvers/flattening/pointer_logic.cpp

@@ -108,75 +108,34 @@ 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();
+  exprt deep_object = get_subexpression_at_offset(
+    object_expr, pointer.offset, subtype, ID_unknown, ns);
+  CHECK_RETURN(deep_object.is_not_nil());
+  if(deep_object.id() != ID_unknown)
+    return address_of_exprt(deep_object, type);
+
+  if(deep_object.op1().is_zero())
+    return address_of_exprt(deep_object.op0(), type);
+
+  const mp_integer subtype_bytes = pointer_offset_size(subtype, ns);
+  CHECK_RETURN(subtype_bytes > 0);
+  if(subtype_bytes > pointer.offset)
   {
-    mp_integer size=
-      pointer_offset_size(src.type().subtype(), ns);
-
-    if(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(deep_object.op0(), 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)
-    {
-      assert(offset>=current_offset);
-
-      const typet &subtype=c.type();
-
-      mp_integer sub_size=pointer_offset_size(subtype, ns);
-      assert(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);
-      }
-
-      assert(new_offset<=offset);
-      current_offset=new_offset;
-      assert(current_offset<=offset);
-    }
-
-    return src;
+    return plus_exprt(
+      address_of_exprt(deep_object.op0(), 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