From 9b34522313e0351d6a18556ba2e73555702e3332 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 17 May 2015 18:26:18 +0100
Subject: [PATCH] Slice with respect to select properties
---
src/goto-instrument/full_slicer.cpp | 21 +++++++++++++
src/goto-instrument/full_slicer.h | 5 +++
src/goto-instrument/full_slicer_class.h | 31 +++++++++++++++++++
.../goto_instrument_parse_options.cpp | 9 +++++-
.../goto_instrument_parse_options.h | 2 +-
5 files changed, 66 insertions(+), 2 deletions(-)
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 6e261d3dbb0..e0741bc24cd 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -473,6 +473,27 @@ void full_slicer(
/*******************************************************************\
+Function: property_slicer
+
+ Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void property_slicer(
+ goto_functionst &goto_functions,
+ const namespacet &ns,
+ const std::list<std::string> &properties)
+{
+ properties_criteriont p(properties);
+ full_slicert()(goto_functions, ns, p);
+}
+
+/*******************************************************************\
+
Function: slicing_criteriont::~slicing_criteriont
Inputs:
diff --git a/src/goto-instrument/full_slicer.h b/src/goto-instrument/full_slicer.h
index 93225ba9880..c361c0ae49b 100644
--- a/src/goto-instrument/full_slicer.h
+++ b/src/goto-instrument/full_slicer.h
@@ -15,6 +15,11 @@ void full_slicer(
goto_functionst &goto_functions,
const namespacet &ns);
+void property_slicer(
+ goto_functionst &goto_functions,
+ const namespacet &ns,
+ const std::list<std::string> &properties);
+
class slicing_criteriont
{
public:
diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h
index 6074128112c..888eeab982d 100644
--- a/src/goto-instrument/full_slicer_class.h
+++ b/src/goto-instrument/full_slicer_class.h
@@ -118,4 +118,35 @@ class assert_criteriont:public slicing_criteriont
}
};
+class properties_criteriont:public slicing_criteriont
+{
+public:
+ explicit properties_criteriont(
+ const std::list<std::string> &properties):
+ property_ids(properties)
+ {
+ }
+
+ virtual bool operator()(goto_programt::const_targett target)
+ {
+ if(!target->is_assert())
+ return false;
+
+ const std::string &p_id=
+ id2string(target->source_location.get_property_id());
+
+ for(std::list<std::string>::const_iterator
+ it=property_ids.begin();
+ it!=property_ids.end();
+ ++it)
+ if(p_id==*it)
+ return true;
+
+ return false;
+ }
+
+protected:
+ const std::list<std::string> &property_ids;
+};
+
#endif
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 4fd004550e2..9578df5e63a 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1216,6 +1216,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
// add loop ids
goto_functions.compute_loop_numbers();
+ // label the assertions
+ label_properties(goto_functions);
+
// nondet volatile?
if(cmdline.isset("nondet-volatile"))
{
@@ -1238,7 +1241,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
symbol_table, goto_functions, cmdline.isset("pointer-check"));
status() << "Performing a full slice" << eom;
- full_slicer(goto_functions, ns);
+ if(cmdline.isset("property"))
+ property_slicer(goto_functions, ns, cmdline.get_values("property"));
+ else
+ full_slicer(goto_functions, ns);
}
// label the assertions
@@ -1339,6 +1345,7 @@ void goto_instrument_parse_optionst::help()
"Slicing:\n"
" --reachability-slice slice away instructions that can't reach assertions\n"
" --full-slice slice away instructions that don't affect assertions\n"
+ " --property id slice with respect to specific property only\n"
"\n"
"Further transformations:\n"
" --constant-propagator propagate constants and simplify expressions\n"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index e0b24cd1ee3..9ea0ead4fbe 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -49,7 +49,7 @@ Author: Daniel Kroening, kroening@kroening.com
"(show-uninitialized)(show-locations)" \
"(full-slice)(reachability-slice)" \
"(inline)" \
- "(show-claims)(show-properties)" \
+ "(show-claims)(show-properties)(property):" \
"(show-symbol-table)(show-points-to)(show-rw-set)" \
"(cav11)" \
"(show-natural-loops)(accelerate)(havoc-loops)" \