cprover
call_sequences.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Printing function call sequences for Ofer
4 
5 Author: Daniel Kroening
6 
7 Date: April 2013
8 
9 \*******************************************************************/
10 
13 
14 #include "call_sequences.h"
15 
16 #include <stack>
17 #include <iostream>
18 #include <unordered_set>
19 
20 #include <util/std_expr.h>
21 #include <util/simplify_expr.h>
22 
24  const irep_idt &function,
25  const goto_programt &goto_program,
26  const goto_programt::const_targett start)
27 {
28  std::cout << "# From " << function << '\n';
29 
30  std::stack<goto_programt::const_targett> stack;
31  std::set<goto_programt::const_targett> seen;
32 
33  if(start!=goto_program.instructions.end())
34  stack.push(start);
35 
36  while(!stack.empty())
37  {
38  goto_programt::const_targett t=stack.top();
39  stack.pop();
40 
41  if(!seen.insert(t).second)
42  continue; // seen it already
43 
44  if(t->is_function_call())
45  {
46  const exprt &function2=to_code_function_call(t->code).function();
47  if(function2.id()==ID_symbol)
48  {
49  // print pair function, function2
50  std::cout << function << " -> "
51  << to_symbol_expr(function2).get_identifier() << '\n';
52  }
53  continue; // abort search
54  }
55 
56  // get successors and add to stack
57  for(const auto &it : goto_program.get_successors(t))
58  {
59  stack.push(it);
60  }
61  }
62 }
63 
65  const irep_idt &function,
66  const goto_programt &goto_program)
67 {
68  // this is quadratic
69 
70  std::cout << "# " << function << '\n';
71 
73  function,
74  goto_program,
75  goto_program.instructions.begin());
76 
77  forall_goto_program_instructions(i_it, goto_program)
78  {
79  if(!i_it->is_function_call())
80  continue;
81 
82  const exprt &f1=to_code_function_call(i_it->code).function();
83 
84  if(f1.id()!=ID_symbol)
85  continue;
86 
87  // find any calls reachable from this one
89  next++;
90 
92  to_symbol_expr(f1).get_identifier(),
93  goto_program,
94  next);
95  }
96 
97  std::cout << '\n';
98 }
99 
100 void show_call_sequences(const goto_functionst &goto_functions)
101 {
102  // do per function
103 
104  forall_goto_functions(f_it, goto_functions)
105  show_call_sequences(f_it->first, f_it->second.body);
106 }
107 
109 {
110 public:
112  const goto_functionst &_goto_functions,
113  const std::vector<irep_idt> &_sequence):
114  goto_functions(_goto_functions),
115  sequence(_sequence)
116  {
117  }
118 
119  void operator()();
120 
121 protected:
123  const std::vector<irep_idt> &sequence;
124 
126  {
127  goto_functionst::function_mapt::const_iterator f;
129 
130  bool operator==(const call_stack_entryt &other) const
131  {
132  return
133  f->first==other.f->first &&
134  return_address==other.return_address;
135  }
136  };
137 
138  struct statet
139  {
140  goto_functionst::function_mapt::const_iterator f;
142  std::vector<call_stack_entryt> call_stack;
143  unsigned index;
144 
145  bool operator==(const statet &other) const
146  {
147  return
148  f->first==other.f->first &&
149  pc==other.pc &&
150  call_stack==other.call_stack &&
151  index==other.index;
152  }
153  };
154 
155  // NOLINTNEXTLINE(readability/identifiers)
156  struct state_hash
157  {
158  std::size_t operator()(const statet &s) const
159  {
160  size_t pc_hash=
161  s.pc==s.f->second.body.instructions.end()?0:
162  (size_t)&*s.pc;
163 
164  return hash_string(s.f->first)^
165  pc_hash^
166  s.index^s.call_stack.size();
167  }
168  };
169 
170  typedef std::unordered_set<statet, state_hash> statest;
171  statest states;
172 };
173 
175 {
176  std::stack<statet> queue;
177 
178  if(sequence.empty())
179  {
180  std::cout << "empty sequence given\n";
181  return;
182  }
183 
184  irep_idt entry=sequence.front();
185 
186  goto_functionst::function_mapt::const_iterator f_it=
187  goto_functions.function_map.find(entry);
188 
189  if(f_it!=goto_functions.function_map.end())
190  {
191  queue.push(statet());
192  queue.top().f=f_it;
193  queue.top().pc=f_it->second.body.instructions.begin();
194  queue.top().index=1;
195  }
196 
197  while(!queue.empty())
198  {
199  statet &e=queue.top();
200 
201  // seen already?
202  if(states.find(e)!=states.end())
203  {
204  // drop, continue
205  queue.pop();
206  continue;
207  }
208 
209  // insert
210  states.insert(e);
211 
212  // satisfies sequence?
213  if(e.index==sequence.size())
214  {
215  std::cout << "sequence feasible\n";
216  return;
217  }
218 
219  // new, explore
220  if(e.pc==e.f->second.body.instructions.end())
221  {
222  if(e.call_stack.empty())
223  queue.pop();
224  else
225  {
226  // successor is the return location
227  e.pc=e.call_stack.back().return_address;
228  e.f=e.call_stack.back().f;
229  e.call_stack.pop_back();
230  }
231  }
232  else if(e.pc->is_function_call())
233  {
234  const exprt &function=to_code_function_call(e.pc->code).function();
235  if(function.id()==ID_symbol)
236  {
237  irep_idt identifier=to_symbol_expr(function).get_identifier();
238 
239  if(sequence[e.index]==identifier)
240  {
241  e.index++; // yes, we have seen it
242 
243  goto_functionst::function_mapt::const_iterator f_call_it=
244  goto_functions.function_map.find(identifier);
245 
246  if(f_call_it==goto_functions.function_map.end())
247  e.pc++;
248  else
249  {
250  e.pc++;
251  e.call_stack.push_back(call_stack_entryt());
252  e.call_stack.back().return_address=e.pc;
253  e.call_stack.back().f=e.f;
254  e.pc=f_call_it->second.body.instructions.begin();
255  e.f=f_call_it;
256  }
257  }
258  else
259  queue.pop();
260  }
261  }
262  else if(e.pc->is_goto())
263  {
264  goto_programt::const_targett t=e.pc->get_target();
265 
266  if(e.pc->guard.is_true())
267  e.pc=t;
268  else
269  {
270  e.pc++;
271  queue.push(e); // deque doesn't invalidate references
272  queue.top().pc=t;
273  }
274  }
275  else
276  {
277  e.pc++;
278  }
279  }
280 
281  std::cout << "sequence not feasible\n";
282 }
283 
285 {
286  // read the sequence from stdin
287 
288  std::vector<irep_idt> sequence;
289 
290  std::string line;
291  while(std::getline(std::cin, line))
292  {
293  if(line!="" && line[line.size()-1]=='\r')
294  line.resize(line.size()-1);
295 
296  if(line!="")
297  sequence.push_back(line);
298  }
299 
300  check_call_sequencet(goto_functions, sequence)();
301 }
302 
304  const namespacet &ns,
305  const irep_idt &function,
306  const goto_programt &goto_program)
307 {
308  forall_goto_program_instructions(i_it, goto_program)
309  {
310  if(!i_it->is_function_call())
311  continue;
312 
313  const code_function_callt call=to_code_function_call(i_it->code);
314 
315  const exprt &f=call.function();
316 
317  if(f.id()!=ID_symbol)
318  continue;
319 
320  const irep_idt &identifier=to_symbol_expr(f).get_identifier();
321  if(identifier=="__CPROVER_initialize")
322  continue;
323 
324  std::string name=from_expr(ns, identifier, f);
325  std::string::size_type java_type_suffix=name.find(":(");
326  if(java_type_suffix!=std::string::npos)
327  name.erase(java_type_suffix);
328 
329  std::cout << "found call to " << name;
330 
331  if(!call.arguments().empty())
332  {
333  std::cout << " with arguments ";
334  for(exprt::operandst::const_iterator
335  it=call.arguments().begin();
336  it!=call.arguments().end();
337  ++it)
338  {
339  if(it!=call.arguments().begin())
340  std::cout << ", ";
341  std::cout << from_expr(ns, identifier, simplify_expr(*it, ns));
342  }
343  }
344 
345  std::cout << '\n';
346  }
347 }
348 
350  const namespacet &ns,
352 {
353  // do per function
354 
355  forall_goto_functions(f_it, goto_functions)
356  list_calls_and_arguments(ns, f_it->first, f_it->second.body);
357 }
exprt simplify_expr(const exprt &src, const namespacet &ns)
check_call_sequencet(const goto_functionst &_goto_functions, const std::vector< irep_idt > &_sequence)
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
Definition: std_expr.h:120
const goto_functionst & goto_functions
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void check_call_sequence(const goto_functionst &goto_functions)
unsignedbv_typet size_type()
Definition: c_types.cpp:57
Memory-mapped I/O Instrumentation for Goto Programs.
const std::vector< irep_idt > & sequence
std::list< Target > get_successors(Target target) const
bool operator==(const statet &other) const
goto_programt::const_targett return_address
const irep_idt & id() const
Definition: irep.h:189
instructionst::const_iterator const_targett
argumentst & arguments()
Definition: std_code.h:689
goto_programt::const_targett pc
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool operator==(const call_stack_entryt &other) const
std::size_t operator()(const statet &s) const
std::unordered_set< statet, state_hash > statest
A function call.
Definition: std_code.h:657
goto_functionst::function_mapt::const_iterator f
void show_call_sequences(const irep_idt &function, const goto_programt &goto_program, const goto_programt::const_targett start)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
static void list_calls_and_arguments(const namespacet &ns, const irep_idt &function, const goto_programt &goto_program)
size_t hash_string(const dstringt &s)
Definition: dstring.h:168
goto_functionst::function_mapt::const_iterator f
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
std::vector< call_stack_entryt > call_stack
#define forall_goto_functions(it, functions)
#define stack(x)
Definition: parser.h:144
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
unsigned int statet
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700