cprover
Loading...
Searching...
No Matches
compute_called_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Query Called Functions
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <util/pointer_expr.h>
15#include <util/std_expr.h>
16
17#include "goto_model.h"
18
21 const exprt &src,
22 std::unordered_set<irep_idt> &address_taken)
23{
24 forall_operands(it, src)
25 compute_address_taken_functions(*it, address_taken);
26
27 if(src.id() == ID_address_of)
28 {
29 const address_of_exprt &address = to_address_of_expr(src);
30
31 if(
32 address.type().id() == ID_pointer &&
33 to_pointer_type(address.type()).base_type().id() == ID_code)
34 {
35 const exprt &target = address.object();
36 if(target.id() == ID_symbol)
37 address_taken.insert(to_symbol_expr(target).get_identifier());
38 }
39 }
40}
41
44 const exprt &src,
45 std::unordered_set<irep_idt> &address_taken)
46{
47 forall_operands(it, src)
48 compute_functions(*it, address_taken);
49
50 if(src.type().id()==ID_code &&
51 src.id()==ID_symbol)
52 address_taken.insert(to_symbol_expr(src).get_identifier());
53}
54
57 const goto_programt &goto_program,
58 std::unordered_set<irep_idt> &address_taken)
59{
60 for(const auto &i : goto_program.instructions)
61 {
62 i.apply([&address_taken](const exprt &expr) {
63 compute_address_taken_functions(expr, address_taken);
64 });
65 }
66}
67
70 const goto_functionst &goto_functions,
71 std::unordered_set<irep_idt> &address_taken)
72{
73 for(const auto &gf_entry : goto_functions.function_map)
74 compute_address_taken_functions(gf_entry.second.body, address_taken);
75}
76
78std::unordered_set<irep_idt>
80{
81 std::unordered_set<irep_idt> address_taken;
82 compute_address_taken_functions(goto_functions, address_taken);
83 return address_taken;
84}
85
87std::unordered_set<irep_idt>
89{
90 std::unordered_set<irep_idt> working_queue;
91 std::unordered_set<irep_idt> functions;
92
93 // start from entry point
94 working_queue.insert(goto_functions.entry_point());
95
96 while(!working_queue.empty())
97 {
98 irep_idt id=*working_queue.begin();
99 working_queue.erase(working_queue.begin());
100
101 if(!functions.insert(id).second)
102 continue;
103
104 const goto_functionst::function_mapt::const_iterator f_it=
105 goto_functions.function_map.find(id);
106
107 if(f_it==goto_functions.function_map.end())
108 continue;
109
110 const goto_programt &program=
111 f_it->second.body;
112
113 compute_address_taken_functions(program, working_queue);
114
115 for(const auto &instruction : program.instructions)
116 {
117 if(instruction.is_function_call())
118 {
119 compute_functions(instruction.call_function(), working_queue);
120 }
121 }
122 }
123
124 return functions;
125}
126
128std::unordered_set<irep_idt>
130{
131 return compute_called_functions(goto_model.goto_functions);
132}
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
std::string::const_iterator begin() const
Definition: dstring.h:176
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
const irep_idt & id() const
Definition: irep.h:396
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
void compute_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions in the expression
void compute_address_taken_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions whose address is taken
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Query Called Functions.
#define forall_operands(it, expr)
Definition: expr.h:18
Symbol Table + CFG.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189