cprover
aggressive_slicer.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Aggressive Slicer
4 
5 Author: Elizabeth Polgreen, polgreen@amazon.com
6 
7 \*******************************************************************/
8 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
15 #define CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
16 
17 #include <list>
18 #include <string>
19 #include <unordered_set>
20 
21 #include <util/irep.h>
22 
23 #include <analyses/call_graph.h>
24 
26 
27 class goto_modelt;
28 class message_handlert;
29 
37 {
38 public:
40  : call_depth(0),
42  start_function(_goto_model.goto_functions.entry_point()),
43  goto_model(_goto_model),
44  message_handler(_msg)
45  {
46  call_grapht undirected_call_graph =
48  call_graph = undirected_call_graph.get_directed_graph();
49  }
50 
55  void doit();
56 
61  void preserve_functions(const std::list<std::string> &function_list)
62  {
63  for(const auto &f : function_list)
64  functions_to_keep.insert(f);
65  };
66 
67  std::list<std::string> user_specified_properties;
68  std::size_t call_depth;
69  std::list<std::string> name_snippets;
71 
72 private:
76  std::set<irep_idt> functions_to_keep;
78 
83 
90  void note_functions_to_keep(const irep_idt &destination_function);
91 
98 };
99 
100 // clang-format off
101 #define OPT_AGGRESSIVE_SLICER \
102  "(aggressive-slice)" \
103  "(aggressive-slice-call-depth):" \
104  "(aggressive-slice-preserve-function):" \
105  "(aggressive-slice-preserve-functions-containing):" \
106  "(aggressive-slice-preserve-all-direct-paths)"
107 
108 // clang-format on
109 
110 #endif // CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
aggressive_slicert::goto_model
goto_modelt & goto_model
Definition: aggressive_slicer.h:74
goto_modelt
Definition: goto_model.h:26
aggressive_slicert::preserve_all_direct_paths
bool preserve_all_direct_paths
Definition: aggressive_slicer.h:70
call_graph.h
Function Call Graphs.
aggressive_slicert::note_functions_to_keep
void note_functions_to_keep(const irep_idt &destination_function)
notes functions to keep in the slice based on the program start function and the given destination fu...
Definition: aggressive_slicer.cpp:19
aggressive_slicert::find_functions_that_contain_name_snippet
void find_functions_that_contain_name_snippet()
Finds all functions whose name contains a name snippet and adds them to the std::unordered_set of ire...
Definition: aggressive_slicer.cpp:58
call_grapht::create_from_root_function
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:48
aggressive_slicert::doit
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
Definition: aggressive_slicer.cpp:70
call_grapht::directed_grapht
Directed graph representation of this call graph.
Definition: call_graph.h:135
aggressive_slicert::get_all_functions_containing_properties
void get_all_functions_containing_properties()
Finds all functions that contain a property, and adds them to the list of functions to keep.
Definition: aggressive_slicer.cpp:40
aggressive_slicert::call_depth
std::size_t call_depth
Definition: aggressive_slicer.h:68
message_handlert
Definition: message.h:28
call_grapht::get_directed_graph
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms.
Definition: call_graph.cpp:208
aggressive_slicert::aggressive_slicert
aggressive_slicert(goto_modelt &_goto_model, message_handlert &_msg)
Definition: aggressive_slicer.h:39
aggressive_slicert::user_specified_properties
std::list< std::string > user_specified_properties
Definition: aggressive_slicer.h:65
call_grapht
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:39
aggressive_slicert
The aggressive slicer removes the body of all the functions except those on the shortest path,...
Definition: aggressive_slicer.h:37
aggressive_slicert::message_handler
message_handlert & message_handler
Definition: aggressive_slicer.h:75
aggressive_slicert::start_function
const irep_idt start_function
Definition: aggressive_slicer.h:73
aggressive_slicert::name_snippets
std::list< std::string > name_snippets
Definition: aggressive_slicer.h:69
aggressive_slicert::preserve_functions
void preserve_functions(const std::list< std::string > &function_list)
Adds a list of functions to the set of functions for the aggressive slicer to preserve.
Definition: aggressive_slicer.h:61
static_lifetime_init.h
aggressive_slicert::call_graph
call_grapht::directed_grapht call_graph
Definition: aggressive_slicer.h:77
aggressive_slicert::functions_to_keep
std::set< irep_idt > functions_to_keep
Definition: aggressive_slicer.h:76
irep.h