slicer: add function path slicer

This slicer keeps any function in the program, in case it is backward
or forward reachable from the target function. The analysis can be
repeated for multiple functions.

Note: This implementation cannot deal with order of function calls, e.g.
if functions a,b and c should be kept, then a path that has
a, which calls c, which calls b
will also be kept. However, path where not all functions will be called,
will be dropped.

Author: Petr Bauch

regression/goto-instrument/fp-reachability-slice1/main.c

@@ -0,0 +1,34 @@
+void a()
+{
+  int e;
+}
+
+void b()
+{
+  double f;
+  if(f == 0)
+    a();
+}
+
+void c()
+{
+  int d;
+}
+
+int main()
+{
+  int k;
+  if(k == 0)
+  {
+    int l;
+    a();
+    c();
+  }
+  else
+  {
+    b();
+  }
+  int n;
+  a();
+  return n;
+}

regression/goto-instrument/fp-reachability-slice1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--fp-reachability-slice c
+^EXIT=0$
+^SIGNAL=0$
+1: ASSUME FALSE
+dead e;
+dead d;
+--
+^warning: ignoring
+dead f;

regression/goto-instrument/fp-reachability-slice2/main.c

@@ -0,0 +1,34 @@
+void a()
+{
+  int e;
+}
+
+void b()
+{
+  double f;
+  if(f == 0)
+    a();
+}
+
+void c()
+{
+  int d;
+}
+
+int main()
+{
+  int k;
+  if(k == 0)
+  {
+    int l;
+    a();
+    c();
+  }
+  else
+  {
+    b();
+  }
+  int n;
+  a();
+  return n;
+}

regression/goto-instrument/fp-reachability-slice2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--fp-reachability-slice a,c
+^EXIT=0$
+^SIGNAL=0$
+dead d;
+dead e;
+--
+^warning: ignoring
+dead f;

regression/goto-instrument/fp-reachability-slice3/main.c

@@ -0,0 +1,34 @@
+void a()
+{
+  int e;
+}
+
+void b()
+{
+  double f;
+  if(f == 0)
+    a();
+}
+
+void c()
+{
+  int d;
+}
+
+int main()
+{
+  int k;
+  if(k == 0)
+  {
+    int l;
+    a();
+    c();
+  }
+  else
+  {
+    b();
+  }
+  int n;
+  a();
+  return n;
+}

regression/goto-instrument/fp-reachability-slice3/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--fp-reachability-slice b,c
+^EXIT=0$
+^SIGNAL=0$
+1 file main.c line 34
+--
+^warning: ignoring
+dead d;
+dead e;
+dead f;

src/goto-instrument/reachability_slicer.cpp

@@ -17,9 +17,12 @@ Author: Daniel Kroening, [email protected]
 
 #include <stack>
 
+#include <goto-programs/cfg.h>
+#include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
-#include <goto-programs/cfg.h>
+
+#include "util/message.h"
 
 #include "full_slicer_class.h"
 #include "reachability_slicer_class.h"
@@ -91,8 +94,7 @@ void reachability_slicert::fixedpoint_to_assertions(
           "all function return edges should point to the successor of a "
           "FUNCTION_CALL instruction");
         stack.emplace_back(edge.first, true);
-        stack.emplace_back(
-          cfg.entry_map[std::prev(node.PC)], caller_is_known);
+        stack.emplace_back(cfg.entry_map[std::prev(node.PC)], caller_is_known);
       }
       else if(pred_node.PC->is_function_call())
       {
@@ -193,7 +195,7 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
     {
       Forall_goto_program_instructions(i_it, f_it->second.body)
       {
-        const cfgt::nodet &e=cfg[cfg.entry_map[i_it]];
+        cfgt::nodet &e = cfg[cfg.entry_map[i_it]];
         if(
           !e.reaches_assertion && !e.reachable_from_assertion &&
           !i_it->is_end_function())
@@ -240,6 +242,31 @@ void reachability_slicer(
   s(goto_model.goto_functions, p, include_forward_reachability);
 }
 
+/// Perform reachability slicing on goto_model for selected functions.
+/// \param goto_model Goto program to slice
+/// \param functions_list The functions relevant for the slicing (i.e. starting
+/// point for the search in the cfg). Anything that is reachable in the CFG
+/// starting from these functions will be kept.
+void function_path_reachability_slicer(
+  goto_modelt &goto_model,
+  const std::string &functions_list)
+{
+  std::istringstream functions_stream(functions_list);
+  std::string single_function;
+  while(std::getline(functions_stream, single_function, ','))
+  {
+    in_function_criteriont matching_criterion(single_function);
+    reachability_slicert slicer;
+    slicer(goto_model.goto_functions, matching_criterion, true);
+  }
+
+  remove_calls_no_bodyt remove_calls_no_body;
+  remove_calls_no_body(goto_model.goto_functions);
+
+  goto_model.goto_functions.update();
+  goto_model.goto_functions.compute_loop_numbers();
+}
+
 /// Perform reachability slicing on goto_model, with respect to criterion
 /// comprising all properties. Only instructions from which the criterion
 /// is reachable will be kept.

src/goto-instrument/reachability_slicer.h

@@ -23,6 +23,10 @@ void reachability_slicer(
   goto_modelt &,
   const std::list<std::string> &properties);
 
+void function_path_reachability_slicer(
+  goto_modelt &goto_model,
+  const std::string &functions_list);
+
 void reachability_slicer(
   goto_modelt &,
   const bool include_forward_reachability);
@@ -33,13 +37,16 @@ void reachability_slicer(
   const bool include_forward_reachability);
 
 // clang-format off
-#define OPT_REACHABILITY_SLICER \
-  "(reachability-slice)(reachability-slice-fb)" // NOLINT(*)
-
-#define HELP_REACHABILITY_SLICER \
-  " --reachability-slice         remove instructions that cannot appear on\n" \
-  "                              a trace from entry point to a property\n" \
-  " --reachability-slice-fb      remove instructions that cannot appear on\n" \
-  "                              a trace from entry point through a property\n" // NOLINT(*)
+#define OPT_REACHABILITY_SLICER                                                \
+  "(fp-reachability-slice):(reachability-slice)(reachability-slice-fb)" // NOLINT(*)
+
+#define HELP_REACHABILITY_SLICER                                               \
+  " --fp-reachability-slice <f>  remove instructions that cannot appear on a " \
+  "trace that visits all given functions. The list of functions has to be "    \
+  "given as a comma separated list.\n"                                         \
+  " --reachability-slice         remove instructions that cannot appear on a " \
+  "trace from entry point to a property\n"                                     \
+  " --reachability-slice-fb      remove instructions that cannot appear on a " \
+  "trace from entry point through a property\n" // NOLINT(*)
 // clang-format on
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H