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 {
43 
44  for(const auto &fct : goto_model.goto_functions.function_map)
45  {
46  if(!to_code_type(ns.lookup(fct.first).type).get_inlined())
47  {
48  for(const auto &ins : fct.second.body.instructions)
49  if(ins.is_assert())
50  {
51  if(functions_to_keep.insert(fct.first).second)
52  note_functions_to_keep(fct.first);
53  }
54  }
55  }
56 }
57 
59 {
60  for(const auto &name_snippet : name_snippets)
61  {
62  for(const auto &gf_entry : goto_model.goto_functions.function_map)
63  {
64  if(id2string(gf_entry.first).find(name_snippet) != std::string::npos)
65  functions_to_keep.insert(gf_entry.first);
66  }
67  }
68 }
69 
71 {
73 
76 
77  // if no properties are specified, preserve all functions containing
78  // any property
79  if(user_specified_properties.empty())
80  {
81  message.debug() << "No properties given, so aggressive slicer "
82  << "is running over all possible properties"
83  << messaget::eom;
85  }
86 
87  // if a name snippet is given, get list of all functions containing
88  // name snippet to preserve
89  if(!name_snippets.empty())
91 
92  for(const auto &p : user_specified_properties)
93  {
94  auto property_loc = find_property(p, goto_model.goto_functions);
95  if(!property_loc.has_value())
96  throw "unable to find property in call graph";
97  note_functions_to_keep(property_loc.value().get_function());
98  }
99 
100  // Add functions within distance of shortest path functions
101  // to the list
102  if(call_depth != 0)
103  {
104  for(const auto &func : get_functions_reachable_within_n_steps(
106  functions_to_keep.insert(func);
107  }
108 
109  message.debug() << "Preserving the following functions \n";
110  for(const auto &func : functions_to_keep)
111  message.debug() << func << messaget::eom;
112 
113  for(const auto &gf_entry : goto_model.goto_functions.function_map)
114  {
115  if(functions_to_keep.find(gf_entry.first) == functions_to_keep.end())
116  remove_function(goto_model, gf_entry.first, message_handler);
117  }
118 }
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
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.
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.
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.
Function Call Graph Helpers.
goto_modelt & goto_model
message_handlert & message_handler
std::list< std::string > user_specified_properties
call_grapht::directed_grapht call_graph
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
std::list< std::string > name_snippets
void get_all_functions_containing_properties()
Finds all functions that contain a property, and adds them to the list of 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...
const irep_idt start_function
std::set< irep_idt > functions_to_keep
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...
bool get_inlined() const
Definition: std_types.h:870
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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...
Remove function definition.
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.
Show the properties.
#define INITIALIZE_FUNCTION
static const char * message(const statust &status)
Makes a status message string from a status.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949