From 855dcfaad693edac589891d7878a02ea075befff Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jan 2019 19:54:49 +0000 Subject: [PATCH] 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. --- src/goto-symex/goto_symex.h | 2 +- src/goto-symex/symex_clean_expr.cpp | 41 +++++++++++++++++++++++------ src/goto-symex/symex_other.cpp | 36 ++++++++++++------------- 3 files changed, 52 insertions(+), 27 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 556e784e641..1706bfd7eaa 100644 --- a/src/goto-symex/goto_symex.h +++ b/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); diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 5e57fb178f0..394c3f12d45 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -16,20 +16,26 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include + +#include "symex_dereference_state.h" + +#include /// 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) { diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 96871518b02..4ed1c3eaa7f 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -128,7 +128,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 +139,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 +181,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 +191,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 +227,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 +238,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 +271,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