Fix process_array_expr to take into account pointer offset

Author: tautschnig

regression/cbmc/memcpy2/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  char A[3] = {'a', 'b', 'c'};
+  char *p = A;
+  char v1, v2;
+
+  memcpy(&v1, p, 1);
+  ++p;
+  memcpy(&v2, p, 1);
+
+  assert(v1 == 'a');
+  assert(v2 == 'b');
+
+  return 0;
+}

regression/cbmc/memcpy2/test.desc

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

src/goto-symex/goto_symex.h

@@ -252,7 +252,6 @@ class goto_symext
   void trigger_auto_object(const exprt &, statet &);
   void initialize_auto_object(const exprt &, statet &);
   void process_array_expr(exprt &);
-  void process_array_expr_rec(exprt &, const typet &) const;
   exprt make_auto_object(const typet &, statet &);
   virtual void dereference(exprt &, statet &, const bool write);
 

src/goto-symex/symex_clean_expr.cpp

@@ -15,77 +15,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/base_type.h>
-
+#include <util/pointer_offset_size.h>
 #include <util/c_types.h>
 
-void goto_symext::process_array_expr_rec(
-  exprt &expr,
-  const typet &type) const
-{
-  if(expr.id()==ID_if)
-  {
-    if_exprt &if_expr=to_if_expr(expr);
-    process_array_expr_rec(if_expr.true_case(), type);
-    process_array_expr_rec(if_expr.false_case(), type);
-  }
-  else if(expr.id()==ID_index)
-  {
-    // strip index
-    index_exprt &index_expr=to_index_expr(expr);
-    exprt tmp=index_expr.array();
-    expr.swap(tmp);
-  }
-  else if(expr.id()==ID_typecast)
-  {
-    // strip
-    exprt tmp=to_typecast_expr(expr).op0();
-    expr.swap(tmp);
-    process_array_expr_rec(expr, type);
-  }
-  else if(expr.id()==ID_address_of)
-  {
-    // strip
-    exprt tmp=to_address_of_expr(expr).op0();
-    expr.swap(tmp);
-    process_array_expr_rec(expr, type);
-  }
-  else if(expr.id()==ID_byte_extract_little_endian ||
-          expr.id()==ID_byte_extract_big_endian)
-  {
-    // pick the root object
-    exprt tmp=to_byte_extract_expr(expr).op();
-    expr.swap(tmp);
-    process_array_expr_rec(expr, type);
-  }
-  else if(expr.id()==ID_symbol &&
-          expr.get_bool(ID_C_SSA_symbol) &&
-          to_ssa_expr(expr).get_original_expr().id()==ID_index)
-  {
-    const ssa_exprt &ssa=to_ssa_expr(expr);
-    const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
-    exprt tmp=index_expr.array();
-    expr.swap(tmp);
-  }
-  else
-  {
-    Forall_operands(it, expr)
-    {
-      typet t=it->type();
-      process_array_expr_rec(*it, t);
-    }
-  }
-
-  if(!base_type_eq(expr.type(), type, ns))
-  {
-    byte_extract_exprt be(byte_extract_id());
-    be.type()=type;
-    be.op()=expr;
-    be.offset()=from_integer(0, index_type());
-
-    expr.swap(be);
-  }
-}
-
+/// Given an expression, find the root object and the offset into it.
+///
+/// The extra complication to be considered here is that the expression may
+/// have any number of ternary expressions mixed with type casts.
 void goto_symext::process_array_expr(exprt &expr)
 {
   // This may change the type of the expression!
@@ -94,41 +30,28 @@ void goto_symext::process_array_expr(exprt &expr)
   {
     if_exprt &if_expr=to_if_expr(expr);
     process_array_expr(if_expr.true_case());
+    process_array_expr(if_expr.false_case());
 
-    process_array_expr_rec(if_expr.false_case(),
-                           if_expr.true_case().type());
+    if(!base_type_eq(if_expr.true_case(), if_expr.false_case(), ns))
+    {
+      byte_extract_exprt be(
+        byte_extract_id(),
+        if_expr.false_case(),
+        from_integer(0, index_type()),
+        if_expr.true_case().type());
+
+      if_expr.false_case().swap(be);
+    }
 
     if_expr.type()=if_expr.true_case().type();
   }
-  else if(expr.id()==ID_index)
-  {
-    // strip index
-    index_exprt &index_expr=to_index_expr(expr);
-    exprt tmp=index_expr.array();
-    expr.swap(tmp);
-  }
-  else if(expr.id()==ID_typecast)
-  {
-    // strip
-    exprt tmp=to_typecast_expr(expr).op0();
-    expr.swap(tmp);
-    process_array_expr(expr);
-  }
   else if(expr.id()==ID_address_of)
   {
     // strip
     exprt tmp=to_address_of_expr(expr).op0();
     expr.swap(tmp);
     process_array_expr(expr);
   }
-  else if(expr.id()==ID_byte_extract_little_endian ||
-          expr.id()==ID_byte_extract_big_endian)
-  {
-    // pick the root object
-    exprt tmp=to_byte_extract_expr(expr).op();
-    expr.swap(tmp);
-    process_array_expr(expr);
-  }
   else if(expr.id()==ID_symbol &&
           expr.get_bool(ID_C_SSA_symbol) &&
           to_ssa_expr(expr).get_original_expr().id()==ID_index)
@@ -137,10 +60,58 @@ void goto_symext::process_array_expr(exprt &expr)
     const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
     exprt tmp=index_expr.array();
     expr.swap(tmp);
+
+    process_array_expr(expr);
+  }
+  else if(expr.id() != ID_symbol)
+  {
+    object_descriptor_exprt ode;
+    ode.build(expr, ns);
+    do_simplify(ode.offset());
+
+    expr = ode.root_object();
+
+    if(!ode.offset().is_zero())
+    {
+      if(expr.type().id() != ID_array)
+      {
+        exprt array_size = size_of_expr(expr.type(), ns);
+        do_simplify(array_size);
+        expr =
+          byte_extract_exprt(
+            byte_extract_id(),
+            expr,
+            from_integer(0, index_type()),
+            array_typet(char_type(), array_size));
+      }
+
+      // given an array type T[N], i.e., an array of N elements of type T, and a
+      // byte offset B, compute the array offset B/sizeof(T) and build a new
+      // type T[N-(B/sizeof(T))]
+      const array_typet &prev_array_type = to_array_type(expr.type());
+      const typet &array_size_type = prev_array_type.size().type();
+      const typet &subtype = prev_array_type.subtype();
+
+      exprt new_offset(ode.offset());
+      if(new_offset.type() != array_size_type)
+        new_offset.make_typecast(array_size_type);
+      exprt subtype_size = size_of_expr(subtype, ns);
+      if(subtype_size.type() != array_size_type)
+        subtype_size.make_typecast(array_size_type);
+      new_offset = div_exprt(new_offset, subtype_size);
+      minus_exprt new_size(prev_array_type.size(), new_offset);
+      do_simplify(new_size);
+
+      array_typet new_array_type(subtype, new_size);
+
+      expr =
+        byte_extract_exprt(
+          byte_extract_id(),
+          expr,
+          ode.offset(),
+          new_array_type);
+    }
   }
-  else
-    Forall_operands(it, expr)
-      process_array_expr(*it);
 }
 
 /// Rewrite index/member expressions in byte_extract to offset