Process array_equal the same way as array_{replace,copy}

array_equal was handled as a special snowflake in both goto-program conversion
and symbolic execution. This simplifies the code and removes a sharing-unaware
pass that ran over all expressions. This commit is only refactoring, no
behavioural changes expected.

This commit also moves a regression test from cbmc-from-CVS to the cbmc folder,
and extends it to cover array_replace.

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-from-CVS/Array_operations1/test.desc

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

@@ -839,51 +839,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)
@@ -1214,7 +1175,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/Array_operations1/test.desc

@@ -245,11 +245,10 @@ 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 &);

src/goto-programs/builtin_functions.cpp

@@ -143,31 +143,6 @@ void goto_symext::process_array_expr(exprt &expr)
       process_array_expr(*it);
 }
 
-void goto_symext::replace_array_equal(exprt &expr)
-{
-  if(expr.id()==ID_array_equal)
-  {
-    assert(expr.operands().size()==2);
-
-    // we expect two index expressions
-    process_array_expr(expr.op0());
-    process_array_expr(expr.op1());
-
-    // type checking
-    if(ns.follow(expr.op0().type())!=
-       ns.follow(expr.op1().type()))
-      expr=false_exprt();
-    else
-    {
-      equal_exprt equality_expr(expr.op0(), expr.op1());
-      expr.swap(equality_expr);
-    }
-  }
-
-  Forall_operands(it, expr)
-    replace_array_equal(*it);
-}
-
 /// Rewrite index/member expressions in byte_extract to offset
 static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
 {
@@ -203,6 +178,4 @@ void goto_symext::clean_expr(
   // lhs
   if(write)
     adjust_byte_extract_rec(expr, ns);
-
-  replace_array_equal(expr);
 }

src/goto-symex/goto_symex.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/rename.h>
 #include <util/base_type.h>
 #include <util/std_expr.h>
@@ -259,6 +260,57 @@ void goto_symext::symex_other(
     assignment.rhs()=array_of_exprt(clean_code.op1(), array_type);
     symex_assign(state, assignment);
   }
+  else if(statement==ID_array_equal)
+  {
+    DATA_INVARIANT(
+      code.operands().size() == 3,
+      "array_equal expected to take three arguments");
+
+    codet clean_code(code);
+
+    // we need to add dereferencing for the first two operands
+    dereference_exprt d0, d1;
+    d0.op0()=code.op0();
+    d0.type()=empty_typet();
+    d1.op0()=code.op1();
+    d1.type()=empty_typet();
+
+    clean_code.op0()=d0;
+    clean_code.op1()=d1;
+
+    clean_expr(clean_code.op0(), state, false);
+    exprt op0_offset=from_integer(0, index_type());
+    if(clean_code.op0().id()==byte_extract_id() &&
+       clean_code.op0().type().id()==ID_empty)
+    {
+      op0_offset=to_byte_extract_expr(clean_code.op0()).offset();
+      clean_code.op0()=clean_code.op0().op0();
+    }
+    clean_expr(clean_code.op1(), state, false);
+    exprt op1_offset=from_integer(0, index_type());
+    if(clean_code.op1().id()==byte_extract_id() &&
+       clean_code.op1().type().id()==ID_empty)
+    {
+      op1_offset=to_byte_extract_expr(clean_code.op1()).offset();
+      clean_code.op1()=clean_code.op1().op0();
+    }
+
+    process_array_expr(clean_code.op0());
+    clean_expr(clean_code.op0(), state, false);
+    process_array_expr(clean_code.op1());
+    clean_expr(clean_code.op1(), state, false);
+
+    if(!base_type_eq(clean_code.op0().type(),
+                     clean_code.op1().type(), ns))
+    {
+      clean_code.op2() = false_exprt();
+    }
+
+    code_assignt assignment(
+      clean_code.op2(),
+      equal_exprt(clean_code.op0(), clean_code.op1()));
+    symex_assign(state, assignment);
+  }
   else if(statement==ID_user_specified_predicate ||
           statement==ID_user_specified_parameter_predicates ||
           statement==ID_user_specified_return_predicates)