Merge pull request diffblue#449 from diffblue/smowton/fix/csvsa-sort-working-set

CSVSA: sort the working set to prioritise earlier and deeper instructions

Author: smowton

src/pointer-analysis/context_sensitive_value_set_analysis.cpp

@@ -641,4 +641,17 @@ csvsa_load_and_analyze_functions(
   return driver;
 }
 
+bool context_sensitive_value_set_analysis_drivert
+  ::compare_working_set_entriest::operator()(
+  const working_set_entryt &a, const working_set_entryt &b)
+{
+  // In the same context, investigate earlier instructions first.
+  // Of differing contexts, investigate the one created later first (this
+  // favours investigating a callee before continuing to look at its caller).
+  if(a.first == b.first)
+    return a.second->location_number < b.second->location_number;
+  else
+    return a.first > b.first;
+}
+
 const goto_functionst csvsa_function_contextt::empty_goto_functions;

src/pointer-analysis/context_sensitive_value_set_analysis.h

@@ -76,11 +76,23 @@ class context_sensitive_value_set_analysis_drivert : public messaget
   /// pointed at the usual goto_modelt or similar in future.
   const get_goto_programt get_goto_program;
 
+  typedef std::pair<context_indext, locationt> working_set_entryt;
+
+  /// Compares two working set entries, ordering those with higher context
+  /// numbers first (favouring callees over callers) and then lower location
+  /// numbers (favouring complete exploration of a loop, for example, before
+  /// its successors, assuming programs generally flow forwards)
+  struct compare_working_set_entriest
+  {
+    bool operator()(const working_set_entryt &a, const working_set_entryt &b);
+  };
+
   /// Working set, containing <context-pointer, instruction> pairs (constrast
   /// the normal value-set analysis working set, which only contains
   /// instructions). Pointers are non-owning, and are never held beyond the
   /// lifespan of `context_graph` (which owns the contexts).
-  std::set<std::pair<context_indext, locationt>> working_set;
+  std::set<std::pair<context_indext, locationt>, compare_working_set_entriest>
+    working_set;
 
   /// Graph of analysis contexts, each concerning a particular use context of a
   /// particular function (e.g. "function f when called from main line 5")