diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index fe893a59706..bf405ee81fc 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -17,10 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include +#include void goto_symext::symex_goto(statet &state) { @@ -353,138 +353,194 @@ void goto_symext::merge_value_sets( dest.value_set.make_union(src.value_set); } -void goto_symext::phi_function( - const statet::goto_statet &goto_state, - statet &dest_state) +/// Applies f to `(k, ssa, i, j)` if the first map maps k to (ssa, i) and +/// the second to (ssa', j). If the first map has an entry for k but not the +/// second one then j is 0, and when the first map has no entry for k then i = 0 +static void for_each2( + const std::map> &first_map, + const std::map> &second_map, + const std::function &f) { - auto ssa_of_current_name = - [&](const std::pair> &pair) { - return pair.second.first; - }; - - auto dest_state_names_range = - make_range(dest_state.level2.current_names) - .filter( - [&](const std::pair> &pair) { - // We ignore the identifiers that are already in goto_state names - return goto_state.level2_current_names.count(pair.first) == 0; - }) - .map(ssa_of_current_name); - - // go over all variables to see what changed - auto all_current_names_range = make_range(goto_state.level2_current_names) - .map(ssa_of_current_name) - .concat(dest_state_names_range); - - guardt diff_guard; - if(!all_current_names_range.empty()) + auto second_it = second_map.begin(); + for(const auto &first_pair : first_map) { - diff_guard=goto_state.guard; - - // this gets the diff between the guards - diff_guard-=dest_state.guard; + while(second_it != second_map.end() && second_it->first < first_pair.first) + { + f(second_it->second.first, 0, second_it->second.second); + ++second_it; + } + const ssa_exprt &ssa = first_pair.second.first; + const unsigned count = first_pair.second.second; + if(second_it != second_map.end() && second_it->first == first_pair.first) + { + f(ssa, count, second_it->second.second); + ++second_it; + } + else + f(ssa, count, 0); } - - for(const auto &ssa : all_current_names_range) + while(second_it != second_map.end()) { - const irep_idt l1_identifier = ssa.get_identifier(); - const irep_idt &obj_identifier = ssa.get_object_name(); + f(second_it->second.first, 0, second_it->second.second); + ++second_it; + } +} - if(obj_identifier==guard_identifier) - continue; // just a guard, don't bother +/// Helper function for \c phi_function which merges the names of an identifier +/// for two different states. +/// \param goto_state: first state +/// \param[in, out] dest_state: second state +/// \param ns: namespace +/// \param diff_guard: difference between the guards of the two states +/// \param guard_identifier: prefix used for goto symex guards +/// \param[out] log: logger for debug messages +/// \param do_simplify: should the right-hand-side of the assignment that is +/// added to the target be simplified +/// \param[out] target: equation that will receive the resulting assignment +/// \param ssa: SSA expression to merge +/// \param goto_count: current level 2 count in \p goto_state of +/// \p l1_identifier +/// \param dest_count: level 2 count in \p dest_state of \p l1_identifier +static void merge_names( + const goto_symext::statet::goto_statet &goto_state, + goto_symext::statet &dest_state, + const namespacet &ns, + const guardt &diff_guard, + const irep_idt &guard_identifier, + messaget &log, + const bool do_simplify, + symex_target_equationt &target, + const ssa_exprt &ssa, + const unsigned goto_count, + const unsigned dest_count) +{ + const irep_idt l1_identifier = ssa.get_identifier(); + const irep_idt &obj_identifier = ssa.get_object_name(); - if(goto_state.level2_current_count(l1_identifier)== - dest_state.level2.current_count(l1_identifier)) - continue; // not at all changed + if(obj_identifier == guard_identifier) + return; // just a guard, don't bother - // changed! + if(goto_count == dest_count) + return; // not at all changed - // shared variables are renamed on every access anyway, we don't need to - // merge anything - const symbolt &symbol=ns.lookup(obj_identifier); + // changed! - // shared? - if( - dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 && - (symbol.is_shared() || (dest_state.dirty)(symbol.name))) - continue; // no phi nodes for shared stuff - - // don't merge (thread-)locals across different threads, which - // may have been introduced by symex_start_thread (and will - // only later be removed from level2.current_names by pop_frame - // once the thread is executed) - if( - !ssa.get_level_0().empty() && - ssa.get_level_0() != std::to_string(dest_state.source.thread_nr)) - continue; + // shared variables are renamed on every access anyway, we don't need to + // merge anything + const symbolt &symbol = ns.lookup(obj_identifier); - exprt goto_state_rhs = ssa, dest_state_rhs = ssa; + // shared? + if( + dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 && + (symbol.is_shared() || (dest_state.dirty)(symbol.name))) + return; // no phi nodes for shared stuff + + // don't merge (thread-)locals across different threads, which + // may have been introduced by symex_start_thread (and will + // only later be removed from level2.current_names by pop_frame + // once the thread is executed) + const irep_idt level_0 = ssa.get_level_0(); + if(!level_0.empty() && level_0 != std::to_string(dest_state.source.thread_nr)) + return; - { - const auto p_it = goto_state.propagation.find(l1_identifier); + exprt goto_state_rhs = ssa, dest_state_rhs = ssa; - if(p_it != goto_state.propagation.end()) - goto_state_rhs=p_it->second; - else - to_ssa_expr(goto_state_rhs).set_level_2( - goto_state.level2_current_count(l1_identifier)); - } + { + const auto p_it = goto_state.propagation.find(l1_identifier); - { - const auto p_it = dest_state.propagation.find(l1_identifier); + if(p_it != goto_state.propagation.end()) + goto_state_rhs = p_it->second; + else + to_ssa_expr(goto_state_rhs).set_level_2(goto_count); + } - if(p_it != dest_state.propagation.end()) - dest_state_rhs=p_it->second; - else - to_ssa_expr(dest_state_rhs).set_level_2( - dest_state.level2.current_count(l1_identifier)); - } + { + const auto p_it = dest_state.propagation.find(l1_identifier); - exprt rhs; - - // Don't add a conditional to the assignment when: - // 1. Either guard is false, so we can't follow that branch. - // 2. Either identifier is of generation zero, and so hasn't been - // initialized and therefor an invalid target. - if(dest_state.guard.is_false()) - rhs=goto_state_rhs; - else if(goto_state.guard.is_false()) - rhs=dest_state_rhs; - else if(goto_state.level2_current_count(l1_identifier) == 0) - { - rhs = dest_state_rhs; - } - else if(dest_state.level2.current_count(l1_identifier) == 0) - { - rhs = goto_state_rhs; - } + if(p_it != dest_state.propagation.end()) + dest_state_rhs = p_it->second; else - { - rhs=if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs); - do_simplify(rhs); - } + to_ssa_expr(dest_state_rhs).set_level_2(dest_count); + } - ssa_exprt new_lhs = ssa; - const bool record_events=dest_state.record_events; - dest_state.record_events=false; - dest_state.assignment(new_lhs, rhs, ns, true, true); - dest_state.record_events=record_events; - - log.conditional_output( - log.debug(), - [this, &new_lhs](messaget::mstreamt &mstream) { - mstream << "Assignment to " << new_lhs.get_identifier() - << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]" - << messaget::eom; - }); - - target.assignment( - true_exprt(), - new_lhs, new_lhs, new_lhs.get_original_expr(), - rhs, - dest_state.source, - symex_targett::assignment_typet::PHI); + exprt rhs; + + // Don't add a conditional to the assignment when: + // 1. Either guard is false, so we can't follow that branch. + // 2. Either identifier is of generation zero, and so hasn't been + // initialized and therefor an invalid target. + if(dest_state.guard.is_false()) + rhs = goto_state_rhs; + else if(goto_state.guard.is_false()) + rhs = dest_state_rhs; + else if(goto_count == 0) + { + rhs = dest_state_rhs; } + else if(dest_count == 0) + { + rhs = goto_state_rhs; + } + else + { + rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs); + if(do_simplify) + simplify(rhs, ns); + } + + ssa_exprt new_lhs = ssa; + const bool record_events = dest_state.record_events; + dest_state.record_events = false; + dest_state.assignment(new_lhs, rhs, ns, true, true); + dest_state.record_events = record_events; + + log.conditional_output( + log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) { + mstream << "Assignment to " << new_lhs.get_identifier() << " [" + << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]" + << messaget::eom; + }); + + target.assignment( + true_exprt(), + new_lhs, + new_lhs, + new_lhs.get_original_expr(), + rhs, + dest_state.source, + symex_targett::assignment_typet::PHI); +} + +void goto_symext::phi_function( + const statet::goto_statet &goto_state, + statet &dest_state) +{ + if( + goto_state.level2_current_names.empty() && + dest_state.level2.current_names.empty()) + return; + + guardt diff_guard = goto_state.guard; + // this gets the diff between the guards + diff_guard -= dest_state.guard; + + for_each2( + goto_state.level2_current_names, + dest_state.level2.current_names, + [&](const ssa_exprt &ssa, unsigned goto_count, unsigned dest_count) { + merge_names( + goto_state, + dest_state, + ns, + diff_guard, + guard_identifier, + log, + symex_config.simplify_opt, + target, + ssa, + goto_count, + dest_count); + }); } void goto_symext::loop_bound_exceeded(