Reachability slicer: mark reachable code more precisely

The reachability slicer currently uses a very simple graph walk, and in particular walks out of a function
to all possible callers, regardless of whether we know the actual caller. This commit fixes that shortcoming
by adding the callsite successor *at the callsite*, and tracking the fact that the callee's successor has
already been taken care of in the graph search stack, thus allowing it to ignore the END_FUNCTION -> callsite
edges which are less precise.

Functions whose caller is genuinely unknown, such as the root function containing a reachability target (e.g.
assert instruction) are treated as before, considering all possible callees. The backwards search is improved
similarly to the forwards.

Author: smowton

src/goto-instrument/reachability_slicer.cpp

@@ -54,11 +54,47 @@ void reachability_slicert::fixedpoint_to_assertions(
   const is_threadedt &is_threaded,
   slicing_criteriont &criterion)
 {
-  std::vector<cfgt::node_indext> src = get_sources(is_threaded, criterion);
+  std::vector<search_stack_entryt> stack;
+  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
+  for(const auto source : sources)
+    stack.emplace_back(source, false);
 
-  std::vector<cfgt::node_indext> reachable = cfg.get_reachable(src, false);
-  for(const auto index : reachable)
-    cfg[index].reaches_assertion = true;
+  while(!stack.empty())
+  {
+    auto &node = cfg[stack.back().node_index];
+    auto caller_is_known = stack.back().caller_is_known;
+    stack.pop_back();
+
+    if(node.reaches_assertion)
+      continue;
+    node.reaches_assertion = true;
+
+    for(const auto &edge : node.in)
+    {
+      const auto &pred_node = cfg[edge.first];
+
+      if(pred_node.PC->is_end_function())
+      {
+        // This is an end-of-function -> successor-of-callsite edge.
+        // Thus node.PC must have a predecessor instruction which is the calling
+        // instruction. Queue both the caller and the end of the callee.
+        stack.emplace_back(edge.first, true);
+        stack.emplace_back(
+          cfg.entry_map[std::prev(node.PC)], caller_is_known);
+      }
+      else if(pred_node.PC->is_function_call())
+      {
+        // Skip this predecessor, unless this is a bodyless function, or we
+        // don't know who our callee was:
+        if(!caller_is_known || std::next(pred_node.PC) == node.PC)
+          stack.emplace_back(edge.first, caller_is_known);
+      }
+      else
+      {
+        stack.emplace_back(edge.first, caller_is_known);
+      }
+    }
+  }
 }
 
 /// Perform forwards depth-first search of the control-flow graph of the
@@ -71,11 +107,67 @@ void reachability_slicert::fixedpoint_from_assertions(
   const is_threadedt &is_threaded,
   slicing_criteriont &criterion)
 {
-  std::vector<cfgt::node_indext> src = get_sources(is_threaded, criterion);
+  std::vector<search_stack_entryt> stack;
+  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
+  for(const auto source : sources)
+    stack.emplace_back(source, false);
+
+  while(!stack.empty())
+  {
+    auto &node = cfg[stack.back().node_index];
+    auto caller_is_known = stack.back().caller_is_known;
+    stack.pop_back();
+
 
-  const std::vector<cfgt::node_indext> reachable = cfg.get_reachable(src, true);
-  for(const auto index : reachable)
-    cfg[index].reachable_from_assertion = true;
+    if(node.reachable_from_assertion)
+      continue;
+    node.reachable_from_assertion = true;
+
+    if(node.PC->is_function_call())
+    {
+      // Queue the instruction's natural successor (function head, or next
+      // instruction if the function is bodyless)
+      INVARIANT(node.out.size() == 1, "Call sites should have one successor");
+      auto successor_index = node.out.begin()->first;
+
+      // If the function has a body, mark the function head, but note that we
+      // have already taken care of the return site.
+      const auto &callee_head_node = cfg[successor_index];
+      auto callee_it = callee_head_node.PC;
+      if(callee_it != std::next(node.PC))
+      {
+        stack.emplace_back(successor_index, true);
+
+        // Check if it can return, and if so mark the callsite's successor:
+        while(!callee_it->is_end_function())
+          ++callee_it;
+
+        if(cfg[cfg.entry_map[callee_it]].out.size() != 0)
+        {
+          stack.emplace_back(
+            cfg.entry_map[std::next(node.PC)], caller_is_known);
+        }
+      }
+      else
+      {
+        // Bodyless function -- mark the successor instruction only.
+        stack.emplace_back(successor_index, caller_is_known);
+      }
+    }
+    else if(node.PC->is_end_function())
+    {
+      if(!caller_is_known)
+      {
+        for(const auto &edge : node.out)
+          stack.emplace_back(edge.first, false);
+      }
+    }
+    else
+    {
+      for(const auto &edge : node.out)
+        stack.emplace_back(edge.first, caller_is_known);
+    }
+  }
 }
 
 /// This function removes all instructions that have the flag

src/goto-instrument/reachability_slicer_class.h

@@ -51,6 +51,29 @@ class reachability_slicert
 
   typedef std::stack<cfgt::entryt> queuet;
 
+  /// A search stack entry, used in tracking nodes to mark reachable when
+  /// walking over the CFG in `fixedpoint_to_assertions` and
+  /// `fixedpoint_from_assertions`.
+  struct search_stack_entryt
+  {
+    /// CFG node to mark reachable
+    cfgt::node_indext node_index;
+
+    /// If true, this function's caller is known and has already been queued to
+    /// mark reachable, so there is no need to queue anything when walking out
+    /// of the function, whether forwards (via END_FUNCTION) or backwards (via a
+    /// callsite).
+    /// If false, this function's caller is not known, so when walking forwards
+    /// from the end or backwards from the beginning we should queue all
+    /// possible callers.
+    bool caller_is_known;
+
+    search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known) :
+      node_index(node_index), caller_is_known(caller_is_known)
+    {
+    }
+  };
+
   void fixedpoint_to_assertions(
     const is_threadedt &is_threaded,
     slicing_criteriont &criterion);