Do not misuse symex dereferencing code for finding array objects

The task of process_array_expr is to find the objects pointed to; symex
dereferencing does so as well, but also does many other things. Creating an
artificial dereference_exprt imposes restrictions on what optimisations symex
dereferencing can implement. Instead, just make process_array_expr actually get
the objects (via the value set) and then work on those. This duplicates a bit of
code from symex dereferencing, but now yields full control to process_array_expr
over what it needs to make happen. In future, the process_array_expr code may
even get rewritten without having any dependency on what symex dereferencing
exactly does.

Author: tautschnig

src/goto-symex/goto_symex.h

@@ -229,7 +229,7 @@ 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(statet &, exprt &, bool);
   exprt make_auto_object(const typet &, statet &);
   virtual void dereference(exprt &, statet &, bool write);
 

src/goto-symex/symex_clean_expr.cpp

@@ -16,20 +16,26 @@ Author: Daniel Kroening, [email protected]
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
+
+#include "symex_dereference_state.h"
+
+#include <pointer-analysis/value_set_dereference.h>
 
 /// 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)
+static void
+process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
 {
   // This may change the type of the expression!
 
   if(expr.id()==ID_if)
   {
     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(if_expr.true_case(), do_simplify, ns);
+    process_array_expr(if_expr.false_case(), do_simplify, ns);
 
     if(!base_type_eq(if_expr.true_case(), if_expr.false_case(), ns))
     {
@@ -49,7 +55,7 @@ void goto_symext::process_array_expr(exprt &expr)
     // strip
     exprt tmp = to_address_of_expr(expr).object();
     expr.swap(tmp);
-    process_array_expr(expr);
+    process_array_expr(expr, do_simplify, ns);
   }
   else if(expr.id()==ID_symbol &&
           expr.get_bool(ID_C_SSA_symbol) &&
@@ -60,13 +66,14 @@ void goto_symext::process_array_expr(exprt &expr)
     exprt tmp=index_expr.array();
     expr.swap(tmp);
 
-    process_array_expr(expr);
+    process_array_expr(expr, do_simplify, ns);
   }
   else if(expr.id() != ID_symbol)
   {
     object_descriptor_exprt ode;
     ode.build(expr, ns);
-    do_simplify(ode.offset());
+    if(do_simplify)
+      simplify(ode.offset(), ns);
 
     expr = ode.root_object();
 
@@ -75,7 +82,8 @@ void goto_symext::process_array_expr(exprt &expr)
       if(expr.type().id() != ID_array)
       {
         exprt array_size = size_of_expr(expr.type(), ns);
-        do_simplify(array_size);
+        if(do_simplify)
+          simplify(array_size, ns);
         expr =
           byte_extract_exprt(
             byte_extract_id(),
@@ -99,7 +107,8 @@ void goto_symext::process_array_expr(exprt &expr)
         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);
+      if(do_simplify)
+        simplify(new_size, ns);
 
       array_typet new_array_type(subtype, new_size);
 
@@ -113,6 +122,22 @@ void goto_symext::process_array_expr(exprt &expr)
   }
 }
 
+void goto_symext::process_array_expr(statet &state, exprt &expr, bool is_lhs)
+{
+  symex_dereference_statet symex_dereference_state(*this, state);
+
+  value_set_dereferencet dereference(
+    ns, state.symbol_table, symex_dereference_state, language_mode, false);
+
+  expr = dereference.dereference(
+    expr,
+    guardt{true_exprt()},
+    is_lhs ? value_set_dereferencet::modet::WRITE
+           : value_set_dereferencet::modet::READ);
+
+  ::process_array_expr(expr, symex_config.simplify_opt, ns);
+}
+
 /// Rewrite index/member expressions in byte_extract to offset
 static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
 {

src/goto-symex/symex_other.cpp

@@ -9,6 +9,9 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Symbolic Execution
 
+#include <iostream>
+#include <util/format_expr.h>
+
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
@@ -128,7 +131,7 @@ void goto_symext::symex_other(
           statement==ID_array_replace)
   {
     // array_copy and array_replace take two pointers (to arrays); we need to:
-    // 1. dereference the pointers (via clean_expr)
+    // 1. remove any dereference expressions (via clean_expr)
     // 2. find the actual array objects/candidates for objects (via
     // process_array_expr)
     // 3. build an assignment where the type on lhs and rhs is:
@@ -139,14 +142,14 @@ void goto_symext::symex_other(
       "expected array_copy/array_replace statement to have two operands");
 
     // we need to add dereferencing for both operands
-    dereference_exprt dest_array(code.op0());
-    clean_expr(dest_array, state, true);
-    dereference_exprt src_array(code.op1());
+    exprt dest_array(code.op0());
+    clean_expr(dest_array, state, false);
+    exprt src_array(code.op1());
     clean_expr(src_array, state, false);
 
     // obtain the actual arrays
-    process_array_expr(dest_array);
-    process_array_expr(src_array);
+    process_array_expr(state, dest_array, true);
+    process_array_expr(state, src_array, false);
 
     // check for size (or type) mismatch and adjust
     if(!base_type_eq(dest_array.type(), src_array.type(), ns))
@@ -181,7 +184,7 @@ void goto_symext::symex_other(
   {
     // array_set takes a pointer (to an array) and a value that each element
     // should be set to; we need to:
-    // 1. dereference the pointer (via clean_expr)
+    // 1. remove any dereference expressions (via clean_expr)
     // 2. find the actual array object/candidates for objects (via
     // process_array_expr)
     // 3. use the type of the resulting array to construct an array_of
@@ -191,11 +194,11 @@ void goto_symext::symex_other(
       "expected array_set statement to have two operands");
 
     // we need to add dereferencing for the first operand
-    exprt array_expr = dereference_exprt(code.op0());
-    clean_expr(array_expr, state, true);
+    exprt array_expr(code.op0());
+    clean_expr(array_expr, state, false);
 
     // obtain the actual array(s)
-    process_array_expr(array_expr);
+    process_array_expr(state, array_expr, true);
 
     // prepare to build the array_of
     exprt value = code.op1();
@@ -227,7 +230,7 @@ void goto_symext::symex_other(
   {
     // array_equal takes two pointers (to arrays) and the symbol that the result
     // should get assigned to; we need to:
-    // 1. dereference the pointers (via clean_expr)
+    // 1. remove any dereference expressions (via clean_expr)
     // 2. find the actual array objects/candidates for objects (via
     // process_array_expr)
     // 3. build an assignment where the lhs is the previous third argument, and
@@ -238,14 +241,14 @@ void goto_symext::symex_other(
       "expected array_equal statement to have three operands");
 
     // we need to add dereferencing for the first two
-    dereference_exprt array1(code.op0());
+    exprt array1(code.op0());
     clean_expr(array1, state, false);
-    dereference_exprt array2(code.op1());
+    exprt array2(code.op1());
     clean_expr(array2, state, false);
 
     // obtain the actual arrays
-    process_array_expr(array1);
-    process_array_expr(array2);
+    process_array_expr(state, array1, false);
+    process_array_expr(state, array2, false);
 
     code_assignt assignment(code.op2(), equal_exprt(array1, array2));
 
@@ -271,10 +274,10 @@ void goto_symext::symex_other(
       code.operands().size() == 1,
       "expected havoc_object statement to have one operand");
 
-    // we need to add dereferencing for the first operand
-    dereference_exprt object(code.op0(), empty_typet());
-    clean_expr(object, state, true);
+    exprt object(code.op0());
+    clean_expr(object, state, false);
 
+    process_array_expr(state, object, true);
     havoc_rec(state, guardt(true_exprt()), object);
   }
   else