From dfc3b6ef726d11e6c9405663057c5b9327ccee70 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 3 Mar 2017 08:17:34 +0000 Subject: [PATCH] Support --property with --reachability-slice Make the support for property-guided slicing the same for both --full-slice and --reachability-slice. Furthermore replace sliced code by assume(false) instead of unbounded (self-)loops. --- CHANGELOG | 7 ++++ src/goto-instrument/full_slicer.cpp | 3 -- src/goto-instrument/full_slicer_class.h | 6 ++-- .../goto_instrument_parse_options.cpp | 5 ++- src/goto-instrument/reachability_slicer.cpp | 35 ++++++++++++++++--- src/goto-instrument/reachability_slicer.h | 4 +++ .../reachability_slicer_class.h | 12 +++++-- 7 files changed, 57 insertions(+), 15 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 0f15c3d5081..6c613977e3a 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,10 @@ +5.8 +=== + +* GOTO-INSTRUMENT: --reachability-slice can be used with --property to slice + down to a single property only. + + 5.7 === diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index f7b42a0af3c..887805ad80a 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -13,9 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - -#include "full_slicer.h" #include "full_slicer_class.h" /*******************************************************************\ diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h index 4495fa95246..93894513f57 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-instrument/full_slicer_class.h @@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include + +#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 diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 21000a78da6..1c60205b5c7 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1441,7 +1441,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? diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 231ae40cde9..073f9284add 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "full_slicer_class.h" #include "reachability_slicer.h" #include "reachability_slicer_class.h" @@ -29,7 +30,8 @@ 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; @@ -37,7 +39,7 @@ void reachability_slicert::fixedpoint_assertions( 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 &properties) +{ + reachability_slicert s; + properties_criteriont p(properties); + s(goto_functions, p); } diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h index 7ce03a1d612..e45aa81f27e 100644 --- a/src/goto-instrument/reachability_slicer.h +++ b/src/goto-instrument/reachability_slicer.h @@ -13,4 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com void reachability_slicer(goto_functionst &goto_functions); +void reachability_slicer( + goto_functionst &goto_functions, + const std::list &properties); + #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 index 85f1e62a345..224259b57cd 100644 --- a/src/goto-instrument/reachability_slicer_class.h +++ b/src/goto-instrument/reachability_slicer_class.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +class slicing_criteriont; + /*******************************************************************\ Class: reachability_slicert @@ -25,11 +27,13 @@ Author: Daniel Kroening, kroening@kroening.com 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 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); };