Upstream slice functions

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/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/full_slicer_class.h

@@ -113,6 +113,23 @@ class assert_criteriont:public slicing_criteriont
   }
 };
 
+class in_function_criteriont : public slicing_criteriont
+{
+public:
+  explicit in_function_criteriont(const std::string &function_name)
+    : target_function(function_name)
+  {
+  }
+
+  virtual bool operator()(goto_programt::const_targett target)
+  {
+    return target->function == target_function;
+  }
+
+protected:
+  const irep_idt target_function;
+};
+
 class properties_criteriont:public slicing_criteriont
 {
 public:

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

@@ -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,29 @@ 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::list<std::string> &functions_list)
+{
+  for(const auto &function : functions_list)
+  {
+    in_function_criteriont matching_criterion(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::list<std::string> &functions_list);
+
 void reachability_slicer(
   goto_modelt &,
   const bool include_forward_reachability);
@@ -33,13 +37,18 @@ 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\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);