Merge pull request #21 from tautschnig/property-specific-slicing

Slice with respect to select properties

Author: kroening

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:

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:

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

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1224,6 +1224,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"))
   {
@@ -1246,7 +1249,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
@@ -1347,6 +1353,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"

src/goto-instrument/goto_instrument_parse_options.h

@@ -49,7 +49,7 @@ Author: Daniel Kroening, [email protected]
   "(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)" \