aggressive_slicer.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Aggressive Slicer
 
Author: Elizabeth Polgreen, polgreen@amazon.com
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
#define CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
 
#include <list>
#include <string>
 
#include <util/irep.h>
 
#include <analyses/call_graph.h>
 
#include <goto-programs/goto_model.h>
 
class message_handlert;

class aggressive_slicert
{
public:
  aggressive_slicert(goto_modelt &_goto_model, message_handlert &_msg)
    : call_depth(0),
      preserve_all_direct_paths(false),
      start_function(_goto_model.goto_functions.entry_point()),
      goto_model(_goto_model),
      message_handler(_msg)
  {
    call_grapht undirected_call_graph =
      call_grapht::create_from_root_function(goto_model, start_function, false);
    call_graph = undirected_call_graph.get_directed_graph();
  }

  void doit();

  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:
  const 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;

  void find_functions_that_contain_name_snippet();

  void note_functions_to_keep(const irep_idt &destination_function);

  void get_all_functions_containing_properties();
};
 
// clang-format off
#define OPT_AGGRESSIVE_SLICER \
    "(aggressive-slice)" \
    "(aggressive-slice-call-depth):" \
    "(aggressive-slice-preserve-function):" \
    "(aggressive-slice-preserve-functions-containing):" \
    "(aggressive-slice-preserve-all-direct-paths)"
 
// clang-format on
 
#endif // CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H