Aggressive slicer

Aggressive slicer removes functions that may be relevant to the property/ies concerned. Preserves either all direct paths, or all functions on shortest path between start function(s) and function(s) containing property/ies.

Can be configured as described in the help text.

Author: polgreen

src/goto-instrument/Makefile

@@ -12,6 +12,7 @@ SRC = accelerate/accelerate.cpp \
       accelerate/scratch_program.cpp \
       accelerate/trace_automaton.cpp \
       accelerate/util.cpp \
+      aggressive_slicer.cpp \
       alignment_checks.cpp \
       branch.cpp \
       call_sequences.cpp \

src/goto-instrument/aggressive_slicer.cpp

@@ -0,0 +1,112 @@
+/*
+ * aggressive_slicer.cpp
+ *
+ *  Created on: 18 Jun 2018
+ *      Author: polgreen
+ */
+
+#include "aggressive_slicer.h"
+#include "remove_function.h"
+#include <analyses/call_graph_helpers.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/show_properties.h>
+#include <util/message.h>
+
+void aggressive_slicert::slice_for_function(irep_idt destination_function)
+{
+  if(preserve_all_direct_paths)
+  {
+    /// Note that we have previously disconnected all nodes unreachable
+    /// from the start function,
+    /// which means that any reaching functions are also reachable from
+    /// the start function.
+    for(const auto &func :
+        get_reaching_functions(call_graph, destination_function))
+      functions_to_keep.insert(func);
+  }
+  else
+  {
+    for(const auto &func : get_shortest_function_path(
+          call_graph, start_function, destination_function))
+      functions_to_keep.insert(func);
+  }
+}
+
+void aggressive_slicert::get_all_functions_containing_properties()
+{
+  for(const auto &fct : goto_model.goto_functions.function_map)
+  {
+    if(!fct.second.is_inlined())
+    {
+      for(const auto &ins : fct.second.body.instructions)
+        if(ins.is_assert())
+          slice_for_function(ins.function);
+    }
+  }
+}
+
+void aggressive_slicert::find_functions_that_contain_name_snippet()
+{
+  for(const auto &name_snippet : name_snippets)
+  {
+    forall_goto_functions(f_it, goto_model.goto_functions)
+    {
+      if(id2string(f_it->first).find(name_snippet) != std::string::npos)
+        functions_to_keep.insert(f_it->first);
+    }
+  }
+}
+
+void aggressive_slicert::doit()
+{
+  messaget message(message_handler);
+
+  functions_to_keep.insert(CPROVER_PREFIX "initialize");
+  functions_to_keep.insert(start_function);
+
+  // Necessary to compute cone of influence
+  if(preserve_all_direct_paths)
+    disconnect_unreachable_functions(call_graph, start_function);
+
+  // if no properties are specified, preserve all functions containing
+  // any property
+  if(user_specified_properties.empty())
+  {
+    message.debug() << "No properties given, so aggressive slicer "
+                    << "is running over all possible properties"
+                    << messaget::eom;
+    get_all_functions_containing_properties();
+  }
+
+  // if a name snippet is given, get list of all functions containing
+  // name snippet to preserve
+  if(!name_snippets.empty())
+    find_functions_that_contain_name_snippet();
+
+  for(const auto &p : user_specified_properties)
+  {
+    auto property_loc = find_property(p, goto_model.goto_functions);
+    if(!property_loc.has_value())
+      throw "unable to find property in call graph";
+    slice_for_function(property_loc.value().get_function());
+  }
+
+  // Add functions within distance of shortest path functions
+  // to the list
+  if(call_depth != 0)
+  {
+    for(const auto &func : get_functions_reachable_within_n_steps(
+          call_graph, functions_to_keep, call_depth, true))
+      functions_to_keep.insert(func);
+  }
+
+  message.debug() << "Preserving the following functions \n";
+  for(const auto &func : functions_to_keep)
+    message.debug() << func << messaget::eom;
+
+  forall_goto_functions(f_it, goto_model.goto_functions)
+  {
+    if(functions_to_keep.find(f_it->first) == functions_to_keep.end())
+      remove_function(goto_model, f_it->first, message_handler);
+  }
+}

src/goto-instrument/aggressive_slicer.h

@@ -0,0 +1,95 @@
+/*******************************************************************\
+
+Module: Aggressive Slicer
+
+Author: Elizabeth Polgreen, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Aggressive slicer
+/// Consider the control flow graph of the goto program and a criterion
+/// description of aggressive slicer here
+
+#ifndef CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
+#define CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
+
+#include <list>
+#include <string>
+#include <unordered_set>
+
+#include <util/irep.h>
+
+#include <analyses/call_graph.h>
+
+class goto_modelt;
+class message_handlert;
+
+/// \brief The aggressive slicer removes the body of all the functions except
+/// those on the shortest path, those within the call-depth of the
+/// shortest path, those given by name as command line argument,
+/// and those that contain a given irep_idt snippet
+/// If no properties are set by the user, we preserve all functions on
+/// the shortest paths to each property.
+class aggressive_slicert
+{
+public:
+  aggressive_slicert(goto_modelt &_goto_model, message_handlert &_msg)
+    : preserve_all_direct_paths(false),
+      goto_model(_goto_model),
+      message_handler(_msg)
+  {
+    start_function = goto_model.goto_functions.entry_point();
+    call_depth = 0;
+    call_grapht undirected_call_graph(goto_model);
+    call_graph = undirected_call_graph.get_directed_graph();
+  }
+
+  ///  \brief Removes the body of all functions except those on the
+  /// shortest path or functions
+  /// that are reachable from functions on the shortest path within
+  /// N calls, where N is given by the parameter "distance"
+  void doit();
+
+  /// \brief Adds a list of functions to the set of functions for the aggressive
+  /// slicer to preserve
+  /// \param  function_list:  a list of functions in form
+  /// std::list<std::string>, as returned by get_cmdline_option.
+  void preserve_functions(const std::list<std::string> &function_list)
+  {
+    for(const auto &f : function_list)
+      functions_to_keep.insert(f);
+  };
+
+  std::list<std::string> user_specified_properties;
+  std::size_t call_depth;
+  std::list<std::string> name_snippets;
+  bool preserve_all_direct_paths;
+
+private:
+  irep_idt start_function;
+  goto_modelt &goto_model;
+  message_handlert &message_handler;
+  std::set<irep_idt> functions_to_keep;
+  call_grapht::directed_grapht call_graph;
+
+  /// \brief Finds all functions whose name contains a name snippet
+  /// and adds them to the std::unordered_set of irep_idts of functions
+  /// for the aggressive slicer to preserve
+  void find_functions_that_contain_name_snippet();
+
+  /// \brief performs a slice from the start function to the given destination
+  /// function according to the configuration parameters set in the aggressive
+  /// slicer. Inserts functions to preserve into the functions_to_keep set
+  /// \param destination_function name of destination function for slice
+  void slice_for_function(irep_idt destination_function);
+
+  /// \brief Finds all functions that contain a property,
+  /// and adds them to the list of functions to keep. This
+  /// function is only called if no properties are given by the user.
+  /// This behaviour mirrors the behaviour of the other program
+  /// slicers (reachability, global, full)
+  void get_all_functions_containing_properties();
+};
+
+#endif /* CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H  */

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -100,6 +100,7 @@ Author: Daniel Kroening, [email protected]
 #include "undefined_functions.h"
 #include "remove_function.h"
 #include "splice_call.h"
+#include "aggressive_slicer.h"
 
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()
@@ -1433,6 +1434,46 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       *message_handler);
   }
 
+  // aggressive slicer
+  if(cmdline.isset("aggressive-slice"))
+  {
+    do_indirect_call_and_rtti_removal();
+
+    status() << "Slicing away initializations of unused global variables"
+             << eom;
+    slice_global_inits(goto_model);
+
+    status() << "Performing an aggressive slice" << eom;
+    aggressive_slicert aggressive_slicer(goto_model, get_message_handler());
+
+    if(cmdline.isset("call-depth"))
+      aggressive_slicer.call_depth =
+        safe_string2unsigned(cmdline.get_value("call-depth"));
+
+    if(cmdline.isset("preserve-function"))
+      aggressive_slicer.preserve_functions(
+        cmdline.get_values("preserve-function"));
+
+    if(cmdline.isset("property"))
+      aggressive_slicer.user_specified_properties =
+        cmdline.get_values("property");
+
+    if(cmdline.isset("preserve-functions-containing"))
+      aggressive_slicer.name_snippets =
+        cmdline.get_values("preserve-functions-containing");
+
+    aggressive_slicer.preserve_all_direct_paths =
+      cmdline.isset("preserve-all-direct-paths");
+
+    aggressive_slicer.doit();
+
+    status() << "Performing a reachability slice" << eom;
+    if(cmdline.isset("property"))
+      reachability_slicer(goto_model, cmdline.get_values("property"));
+    else
+      reachability_slicer(goto_model);
+  }
+
   // recalculate numbers, etc.
   goto_model.goto_functions.update();
 }
@@ -1535,6 +1576,14 @@ void goto_instrument_parse_optionst::help()
     " --full-slice                 slice away instructions that don't affect assertions\n" // NOLINT(*)
     " --property id                slice with respect to specific property only\n" // NOLINT(*)
     " --slice-global-inits         slice away initializations of unused global variables\n" // NOLINT(*)
+    " --aggressive-slice           remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
+    "                              the start function and the function containing the property(s)\n" // NOLINT(*)
+    " --call-depth <n>             used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
+    "                              of the functions on the shortest path\n"
+    " --preserve-function <f>      force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
+    " --preserve-function containing <f>\n"
+    "                              force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
+    "--preserve-all-direct-paths   force aggressive slicer to preserve all direct paths\n"
     "\n"
     "Further transformations:\n"
     " --constant-propagator        propagate constants and simplify expressions\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -90,6 +90,11 @@ Author: Daniel Kroening, [email protected]
   "(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
+  "(aggressive-slice)" \
+  "(call-depth):" \
+  "(preserve-function):" \
+  "(preserve-functions-containing):" \
+  "(preserve-all-direct-paths)" \
   OPT_FLUSH \
   "(splice-call):" \
   OPT_REMOVE_CALLS_NO_BODY \