diff --git a/src/analyses/variable-sensitivity/three_way_merge_abstract_interpreter.cpp b/src/analyses/variable-sensitivity/three_way_merge_abstract_interpreter.cpp index 8735c499b91..86b588e4c28 100644 --- a/src/analyses/variable-sensitivity/three_way_merge_abstract_interpreter.cpp +++ b/src/analyses/variable-sensitivity/three_way_merge_abstract_interpreter.cpp @@ -160,22 +160,21 @@ bool ai_three_way_merget::visit_edge_function_call( *this, ns); - // TODO : this is probably needed to avoid three_way_merge modifying one of - // its arguments as it goes. A better solution would be to refactor - // merge_three_way_function_return. - const std::unique_ptr ptr_s_working_copy( - make_temporary_state(s_working)); + // The base for the three way merge is the call site + const std::unique_ptr ptr_call_site_working( + make_temporary_state(get_state(p_call_site))); + auto tmp2 = + dynamic_cast(&(*ptr_call_site_working)); + INVARIANT(tmp2 != nullptr, "Three-way merge requires domain support"); + variable_sensitivity_domaint &s_call_site_working = *tmp2; log.progress() << "three way merge... "; - s_working.merge_three_way_function_return( - get_state(p_call_site), - get_state(p_callee_start), - *ptr_s_working_copy, - ns); + s_call_site_working.merge_three_way_function_return( + get_state(p_callee_start), s_working, ns); log.progress() << "merging... "; if( - merge(s_working, p_callee_end, p_return_site) || + merge(s_call_site_working, p_callee_end, p_return_site) || (return_step.first == ai_history_baset::step_statust::NEW && !s_working.is_bottom())) { diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp index 00ebc332863..df2bbc557ab 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp @@ -438,20 +438,9 @@ bool variable_sensitivity_dependence_domaint::merge( } /** - * Perform a context aware merge of the changes that have been applied - * between function_start and the current state. Anything that has not been - * modified will be taken from the \p function_call domain. - * - * \param function_call: The local of the merge - values from here will be - * taken if they have not been modified - * \param function_start: The base of the merge - changes that have been made - * between here and the end will be retained. - * \param function_end: The end of the merge - changes that have been made -/// between the start and here will be retained. - * \param ns: The global namespace + * \copydoc variable_sensitivity_domaint::merge_three_way_function_return */ void variable_sensitivity_dependence_domaint::merge_three_way_function_return( - const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns) @@ -462,7 +451,7 @@ void variable_sensitivity_dependence_domaint::merge_three_way_function_return( // the three way merge is that the underlying variable sensitivity domain // does its three way merge. variable_sensitivity_domaint::merge_three_way_function_return( - function_call, function_start, function_end, ns); + function_start, function_end, ns); } /** diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h index 5f98578d6cf..c3a8cad69f3 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h @@ -132,7 +132,6 @@ class variable_sensitivity_dependence_domaint trace_ptrt to) override; void merge_three_way_function_return( - const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns) override; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index a75aebb51c0..b348096522c 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -275,13 +275,6 @@ bool variable_sensitivity_domaint::is_top() const return abstract_state.is_top(); } -std::vector variable_sensitivity_domaint::get_modified_symbols( - const variable_sensitivity_domaint &other) const -{ - return abstract_environmentt::modified_symbols( - abstract_state, other.abstract_state); -} - void variable_sensitivity_domaint::transform_function_call( locationt from, locationt to, @@ -424,14 +417,10 @@ bool variable_sensitivity_domaint::ignore_function_call_transform( } void variable_sensitivity_domaint::merge_three_way_function_return( - const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns) { - const variable_sensitivity_domaint &cast_function_call = - static_cast(function_call); - const variable_sensitivity_domaint &cast_function_start = static_cast(function_start); @@ -439,7 +428,8 @@ void variable_sensitivity_domaint::merge_three_way_function_return( static_cast(function_end); const std::vector &modified_symbol_names = - cast_function_start.get_modified_symbols(cast_function_end); + abstract_environmentt::modified_symbols( + cast_function_start.abstract_state, cast_function_end.abstract_state); std::vector modified_symbols; modified_symbols.reserve(modified_symbol_names.size()); @@ -449,22 +439,14 @@ void variable_sensitivity_domaint::merge_three_way_function_return( std::back_inserter(modified_symbols), [&ns](const irep_idt &id) { return ns.lookup(id).symbol_expr(); }); - abstract_state = cast_function_call.abstract_state; - apply_domain(modified_symbols, cast_function_end, ns); - - return; -} - -void variable_sensitivity_domaint::apply_domain( - std::vector modified_symbols, - const variable_sensitivity_domaint &source, - const namespacet &ns) -{ for(const auto &symbol : modified_symbols) { - abstract_object_pointert value = source.abstract_state.eval(symbol, ns); + abstract_object_pointert value = + cast_function_end.abstract_state.eval(symbol, ns); abstract_state.assign(symbol, value, ns); } + + return; } void variable_sensitivity_domaint::assume(exprt expr, namespacet ns) diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index 179fd9fb683..f2f54706011 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -172,18 +172,17 @@ class variable_sensitivity_domaint : public ai_domain_baset virtual bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to); - /// Perform a context aware merge of the changes that have been applied - /// between function_start and the current state. Anything that has not been - /// modified will be taken from the \p function_call domain. - /// \param function_call: The local of the merge - values from here will be - /// taken if they have not been modified - /// \param function_start: The base of the merge - changes that have been made + /// Merges just the things that have changes between + /// "function_start" and "function_end" into "this". + /// To be used correctly "this" must be derived from the function + /// call site. Anything that is not modified in the function (such + /// as globals) will not be changed. + /// \param function_start: The base of the diff - changes that have been made /// between here and the end will be retained. /// \param function_end: The end of the merge - changes that have been made /// between the start and here will be retained. /// \param ns: The global namespace virtual void merge_three_way_function_return( - const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns); @@ -241,22 +240,6 @@ class variable_sensitivity_domaint : public ai_domain_baset /// \return Returns true if the function should be ignored bool ignore_function_call_transform(const irep_idt &function_id) const; - /// Get symbols that have been modified since this domain and other - /// \param other: The domain that things may have been modified in - /// \return A list of symbols whose write location is different - std::vector - get_modified_symbols(const variable_sensitivity_domaint &other) const; - - /// Given a domain and some symbols, apply those symbols values - /// to the current domain - /// \param modified_symbols: The symbols to write - /// \param target: The domain to take the values from - /// \param ns: The global namespace - void apply_domain( - std::vector modified_symbols, - const variable_sensitivity_domaint &target, - const namespacet &ns); - void assume(exprt expr, namespacet ns); abstract_environmentt abstract_state;