CBMC
Loading...
Searching...
No Matches
call_sequences.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Printing function call sequences for Ofer
4
5Author: Daniel Kroening
6
7Date: April 2013
8
9\*******************************************************************/
10
13
14#include "call_sequences.h"
15
16#include <stack>
17#include <iostream>
18
19#include <util/simplify_expr.h>
20
22
24
26
28 const irep_idt &caller,
29 const goto_programt &goto_program)
30{
31 // show calls in blocks within caller body
32 // dfs on code blocks using stack
33 std::cout << "# " << caller << '\n';
34 std::stack<goto_programt::const_targett> stack;
35 std::set<goto_programt::const_targett, goto_programt::target_less_than> seen;
36 const goto_programt::const_targett start=goto_program.instructions.begin();
37
38 if(start!=goto_program.instructions.end())
39 stack.push(start);
40
41 while(!stack.empty())
42 {
43 goto_programt::const_targett t=stack.top();
44 stack.pop();
45
46 if(!seen.insert(t).second)
47 continue; // seen it already
48 if(t->is_function_call())
49 {
50 const exprt &callee = t->call_function();
51 if(callee.id()==ID_symbol)
52 {
53 std::cout << caller << " -> "
54 << to_symbol_expr(callee).get_identifier() << '\n';
55 }
56 }
57
58 // get successors and add to stack
59 for(const auto &it : goto_program.get_successors(t))
60 {
61 stack.push(it);
62 }
63 }
64 std::cout << '\n';
65}
66
67void show_call_sequences(const goto_modelt &goto_model)
68{
69 // do per function
70 // show the calls in the body of the specific function
71
72 for(const auto &gf_entry : goto_model.goto_functions.function_map)
73 show_call_sequences(gf_entry.first, gf_entry.second.body);
74}
75
77{
78public:
81 const std::vector<irep_idt> &_sequence):
84 {
85 }
86
87 void operator()();
88
89protected:
91 const std::vector<irep_idt> &sequence;
92
94 {
95 goto_functionst::function_mapt::const_iterator f;
97
98 bool operator==(const call_stack_entryt &other) const
99 {
100 return
101 f->first==other.f->first &&
103 }
104 };
105
106 struct statet
107 {
108 goto_functionst::function_mapt::const_iterator f;
110 std::vector<call_stack_entryt> call_stack;
111 unsigned index;
112
113 bool operator==(const statet &other) const
114 {
115 return
116 f->first==other.f->first &&
117 pc==other.pc &&
118 call_stack==other.call_stack &&
119 index==other.index;
120 }
121 };
122
123 // NOLINTNEXTLINE(readability/identifiers)
125 {
126 std::size_t operator()(const statet &s) const
127 {
128 size_t pc_hash=
129 s.pc==s.f->second.body.instructions.end()?0:
130 (size_t)&*s.pc;
131
132 return hash_string(s.f->first)^
133 pc_hash^
134 s.index^s.call_stack.size();
135 }
136 };
137
138 typedef std::unordered_set<statet, state_hash> statest;
140};
141
143{
144 std::stack<statet> queue;
145
146 if(sequence.empty())
147 {
148 std::cout << "empty sequence given\n";
149 return;
150 }
151
152 irep_idt entry=sequence.front();
153
154 goto_functionst::function_mapt::const_iterator f_it=
155 goto_functions.function_map.find(entry);
156
157 if(f_it!=goto_functions.function_map.end())
158 {
159 queue.push(statet());
160 queue.top().f=f_it;
161 queue.top().pc=f_it->second.body.instructions.begin();
162 queue.top().index=1;
163 }
164
165 while(!queue.empty())
166 {
167 statet &e=queue.top();
168
169 // seen already?
170 if(states.find(e)!=states.end())
171 {
172 // drop, continue
173 queue.pop();
174 continue;
175 }
176
177 // insert
178 states.insert(e);
179
180 // satisfies sequence?
181 if(e.index==sequence.size())
182 {
183 std::cout << "sequence feasible\n";
184 return;
185 }
186
187 // new, explore
188 if(e.pc==e.f->second.body.instructions.end())
189 {
190 if(e.call_stack.empty())
191 queue.pop();
192 else
193 {
194 // successor is the return location
195 e.pc=e.call_stack.back().return_address;
196 e.f=e.call_stack.back().f;
197 e.call_stack.pop_back();
198 }
199 }
200 else if(e.pc->is_function_call())
201 {
202 const exprt &function = e.pc->call_function();
203 if(function.id()==ID_symbol)
204 {
205 irep_idt identifier=to_symbol_expr(function).get_identifier();
206
207 if(sequence[e.index]==identifier)
208 {
209 e.index++; // yes, we have seen it
210
211 goto_functionst::function_mapt::const_iterator f_call_it=
212 goto_functions.function_map.find(identifier);
213
214 if(f_call_it==goto_functions.function_map.end())
215 e.pc++;
216 else
217 {
218 e.pc++;
219 e.call_stack.push_back(call_stack_entryt());
220 e.call_stack.back().return_address=e.pc;
221 e.call_stack.back().f=e.f;
222 e.pc=f_call_it->second.body.instructions.begin();
223 e.f=f_call_it;
224 }
225 }
226 else
227 queue.pop();
228 }
229 }
230 else if(e.pc->is_goto())
231 {
232 goto_programt::const_targett t=e.pc->get_target();
233
234 if(e.pc->condition().is_true())
235 e.pc=t;
236 else
237 {
238 e.pc++;
239 queue.push(e); // deque doesn't invalidate references
240 queue.top().pc=t;
241 }
242 }
243 else
244 {
245 e.pc++;
246 }
247 }
248
249 std::cout << "sequence not feasible\n";
250}
251
252void check_call_sequence(const goto_modelt &goto_model)
253{
254 // read the sequence from stdin
255
256 std::vector<irep_idt> sequence;
257
258 std::string line;
259 while(std::getline(std::cin, line))
260 {
261 if(!line.empty() && line[line.size() - 1] == '\r')
262 line.resize(line.size()-1);
263
264 if(!line.empty())
265 sequence.push_back(line);
266 }
267
268 check_call_sequencet(goto_model, sequence)();
269}
270
272 const namespacet &ns,
273 const goto_programt &goto_program)
274{
275 for(const auto &instruction : goto_program.instructions)
276 {
277 if(!instruction.is_function_call())
278 continue;
279
280 const exprt &f = instruction.call_function();
281
282 if(f.id()!=ID_symbol)
283 continue;
284
285 const irep_idt &identifier=to_symbol_expr(f).get_identifier();
286 if(identifier == INITIALIZE_FUNCTION)
287 continue;
288
289 std::string name=from_expr(ns, identifier, f);
290 std::string::size_type java_type_suffix=name.find(":(");
291 if(java_type_suffix!=std::string::npos)
292 name.erase(java_type_suffix);
293
294 std::cout << "found call to " << name;
295
296 if(!instruction.call_arguments().empty())
297 {
298 std::cout << " with arguments ";
299 for(exprt::operandst::const_iterator it =
300 instruction.call_arguments().begin();
301 it != instruction.call_arguments().end();
302 ++it)
303 {
304 if(it != instruction.call_arguments().begin())
305 std::cout << ", ";
306 std::cout << from_expr(ns, identifier, simplify_expr(*it, ns));
307 }
308 }
309
310 std::cout << '\n';
311 }
312}
313
315{
316 // do per function
317
318 const namespacet ns(goto_model.symbol_table);
319
320 for(const auto &gf_entry : goto_model.goto_functions.function_map)
321 list_calls_and_arguments(ns, gf_entry.second.body);
322}
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
void check_call_sequence(const goto_modelt &goto_model)
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Memory-mapped I/O Instrumentation for Goto Programs.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
check_call_sequencet(const goto_modelt &_goto_model, const std::vector< irep_idt > &_sequence)
std::unordered_set< statet, state_hash > statest
const std::vector< irep_idt > & sequence
const goto_functionst & goto_functions
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
size_t hash_string(const dstringt &s)
Definition dstring.h:228
Symbol Table + CFG.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
exprt simplify_expr(exprt src, const namespacet &ns)
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
goto_functionst::function_mapt::const_iterator f
goto_programt::const_targett return_address
bool operator==(const call_stack_entryt &other) const
std::size_t operator()(const statet &s) const
goto_functionst::function_mapt::const_iterator f
goto_programt::const_targett pc
bool operator==(const statet &other) const
std::vector< call_stack_entryt > call_stack