Merge pull request diffblue#427 from diffblue/smowton/feature/lvsa-avoid-storing-all-domains

LVSA: only store selected domains

Author: smowton

cbmc/src/analyses/static_analysis.cpp

@@ -221,28 +221,6 @@ bool static_analysis_baset::fixedpoint(
   return new_data;
 }
 
-bool static_analysis_baset::fixedpoint(
-  const goto_programt &goto_program,
-  const goto_functionst &goto_functions,
-  working_sett &working_set)
-{
-  if(goto_program.instructions.empty())
-    return false;
-
-  bool new_data = false;
-
-  while(!working_set.empty())
-  {
-    ++nsteps;
-    locationt l = get_next(working_set);
-
-    if(visit(l, working_set, goto_program, goto_functions))
-      new_data = true;
-  }
-
-  return new_data;
-}
-
 bool static_analysis_baset::visit(
   locationt l,
   working_sett &working_set,
@@ -254,23 +232,46 @@ bool static_analysis_baset::visit(
   statet &current=get_state(l);
 
   current.seen=true;
+  bool must_retain_current_state = must_retain_state(l);
 
-  for(const auto &to_l : goto_program.get_successors(l))
+  const auto &successors = goto_program.get_successors(l);
+  for(const auto &to_l : successors)
   {
     if(to_l==goto_program.instructions.end())
       continue;
 
-    std::unique_ptr<statet> tmp_state(
-      make_temporary_state(current));
+    std::unique_ptr<statet> tmp_state;
+
+    // Note this condition is stricter than `!must_retain_current_state` because
+    // when we have multiple successors `transform_or_apply_function_call` may
+    // do something different for different successors, in which case we must
+    // use a clean copy of the pre-existing state each time.
+    bool may_work_in_place =
+      successors.size() == 1 && !must_retain_current_state;
 
-    statet &new_values=*tmp_state;
+    if(!may_work_in_place)
+      tmp_state = make_temporary_state(current);
+
+    statet &new_values =
+      may_work_in_place ?
+      current :
+      *tmp_state;
 
     transform_or_apply_function_call(l, to_l, goto_functions, new_values);
 
     statet &other=get_state(to_l);
 
-    bool have_new_values=
-      merge(other, new_values, to_l);
+    bool have_new_values;
+
+    if(other.is_empty())
+    {
+      move(other, std::move(new_values));
+      have_new_values = !other.is_empty();
+    }
+    else
+    {
+      have_new_values = merge(other, new_values, to_l);
+    }
 
     if(have_new_values)
       new_data=true;
@@ -279,6 +280,13 @@ bool static_analysis_baset::visit(
       put_in_working_set(working_set, to_l);
   }
 
+  if(!must_retain_current_state)
+  {
+    // If this state isn't needed any longer, destroy it now:
+    current.initialize(ns, l);
+    current.seen = false;
+  }
+
   return new_data;
 }
 
@@ -573,3 +581,21 @@ void static_analysis_baset::transform_or_apply_function_call(
   else
     new_values.transform(ns, l, to_l);
 }
+
+bool static_analysis_baset::must_retain_state(locationt l)
+{
+  // If the derived class doesn't specify otherwise, assume the old default
+  // behaviour: always retain state.
+  if(!must_retain_state_callback)
+    return true;
+
+  // Regardless, always keep states with multiple predecessors, which is
+  // required for termination when loops are present, and saves redundant
+  // re-investigation of successors for other kinds of convergence.
+  if(l->incoming_edges.size() > 1)
+    return true;
+
+  // Finally, retain states where the particular subclass specifies they
+  // should be kept:
+  return must_retain_state_callback(l);
+}

cbmc/src/analyses/static_analysis.h

@@ -49,6 +49,8 @@ class domain_baset
   {
   }
 
+  virtual bool is_empty() const = 0;
+
   // how function calls are treated:
   // a) there is an edge from each call site to the function head
   // b) there is an edge from each return to the last instruction (END_FUNCTION)
@@ -109,10 +111,13 @@ class static_analysis_baset
   typedef domain_baset statet;
   typedef goto_programt::const_targett locationt;
 
-  explicit static_analysis_baset(const namespacet &_ns):
+  explicit static_analysis_baset(
+    const namespacet &_ns,
+    std::function<bool(locationt)> must_retain_state_callback) :
     nsteps(0),
     ns(_ns),
-    initialized(false)
+    initialized(false),
+    must_retain_state_callback(must_retain_state_callback)
   {
     ignore_recursion=get_ignore_recursion();
   }
@@ -217,10 +222,6 @@ class static_analysis_baset
   bool fixedpoint(
     const goto_programt &goto_program,
     const goto_functionst &goto_functions);
-  bool fixedpoint(
-    const goto_programt &goto_program,
-    const goto_functionst &goto_functions,
-    working_sett &working_set);
 
   virtual void fixedpoint(
     const goto_functionst &goto_functions)=0;
@@ -253,6 +254,8 @@ class static_analysis_baset
   // for concurrent fixedpoint
   virtual bool merge_shared(statet &a, const statet &b, locationt to)=0;
 
+  virtual void move(statet &a, statet &&b)=0;
+
   typedef std::set<irep_idt> functions_donet;
   functions_donet functions_done;
 
@@ -267,6 +270,10 @@ class static_analysis_baset
 
   bool initialized;
 
+  std::function<bool(locationt)> must_retain_state_callback;
+
+  bool must_retain_state(locationt);
+
   // function calls
   void do_function_call_rec(
     locationt l_call, locationt l_return,
@@ -314,8 +321,10 @@ class static_analysist:public static_analysis_baset
 {
 public:
   // constructor
-  explicit static_analysist(const namespacet &_ns):
-    static_analysis_baset(_ns)
+  explicit static_analysist(
+    const namespacet &_ns,
+    std::function<bool(locationt)> must_retain_state = nullptr) :
+    static_analysis_baset(_ns, must_retain_state)
   {
   }
 
@@ -382,6 +391,11 @@ class static_analysist:public static_analysis_baset
     return util_make_unique<T>(static_cast<const T &>(s));
   }
 
+  virtual void move(statet &a, statet &&b)
+  {
+    static_cast<T &>(a).move_state_from(static_cast<T &&>(b));
+  }
+
   virtual void generate_state(locationt l)
   {
     state_map[l].initialize(ns, l);

cbmc/src/pointer-analysis/value_set.h

@@ -489,6 +489,11 @@ class value_sett
     exprt &expr,
     const namespacet &ns) const;
 
+  void move_state_from(value_sett &&other)
+  {
+    this->values = std::move(other.values);
+  }
+
 protected:
   /// Reads the set of objects pointed to by `expr`, including making
   /// recursive lookups for dereference operations etc.

cbmc/src/pointer-analysis/value_set_analysis.h

@@ -36,7 +36,10 @@ class value_set_analysis_templatet:
   typedef static_analysist<domaint> baset;
   typedef typename baset::locationt locationt;
 
-  explicit value_set_analysis_templatet(const namespacet &ns):baset(ns)
+  explicit value_set_analysis_templatet(
+    const namespacet &ns,
+    std::function<bool(locationt)> must_retain_state = nullptr) :
+    baset(ns, must_retain_state)
   {
   }
 

cbmc/src/pointer-analysis/value_set_domain.h

@@ -51,6 +51,11 @@ class value_set_domain_templatet:public domain_baset
     value_set.function=l->function;
   }
 
+  bool is_empty() const override
+  {
+    return value_set.values.empty();
+  }
+
   void transform(
     const namespacet &ns,
     locationt from_l,
@@ -63,6 +68,11 @@ class value_set_domain_templatet:public domain_baset
   {
     value_set.get_reference_set(expr, dest, ns);
   }
+
+  void move_state_from(value_set_domain_templatet<VST> &&other)
+  {
+    value_set.move_state_from(std::move(other.value_set));
+  }
 };
 
 typedef value_set_domain_templatet<value_sett> value_set_domaint;

regression/LVSA/lvsa_driver.py

@@ -1,5 +1,6 @@
 import json
 import os
+import copy
 from enum import Enum
 
 from regression.executable_runner import ExecutableRunner
@@ -191,6 +192,48 @@ def check_contains_precise_evs(self, expected_number=1, is_initializer=False, ac
     def get_dynamic_object_ids(self):
         return [dynamic_object.instance['id'] for dynamic_object in self.dynamic_objects]
 
+def report_difference_with_context(state1, state2, context):
+    if type(state1) != type(state2):
+        return (context, str(type(state1)), str(type(state2)))
+    if isinstance(state1, list) or \
+       isinstance(state1, dict) or \
+       isinstance(state1, set):
+        if len(state1) != len(state2):
+            return(context + ["length"], len(state1), len(state2))
+        context.append(None)
+        if isinstance(state1, list):
+            for (idx, (element1, element2)) in enumerate(zip(state1, state2)):
+                context[-1] = idx
+                subrep = \
+                    report_difference_with_context(element1, element2, context)
+                if subrep is not None:
+                    return subrep
+        elif isinstance(state1, set):
+            for element1 in state1:
+                if element1 not in state2:
+                    return (context, element1, "Element not present in set")
+        else:
+            for key in state1:
+                if key not in state2:
+                    return (context, "Key {} present".format(key), "Key absent")
+                context[-1] = key
+                subrep = report_difference_with_context( \
+                    state1[key], state2[key], context)
+                if subrep is not None:
+                    return subrep
+        context.pop()
+    else:
+        if state1 != state2:
+            return (context, state1, state2)
+    return None
+
+def report_first_state_difference(state1, state2, desc1, desc2):
+    state_difference = report_difference_with_context(state1, state2, [])
+    if state_difference is not None:
+        return "In context: {}\n{}: {}\n{}: {}".format(
+            state_difference[0],
+            desc1, state_difference[1],
+            desc2, state_difference[2])
 
 class LvsaExpectation:
     """Encapsulate the output of LvsaDriver"""
@@ -281,6 +324,9 @@ def get_value_set_for_dynamic_object_value_set(self, dynamic_object_id, suffix,
     def get_all_value_sets(self):
         return [ValueSetExpectation(var_state) for var_state in self.state]
 
+    def report_first_difference(self, other, self_desc, other_desc):
+        return report_first_state_difference(
+            self.state, other.state, self_desc, other_desc)
 
 class LvsaDriver:
     """Run LVSA"""
@@ -324,4 +370,52 @@ def run(self):
         executable_runner = ExecutableRunner(cmd)
         (stdout, _, _) = executable_runner.run()
 
-        return LvsaExpectation(stdout, fq_class_name, fq_function_name)
+        result = LvsaExpectation(stdout, fq_class_name, fq_function_name)
+
+        # Check that LVSA's selective domain storage is working correctly: also
+        # run this command in debug mode, which retains domains for all program
+        # points, and check it has the same results.
+
+        debug_cmd = copy.copy(cmd)
+        debug_cmd.append("--lvsa-show-all-program-points")
+
+        debug_runner = ExecutableRunner(debug_cmd)
+        (debug_stdout, _, _) = debug_runner.run()
+
+        debug_result = \
+            LvsaExpectation(debug_stdout, fq_class_name, fq_function_name)
+
+        difference = result.report_first_difference(
+            debug_result, "Selective domain storage", "Storing all domains")
+
+        if difference is not None:
+            raise Exception(difference)
+
+        # Further check that the results with domain reconstruction (when
+        # program points are rebuilt from those selectively stored) exactly
+        # match those produced by retaining all domains in the first place:
+
+        test_reconstruction_cmd = copy.copy(debug_cmd)
+        test_reconstruction_cmd.append(
+            "--lvsa-reconstruct-intermediate-program-points")
+
+        test_reconstruction_runner = ExecutableRunner(test_reconstruction_cmd)
+        (test_reconstruction_stdout, _, _) = test_reconstruction_runner.run()
+
+        debug_full_result = json.loads(debug_stdout)
+        debug_full_result = \
+            [x for x in debug_full_result if x.get('messageType') == 'LVSA-ALL-FUNCTIONS-DUMP']
+        test_reconstruction_full_result = json.loads(test_reconstruction_stdout)
+        test_reconstruction_full_result = \
+            [x for x in test_reconstruction_full_result if x.get('messageType') == 'LVSA-ALL-FUNCTIONS-DUMP']
+
+        reconstruction_difference = report_first_state_difference(
+            debug_full_result,
+            test_reconstruction_full_result,
+            "Conventionally computed domains",
+            "Reconstructed intermediate domains")
+
+        if reconstruction_difference is not None:
+            raise Exception(reconstruction_difference)
+
+        return result