Merge pull request #2758 from nmanthey/upstream-slice-functions

Upstream slice functions

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/cbmc/cbmc_parse_options.cpp

@@ -940,6 +940,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)" \