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  {
63  {
64  if(id2string(f_it->first).find(name_snippet) != std::string::npos)
65  functions_to_keep.insert(f_it->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 
114  {
115  if(functions_to_keep.find(f_it->first) == functions_to_keep.end())
117  }
118 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
get_reaching_functions
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.
Definition: call_graph_helpers.cpp:68
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_model.h
Symbol Table + CFG.
get_functions_reachable_within_n_steps
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.
Definition: call_graph_helpers.cpp:74
aggressive_slicert::preserve_all_direct_paths
bool preserve_all_direct_paths
Definition: aggressive_slicer.h:70
messaget::eom
static eomt eom
Definition: message.h:297
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
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
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
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
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
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
remove_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...
Definition: remove_function.cpp:26
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
show_properties.h
Show the properties.
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
remove_function.h
Remove function definition.
call_graph_helpers.h
Function Call Graph Helpers.
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
aggressive_slicert::user_specified_properties
std::list< std::string > user_specified_properties
Definition: aggressive_slicer.h:65
aggressive_slicer.h
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
aggressive_slicert::message_handler
message_handlert & message_handler
Definition: aggressive_slicer.h:75
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
aggressive_slicert::start_function
const irep_idt start_function
Definition: aggressive_slicer.h:73
get_shortest_function_path
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.
Definition: call_graph_helpers.cpp:107
find_property
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.
Definition: show_properties.cpp:25
aggressive_slicert::name_snippets
std::list< std::string > name_snippets
Definition: aggressive_slicer.h:69
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:867
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
message.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
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