Changes to the reachability slicer

Vojtech Forejt · Vojtech Forejt · commit 6120c172d15f · 2018-03-22T10:48:23.000Z
* Add forwards reachability to the slicer, in addition to the backwards reachability currently implemented.
* Add command-line options for the slicer in jbmc and cbmc.
* Refactor the way reachability is computed in the slicer, using grapht rather than own implementation
diff --git a/regression/cbmc-java/reachability-slice/A.class b/regression/cbmc-java/reachability-slice/A.class
diff --git a/regression/cbmc-java/reachability-slice/A.java b/regression/cbmc-java/reachability-slice/A.java
@@ -0,0 +1,14 @@
+public class A {
+
+    public void foo(int i ) {
+      // We use integer constants that we grep for later in a goto program.
+      int x = 1001 + i;
+      if (i > 0) {
+        x = 1002 + i; // property "java::A.foo:(I)V.coverage.3", see https://github.com/diffblue/cbmc/pull/1943#discussion_r175367063 for a discusison.
+        x = 1003 + i;
+      }
+      else
+        x = 1004 + i;
+      x = 1005 + i;  
+    }
+}
diff --git a/regression/cbmc-java/reachability-slice/test.desc b/regression/cbmc-java/reachability-slice/test.desc
@@ -0,0 +1,11 @@
+CORE
+A.class
+--reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
+1001
+--
+1003
+1004
+1005
+--
+Note: 1002 might and might not be removed, based on where the assertion for coverage resides.
+At the time of writing of this test, 1002 is removed.
diff --git a/regression/cbmc-java/reachability-slice/test2.desc b/regression/cbmc-java/reachability-slice/test2.desc
@@ -0,0 +1,9 @@
+CORE
+A.class
+--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
+1001
+1002
+1003
+1005
+--
+1004
diff --git a/regression/cbmc-java/reachability-slice/test3.desc b/regression/cbmc-java/reachability-slice/test3.desc
@@ -0,0 +1,8 @@
+CORE
+A.class
+--reachability-slice --show-goto-functions --cover location
+1001
+1002
+1003
+1004
+1005
diff --git a/regression/cbmc/reachability-slice/test.c b/regression/cbmc/reachability-slice/test.c
@@ -0,0 +1,13 @@
+void foo(int i)
+{
+  // We use integer constants that we grep for later in a goto program.
+  int x = 1001 + i;
+  if(i > 0)
+  { //foo.coverage.2
+    x = 1002 + i;
+    x = 1003 + i;
+  }
+  else
+    x = 1004 + i;
+  x = 1005 + i;
+}
diff --git a/regression/cbmc/reachability-slice/test.desc b/regression/cbmc/reachability-slice/test.desc
@@ -0,0 +1,9 @@
+CORE
+test.c
+--reachability-slice --show-goto-functions --cover location --property foo.coverage.2
+1001
+--
+1004
+1005
+--
+We do not include 1002 and 1003, whether this is hit depends on where assertion is put
diff --git a/regression/cbmc/reachability-slice/test2.desc b/regression/cbmc/reachability-slice/test2.desc
@@ -0,0 +1,9 @@
+CORE
+test.c
+--reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2
+1001
+1002
+1003
+1005
+--
+1004
diff --git a/regression/cbmc/reachability-slice/test3.desc b/regression/cbmc/reachability-slice/test3.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--reachability-slice --show-goto-functions --cover location
+1001
+1002
+1003
+1004
+--
+--
+We do not include 1005 since it might or might not be present based on where the assertion is in the block.
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
@@ -31,6 +31,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../pointer-analysis/add_failed_symbols$(OBJEXT) \
       ../pointer-analysis/rewrite_index$(OBJEXT) \
       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/cover$(OBJEXT) \
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -54,6 +54,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
 
+#include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/cover.h>
@@ -801,6 +802,32 @@ bool cbmc_parse_optionst::process_goto_program(
     // this would cause the property identifiers to change.
     label_properties(goto_model);
 
+    // reachability slice?
+    if(cmdline.isset("reachability-slice-fb"))
+    {
+      if(cmdline.isset("reachability-slice"))
+      {
+        error() << "--reachability-slice and --reachability-slice-fb "
+                << "must not be given together" << eom;
+        return true;
+      }
+
+      status() << "Performing a forwards-backwards reachability slice" << eom;
+      if(cmdline.isset("property"))
+        reachability_slicer(goto_model, cmdline.get_values("property"), true);
+      else
+        reachability_slicer(goto_model, true);
+    }
+
+    if(cmdline.isset("reachability-slice"))
+    {
+      status() << "Performing a reachability slice" << eom;
+      if(cmdline.isset("property"))
+        reachability_slicer(goto_model, cmdline.get_values("property"));
+      else
+        reachability_slicer(goto_model);
+    }
+
     // full slice?
     if(cmdline.isset("full-slice"))
     {
@@ -926,6 +953,8 @@ void cbmc_parse_optionst::help()
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
+    HELP_REACHABILITY_SLICER
+    " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     "\n"
     "Semantic transformations:\n"
     // NOLINTNEXTLINE(whitespace/line_length)
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -36,6 +36,7 @@ class optionst;
   "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
+  OPT_REACHABILITY_SLICER \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp
@@ -7,7 +7,11 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 /// \file
-/// Slicer
+/// Reachability Slicer
+/// Consider the control flow graph of the goto program and a criterion, and
+/// remove the parts of the graph from which the criterion is not reachable
+/// (and possibly, depending on the parameters, keep those that can be reached
+/// from the criterion).
 
 #include "reachability_slicer.h"
 
@@ -20,41 +24,62 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "full_slicer_class.h"
 #include "reachability_slicer_class.h"
 
-void reachability_slicert::fixedpoint_assertions(
+/// Get the set of nodes that correspond to the given criterion, or that can
+/// appear in concurrent execution. None of these should be sliced away so
+/// they are used as a basis for the search.
+/// \param is_threaded Instructions that might be executed concurrently
+/// \param criterion The criterion we care about
+std::vector<reachability_slicert::cfgt::node_indext>
+reachability_slicert::get_sources(
   const is_threadedt &is_threaded,
   slicing_criteriont &criterion)
 {
-  queuet queue;
+  std::vector<cfgt::node_indext> sources;
+  for(const auto &e_it : cfg.entry_map)
+  {
+    if(criterion(e_it.first) || is_threaded(e_it.first))
+      sources.push_back(e_it.second);
+  }
 
-  for(cfgt::entry_mapt::iterator
-      e_it=cfg.entry_map.begin();
-      e_it!=cfg.entry_map.end();
-      e_it++)
-    if(criterion(e_it->first) ||
-       is_threaded(e_it->first))
-      queue.push(e_it->second);
+  return sources;
+}
 
-  while(!queue.empty())
-  {
-    cfgt::entryt e=queue.top();
-    cfgt::nodet &node=cfg[e];
-    queue.pop();
+/// 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
+/// 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_to_assertions(
+  const is_threadedt &is_threaded,
+  slicing_criteriont &criterion)
+{
+  std::vector<cfgt::node_indext> src = get_sources(is_threaded, criterion);
 
-    if(node.reaches_assertion)
-      continue;
+  std::vector<cfgt::node_indext> reachable = cfg.get_reachable(src, false);
+  for(const auto index : reachable)
+    cfg[index].reaches_assertion = true;
+}
 
-    node.reaches_assertion=true;
+/// 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.
+/// \param is_threaded Instructions that might be executed concurrently
+/// \param criterion the criterion we are trying to hit
+void reachability_slicert::fixedpoint_from_assertions(
+  const is_threadedt &is_threaded,
+  slicing_criteriont &criterion)
+{
+  std::vector<cfgt::node_indext> src = get_sources(is_threaded, criterion);
 
-    for(cfgt::edgest::const_iterator
-        p_it=node.in.begin();
-        p_it!=node.in.end();
-        p_it++)
-    {
-      queue.push(p_it->first);
-    }
-  }
+  const std::vector<cfgt::node_indext> reachable = cfg.get_reachable(src, true);
+  for(const auto index : reachable)
+    cfg[index].reachable_from_assertion = true;
 }
 
+/// This function removes all instructions that have the flag
+/// reaches_assertion 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
@@ -66,8 +91,9 @@ 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]];
-        if(!e.reaches_assertion &&
-           !i_it->is_end_function())
+        if(
+          !e.reaches_assertion && !e.reachable_from_assertion &&
+          !i_it->is_end_function())
           i_it->make_assumption(false_exprt());
       }
 
@@ -80,18 +106,55 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
   goto_functions.update();
 }
 
-void reachability_slicer(goto_modelt &goto_model)
+/// Perform reachability slicing on goto_model, with respect to the
+/// criterion given by all properties.
+/// \param goto_model Goto program to slice
+/// \param include_forward_reachability Determines if only instructions
+/// from which the criterion is reachable should be kept (false) or also
+/// those reachable from the criterion (true)
+void reachability_slicer(
+  goto_modelt &goto_model,
+  const bool include_forward_reachability)
 {
   reachability_slicert s;
   assert_criteriont a;
-  s(goto_model.goto_functions, a);
+  s(goto_model.goto_functions, a, include_forward_reachability);
 }
 
+/// Perform reachability slicing on goto_model for selected properties.
+/// \param goto_model Goto program to slice
+/// \param properties The properties relevant for the slicing (i.e. starting
+/// point for the search in the cfg)
+/// \param include_forward_reachability Determines if only instructions
+/// from which the criterion is reachable should be kept (false) or also
+/// those reachable from the criterion (true)
 void reachability_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &properties)
+  const std::list<std::string> &properties,
+  const bool include_forward_reachability)
 {
   reachability_slicert s;
   properties_criteriont p(properties);
-  s(goto_model.goto_functions, p);
+  s(goto_model.goto_functions, p, include_forward_reachability);
+}
+
+/// Perform reachability slicing on goto_model, with respect to criterion
+/// comprising all properties. Only instructions from which the criterion
+/// is reachable will be kept.
+/// \param goto_model Goto program to slice
+void reachability_slicer(goto_modelt &goto_model)
+{
+  reachability_slicer(goto_model, false);
+}
+
+/// Perform reachability slicing on goto_model for selected properties. Only
+/// instructions from which the criterion is reachable will be kept.
+/// \param goto_model Goto program to slice
+/// \param properties The properties relevant for the slicing (i.e. starting
+/// point for the search in the cfg)
+void reachability_slicer(
+  goto_modelt &goto_model,
+  const std::list<std::string> &properties)
+{
+  reachability_slicer(goto_model, properties, false);
 }
diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h
@@ -23,4 +23,22 @@ void reachability_slicer(
   goto_modelt &,
   const std::list<std::string> &properties);
 
+void reachability_slicer(
+  goto_modelt &,
+  const bool include_forward_reachability);
+
+void reachability_slicer(
+  goto_modelt &,
+  const std::list<std::string> &properties,
+  const bool include_forward_reachability);
+
+#define OPT_REACHABILITY_SLICER                                                \
+  "(reachability-slice)(reachability-slice-fb)" // NOLINT(*)
+
+#define HELP_REACHABILITY_SLICER                                               \
+  " --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(*)
+
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H
diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h
diff --git a/src/jbmc/Makefile b/src/jbmc/Makefile
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
diff --git a/src/util/graph.h b/src/util/graph.h

-Original file line number
+Diff line change
@@ @@ -0,0 +1,9 @@ @@
 +CORE
 +A.class
 +--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
 +1001
 +1002
 +1003
 +1005
 +--
 +1004