Three way merge initial checkin

Author: thk123

src/analyses/ai.cpp

@@ -460,7 +460,7 @@ bool ai_baset::do_function_call(
     const statet &end_state=get_state(l_end);
 
     locationt l_begin=goto_function.body.instructions.begin();
-    const statet &start_state=get_state(l_begin);
+    //const statet &start_state=get_state(l_begin);
 
     if(end_state.is_bottom())
       return false; // function exit point not reachable
@@ -476,18 +476,40 @@ bool ai_baset::do_function_call(
 
 
     // Propagate those
-    any_changes|=merge(get_state(l_call), l_end, l_return);
+    //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;
-    const auto &modified_symbols=get_modified_symbols(start_state, *tmp_state);
+#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> 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);
 
-    restore_domain(modified_symbols, *tmp_state, get_state(l_return), ns);
+    any_changes|=merge(*tmp_return_state, l_end, l_return);
+    //restore_domain(modified_symbols, *tmp_state, get_state(l_return), ns);
   }
 
   return any_changes;

src/analyses/ai.h

@@ -105,6 +105,16 @@ class ai_domain_baset
   virtual bool ai_simplify_lhs(
     exprt &condition,
     const namespacet &ns) const;
+
+  virtual void merge_three_way_function_return(
+    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
+  }
+
 };
 
 // don't use me -- I am just a base class
@@ -328,8 +338,6 @@ class ai_baset
 
   virtual bool merge(const statet &src, locationt from, locationt to)=0;
 
-  virtual std::vector<symbol_exprt> get_modified_symbols(const statet &src, const statet &other)=0;
-  virtual void restore_domain(std::vector<symbol_exprt> modified_symbols, const statet &source_domain, statet &target_domain, const namespacet ns)=0;
   // for concurrent fixedpoint
   virtual bool merge_shared(
     const statet &src,
@@ -416,18 +424,6 @@ class ait:public ai_baset
       static_cast<const domainT &>(src), from, to);
   }
 
-  std::vector<symbol_exprt> get_modified_symbols(const statet &src, const statet &other) override
-  {
-    return static_cast<const domainT &>(src).get_modified_symbols(
-      static_cast<const domainT &>(other));
-  }
-
-  void restore_domain(std::vector<symbol_exprt> modified_symbols, const statet &source_domain, statet &target_domain, const namespacet ns) override
-  {
-    static_cast<const domainT &>(source_domain).restore_domain(
-        modified_symbols, static_cast<domainT &>(target_domain), ns);
-  }
-
   statet *make_temporary_state(const statet &s) override
   {
     return new domainT(static_cast<const domainT &>(s));

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -529,16 +529,37 @@ bool variable_sensitivity_domaint::ignore_function_call_transform(
   };
 
   return ignored_internal_function.find(function_id)!=
-    ignored_internal_function.cend();
+  ignored_internal_function.cend();
 }
 
-void variable_sensitivity_domaint::restore_domain(std::vector<symbol_exprt> modified_symbols,   
-  variable_sensitivity_domaint &target,
-  const namespacet &ns) const
+void variable_sensitivity_domaint::merge_three_way_function_return(
+  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);
+
+  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<symbol_exprt> &modified_symbols=
+    cast_function_start.get_modified_symbols(cast_function_end);
+
+  apply_domain(modified_symbols, cast_function_end, ns);
+}
+
+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 = abstract_state.eval(symbol, ns);
-        target.abstract_state.assign(symbol, value, ns);
+        auto value = source.abstract_state.eval(symbol, ns);
+        this->abstract_state.assign(symbol, value, ns);
     }
 }

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -99,20 +99,28 @@ class variable_sensitivity_domaint:public ai_domain_baset
     locationt from,
     locationt to);
 
+  void merge_three_way_function_return(
+    const ai_domain_baset &function_start,
+    const ai_domain_baset &function_end,
+    const namespacet &ns) override;
+
   bool ai_simplify(
     exprt &condition,
     const namespacet &ns) const override;
 
   bool is_bottom() const override;
   bool is_top() const override;
 
-  virtual std::vector<symbol_exprt> get_modified_symbols(const variable_sensitivity_domaint &other) const
+  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 restore_domain(std::vector<symbol_exprt> modified_symbols,  
-    variable_sensitivity_domaint &target, const namespacet &ns) const;
+
+  virtual void apply_domain(
+    std::vector<symbol_exprt> modified_symbols,
+    const variable_sensitivity_domaint &target,
+    const namespacet &ns);
 
 private:
   void transform_function_call(