Merge pull request diffblue#322 from diffblue/owen-jones-diffblue/merge-logic-for-precise-EVSs

merge logic for precise EVSs

Author: owen-jones-diffblue

src/pointer-analysis/local_value_set.h

@@ -22,7 +22,10 @@ class local_value_sett:public value_sett
   mutable unsigned int num_writes_to_field_of_external_object=0;
   mutable bool no_merges=true;
 
-  bool should_apply_precise_external_value_sets() const
+  /// Determines whether we should export precise or per_field external value
+  /// sets in function summaries.
+  /// \return
+  bool should_export_precise_external_value_sets() const
   {
 #ifdef DO_NOT_USE_PRECISE_EXTERNAL_VALUE_SETS
     return false;

src/pointer-analysis/local_value_set_analysis.cpp

@@ -427,25 +427,6 @@ void local_value_set_analysist::transform_function_stub(
     }
     else if(has_prefix(lhs_fieldname.base_name, precise_evs_prefix))
     {
-      std::vector<std::string> suffix_vec;
-      /// Split the field name into individual field dereferences, so ".x.y"
-      /// turns into ['.x', '.y']
-      const char delim='.';
-      std::string::const_iterator start=lhs_fieldname.field_name.begin();
-      for(
-        std::string::const_iterator it
-          =std::next(lhs_fieldname.field_name.begin());
-        it!=lhs_fieldname.field_name.end();
-        ++it)
-      {
-        if(*it==delim)
-        {
-          suffix_vec.emplace_back(start, it);
-          start=it;
-        }
-      }
-      suffix_vec.emplace_back(start, lhs_fieldname.field_name.end());
-
       const external_value_set_exprt::access_path_entriest
         &access_path_entries =
           to_external_value_set(lhs_fieldname.structured_lhs)
@@ -552,6 +533,88 @@ bool local_value_set_analysist::is_singular(const std::set<exprt> &values)
   return baset::is_singular(values);
 }
 
+void local_value_set_analysist::operator()(const goto_programt &goto_program)
+{
+  initialize(goto_program);
+  /// This is a dummy variable that will always be empty because we handle
+  /// function calls specially
+  goto_functionst goto_functions;
+
+  while(true)
+  {
+    bool fixedpoint_changed_valuesets =
+      static_analysis_baset::fixedpoint(goto_program, goto_functions);
+
+    if(!fixedpoint_changed_valuesets)
+      break;
+
+    bool initializer_precise_evs_added =
+      add_precise_evs_initializers(goto_program);
+
+    if(!initializer_precise_evs_added)
+      break;
+  }
+}
+
+bool local_value_set_analysist::add_precise_evs_initializers(
+  const goto_programt &goto_program)
+{
+  const std::string precise_evs_prefix = PRECISE_EVS_PREFIX;
+  bool any_changes = false;
+
+  for(locationt loc = goto_program.instructions.begin();
+      loc != goto_program.instructions.end();
+      ++loc)
+  {
+    if(loc->incoming_edges.size() <= 1)
+      continue;
+
+    /// At each place in the control flow graph where two or more paths join
+    /// together, we look through all the predecessors and see which precise
+    /// EVSs occur in the left hand sides of their domains.
+    std::map<irep_idt, unsigned long> precise_evs_counts;
+
+    for(goto_programt::instructionst::const_iterator predecessor :
+        loc->incoming_edges)
+    {
+      for(const auto &value : (*this)[predecessor].value_set.values)
+      {
+        const exprt &lhs = value.second.structured_lhs;
+
+        if(
+          can_cast_expr<external_value_set_exprt>(lhs) &&
+          to_external_value_set(lhs).get_external_value_set_type() ==
+            external_value_set_typet::PRECISE)
+        {
+          ++precise_evs_counts[value.first];
+        }
+      }
+    }
+
+    /// For each precise EVSs which occurs in some predecessor but not
+    /// all, we add a copy of the EVS with is_initializer set to true to the
+    /// value-set at the join instruction, to account for the fact that there
+    /// is a path to this point where it still has its initial value.
+    for(const auto identifier_count : precise_evs_counts)
+    {
+      if(identifier_count.second < loc->incoming_edges.size())
+      {
+        local_value_sett &value_set = (*this)[loc].value_set;
+        value_sett::entryt &entry = value_set.values[identifier_count.first];
+
+        external_value_set_exprt init_evs =
+          to_external_value_set(entry.structured_lhs).as_initializer();
+
+        bool object_map_changed = value_set.insert(entry.object_map, init_evs);
+
+        if(object_map_changed)
+          any_changes = true;
+      }
+    }
+  }
+  return any_changes;
+}
+
 /// Finds expressions that are reachable from parameters or global variables
 /// according to a given value-set-analysis state. For example:
 ///
@@ -631,7 +694,7 @@ void lvsaa_single_external_set_summaryt::from_final_state(
   // field ones. If this is not possible then we export per field ones
   // and not precise ones.
   const bool should_export_precise_evs=
-    final_state.should_apply_precise_external_value_sets();
+    final_state.should_export_precise_external_value_sets();
 
   // Picks which value-set LHS expressions may be external to this function:
   for(auto it=final_state.values.begin();

src/pointer-analysis/local_value_set_analysis.h

@@ -145,6 +145,13 @@ class local_value_set_analysist
   /// \param goto_program: function under analysis
   virtual void initialize(const goto_programt &goto_program) override;
 
+  /// Overloads static_analysis_baset::operator(). Find the fixed point of
+  /// the analysis, then add initial values for precise external value sets
+  /// if needed. Repeat these two steps until one of them does not make any
+  /// changes.
+  /// \param goto_program: the program under analysis
+  virtual void operator()(const goto_programt &goto_program) override;
+
   /// Overrides static_analysist's default behaviour on reaching a callsite,
   /// resulting in a call to `transform_function_stub` instead.
   virtual bool should_enter_function(const irep_idt& f) override
@@ -219,6 +226,12 @@ class local_value_set_analysist
   /// Requests `static_analysist` to call `transform_function_stub` on a
   /// recursive function call, rather than ignoring the call as per default.
   virtual bool get_ignore_recursion() override { return false; }
+
+  /// Look for join points in the control flow graph and add initial  values
+  /// for precise external value sets to their value-sets if needed.
+  /// \param goto_program: the program under analysis
+  /// \return true if any value-sets were changed
+  bool add_precise_evs_initializers(const goto_programt &goto_program);
 };
 
 #endif

src/pointer-analysis/local_value_set_domain.h

@@ -17,8 +17,6 @@ class local_value_set_domaint:
   bool merge(const local_value_set_domaint &other, locationt to)
   {
     value_set.make_union_bookkeeping_data_structures(other.value_set);
-    if(to->incoming_edges.size()>1)
-      value_set.no_merges=false;
     return value_set.make_union(other.value_set);
   }
 };