Fix reachability slicer when used with recursive or unreachable functions

Author: tautschnig

regression/cbmc/reachability-slice-interproc2/main.c

@@ -0,0 +1,23 @@
+void b();
+
+void c()
+{
+  __CPROVER_assert(0, "");
+  b();
+}
+
+void b()
+{
+  a();
+  c();
+}
+
+void a()
+{
+  c();
+}
+
+int main()
+{
+  a();
+}

regression/cbmc/reachability-slice-interproc2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--reachability-slice --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+main\(\)
+--
+^warning: ignoring

src/goto-instrument/reachability_slicer.cpp

@@ -74,9 +74,18 @@ void reachability_slicert::fixedpoint_to_assertions(
     const auto caller_is_known = stack.back().caller_is_known;
     stack.pop_back();
 
-    if(node.reaches_assertion)
+    if(
+      node.reaches_assertion ==
+        slicer_entryt::dfs_statust::BODY_AND_CALLERS_SEEN ||
+      (caller_is_known &&
+       node.reaches_assertion == slicer_entryt::dfs_statust::BODY_SEEN))
+    {
       continue;
-    node.reaches_assertion = true;
+    }
+    node.reaches_assertion =
+      caller_is_known ?
+      slicer_entryt::dfs_statust::BODY_SEEN :
+      slicer_entryt::dfs_statust::BODY_AND_CALLERS_SEEN;
 
     for(const auto &edge : node.in)
     {
@@ -195,9 +204,12 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
       {
         const cfgt::nodet &e=cfg[cfg.entry_map[i_it]];
         if(
-          !e.reaches_assertion && !e.reachable_from_assertion &&
+          e.reaches_assertion == slicer_entryt::dfs_statust::NOT_SEEN &&
+          !e.reachable_from_assertion &&
           !i_it->is_end_function())
+        {
           i_it->make_assumption(false_exprt());
+        }
       }
 
       // replace unreachable code by skip

src/goto-instrument/reachability_slicer_class.h

@@ -38,11 +38,24 @@ class reachability_slicert
 protected:
   struct slicer_entryt
   {
-    slicer_entryt() : reaches_assertion(false), reachable_from_assertion(false)
+    slicer_entryt()
+      : reaches_assertion(dfs_statust::NOT_SEEN),
+        reachable_from_assertion(false)
     {
     }
 
-    bool reaches_assertion;
+    /// The status of each node during backwards depth-first traversal:
+    /// initially NOT_SEEN, and then BODY_SEEN if the callers of the function
+    /// the node belongs to will not be explored (implying that the node may
+    /// need to be visited again such that its callers are explored), and then
+    /// possibly BODY_AND_CALLERS_SEEN. At that point the node need no longer be
+    /// re-visited.
+    enum class dfs_statust
+    {
+      NOT_SEEN,
+      BODY_SEEN,
+      BODY_AND_CALLERS_SEEN
+    } reaches_assertion;
     bool reachable_from_assertion;
   };