slicer: add function path to goto-instrument

This commit adds the command line argument handling for the
function path slicer.

To keep all possible exeuction traces that hit both function a and b, an
example invocation could look as follows:

goto-instrument --fp-reachability-slice a,b input output

Note, any trace that touches only a, but not b, will not be kept in the
program.

Author: Petr Bauch

src/cbmc/cbmc_parse_options.cpp

@@ -933,6 +933,7 @@ void cbmc_parse_optionst::help()
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
+    HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1430,6 +1430,15 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       reachability_slicer(goto_model);
   }
 
+  if(cmdline.isset("fp-reachability-slice"))
+  {
+    do_indirect_call_and_rtti_removal();
+
+    status() << "Performing a function pointer reachability slice" << eom;
+    function_path_reachability_slicer(
+      goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
+  }
+
   // full slice?
   if(cmdline.isset("full-slice"))
   {
@@ -1610,7 +1619,7 @@ void goto_instrument_parse_optionst::help()
     " --render-cluster-function    clusterises the dot by functions\n"
     "\n"
     "Slicing:\n"
-    " --reachability-slice         slice away instructions that can't reach assertions\n" // NOLINT(*)
+    HELP_REACHABILITY_SLICER
     " --full-slice                 slice away instructions that don't affect assertions\n" // NOLINT(*)
     " --property id                slice with respect to specific property only\n" // NOLINT(*)
     " --slice-global-inits         slice away initializations of unused global variables\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -71,6 +71,7 @@ Author: Daniel Kroening, [email protected]
   "(show-struct-alignment)(interval-analysis)(show-intervals)" \
   "(show-uninitialized)(show-locations)" \
   "(full-slice)(reachability-slice)(slice-global-inits)" \
+  "(fp-reachability-slice):" \
   "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
   OPT_REMOVE_CONST_FUNCTION_POINTERS \
   "(print-internal-representation)" \

src/goto-instrument/reachability_slicer.cpp

@@ -245,17 +245,15 @@ void reachability_slicer(
 /// 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
+/// 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)
+  const std::list<std::string> &functions_list)
 {
-  std::istringstream functions_stream(functions_list);
-  std::string single_function;
-  while(std::getline(functions_stream, single_function, ','))
+  for(const auto &function : functions_list)
   {
-    in_function_criteriont matching_criterion(single_function);
+    in_function_criteriont matching_criterion(function);
     reachability_slicert slicer;
     slicer(goto_model.goto_functions, matching_criterion, true);
   }

src/goto-instrument/reachability_slicer.h

@@ -25,7 +25,7 @@ void reachability_slicer(
 
 void function_path_reachability_slicer(
   goto_modelt &goto_model,
-  const std::string &functions_list);
+  const std::list<std::string> &functions_list);
 
 void reachability_slicer(
   goto_modelt &,
@@ -40,13 +40,15 @@ void reachability_slicer(
 #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(*)
+#define HELP_REACHABILITY_SLICER                                                      \
+  " --fp-reachability-slice f    remove instructions that cannot appear on a trace\n" \
+  "                              that visits all given functions. The list of\n"      \
+  "                              functions has to be given as a comma separated\n"    \
+  "                              list f.\n"                                           \
+  " --reachability-slice         remove instructions that cannot appear on a trace\n" \
+  "                              from entry point to a property\n" // NOLINT(*)
+#define HELP_REACHABILITY_SLICER_FB                                                   \
+  " --reachability-slice-fb      remove instructions that cannot appear on a trace\n" \
+  "                              from entry point through a property\n" // NOLINT(*)
 // clang-format on
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H

src/util/cmdline.cpp

@@ -118,6 +118,23 @@ const std::list<std::string> &cmdlinet::get_values(
     return immutable_empty_list;
 }
 
+std::list<std::string>
+cmdlinet::get_comma_separated_values(const char *option) const
+{
+  std::list<std::string> separated_values;
+  auto i = getoptnr(option);
+  if(i.has_value() && !options[*i].values.empty())
+  {
+    std::istringstream values_stream(options[*i].values.front());
+    std::string single_value;
+    while(std::getline(values_stream, single_value, ','))
+    {
+      separated_values.push_back(single_value);
+    }
+  }
+  return separated_values;
+}
+
 optionalt<std::size_t> cmdlinet::getoptnr(char option) const
 {
   for(std::size_t i=0; i<options.size(); i++)

src/util/cmdline.h

@@ -27,6 +27,8 @@ class cmdlinet
   const std::list<std::string> &get_values(const std::string &option) const;
   const std::list<std::string> &get_values(char option) const;
 
+  std::list<std::string> get_comma_separated_values(const char *option) const;
+
   virtual bool isset(char option) const;
   virtual bool isset(const char *option) const;
   virtual void set(const std::string &option);