Reworked three way merge that works when enabled and not

Author: thk123

src/analyses/ai.cpp

@@ -416,13 +416,6 @@ bool ai_baset::do_function_call(
 
     bool new_data=false;
 
-    std::cout << "BEFORE MERGING" << std::endl;
-    tmp_state->output(std::cout, *this, ns);
-    statet &dest=get_state(l_begin);
-    dest.output(std::cout, *this, ns);
-
-    std::cout << "-------------" << std::endl;
-
     // merge the new stuff
     if(merge(*tmp_state, l_call, l_begin))
       new_data=true;
@@ -432,25 +425,8 @@ bool ai_baset::do_function_call(
       fixedpoint(goto_function.body, goto_functions, ns);
   }
 
-#if 0
-  {
-    // do edge from end of function to instruction after call
-    locationt l_begin=goto_function.body.instructions.begin();
-    const statet &starting_state=get_state(l_begin);
-
-    std::unique_ptr<statet> tmp_state(make_temporary_state(starting_state));
-
-    /// Merge 25 into 26
-    /// Source state is 25 (src = get_state(25)
-    /// Destination state is 26 (i.e to = 26)
-
-    // src, from, to
-    any_changes|=merge(*tmp_state, l_begin, l_return);
-  }
-#endif
 
   // This is the edge from function end to return site.
-
   {
     // get location at end of the procedure we have called
     locationt l_end=--goto_function.body.instructions.end();
@@ -468,48 +444,13 @@ bool ai_baset::do_function_call(
     std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
     tmp_state->transform(l_end, l_return, *this, ns);
 
-    // We want to get a state that has only the changes from the function
-    //const auto &symbols=get_modified_symbols(start_state, end_state);
-
-
-
-
-
-    // Propagate those
-    //any_changes|=merge(get_state(l_call), l_end, l_return);
-
-#if 0
-    std::cout << "Function call " << f_it->first << " complete, modified symbols:" << std::endl;
-#endif
-    //const auto &modified_symbols=get_modified_symbols(start_state, *tmp_state);
-
-#if 0
-    for(const auto &modified_symbol:modified_symbols)
-    {
-      std::cout << "\t" << modified_symbol.get_identifier() << "\n";
-    }
-    std::cout << std::endl;
-#endif
-
-    // ------------
-    // END_FUNCTION
-    // ------------
-
-    // 3 way merge normally has BASE, LOCAL and REMOTE
-    // We take the changes applied between BASE and REMOTE and re-apply them to
-    // local
-    // This would look like:
-    // BASE: function_begin
-    // REMOTE: function_end
-    // LOCAL: function_call
-
+    std::unique_ptr<statet> pre_merge_tmp_state(make_temporary_state(*tmp_state));
 
-    std::unique_ptr<statet> tmp_return_state(make_temporary_state(get_state(l_call)));
-    tmp_return_state->merge_three_way_function_return(
-      get_state(l_begin), get_state(l_end), ns);
+    // We try to
+    tmp_state->merge_three_way_function_return(
+      get_state(l_call), get_state(l_begin), *pre_merge_tmp_state, ns);
 
-    any_changes|=merge(*tmp_return_state, l_end, l_return);
-    //restore_domain(modified_symbols, *tmp_state, get_state(l_return), ns);
+    any_changes|=merge(*tmp_state, l_end, l_return);
   }
 
   return any_changes;

src/analyses/ai.h

@@ -106,13 +106,15 @@ class ai_domain_baset
     exprt &condition,
     const namespacet &ns) const;
 
+  // Applies the changes between the start and end to the domain
   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)
   {
-    // Do nothing - the result of the merge is to take
-    // all the changes in the "remote" version
+    // Take the state at the end of the function as a over-approximation
+    // of applying the changes in the function
   }
 
 };

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -833,6 +833,7 @@ std::vector<symbol_exprt> abstract_environmentt::modified_symbols(
       bool all_matched=intersection.size()==a.size() &&
         intersection.size()==b.size();
 
+#if 0
       std::cout << entry.first.get_identifier() << ": {";
       for(const auto &entry:lhs_location)
       {
@@ -845,6 +846,7 @@ std::vector<symbol_exprt> abstract_environmentt::modified_symbols(
         std::cout << entry->location_number << ", ";
       }
       std::cout << " }" << std::endl;
+#endif
 
       if (!all_matched)
       {

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -370,6 +370,17 @@ bool variable_sensitivity_domaint::is_top() const
   return abstract_state.is_top();
 }
 
+/// 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<symbol_exprt>
+  variable_sensitivity_domaint::get_modified_symbols(
+    const variable_sensitivity_domaint &other) const
+{
+  return abstract_environmentt::modified_symbols(
+    abstract_state, other.abstract_state);
+}
+
 /*******************************************************************\
 
 Function: variable_sensitivity_domaint::transform_function_call
@@ -532,34 +543,58 @@ bool variable_sensitivity_domaint::ignore_function_call_transform(
   ignored_internal_function.cend();
 }
 
+/// 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 this will be retained.
+/// \param ns: The global namespace
 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_site=
-//    static_cast<const variable_sensitivity_domaint &>(function_call_site);
+  // TODO(tkiley): flag to turn of the context aware merge
+  if(true)
+  {
+    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_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 variable_sensitivity_domaint &cast_function_end=
+      static_cast<const variable_sensitivity_domaint &>(function_end);
 
-  const std::vector<symbol_exprt> &modified_symbols=
-    cast_function_start.get_modified_symbols(cast_function_end);
+    const std::vector<symbol_exprt> &modified_symbols=
+      cast_function_start.get_modified_symbols(cast_function_end);
 
-  apply_domain(modified_symbols, cast_function_end, ns);
+    abstract_state=cast_function_call.abstract_state;
+    apply_domain(modified_symbols, cast_function_end, ns);
+  }
+  else
+  {
+    ai_domain_baset::merge_three_way_function_return(
+      function_call, function_start, function_end, ns);
+  }
 }
 
+/// Given a domain and some symbols, apply those symbols values
+/// to the current domain
+/// \param modified_symbols: The symbols to write
+/// \param source: The domain to take the values from
+/// \param ns: The global namespace
 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)
-    {
-        auto value = source.abstract_state.eval(symbol, ns);
-        this->abstract_state.assign(symbol, value, ns);
-    }
+  for (const auto &symbol : modified_symbols)
+  {
+    abstract_object_pointert value=source.abstract_state.eval(symbol, ns);
+    abstract_state.assign(symbol, value, ns);
+  }
 }

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -100,6 +100,7 @@ class variable_sensitivity_domaint:public ai_domain_baset
     locationt to);
 
   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;
@@ -111,17 +112,6 @@ class variable_sensitivity_domaint:public ai_domain_baset
   bool is_bottom() const override;
   bool is_top() const override;
 
-  std::vector<symbol_exprt> get_modified_symbols(const variable_sensitivity_domaint &other) const
-  {
-    return abstract_environmentt::modified_symbols(abstract_state, other.abstract_state);
-  }
-
-
-  virtual void apply_domain(
-    std::vector<symbol_exprt> modified_symbols,
-    const variable_sensitivity_domaint &target,
-    const namespacet &ns);
-
 private:
   void transform_function_call(
     locationt from,
@@ -131,6 +121,14 @@ class variable_sensitivity_domaint:public ai_domain_baset
 
   bool ignore_function_call_transform(const irep_idt &function_id) const;
 
+  std::vector<symbol_exprt> get_modified_symbols(
+    const variable_sensitivity_domaint &other) const;
+
+  void apply_domain(
+    std::vector<symbol_exprt> modified_symbols,
+    const variable_sensitivity_domaint &target,
+    const namespacet &ns);
+
   abstract_environmentt abstract_state;
 };