Merge pull request #7929 from martin-cs/refactor/tidy-up-three-way-merge

Refactor/tidy up three way merge

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<statet> ptr_s_working_copy(
-      make_temporary_state(s_working));
+    // The base for the three way merge is the call site
+    const std::unique_ptr<statet> ptr_call_site_working(
+      make_temporary_state(get_state(p_call_site)));
+    auto tmp2 =
+      dynamic_cast<variable_sensitivity_domaint *>(&(*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()))
     {

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);
 }
 
 /**

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;

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<irep_idt> 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,22 +417,19 @@ 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<const variable_sensitivity_domaint &>(function_call);
-
   const variable_sensitivity_domaint &cast_function_start =
     static_cast<const variable_sensitivity_domaint &>(function_start);
 
   const variable_sensitivity_domaint &cast_function_end =
     static_cast<const variable_sensitivity_domaint &>(function_end);
 
   const std::vector<irep_idt> &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<symbol_exprt> 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<symbol_exprt> 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)

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<irep_idt>
-  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<symbol_exprt> modified_symbols,
-    const variable_sensitivity_domaint &target,
-    const namespacet &ns);
-
   void assume(exprt expr, namespacet ns);
 
   abstract_environmentt abstract_state;