cprover
aggressive_slicer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Aggressive slicer
4 
5 Author: Elizabeth Polgreen, elizabeth.polgreen@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #include "aggressive_slicer.h"
13 #include "remove_function.h"
17 #include <util/message.h>
18 
20  const irep_idt &destination_function)
21 {
23  {
28  for(const auto &func :
29  get_reaching_functions(call_graph, destination_function))
30  functions_to_keep.insert(func);
31  }
32  else
33  {
34  for(const auto &func : get_shortest_function_path(
35  call_graph, start_function, destination_function))
36  functions_to_keep.insert(func);
37  }
38 }
39 
41 {
42  for(const auto &fct : goto_model.goto_functions.function_map)
43  {
44  if(!fct.second.is_inlined())
45  {
46  for(const auto &ins : fct.second.body.instructions)
47  if(ins.is_assert())
48  {
49  if(functions_to_keep.insert(ins.function).second)
50  note_functions_to_keep(ins.function);
51  }
52  }
53  }
54 }
55 
57 {
58  for(const auto &name_snippet : name_snippets)
59  {
61  {
62  if(id2string(f_it->first).find(name_snippet) != std::string::npos)
63  functions_to_keep.insert(f_it->first);
64  }
65  }
66 }
67 
69 {
70  messaget message(message_handler);
71 
74 
75  // if no properties are specified, preserve all functions containing
76  // any property
77  if(user_specified_properties.empty())
78  {
79  message.debug() << "No properties given, so aggressive slicer "
80  << "is running over all possible properties"
81  << messaget::eom;
83  }
84 
85  // if a name snippet is given, get list of all functions containing
86  // name snippet to preserve
87  if(!name_snippets.empty())
89 
90  for(const auto &p : user_specified_properties)
91  {
92  auto property_loc = find_property(p, goto_model.goto_functions);
93  if(!property_loc.has_value())
94  throw "unable to find property in call graph";
95  note_functions_to_keep(property_loc.value().get_function());
96  }
97 
98  // Add functions within distance of shortest path functions
99  // to the list
100  if(call_depth != 0)
101  {
102  for(const auto &func : get_functions_reachable_within_n_steps(
104  functions_to_keep.insert(func);
105  }
106 
107  message.debug() << "Preserving the following functions \n";
108  for(const auto &func : functions_to_keep)
109  message.debug() << func << messaget::eom;
110 
112  {
113  if(functions_to_keep.find(f_it->first) == functions_to_keep.end())
115  }
116 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Remove function definition.
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...
function_mapt function_map
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...
void get_all_functions_containing_properties()
Finds all functions that contain a property, and adds them to the list of functions to keep...
call_grapht::directed_grapht call_graph
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Symbol Table + CFG.
#define INITIALIZE_FUNCTION
void remove_function(goto_modelt &goto_model, const irep_idt &identifier, message_handlert &message_handler)
Remove the body of function "identifier" such that an analysis will treat it as a side-effect free fu...
std::list< std::string > name_snippets
std::set< irep_idt > functions_to_keep
std::set< irep_idt > get_functions_reachable_within_n_steps(const call_grapht::directed_grapht &graph, const std::set< irep_idt > &start_functions, std::size_t n)
Get either callers or callees reachable from a given list of functions within N steps.
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
message_handlert & message_handler
std::set< irep_idt > get_reaching_functions(const call_grapht::directed_grapht &graph, const irep_idt &function)
Get functions that can reach a given function.
goto_modelt & goto_model
std::list< std::string > user_specified_properties
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
Function Call Graph Helpers.
Show the properties.
mstreamt & debug() const
Definition: message.h:332
#define forall_goto_functions(it, functions)
const irep_idt start_function
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
optionalt< source_locationt > find_property(const irep_idt &property, const goto_functionst &goto_functions)
Returns a source_locationt that corresponds to the property given by an irep_idt. ...
std::list< irep_idt > get_shortest_function_path(const call_grapht::directed_grapht &graph, const irep_idt &src, const irep_idt &dest)
Get list of functions on the shortest path between two functions.