From b03077b10d71abf3b32f1086dd6dfc44983e43a2 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 17 Jul 2019 15:43:01 +0100 Subject: [PATCH 1/6] Expose check_renaming utility function In the process it is moved (without change) to renaming_level.h/cpp, alongside the similarly-structured get_original_name functions. --- src/goto-symex/goto_symex_state.cpp | 84 ----------------------------- src/goto-symex/renaming_level.cpp | 80 +++++++++++++++++++++++++++ src/goto-symex/renaming_level.h | 12 +++++ 3 files changed, 92 insertions(+), 84 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 31cfcd03ba3..69928378e52 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -48,90 +48,6 @@ goto_symex_statet::goto_symex_statet( goto_symex_statet::~goto_symex_statet()=default; -/// Check that \p expr is correctly renamed to level 2 and return true in case -/// an error is detected. -static bool check_renaming(const exprt &expr); - -static bool check_renaming(const typet &type) -{ - if(type.id()==ID_array) - return check_renaming(to_array_type(type).size()); - else if(type.id() == ID_struct || type.id() == ID_union) - { - for(const auto &c : to_struct_union_type(type).components()) - if(check_renaming(c.type())) - return true; - } - else if(type.has_subtype()) - return check_renaming(to_type_with_subtype(type).subtype()); - - return false; -} - -static bool check_renaming_l1(const exprt &expr) -{ - if(check_renaming(expr.type())) - return true; - - if(expr.id()==ID_symbol) - { - const auto &type = expr.type(); - if(!expr.get_bool(ID_C_SSA_symbol)) - return type.id() != ID_code && type.id() != ID_mathematical_function; - if(!to_ssa_expr(expr).get_level_2().empty()) - return true; - if(to_ssa_expr(expr).get_original_expr().type() != type) - return true; - } - else - { - forall_operands(it, expr) - if(check_renaming_l1(*it)) - return true; - } - - return false; -} - -static bool check_renaming(const exprt &expr) -{ - if(check_renaming(expr.type())) - return true; - - if( - expr.id() == ID_address_of && - to_address_of_expr(expr).object().id() == ID_symbol) - { - return check_renaming_l1(to_address_of_expr(expr).object()); - } - else if( - expr.id() == ID_address_of && - to_address_of_expr(expr).object().id() == ID_index) - { - const auto index_expr = to_index_expr(to_address_of_expr(expr).object()); - return check_renaming_l1(index_expr.array()) || - check_renaming(index_expr.index()); - } - else if(expr.id()==ID_symbol) - { - const auto &type = expr.type(); - if(!expr.get_bool(ID_C_SSA_symbol)) - return type.id() != ID_code && type.id() != ID_mathematical_function; - if(to_ssa_expr(expr).get_level_2().empty()) - return true; - if(to_ssa_expr(expr).get_original_expr().type() != type) - return true; - } - else - { - forall_operands(it, expr) - if(check_renaming(*it)) - return true; - } - - return false; -} - template <> renamedt goto_symex_statet::set_indices(ssa_exprt ssa_expr, const namespacet &ns) diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index e060e429e29..b2ef622fbb9 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -205,3 +205,83 @@ typet get_original_name(typet type) } return type; } + +bool check_renaming(const typet &type) +{ + if(type.id() == ID_array) + return check_renaming(to_array_type(type).size()); + else if(type.id() == ID_struct || type.id() == ID_union) + { + for(const auto &c : to_struct_union_type(type).components()) + if(check_renaming(c.type())) + return true; + } + else if(type.has_subtype()) + return check_renaming(to_type_with_subtype(type).subtype()); + + return false; +} + +bool check_renaming_l1(const exprt &expr) +{ + if(check_renaming(expr.type())) + return true; + + if(expr.id() == ID_symbol) + { + const auto &type = expr.type(); + if(!expr.get_bool(ID_C_SSA_symbol)) + return type.id() != ID_code && type.id() != ID_mathematical_function; + if(!to_ssa_expr(expr).get_level_2().empty()) + return true; + if(to_ssa_expr(expr).get_original_expr().type() != type) + return true; + } + else + { + forall_operands(it, expr) + if(check_renaming_l1(*it)) + return true; + } + + return false; +} + +bool check_renaming(const exprt &expr) +{ + if(check_renaming(expr.type())) + return true; + + if( + expr.id() == ID_address_of && + to_address_of_expr(expr).object().id() == ID_symbol) + { + return check_renaming_l1(to_address_of_expr(expr).object()); + } + else if( + expr.id() == ID_address_of && + to_address_of_expr(expr).object().id() == ID_index) + { + const auto index_expr = to_index_expr(to_address_of_expr(expr).object()); + return check_renaming_l1(index_expr.array()) || + check_renaming(index_expr.index()); + } + else if(expr.id() == ID_symbol) + { + const auto &type = expr.type(); + if(!expr.get_bool(ID_C_SSA_symbol)) + return type.id() != ID_code && type.id() != ID_mathematical_function; + if(to_ssa_expr(expr).get_level_2().empty()) + return true; + if(to_ssa_expr(expr).get_original_expr().type() != type) + return true; + } + else + { + forall_operands(it, expr) + if(check_renaming(*it)) + return true; + } + + return false; +} diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index 876cfe56909..069ea0d6ddc 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -103,4 +103,16 @@ exprt get_original_name(exprt expr); /// Undo all levels of renaming typet get_original_name(typet type); +/// Check that \p expr is correctly renamed to level 2 and return true in case +/// an error is detected. +bool check_renaming(const exprt &expr); + +/// Check that \p expr is correctly renamed to level 1 and return true in case +/// an error is detected. +bool check_renaming_l1(const exprt &expr); + +/// Check that \p type is correctly renamed to level 2 and return true in case +/// an error is detected. +bool check_renaming(const typet &type); + #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H From 7932fdd64bef98c0a8951e28d1b4d01652301343 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 17 Jul 2019 15:43:40 +0100 Subject: [PATCH 2/6] Factor out is_read_only_object function --- src/goto-symex/goto_symex_state.h | 8 ++++++++ src/goto-symex/symex_assign.cpp | 6 +----- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index e636b794c45..33a124863ec 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -239,6 +239,14 @@ class goto_symex_statet final : public goto_statet return fresh_l2_name_provider; } + /// Returns true if \p lvalue is a read-only object, such as the null object + static bool is_read_only_object(const exprt &lvalue) + { + return lvalue.id() == ID_string_constant || lvalue.id() == ID_null_object || + lvalue.id() == "zero_string" || lvalue.id() == "is_zero_string" || + lvalue.id() == "zero_string_length"; + } + private: std::function fresh_l2_name_provider; diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 8cc62d897e0..93fb4c28581 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -67,11 +67,7 @@ void symex_assignt::assign_rec( assign_if(to_if_expr(lhs), full_lhs, rhs, guard); else if(lhs.id()==ID_typecast) assign_typecast(to_typecast_expr(lhs), full_lhs, rhs, guard); - else if(lhs.id() == ID_string_constant || - lhs.id() == ID_null_object || - lhs.id() == "zero_string" || - lhs.id() == "is_zero_string" || - lhs.id() == "zero_string_length") + else if(goto_symex_statet::is_read_only_object(lhs)) { // ignore } From e5e026d2015aedf17b653b9351b18bd030af1c32 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 17 Jul 2019 15:45:21 +0100 Subject: [PATCH 3/6] Implement l2_rename_rvalues(lvalue) This renames the rvalue components of an lvalue expression to L2, such as the index of an array expression or the offset involved in byte-extract operation. Lvalue components (e.g. symbols) are left alone. --- src/goto-symex/goto_symex_state.cpp | 68 +++++++++++++++++++++++++++++ src/goto-symex/goto_symex_state.h | 2 + 2 files changed, 70 insertions(+) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 69928378e52..b68ee8187bb 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -260,6 +261,73 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) } } +exprt goto_symex_statet::l2_rename_rvalues(exprt lvalue, const namespacet &ns) +{ + rename(lvalue.type(), irep_idt(), ns); + + if(lvalue.id() == ID_symbol) + { + // Nothing to do + } + else if(is_read_only_object(lvalue)) + { + // Ignore apparent writes to 'NULL-object' and similar read-only objects + } + else if(lvalue.id() == ID_typecast) + { + auto &typecast_lvalue = to_typecast_expr(lvalue); + typecast_lvalue.op() = l2_rename_rvalues(typecast_lvalue.op(), ns); + } + else if(lvalue.id() == ID_member) + { + auto &member_lvalue = to_member_expr(lvalue); + member_lvalue.compound() = l2_rename_rvalues(member_lvalue.compound(), ns); + } + else if(lvalue.id() == ID_index) + { + // The index is an rvalue: + auto &index_lvalue = to_index_expr(lvalue); + index_lvalue.array() = l2_rename_rvalues(index_lvalue.array(), ns); + index_lvalue.index() = rename(index_lvalue.index(), ns).get(); + } + else if( + lvalue.id() == ID_byte_extract_little_endian || + lvalue.id() == ID_byte_extract_big_endian) + { + // The offset is an rvalue: + auto &byte_extract_lvalue = to_byte_extract_expr(lvalue); + byte_extract_lvalue.op() = l2_rename_rvalues(byte_extract_lvalue.op(), ns); + byte_extract_lvalue.offset() = rename(byte_extract_lvalue.offset(), ns); + } + else if(lvalue.id() == ID_if) + { + // The condition is an rvalue: + auto &if_lvalue = to_if_expr(lvalue); + if_lvalue.cond() = rename(if_lvalue.cond(), ns); + if(!if_lvalue.cond().is_false()) + if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns); + if(!if_lvalue.cond().is_true()) + if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns); + } + else if(lvalue.id() == ID_complex_real) + { + auto &complex_real_lvalue = to_complex_real_expr(lvalue); + complex_real_lvalue.op() = l2_rename_rvalues(complex_real_lvalue.op(), ns); + } + else if(lvalue.id() == ID_complex_imag) + { + auto &complex_imag_lvalue = to_complex_imag_expr(lvalue); + complex_imag_lvalue.op() = l2_rename_rvalues(complex_imag_lvalue.op(), ns); + } + else + { + throw unsupported_operation_exceptiont( + "l2_rename_rvalues case `" + lvalue.id_string() + "' not handled"); + } + + return lvalue; +} + template renamedt goto_symex_statet::rename(exprt expr, const namespacet &ns); diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 33a124863ec..b0ccbec29f2 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -107,6 +107,8 @@ class goto_symex_statet final : public goto_statet template void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns); + exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns); + /// \return lhs renamed to level 2 renamedt assignment( ssa_exprt lhs, // L0/L1 From 4d1f9ca02cabf867d22dd19c673f16db1a348dd0 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 17 Jul 2019 15:46:59 +0100 Subject: [PATCH 4/6] Symex: rename LHS rvalue components and simplify before symex_assign_rec This was already happening in most cases (e.g. symex_dereference would apply field-sensitivity before symex_assign_rec was entered), but the case of a statically non-constant but dynamically constant array index or byte-extract offset would only be handled *after* symex_assign_rec, leading to an asymmetry in which operations were combined into the ssa_exprt and which ones accumulated in the expr_skeletont. With this change the LHS expression is maximally renamed and simplified before symex_assign_rec is entered, which means that any field-sensitive symbols on the LHS are fully constructed as early as possible, and expr_skeletont only accumulates those member, index and byte-extract operations which *cannot* be associated with an ssa_exprt. This means there is no need to undo with-operations or try to simplify byte-extract operations in goto_symext::assign_from_non_struct_symbol, as this has been taken care of already, and the l2_full_lhs can be constructed from the expression skeleton trivially. --- src/goto-symex/goto_symex.cpp | 7 ++++ src/goto-symex/symex_assign.cpp | 43 ++++++++-------------- unit/goto-symex/symex_assign.cpp | 63 ++++++++++++++++++++++++-------- 3 files changed, 71 insertions(+), 42 deletions(-) diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 7a4818fc812..37800249436 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -41,6 +41,13 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code) << messaget::eom; }); + // rvalues present within the lhs (for example, "some_array[this_rvalue]" or + // "byte_extract from an_lvalue offset this_rvalue") can affect whether + // we use field-sensitive symbols or not, so L2-rename them up front: + lhs = state.l2_rename_rvalues(lhs, ns); + do_simplify(lhs); + lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true); + if(rhs.id() == ID_side_effect) { const side_effect_exprt &side_effect_expr = to_side_effect_expr(rhs); diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 93fb4c28581..831df85f6c8 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -362,16 +362,7 @@ void symex_assignt::assign_non_struct_symbol( ns) .get(); - // Note the following two calls are specifically required for - // field-sensitivity. For example, with-expressions, which may have just been - // introduced by assign_struct_member, are transformed into member - // expressions on the LHS. If we add an option to disable field-sensitivity - // in the future these should be omitted. - assignmentt assignment = rewrite_with_to_field_symbols( - state, - shift_indexed_access_to_lhs( - state, {lhs, full_lhs, std::move(l2_rhs)}, ns, symex_config.simplify_opt), - ns); + assignmentt assignment{lhs, full_lhs, l2_rhs}; if(symex_config.simplify_opt) assignment.rhs = simplify_expr(std::move(assignment.rhs), ns); @@ -387,8 +378,15 @@ void symex_assignt::assign_non_struct_symbol( .get(); state.record_events.push(false); - const exprt l2_full_lhs = - state.rename(assignment.original_lhs_skeleton.apply(l2_lhs), ns).get(); + // Note any other symbols mentioned in the skeleton are rvalues -- for example + // array indices -- and were renamed to L2 at the start of + // goto_symext::symex_assign. + const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs); + if(symex_config.run_validation_checks) + { + INVARIANT( + !check_renaming(l2_full_lhs), "l2_full_lhs should be renamed to L2"); + } state.record_events.pop(); auto current_assignment_type = @@ -552,23 +550,14 @@ void symex_assignt::assign_if( exprt::operandst &guard) { // we have (c?a:b)=e; - exprt renamed_guard = state.rename(lhs.cond(), ns).get(); - if(symex_config.simplify_opt) - renamed_guard = simplify_expr(std::move(renamed_guard), ns); - if(!renamed_guard.is_false()) - { - guard.push_back(renamed_guard); - assign_rec(lhs.true_case(), full_lhs, rhs, guard); - guard.pop_back(); - } + guard.push_back(lhs.cond()); + assign_rec(lhs.true_case(), full_lhs, rhs, guard); + guard.pop_back(); - if(!renamed_guard.is_true()) - { - guard.push_back(not_exprt(renamed_guard)); - assign_rec(lhs.false_case(), full_lhs, rhs, guard); - guard.pop_back(); - } + guard.push_back(not_exprt(lhs.cond())); + assign_rec(lhs.false_case(), full_lhs, rhs, guard); + guard.pop_back(); } void symex_assignt::assign_byte_extract( diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp index e4ad23da4b5..ffa69c1b772 100644 --- a/unit/goto-symex/symex_assign.cpp +++ b/unit/goto-symex/symex_assign.cpp @@ -219,33 +219,66 @@ SCENARIO( symex_config, target_equation} .assign_symbol(struct1_ssa, skeleton, rhs, guard); - THEN("An equation is added to the target") + THEN("Two equations are added to the target") { - REQUIRE(target_equation.SSA_steps.size() == 1); - SSA_stept step = target_equation.SSA_steps.back(); - THEN("LHS is `struct1!0#2..field1`") + REQUIRE(target_equation.SSA_steps.size() == 2); + SSA_stept assign_step = target_equation.SSA_steps.front(); + SSA_stept expand_step = target_equation.SSA_steps.back(); + THEN("Assign step LHS is `struct1!0#1`") { - REQUIRE(step.ssa_lhs.get_identifier() == "struct1!0#1..field1"); + REQUIRE(assign_step.ssa_lhs.get_identifier() == "struct1!0#1"); } - THEN("Original full LHS is `struct1.field1`") + THEN("Assign step original full LHS is `struct1.field1`") { REQUIRE( - step.original_full_lhs == + assign_step.original_full_lhs == member_exprt{struct1_sym, "field1", int_type}); } - THEN("SSA full LHS is `struct1!0#1..field1`") + THEN("Assign step SSA full LHS is `struct1!0#1`") { const auto as_symbol = - expr_try_dynamic_cast(step.ssa_lhs); + expr_try_dynamic_cast(assign_step.ssa_lhs); REQUIRE(as_symbol); - REQUIRE(as_symbol->get_identifier() == "struct1!0#1..field1"); + REQUIRE(as_symbol->get_identifier() == "struct1!0#1"); + } + THEN("Assign step RHS is { struct1!0#0..field1 } with field1 = 234") + { + ssa_exprt struct1_v0_field1{ + member_exprt{struct1_sym, "field1", int_type}}; + struct1_v0_field1.set_level_0(0); + struct1_v0_field1.set_level_2(0); + struct_exprt struct_expr(struct_type); + struct_expr.add_to_operands(struct1_v0_field1); + with_exprt struct1_v0_with_field_set = rhs; + struct1_v0_with_field_set.old() = struct_expr; + REQUIRE(assign_step.ssa_rhs == struct1_v0_with_field_set); } - THEN("RHS is 234") + THEN("Expand step LHS is `struct1!0#2..field1`") { - const auto as_constant = - expr_try_dynamic_cast(step.ssa_rhs); - REQUIRE(as_constant); - REQUIRE(numeric_cast_v(*as_constant) == 234); + REQUIRE( + expand_step.ssa_lhs.get_identifier() == "struct1!0#2..field1"); + } + THEN("Expand step original full LHS is `struct1.field1`") + { + REQUIRE( + expand_step.original_full_lhs == + member_exprt{struct1_sym, "field1", int_type}); + } + THEN("Expand step SSA full LHS is `struct1!0#2..field1`") + { + const auto as_symbol = + expr_try_dynamic_cast(expand_step.ssa_lhs); + REQUIRE(as_symbol); + REQUIRE(as_symbol->get_identifier() == "struct1!0#2..field1"); + } + THEN("Expand step RHS is struct1!0#1.field1") + { + ssa_exprt struct1_v1{struct1_sym}; + struct1_v1.set_level_0(0); + struct1_v1.set_level_2(1); + REQUIRE( + expand_step.ssa_rhs == + member_exprt{struct1_v1, "field1", int_type}); } } } From c529e7e01ea004290ded3afffe5e1e3620607047 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 17 Jul 2019 15:51:52 +0100 Subject: [PATCH 5/6] Remove unused shift_indexed_access_to_lhs and rewrite_with_to_field_symbols --- src/goto-symex/symex_assign.cpp | 200 -------------------------------- 1 file changed, 200 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 831df85f6c8..fb654e69acc 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -113,206 +113,6 @@ struct assignmentt final exprt rhs; }; -/// Replace "with" (or "update") expressions in the right-hand side of -/// \p assignment by their update values and move the index or member to the -/// left-hand side of \p assignment. This effectively undoes the work that -/// \ref symex_assignt::assign_array and -/// \ref symex_assignt::assign_struct_member have done, but now making use -/// of the index/member that may only be known after renaming to L2 has taken -/// place. -/// \tparam use_update: use update_exprt instead of with_exprt when building -/// expressions that modify components of an array or a struct -/// \param [in, out] state: symbolic execution state to perform renaming -/// \param assignment: an assignment to rewrite -/// \param ns: namespace -/// \return the updated assignment -template -static assignmentt rewrite_with_to_field_symbols( - goto_symext::statet &state, - assignmentt assignment, - const namespacet &ns) -{ - exprt &ssa_rhs = assignment.rhs; - ssa_exprt &lhs_mod = assignment.lhs; - if(use_update) - { - while(ssa_rhs.id() == ID_update && - to_update_expr(ssa_rhs).designator().size() == 1 && - (lhs_mod.type().id() == ID_array || - lhs_mod.type().id() == ID_struct || - lhs_mod.type().id() == ID_struct_tag)) - { - exprt field_sensitive_lhs; - const update_exprt &update = to_update_expr(ssa_rhs); - PRECONDITION(update.designator().size() == 1); - const exprt &designator = update.designator().front(); - - if(lhs_mod.type().id() == ID_array) - { - field_sensitive_lhs = - index_exprt(lhs_mod, to_index_designator(designator).index()); - } - else - { - field_sensitive_lhs = member_exprt( - lhs_mod, - to_member_designator(designator).get_component_name(), - update.new_value().type()); - } - - state.field_sensitivity.apply(ns, state, field_sensitive_lhs, true); - - if(field_sensitive_lhs.id() != ID_symbol) - break; - - ssa_rhs = update.new_value(); - lhs_mod = to_ssa_expr(field_sensitive_lhs); - } - } - else - { - while( - ssa_rhs.id() == ID_with && to_with_expr(ssa_rhs).operands().size() == 3 && - (lhs_mod.type().id() == ID_array || lhs_mod.type().id() == ID_struct || - lhs_mod.type().id() == ID_struct_tag)) - { - exprt field_sensitive_lhs; - expr_skeletont lhs_skeleton; - const with_exprt &with_expr = to_with_expr(ssa_rhs); - - if(lhs_mod.type().id() == ID_array) - { - field_sensitive_lhs = index_exprt(lhs_mod, with_expr.where()); - // Access in an array can appear as an index_exprt or a byte_extract - auto index_reverted = expr_skeletont::clear_innermost_index_expr( - assignment.original_lhs_skeleton); - lhs_skeleton = index_reverted - ? *index_reverted - : get_value_or_abort( - expr_skeletont::clear_innermost_byte_extract_expr( - assignment.original_lhs_skeleton)); - } - else - { - field_sensitive_lhs = member_exprt( - lhs_mod, - with_expr.where().get(ID_component_name), - with_expr.new_value().type()); - lhs_skeleton = - get_value_or_abort(expr_skeletont::clear_innermost_member_expr( - assignment.original_lhs_skeleton)); - } - - field_sensitive_lhs = state.field_sensitivity.apply( - ns, state, std::move(field_sensitive_lhs), true); - - if(field_sensitive_lhs.id() != ID_symbol) - break; - - ssa_rhs = with_expr.new_value(); - lhs_mod = to_ssa_expr(field_sensitive_lhs); - assignment.original_lhs_skeleton = lhs_skeleton; - } - } - return assignment; -} - -/// Replace byte-update operations that only affect individual fields of an -/// expression by assignments to just those fields. May generate "with" (or -/// "update") expressions, which \ref rewrite_with_to_field_symbols will then -/// take care of. -/// \tparam use_update: use update_exprt instead of with_exprt when building -/// expressions that modify components of an array or a struct -/// \param [in, out] state: symbolic execution state to perform renaming -/// \param assignment: assignment to transform -/// \param ns: namespace -/// \param do_simplify: set to true if, and only if, simplification is enabled -/// \return updated assignment -template -static assignmentt shift_indexed_access_to_lhs( - goto_symext::statet &state, - assignmentt assignment, - const namespacet &ns, - bool do_simplify) -{ - exprt &ssa_rhs = assignment.rhs; - ssa_exprt &lhs_mod = assignment.lhs; - if( - ssa_rhs.id() == ID_byte_update_little_endian || - ssa_rhs.id() == ID_byte_update_big_endian) - { - const byte_update_exprt &byte_update = to_byte_update_expr(ssa_rhs); - exprt byte_extract = byte_extract_exprt( - byte_update.id() == ID_byte_update_big_endian - ? ID_byte_extract_big_endian - : ID_byte_extract_little_endian, - lhs_mod, - byte_update.offset(), - byte_update.value().type()); - if(do_simplify) - simplify(byte_extract, ns); - - if(byte_extract.id() == ID_symbol) - { - return assignmentt{to_ssa_expr(byte_extract), - std::move(assignment.original_lhs_skeleton), - byte_update.value()}; - } - else if(byte_extract.id() == ID_index || byte_extract.id() == ID_member) - { - ssa_rhs = byte_update.value(); - - while(byte_extract.id() == ID_index || byte_extract.id() == ID_member) - { - if(byte_extract.id() == ID_index) - { - index_exprt &idx = to_index_expr(byte_extract); - ssa_rhs = [&]() -> exprt { - if(use_update) - { - update_exprt new_rhs{idx.array(), exprt{}, ssa_rhs}; - new_rhs.designator().push_back(index_designatort{idx.index()}); - return std::move(new_rhs); - } - else - return with_exprt{idx.array(), idx.index(), ssa_rhs}; - }(); - byte_extract = idx.array(); - } - else - { - member_exprt &member = to_member_expr(byte_extract); - const irep_idt &component_name = member.get_component_name(); - ssa_rhs = [&]() -> exprt { - if(use_update) - { - update_exprt new_rhs{member.compound(), exprt{}, ssa_rhs}; - new_rhs.designator().push_back( - member_designatort{component_name}); - return std::move(new_rhs); - } - else - { - with_exprt new_rhs( - member.compound(), exprt(ID_member_name), ssa_rhs); - new_rhs.where().set(ID_component_name, component_name); - return std::move(new_rhs); - } - }(); - byte_extract = member.compound(); - } - } - - // We may have shifted the previous lhs into the rhs; as the lhs is only - // L1-renamed, we need to rename again. - return assignmentt{to_ssa_expr(byte_extract), - std::move(assignment.original_lhs_skeleton), - state.rename(std::move(ssa_rhs), ns).get()}; - } - } - return assignment; -} - /// Assign a struct expression to a symbol. If \ref symex_assignt::assign_symbol /// was used then we would assign the whole symbol, before extracting its /// components, with results like From c4bc80029d83c4e7c572162345065c74cdcce5bf Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 24 Jul 2019 14:31:03 +0100 Subject: [PATCH 6/6] Remove now-unnecessary expr_skeletont methods These are unused now that we don't have shift_indexed_access_to_lhs or rewrite_with_to_field_symbols --- src/goto-symex/expr_skeleton.cpp | 48 -------------------------------- src/goto-symex/expr_skeleton.h | 18 ------------ 2 files changed, 66 deletions(-) diff --git a/src/goto-symex/expr_skeleton.cpp b/src/goto-symex/expr_skeleton.cpp index 537ae2a0861..8039b9b8678 100644 --- a/src/goto-symex/expr_skeleton.cpp +++ b/src/goto-symex/expr_skeleton.cpp @@ -52,51 +52,3 @@ expr_skeletont expr_skeletont::compose(expr_skeletont other) const { return expr_skeletont(apply(other.skeleton)); } - -/// In the expression corresponding to a skeleton returns a pointer to the -/// deepest subexpression before we encounter nil. -static exprt *deepest_not_nil(exprt &e) -{ - exprt *ptr = &e; - while(!ptr->op0().is_nil()) - ptr = &ptr->op0(); - return ptr; -} - -optionalt -expr_skeletont::clear_innermost_index_expr(expr_skeletont skeleton) -{ - exprt *to_update = deepest_not_nil(skeleton.skeleton); - if(index_exprt *index_expr = expr_try_dynamic_cast(*to_update)) - { - index_expr->make_nil(); - return expr_skeletont{std::move(skeleton)}; - } - return {}; -} - -optionalt -expr_skeletont::clear_innermost_member_expr(expr_skeletont skeleton) -{ - exprt *to_update = deepest_not_nil(skeleton.skeleton); - if(member_exprt *member = expr_try_dynamic_cast(*to_update)) - { - member->make_nil(); - return expr_skeletont{std::move(skeleton)}; - } - return {}; -} - -optionalt -expr_skeletont::clear_innermost_byte_extract_expr(expr_skeletont skeleton) -{ - exprt *to_update = deepest_not_nil(skeleton.skeleton); - if( - to_update->id() != ID_byte_extract_big_endian && - to_update->id() != ID_byte_extract_little_endian) - { - return {}; - } - to_update->make_nil(); - return expr_skeletont{std::move(skeleton.skeleton)}; -} diff --git a/src/goto-symex/expr_skeleton.h b/src/goto-symex/expr_skeleton.h index deaa5b203c4..e9f8cd663a2 100644 --- a/src/goto-symex/expr_skeleton.h +++ b/src/goto-symex/expr_skeleton.h @@ -43,24 +43,6 @@ class expr_skeletont final /// `array2[index]`. static expr_skeletont remove_op0(exprt e); - /// If the deepest subexpression in the skeleton is a member expression, - /// replace it with a nil expression and return the obtained skeleton. - static optionalt - clear_innermost_index_expr(expr_skeletont skeleton); - - /// If the deepest subexpression in the skeleton is a member expression, - /// replace it with a nil expression and return the obtained skeleton. - static optionalt - clear_innermost_member_expr(expr_skeletont skeleton); - - /// If the deepest subexpression in the skeleton is a byte-extract expression, - /// replace it with a nil expression and return the obtained skeleton. - /// For instance, for `(byte_extract(☐, 2, int)).field[index]` - /// `☐.field[index]` is returned, while for `byte_extract(☐.field, 2, int)` - /// an empty optional is returned. - static optionalt - clear_innermost_byte_extract_expr(expr_skeletont skeleton); - private: /// In \c skeleton, nil_exprt is used to mark the sub expression to be /// substituted. The nil_exprt always appears recursively following the first