Merge pull request #732 from tautschnig/reachability-slice

Support --property with --reachability-slice

Author: Daniel Kroening

CHANGELOG

@@ -1,6 +1,8 @@
 5.8
 ===
 
+* GOTO-INSTRUMENT: --reachability-slice can be used with --property to slice
+  down to a single property only.
 * GOTO-INSTRUMENT: New option --list-calls-args
 * GOTO-INSTRUMENT: New option --print-path-lenghts
 * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions

src/goto-instrument/full_slicer.cpp

@@ -13,9 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/remove_skip.h>
 
-#include <analyses/dependence_graph.h>
-
-#include "full_slicer.h"
 #include "full_slicer_class.h"
 
 /*******************************************************************\

src/goto-instrument/full_slicer_class.h

@@ -16,7 +16,9 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/cfg.h>
 
-#include <analyses/cfg_dominators.h>
+#include <analyses/dependence_graph.h>
+
+#include "full_slicer.h"
 
 // #define DEBUG_FULL_SLICERT
 #if 0
@@ -30,8 +32,6 @@ echo 'digraph g {' > c.dot ; cat c.goto | \
   dot -Tpdf -oc-red.pdf c-red.dot
 #endif
 
-class dependence_grapht;
-
 /*******************************************************************\
 
    Class: full_slicert

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1502,7 +1502,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("reachability-slice"))
   {
     status() << "Performing a reachability slice" << eom;
-    reachability_slicer(goto_functions);
+    if(cmdline.isset("property"))
+      reachability_slicer(goto_functions, cmdline.get_values("property"));
+    else
+      reachability_slicer(goto_functions);
   }
 
   // full slice?

src/goto-instrument/reachability_slicer.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_unreachable.h>
 #include <goto-programs/cfg.h>
 
+#include "full_slicer_class.h"
 #include "reachability_slicer.h"
 #include "reachability_slicer_class.h"
 
@@ -29,15 +30,16 @@ Function: reachability_slicert::fixedpoint_assertions
 \*******************************************************************/
 
 void reachability_slicert::fixedpoint_assertions(
-  const is_threadedt &is_threaded)
+  const is_threadedt &is_threaded,
+  slicing_criteriont &criterion)
 {
   queuet queue;
 
   for(cfgt::entry_mapt::iterator
       e_it=cfg.entry_map.begin();
       e_it!=cfg.entry_map.end();
       e_it++)
-    if(e_it->first->is_assert() ||
+    if(criterion(e_it->first) ||
        is_threaded(e_it->first))
       queue.push(e_it->second);
 
@@ -77,7 +79,7 @@ Function: reachability_slicert::slice
 void reachability_slicert::slice(goto_functionst &goto_functions)
 {
   // now replace those instructions that do not reach any assertions
-  // by self-loops
+  // by assume(false)
 
   Forall_goto_functions(f_it, goto_functions)
     if(f_it->second.body_available())
@@ -87,7 +89,7 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
         const cfgt::nodet &e=cfg[cfg.entry_map[i_it]];
         if(!e.reaches_assertion &&
            !i_it->is_end_function())
-          i_it->make_goto(i_it);
+          i_it->make_assumption(false_exprt());
       }
 
       // replace unreachable code by skip
@@ -113,5 +115,28 @@ Function: reachability_slicer
 
 void reachability_slicer(goto_functionst &goto_functions)
 {
-  reachability_slicert()(goto_functions);
+  reachability_slicert s;
+  assert_criteriont a;
+  s(goto_functions, a);
+}
+
+/*******************************************************************\
+
+Function: reachability_slicer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void reachability_slicer(
+  goto_functionst &goto_functions,
+  const std::list<std::string> &properties)
+{
+  reachability_slicert s;
+  properties_criteriont p(properties);
+  s(goto_functions, p);
 }

src/goto-instrument/reachability_slicer.h

@@ -13,4 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 void reachability_slicer(goto_functionst &goto_functions);
 
+void reachability_slicer(
+  goto_functionst &goto_functions,
+  const std::list<std::string> &properties);
+
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H

src/goto-instrument/reachability_slicer_class.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/is_threaded.h>
 
+class slicing_criteriont;
+
 /*******************************************************************\
 
    Class: reachability_slicert
@@ -25,11 +27,13 @@ Author: Daniel Kroening, [email protected]
 class reachability_slicert
 {
 public:
-  void operator()(goto_functionst &goto_functions)
+  void operator()(
+    goto_functionst &goto_functions,
+    slicing_criteriont &criterion)
   {
     cfg(goto_functions);
     is_threadedt is_threaded(goto_functions);
-    fixedpoint_assertions(is_threaded);
+    fixedpoint_assertions(is_threaded, criterion);
     slice(goto_functions);
   }
 
@@ -48,7 +52,9 @@ class reachability_slicert
 
   typedef std::stack<cfgt::entryt> queuet;
 
-  void fixedpoint_assertions(const is_threadedt &is_threaded);
+  void fixedpoint_assertions(
+    const is_threadedt &is_threaded,
+    slicing_criteriont &criterion);
 
   void slice(goto_functionst &goto_functions);
 };