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
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...
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
message_handlert & message_handler
static eomt eom
Definition: message.h:284
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:416
#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.