Merge pull request diffblue#503 from diffblue/smowton/feature/ait-sparse-domains

Abstract interpretation framework: allow selective domain retention

Author: smowton

cbmc/src/analyses/ai.cpp

@@ -334,15 +334,33 @@ bool ai_baset::visit(
 
   statet &current=get_state(l);
 
-  for(const auto &to_l : goto_program.get_successors(l))
+  // Check if our user wants to be able to inspect this state after the
+  // fixpoint algorithm terminates.
+  // Default if the instantiating code hasn't supplied any specific advice is
+  // to retain all states.
+  bool must_retain_current_state = must_retain_state(l, goto_program);
+
+  std::list<locationt> 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));
+    // If permissible, alter the existing instruction's state in place;
+    // otherwise use a temporary copy:
+    std::unique_ptr<statet> tmp_state;
 
-    statet &new_values=*tmp_state;
+    // Note this condition is stricter than `!must_retain_current_state` because
+    // when we have multiple successors `transform` 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;
+
+    if(!may_work_in_place)
+      tmp_state = make_temporary_state(current);
+
+    statet &new_values = may_work_in_place ? current : *tmp_state;
 
     bool have_new_values=false;
 
@@ -367,8 +385,11 @@ bool ai_baset::visit(
 
       new_values.transform(l, to_l, *this, ns);
 
-      if(merge(new_values, l, to_l))
-        have_new_values=true;
+      // Note new_values is moved regardless of `may_work_in_place`:
+      // In one case we're working in place and the source domain (`current`)
+      // is about to be `make_bottom`'d below, and in the other we've made
+      // a temporary copy `tmp_state` which is about to die.
+      have_new_values |= merge(std::move(new_values), l, to_l);
     }
 
     if(have_new_values)
@@ -378,6 +399,12 @@ bool ai_baset::visit(
     }
   }
 
+  if(!must_retain_current_state)
+  {
+    // If this state isn't needed any longer, destroy it now:
+    current.make_bottom();
+  }
+
   return new_data;
 }
 
@@ -400,7 +427,7 @@ bool ai_baset::do_function_call(
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
     tmp_state->transform(l_call, l_return, *this, ns);
 
-    return merge(*tmp_state, l_call, l_return);
+    return merge(std::move(*tmp_state), l_call, l_return);
   }
 
   assert(!goto_function.body.instructions.empty());
@@ -420,7 +447,7 @@ bool ai_baset::do_function_call(
     bool new_data=false;
 
     // merge the new stuff
-    if(merge(*tmp_state, l_call, l_begin))
+    if(merge(std::move(*tmp_state), l_call, l_begin))
       new_data=true;
 
     // do we need to do/re-do the fixedpoint of the body?
@@ -445,7 +472,7 @@ bool ai_baset::do_function_call(
     tmp_state->transform(l_end, l_return, *this, ns);
 
     // Propagate those
-    return merge(*tmp_state, l_end, l_return);
+    return merge(std::move(*tmp_state), l_end, l_return);
   }
 }
 
@@ -523,6 +550,42 @@ bool ai_baset::do_function_call_rec(
   return new_data;
 }
 
+/// Determine whether we must retain the state for program point `l` even after
+/// fixpoint analysis completes (e.g. for our user to inspect), or if it solely
+/// for internal use and can be thrown away as and when suits us.
+/// \param l: program point
+/// \param l_program: program that l belongs to
+/// \return true if we must retain the state for that program point
+bool ai_baset::must_retain_state(
+  locationt l, const goto_programt &l_program) const
+{
+  // 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;
+
+  // Similarly retain function head instructions, which may have multiple
+  // incoming call-graph edges:
+  if(l == l_program.instructions.begin())
+    return true;
+
+  // ...and retain function end states, as they will be propagated to many
+  // different callers (they have multiple successors, even though they appear
+  // to have none intraprocedurally).
+  if(l->is_end_function())
+    return true;
+
+  // Finally, retain states where the particular subclass specifies they
+  // should be kept:
+  return must_retain_state_callback(l);
+}
+
 void ai_baset::sequential_fixedpoint(
   const goto_functionst &goto_functions,
   const namespacet &ns)

cbmc/src/analyses/ai.h

@@ -96,14 +96,19 @@ class ai_domain_baset
   // also add
   //
   //   bool merge(const T &b, locationt from, locationt to);
+  // and optionally
+  //   bool merge(T &&b, location from, locationt to);
   //
-  // This computes the join between "this" and "b".
+  // These compute the join between "this" and "b".
   // Return true if "this" has changed.
   // In the usual case, "b" is the updated state after "from"
   // and "this" is the state before "to".
   //
   // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
   // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
+  //
+  // The T &&b overload, if any, must leave `b` in such a state that
+  // `b.make_bottom()` or destruction of `b` could happen next without error.
 
   // This method allows an expression to be simplified / evaluated using the
   // current state.  It is used to evaluate assertions and in program
@@ -131,7 +136,9 @@ class ai_baset
   typedef ai_domain_baset statet;
   typedef goto_programt::const_targett locationt;
 
-  ai_baset()
+  explicit ai_baset(
+    std::function<bool(locationt)> must_retain_state_callback) :
+    must_retain_state_callback(must_retain_state_callback)
   {
   }
 
@@ -308,6 +315,11 @@ class ai_baset
   // the work-queue is sorted by location number
   typedef std::map<unsigned, locationt> working_sett;
 
+  // Callback that indicates if the user of this instance wants a particular
+  // state (program point) to be retained for inspection once the fixpoint is
+  // found. If no callback is supplied we by default retain all states.
+  std::function<bool(locationt)> must_retain_state_callback;
+
   locationt get_next(working_sett &working_set);
 
   void put_in_working_set(
@@ -358,8 +370,11 @@ class ai_baset
     const exprt::operandst &arguments,
     const namespacet &ns);
 
+  bool must_retain_state(locationt, const goto_programt &) const;
+
   // abstract methods
 
+  virtual bool merge(statet &&src, locationt from, locationt to)=0;
   virtual bool merge(const statet &src, locationt from, locationt to)=0;
   // for concurrent fixedpoint
   virtual bool merge_shared(
@@ -378,7 +393,8 @@ class ait:public ai_baset
 {
 public:
   // constructor
-  ait():ai_baset()
+  ait(std::function<bool(locationt)> must_retain_state_callback = nullptr) :
+    ai_baset(must_retain_state_callback)
   {
   }
 
@@ -436,6 +452,13 @@ class ait:public ai_baset
     return it->second;
   }
 
+  bool merge(statet &&src, locationt from, locationt to) override
+  {
+    statet &dest=get_state(to);
+    return static_cast<domainT &>(dest).merge(
+      static_cast<domainT &&>(src), from, to);
+  }
+
   bool merge(const statet &src, locationt from, locationt to) override
   {
     statet &dest=get_state(to);

cbmc/unit/Makefile

@@ -8,6 +8,7 @@ SRC = unit_tests.cpp \
 # Test source files
 SRC += unit_tests.cpp \
        analyses/ai/ai_simplify_lhs.cpp \
+       analyses/ai/ai_selective_domains.cpp \
        analyses/call_graph.cpp \
        analyses/constant_propagator.cpp \
        analyses/disconnect_unreachable_nodes_in_graph.cpp \