Merge pull request #1800 from tautschnig/fix-process_array_expr

 Fix process_array_expr to take into account pointer offset

Author: tautschnig

regression/cbmc-from-CVS/Array_operations1/main.c

@@ -0,0 +1,57 @@
+void test_equal()
+{
+  char array1[100], array2[100];
+  _Bool cmp;
+  int index;
+
+  cmp = __CPROVER_array_equal(array1, array2);
+
+  __CPROVER_assume(index >= 0 && index < 100);
+  __CPROVER_assume(cmp);
+
+  __CPROVER_assert(array1[index] == array2[index], "arrays are equal");
+}
+
+void test_copy()
+{
+  char array1[100], array2[100], array3[90];
+
+  array2[10] = 11;
+  array3[10] = 11;
+  array2[99] = 42;
+  __CPROVER_array_copy(array1, array2);
+
+  __CPROVER_assert(array1[10] == 11, "array1[10] is OK");
+  __CPROVER_assert(array1[99] == 42, "array1[99] is OK");
+
+  __CPROVER_array_copy(array1, array3);
+  __CPROVER_assert(array1[10] == 11, "array1[10] is OK");
+  __CPROVER_assert(array1[99] == 42, "expected to fail");
+}
+
+void test_replace()
+{
+  char array1[100], array2[90];
+
+  array1[99] = 42;
+  array2[10] = 11;
+  __CPROVER_array_replace(array1, array2);
+
+  __CPROVER_assert(array1[10] == 11, "array1[10] is OK");
+  __CPROVER_assert(array1[99] == 42, "array1[99] is OK");
+}
+
+void test_set()
+{
+  char array1[100];
+  __CPROVER_array_set(array1, 111);
+  __CPROVER_assert(array1[44] == 111, "array1[44] is OK");
+}
+
+int main()
+{
+  test_equal();
+  test_copy();
+  test_replace();
+  test_set();
+}

regression/cbmc/Array_operations1/main.c

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[test_copy\.assertion\.4\] expected to fail: FAILURE$
+^\*\* 1 of 8 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/Array_operations1/test.desc

@@ -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/main.c

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

regression/cbmc-from-CVS/Array_operations1/test.desc renamed to regression/cbmc/memcpy2/test.desc

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

regression/cbmc/memcpy3/main.c

@@ -838,51 +838,12 @@ void goto_convertt::do_array_op(
   array_op_statement.operands()=arguments;
   array_op_statement.add_source_location()=function.source_location();
 
-  copy(array_op_statement, OTHER, dest);
-}
-
-void goto_convertt::do_array_equal(
-  const exprt &lhs,
-  const exprt &function,
-  const exprt::operandst &arguments,
-  goto_programt &dest)
-{
-  if(arguments.size()!=2)
-  {
-    error().source_location=function.find_source_location();
-    error() << "array_equal expects two arguments" << eom;
-    throw 0;
-  }
-
-  const typet &arg0_type=ns.follow(arguments[0].type());
-  const typet &arg1_type=ns.follow(arguments[1].type());
+  // lhs is only used with array_equal, in all other cases it should be nil (as
+  // they are of type void)
+  if(id == ID_array_equal)
+    array_op_statement.copy_to_operands(lhs);
 
-  if(arg0_type.id()!=ID_pointer ||
-     arg1_type.id()!=ID_pointer)
-  {
-    error().source_location=function.find_source_location();
-    error() << "array_equal expects pointer arguments" << eom;
-    throw 0;
-  }
-
-  if(lhs.is_not_nil())
-  {
-    code_assignt assignment;
-
-    // add dereferencing here
-    dereference_exprt lhs_array, rhs_array;
-    lhs_array.op0()=arguments[0];
-    rhs_array.op0()=arguments[1];
-    lhs_array.type()=arg0_type.subtype();
-    rhs_array.type()=arg1_type.subtype();
-
-    assignment.lhs()=lhs;
-    assignment.rhs()=binary_exprt(
-      lhs_array, ID_array_equal, rhs_array, lhs.type());
-    assignment.add_source_location()=function.source_location();
-
-    convert(assignment, dest);
-  }
+  copy(array_op_statement, OTHER, dest);
 }
 
 bool is_lvalue(const exprt &expr)
@@ -1213,7 +1174,7 @@ void goto_convertt::do_function_call_symbol(
   }
   else if(identifier==CPROVER_PREFIX "array_equal")
   {
-    do_array_equal(lhs, function, arguments, dest);
+    do_array_op(ID_array_equal, lhs, function, arguments, dest);
   }
   else if(identifier==CPROVER_PREFIX "array_set")
   {

regression/cbmc/memcpy3/test.desc

@@ -245,15 +245,13 @@ class goto_symext
   // this does the following:
   // a) rename non-det choices
   // b) remove pointer dereferencing
-  // c) rewrite array_equal expression into equality
+  // c) clean up byte_extract on the lhs of an assignment
   void clean_expr(
     exprt &, statet &, bool write);
 
-  void replace_array_equal(exprt &);
   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);