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

@@ -55,7 +55,7 @@ static bool is_same_target(
 
 /// Perform backwards depth-first search of the control-flow graph of the
 /// goto program, starting from the nodes corresponding to the criterion and
-/// the instructions that might be executed concurrently. Set reaches_assertion
+/// the instructions that might be executed concurrently. Set backward_state
 /// to true for every instruction visited.
 /// \param is_threaded Instructions that might be executed concurrently
 /// \param criterion the criterion we are trying to hit
@@ -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.backward_state ==
+         slicer_entryt::dfs_statust::BODY_AND_CALLERS_SEEN ||
+       (caller_is_known &&
+        node.backward_state == slicer_entryt::dfs_statust::BODY_SEEN))
+    {
       continue;
-    node.reaches_assertion = true;
+    }
+    node.backward_state =
+      caller_is_known ?
+      slicer_entryt::dfs_statust::BODY_SEEN :
+      slicer_entryt::dfs_statust::BODY_AND_CALLERS_SEEN;
 
     for(const auto &edge : node.in)
     {
@@ -111,8 +120,8 @@ void reachability_slicert::fixedpoint_to_assertions(
 
 /// Perform forwards depth-first search of the control-flow graph of the
 /// goto program, starting from the nodes corresponding to the criterion and
-/// the instructions that might be executed concurrently. Set reaches_assertion
-/// to true for every instruction visited.
+/// the instructions that might be executed concurrently. Set
+/// reachable_from_assertion to true for every instruction visited.
 /// \param is_threaded Instructions that might be executed concurrently
 /// \param criterion the criterion we are trying to hit
 void reachability_slicert::fixedpoint_from_assertions(
@@ -182,7 +191,7 @@ void reachability_slicert::fixedpoint_from_assertions(
 }
 
 /// This function removes all instructions that have the flag
-/// reaches_assertion or reachable_from_assertion set to true;
+/// backward_state or reachable_from_assertion set to true;
 void reachability_slicert::slice(goto_functionst &goto_functions)
 {
   // now replace those instructions that do not reach any assertions
@@ -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.backward_state == 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()
+      : backward_state(dfs_statust::NOT_SEEN),
+        reachable_from_assertion(false)
     {
     }
 
-    bool reaches_assertion;
+    /// The status of each node during backwards depth-first traversal:
+    /// A functions starts out NOT_SEEN, is raised to BODY_SEEN if we have seen
+    /// a call to this function but know where it was called from (at this point
+    /// we mark the function and anything reachable from it), then may finally
+    /// be raised to BODY_AND_CALLERS_SEEN if we don't know what function calls
+    /// this function, and therefore mark all of its callers as well.
+    enum class dfs_statust
+    {
+      NOT_SEEN,
+      BODY_SEEN,
+      BODY_AND_CALLERS_SEEN
+    } backward_state;
     bool reachable_from_assertion;
   };