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 
19 #include <util/simplify_expr.h>
20 
22 
23 #include <langapi/language_util.h>
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> 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=to_code_function_call(t->code).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 
67 void 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  forall_goto_functions(f_it, goto_model.goto_functions)
73  show_call_sequences(f_it->first, f_it->second.body);
74 }
75 
77 {
78 public:
80  const goto_modelt &_goto_model,
81  const std::vector<irep_idt> &_sequence):
82  goto_functions(_goto_model.goto_functions),
83  sequence(_sequence)
84  {
85  }
86 
87  void operator()();
88 
89 protected:
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)
124  struct state_hash
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=to_code_function_call(e.pc->code).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->get_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 
252 void 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  forall_goto_program_instructions(i_it, goto_program)
276  {
277  if(!i_it->is_function_call())
278  continue;
279 
280  const code_function_callt &call = to_code_function_call(i_it->code);
281 
282  const exprt &f=call.function();
283 
284  if(f.id()!=ID_symbol)
285  continue;
286 
287  const irep_idt &identifier=to_symbol_expr(f).get_identifier();
288  if(identifier == INITIALIZE_FUNCTION)
289  continue;
290 
291  std::string name=from_expr(ns, identifier, f);
292  std::string::size_type java_type_suffix=name.find(":(");
293  if(java_type_suffix!=std::string::npos)
294  name.erase(java_type_suffix);
295 
296  std::cout << "found call to " << name;
297 
298  if(!call.arguments().empty())
299  {
300  std::cout << " with arguments ";
301  for(exprt::operandst::const_iterator
302  it=call.arguments().begin();
303  it!=call.arguments().end();
304  ++it)
305  {
306  if(it!=call.arguments().begin())
307  std::cout << ", ";
308  std::cout << from_expr(ns, identifier, simplify_expr(*it, ns));
309  }
310  }
311 
312  std::cout << '\n';
313  }
314 }
315 
316 void list_calls_and_arguments(const goto_modelt &goto_model)
317 {
318  // do per function
319 
320  const namespacet ns(goto_model.symbol_table);
321 
322  forall_goto_functions(f_it, goto_model.goto_functions)
323  list_calls_and_arguments(ns, f_it->second.body);
324 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
check_call_sequencet::statet
Definition: call_sequences.cpp:107
check_call_sequencet::check_call_sequencet
check_call_sequencet(const goto_modelt &_goto_model, const std::vector< irep_idt > &_sequence)
Definition: call_sequences.cpp:79
check_call_sequencet::statet::f
goto_functionst::function_mapt::const_iterator f
Definition: call_sequences.cpp:108
check_call_sequencet::state_hash::operator()
std::size_t operator()(const statet &s) const
Definition: call_sequences.cpp:126
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
check_call_sequencet::statet::operator==
bool operator==(const statet &other) const
Definition: call_sequences.cpp:113
goto_model.h
Symbol Table + CFG.
check_call_sequencet::call_stack_entryt::f
goto_functionst::function_mapt::const_iterator f
Definition: call_sequences.cpp:95
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
check_call_sequencet::call_stack_entryt::return_address
goto_programt::const_targett return_address
Definition: call_sequences.cpp:96
check_call_sequencet::operator()
void operator()()
Definition: call_sequences.cpp:142
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:1084
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
check_call_sequencet::call_stack_entryt::operator==
bool operator==(const call_stack_entryt &other) const
Definition: call_sequences.cpp:98
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
show_call_sequences
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Definition: call_sequences.cpp:27
check_call_sequencet::call_stack_entryt
Definition: call_sequences.cpp:94
check_call_sequence
void check_call_sequence(const goto_modelt &goto_model)
Definition: call_sequences.cpp:252
language_util.h
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
check_call_sequencet::statet::index
unsigned index
Definition: call_sequences.cpp:111
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
hash_string
size_t hash_string(const dstringt &s)
Definition: dstring.h:211
simplify_expr.h
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
check_call_sequencet::statet::call_stack
std::vector< call_stack_entryt > call_stack
Definition: call_sequences.cpp:110
call_sequences.h
Memory-mapped I/O Instrumentation for Goto Programs.
check_call_sequencet::statet::pc
goto_programt::const_targett pc
Definition: call_sequences.cpp:109
check_call_sequencet::states
statest states
Definition: call_sequences.cpp:139
check_call_sequencet::statest
std::unordered_set< statet, state_hash > statest
Definition: call_sequences.cpp:138
check_call_sequencet
Definition: call_sequences.cpp:77
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
check_call_sequencet::goto_functions
const goto_functionst & goto_functions
Definition: call_sequences.cpp:90
check_call_sequencet::sequence
const std::vector< irep_idt > & sequence
Definition: call_sequences.cpp:91
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
static_lifetime_init.h
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
check_call_sequencet::state_hash
Definition: call_sequences.cpp:125
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
statet
unsigned int statet
Definition: trace_automaton.h:24
list_calls_and_arguments
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
Definition: call_sequences.cpp:271