diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index a03ebfdffef..7bf811bb87b 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -31,19 +31,17 @@ std::size_t goto_statet::increase_generation( const ssa_exprt &lhs, std::function fresh_l2_name_provider) { - std::size_t n = fresh_l2_name_provider(l1_identifier); + const std::size_t n = fresh_l2_name_provider(l1_identifier); - const auto r_opt = level2.current_names.find(l1_identifier); - - if(!r_opt) + if(const auto r_opt = level2.current_names.find(l1_identifier)) { - level2.current_names.insert(l1_identifier, std::make_pair(lhs, n)); + std::pair copy = r_opt->get(); + copy.second = n; + level2.current_names.replace(l1_identifier, std::move(copy)); } else { - std::pair copy = r_opt->get(); - copy.second = n; - level2.current_names.replace(l1_identifier, std::move(copy)); + level2.current_names.insert(l1_identifier, std::make_pair(lhs, n)); } return n; diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index d8cb995077d..245b3655e26 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -514,6 +514,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared( } /// thread encoding +/// \return true if \p expr is shared between threads bool goto_symex_statet::l2_thread_write_encoding( const ssa_exprt &expr, const namespacet &ns) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 35c7188c493..4101dd84037 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -217,7 +217,7 @@ class goto_symex_statet final : public goto_statet unsigned remaining_vccs = 0; /// Allocates a fresh L2 name for the given L1 identifier, and makes it the - // latest generation on this path. + /// latest generation on this path. std::size_t increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs) { diff --git a/src/goto-symex/renamed.h b/src/goto-symex/renamed.h index 4781271da15..58fe9ed9818 100644 --- a/src/goto-symex/renamed.h +++ b/src/goto-symex/renamed.h @@ -50,7 +50,7 @@ class renamedt : private underlyingt }; friend renamedt - symex_level0(ssa_exprt, const namespacet &, unsigned); + symex_level0(ssa_exprt, const namespacet &, std::size_t); friend struct symex_level1t; friend struct symex_level2t; friend class goto_symex_statet; diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 1653e93df57..26e8b98af78 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -31,7 +31,7 @@ void get_variables( } renamedt -symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) +symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr) { // already renamed? if(!ssa_expr.get_level_0().empty()) @@ -56,21 +56,23 @@ symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) return renamedt{ssa_expr}; } -void symex_level1t::insert(const renamedt &ssa, unsigned index) +void symex_level1t::insert( + const renamedt &ssa, + std::size_t index) { current_names.insert( ssa.get().get_identifier(), std::make_pair(ssa.get(), index)); } -optionalt> symex_level1t::insert_or_replace( +optionalt> symex_level1t::insert_or_replace( const renamedt &ssa, - unsigned index) + std::size_t index) { const irep_idt &identifier = ssa.get().get_identifier(); const auto old_value = current_names.find(identifier); if(old_value) { - std::pair result = *old_value; + std::pair result = *old_value; current_names.replace(identifier, std::make_pair(ssa.get(), index)); return result; } diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index 168e7031237..428299e0797 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -29,7 +29,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// This is extended by the different symex_level structures which are used /// during symex to ensure static single assignment (SSA) form. using symex_renaming_levelt = - sharing_mapt>; + sharing_mapt>; /// Add the \c ssa_exprt of current_names to vars DEPRECATED(SINCE(2019, 6, 5, "Unused")) @@ -44,7 +44,7 @@ void get_variables( /// a guard, a shared variable or a function. \p ns is queried to decide /// whether we are in one of these cases. renamedt -symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr); +symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr); /// Functor to set the level 1 renaming of SSA expressions. /// Level 1 corresponds to function frames. @@ -52,13 +52,13 @@ symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr); struct symex_level1t { /// Assume \p ssa is not already known - void insert(const renamedt &ssa, unsigned index); + void insert(const renamedt &ssa, std::size_t index); /// Set the index for \p ssa to index. /// \return if an index for \p ssa was already know, returns it's previous /// value. - optionalt> - insert_or_replace(const renamedt &ssa, unsigned index); + optionalt> + insert_or_replace(const renamedt &ssa, std::size_t index); /// \return true if \p ssa has an associated index bool has(const renamedt &ssa) const; diff --git a/src/goto-symex/ssa_step.cpp b/src/goto-symex/ssa_step.cpp index 3deac1253ac..5d92a5516f4 100644 --- a/src/goto-symex/ssa_step.cpp +++ b/src/goto-symex/ssa_step.cpp @@ -221,9 +221,7 @@ SSA_assignment_stept::SSA_assignment_stept( exprt _ssa_full_lhs, exprt _original_full_lhs, exprt _ssa_rhs, - exprt _cond_expr, - symex_targett::assignment_typet _assignment_type, - bool _hidden) + symex_targett::assignment_typet _assignment_type) : SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT) { guard = std::move(_guard); @@ -232,6 +230,8 @@ SSA_assignment_stept::SSA_assignment_stept( original_full_lhs = std::move(_original_full_lhs); ssa_rhs = std::move(_ssa_rhs); assignment_type = _assignment_type; - cond_expr = std::move(_cond_expr); - hidden = _hidden; + cond_expr = equal_exprt{ssa_lhs, ssa_rhs}; + hidden = assignment_type != symex_targett::assignment_typet::STATE && + assignment_type != + symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER; } diff --git a/src/goto-symex/ssa_step.h b/src/goto-symex/ssa_step.h index 84bcbe92642..93b124c724a 100644 --- a/src/goto-symex/ssa_step.h +++ b/src/goto-symex/ssa_step.h @@ -205,9 +205,7 @@ class SSA_assignment_stept : public SSA_stept exprt ssa_full_lhs, exprt original_full_lhs, exprt ssa_rhs, - exprt cond_expr, - symex_targett::assignment_typet assignment_type, - bool hidden); + symex_targett::assignment_typet assignment_type); }; #endif // CPROVER_GOTO_SYMEX_SSA_STEP_H diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 2be9a9262cf..a05369efb6b 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -395,8 +395,7 @@ void goto_symext::symex_assign_from_struct( const exprt::operandst &guard, assignment_typet assignment_type) { - const struct_typet &type = to_struct_type(ns.follow(lhs.type())); - const struct_union_typet::componentst &components = type.components(); + const auto &components = to_struct_type(ns.follow(lhs.type())).components(); PRECONDITION(rhs.operands().size() == components.size()); for(std::size_t i = 0; i < components.size(); ++i) @@ -435,16 +434,15 @@ void goto_symext::symex_assign_symbol( return; } - exprt l2_rhs = [&]() { - exprt guarded_rhs = rhs; - // put assignment guard into the rhs - if(!guard.empty()) - { - guarded_rhs = - if_exprt{conjunction(guard), std::move(guarded_rhs), lhs, rhs.type()}; - } - return state.rename(std::move(guarded_rhs), ns).get(); - }(); + exprt l2_rhs = + state + .rename( + // put assignment guard into the rhs + guard.empty() + ? rhs + : static_cast(if_exprt{conjunction(guard), rhs, lhs}), + ns) + .get(); // Note the following two calls are specifically required for // field-sensitivity. For example, with-expressions, which may have just been @@ -457,7 +455,6 @@ void goto_symext::symex_assign_symbol( do_simplify(assignment.rhs); - const ssa_exprt &l1_lhs = assignment.lhs; const ssa_exprt l2_lhs = state .assignment( assignment.lhs, @@ -468,15 +465,12 @@ void goto_symext::symex_assign_symbol( symex_config.allow_pointer_unsoundness) .get(); - exprt ssa_full_lhs = add_to_lhs(full_lhs, l2_lhs); state.record_events.push(false); - const exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get(); + const exprt l2_full_lhs = + state.rename(add_to_lhs(full_lhs, l2_lhs), ns).get(); state.record_events.pop(); - // do the assignment - const symbolt &symbol = ns.lookup(l2_lhs.get_object_name()); - - if(symbol.is_auxiliary) + if(ns.lookup(l2_lhs.get_object_name()).is_auxiliary) assignment_type=symex_targett::assignment_typet::HIDDEN; log.conditional_output( @@ -486,19 +480,16 @@ void goto_symext::symex_assign_symbol( << messaget::eom; }); - const exprt assignment_guard = - make_and(state.guard.as_expr(), conjunction(guard)); - - const exprt original_lhs = get_original_name(l2_full_lhs); target.assignment( - assignment_guard, + make_and(state.guard.as_expr(), conjunction(guard)), l2_lhs, l2_full_lhs, - original_lhs, + get_original_name(l2_full_lhs), assignment.rhs, state.source, assignment_type); + const ssa_exprt &l1_lhs = assignment.lhs; if(field_sensitivityt::is_divisible(l1_lhs)) { // Split composite symbol lhs into its components diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index affa572a95e..ff7e1f6a382 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -114,17 +114,13 @@ void symex_target_equationt::assignment( { PRECONDITION(ssa_lhs.is_not_nil()); - SSA_steps.emplace_back(SSA_assignment_stept{ - source, - guard, - ssa_lhs, - ssa_full_lhs, - original_full_lhs, - ssa_rhs, - equal_exprt(ssa_lhs, ssa_rhs), - assignment_type, - assignment_type != assignment_typet::STATE && - assignment_type != assignment_typet::VISIBLE_ACTUAL_PARAMETER}); + SSA_steps.emplace_back(SSA_assignment_stept{source, + guard, + ssa_lhs, + ssa_full_lhs, + original_full_lhs, + ssa_rhs, + assignment_type}); merge_ireps(SSA_steps.back()); } diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index 42894c0cefc..53acec47310 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -178,19 +178,19 @@ const irep_idt ssa_exprt::get_l1_object_identifier() const #endif } -void ssa_exprt::set_level_0(unsigned i) +void ssa_exprt::set_level_0(std::size_t i) { set(ID_L0, i); ::update_identifier(*this); } -void ssa_exprt::set_level_1(unsigned i) +void ssa_exprt::set_level_1(std::size_t i) { set(ID_L1, i); ::update_identifier(*this); } -void ssa_exprt::set_level_2(unsigned i) +void ssa_exprt::set_level_2(std::size_t i) { set(ID_L2, i); ::update_identifier(*this); diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index b3503821d8a..a7902db8ab9 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -52,11 +52,11 @@ class ssa_exprt:public symbol_exprt return o.get_identifier(); } - void set_level_0(unsigned i); + void set_level_0(std::size_t i); - void set_level_1(unsigned i); + void set_level_1(std::size_t i); - void set_level_2(unsigned i); + void set_level_2(std::size_t i); void remove_level_2();