From a786eb3f830c5f4684a458a43d0b6abd6fd120fb Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 1 May 2019 08:17:32 +0100 Subject: [PATCH] field_sensitivityt::apply does not take a reference We make apply take the expression by copy and return a transformed one. This makes it more intuitive to use and avoid problems of the kind: index_exprt i; apply(ns, s, i, true); f_of_index_expr(i); where in the call to `f_of_index_expr`, `i` is of type `index_exprt` but may not have `ID_index` thus breaking an invariant which we should intuitively have. --- src/goto-symex/field_sensitivity.cpp | 26 +++++++++++++------------- src/goto-symex/field_sensitivity.h | 8 ++++---- src/goto-symex/goto_symex_state.cpp | 2 +- src/goto-symex/symex_assign.cpp | 7 ++++--- src/goto-symex/symex_dereference.cpp | 8 ++++---- 5 files changed, 26 insertions(+), 25 deletions(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index e3465c2c44e..f6dbc409471 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -18,37 +18,37 @@ Author: Michael Tautschnig // #define ENABLE_ARRAY_FIELD_SENSITIVITY -void field_sensitivityt::apply( +exprt field_sensitivityt::apply( const namespacet &ns, goto_symex_statet &state, - exprt &expr, + exprt expr, bool write) const { if(!run_apply) - return; + return expr; if(expr.id() != ID_address_of) { Forall_operands(it, expr) - apply(ns, state, *it, write); + *it = apply(ns, state, std::move(*it), write); } if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) && !write) { - expr = get_fields(ns, state, to_ssa_expr(expr)); + return get_fields(ns, state, to_ssa_expr(expr)); } else if( !write && expr.id() == ID_member && to_member_expr(expr).struct_op().id() == ID_struct) { - simplify(expr, ns); + return simplify_expr(std::move(expr), ns); } #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY else if( !write && expr.id() == ID_index && to_index_expr(expr).array().id() == ID_array) { - simplify(expr, ns); + return simplify_expr(std::move(expr), ns); } #endif // ENABLE_ARRAY_FIELD_SENSITIVITY else if(expr.id() == ID_member) @@ -73,9 +73,9 @@ void field_sensitivityt::apply( member.struct_op() = tmp.get_original_expr(); tmp.set_expression(member); if(was_l2) - expr = state.rename(tmp, ns).get(); + return state.rename(std::move(tmp), ns).get(); else - expr.swap(tmp); + return std::move(tmp); } } #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY @@ -102,12 +102,13 @@ void field_sensitivityt::apply( index.array() = tmp.get_original_expr(); tmp.set_expression(index); if(was_l2) - expr = state.rename(tmp, ns).get(); + return state.rename(std::move(tmp), ns).get(); else - expr.swap(tmp); + return std::move(tmp); } } #endif // ENABLE_ARRAY_FIELD_SENSITIVITY + return expr; } exprt field_sensitivityt::get_fields( @@ -187,8 +188,7 @@ void field_sensitivityt::field_assignments( symex_targett &target, bool allow_pointer_unsoundness) { - exprt lhs_fs = lhs; - apply(ns, state, lhs_fs, false); + const exprt lhs_fs = apply(ns, state, lhs, false); bool run_apply_bak = run_apply; run_apply = false; diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h index 35b10c90fbd..5c5c675f8ce 100644 --- a/src/goto-symex/field_sensitivity.h +++ b/src/goto-symex/field_sensitivity.h @@ -45,11 +45,11 @@ class field_sensitivityt /// existing member or index expressions into symbols are performed. /// \param ns: a namespace to resolve type symbols/tag types /// \param [in,out] state: symbolic execution state - /// \param [in,out] expr: an expression to be (recursively) transformed - this - /// parameter is both input and output. + /// \param expr: an expression to be (recursively) transformed. /// \param write: set to true if the expression is to be used as an lvalue. - void - apply(const namespacet &ns, goto_symex_statet &state, exprt &expr, bool write) + /// \return the transformed expression + exprt + apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const; /// Compute an expression representing the individual components of a diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 3943cf34788..b4da35b1185 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -337,7 +337,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) "if_exprt"); if(level == L2) - field_sensitivity.apply(ns, *this, expr, false); + expr = field_sensitivity.apply(ns, *this, std::move(expr), false); return renamedt{std::move(expr)}; } diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index d4f27280980..6ec66cba127 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -271,7 +271,8 @@ static void rewrite_with_to_field_symbols( with_expr.new_value().type()); } - state.field_sensitivity.apply(ns, state, field_sensitive_lhs, true); + field_sensitive_lhs = state.field_sensitivity.apply( + ns, state, std::move(field_sensitive_lhs), true); if(field_sensitive_lhs.id() != ID_symbol) break; @@ -392,8 +393,8 @@ void goto_symext::symex_assign_from_struct( for(std::size_t i = 0; i < components.size(); ++i) { const auto &comp = components[i]; - exprt lhs_field = member_exprt(lhs, comp.get_name(), comp.type()); - state.field_sensitivity.apply(ns, state, lhs_field, true); + const exprt lhs_field = state.field_sensitivity.apply( + ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true); INVARIANT( lhs_field.id() == ID_symbol, "member of symbol should be susceptible to field-sensitivity"); diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index e6879fd491e..1e6d54747f5 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -244,7 +244,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write) // ...and may have introduced a member-of-symbol construct with a // corresponding SSA symbol: - state.field_sensitivity.apply(ns, state, expr, write); + expr = state.field_sensitivity.apply(ns, state, std::move(expr), write); } else if( expr.id() == ID_index && to_index_expr(expr).array().id() == ID_member && @@ -359,8 +359,8 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write) // from different frames. Would be enough to rename // symbols whose address is taken. PRECONDITION(!state.call_stack().empty()); - exprt l1_expr = state.rename(expr, ns).get(); - state.field_sensitivity.apply(ns, state, l1_expr, write); + exprt l1_expr = state.field_sensitivity.apply( + ns, state, state.rename(expr, ns).get(), write); // start the recursion! dereference_rec(l1_expr, state, write); @@ -394,5 +394,5 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write) "simplify re-introduced dereferencing"); } - state.field_sensitivity.apply(ns, state, expr, write); + expr = state.field_sensitivity.apply(ns, state, std::move(expr), write); }