cprover
symex_function_call.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <iostream>
15 #include <sstream>
16 #include <cassert>
17 
18 #include <util/cprover_prefix.h>
19 #include <util/prefix.h>
20 #include <util/arith_tools.h>
21 #include <util/base_type.h>
22 #include <util/std_expr.h>
23 #include <util/symbol_table.h>
24 
25 #include <util/c_types.h>
26 
27 #include <analyses/dirty.h>
28 
30  const irep_idt &identifier,
31  const unsigned thread_nr,
32  unsigned unwind)
33 {
34  return false;
35 }
36 
38  const irep_idt function_identifier,
39  const goto_functionst::goto_functiont &goto_function,
40  statet &state,
41  const exprt::operandst &arguments)
42 {
43  const code_typet &function_type=goto_function.type;
44 
45  // iterates over the arguments
46  exprt::operandst::const_iterator it1=arguments.begin();
47 
48  // these are the types of the parameters
49  const code_typet::parameterst &parameter_types=
50  function_type.parameters();
51 
52  // iterates over the types of the parameters
53  for(code_typet::parameterst::const_iterator
54  it2=parameter_types.begin();
55  it2!=parameter_types.end();
56  it2++)
57  {
58  const code_typet::parametert &parameter=*it2;
59 
60  // this is the type that the n-th argument should have
61  const typet &parameter_type=parameter.type();
62 
63  const irep_idt &identifier=parameter.get_identifier();
64 
65  if(identifier.empty())
66  throw "no identifier for function parameter";
67 
68  const symbolt &symbol=ns.lookup(identifier);
69  symbol_exprt lhs=symbol.symbol_expr();
70 
71  exprt rhs;
72 
73  // if you run out of actual arguments there was a mismatch
74  if(it1==arguments.end())
75  {
76  std::string warn=
77  "call to `"+id2string(function_identifier)+"': "
78  "not enough arguments, inserting non-deterministic value\n";
79  std::cerr << state.source.pc->source_location.as_string()+": "+warn;
80 
81  rhs=side_effect_expr_nondett(parameter_type);
82  }
83  else
84  rhs=*it1;
85 
86  if(rhs.is_nil())
87  {
88  // 'nil' argument doesn't get assigned
89  }
90  else
91  {
92  // It should be the same exact type.
93  if(!base_type_eq(parameter_type, rhs.type(), ns))
94  {
95  const typet &f_parameter_type=ns.follow(parameter_type);
96  const typet &f_rhs_type=ns.follow(rhs.type());
97 
98  // But we are willing to do some limited conversion.
99  // This is highly dubious, obviously.
100  if((f_parameter_type.id()==ID_signedbv ||
101  f_parameter_type.id()==ID_unsignedbv ||
102  f_parameter_type.id()==ID_c_enum_tag ||
103  f_parameter_type.id()==ID_bool ||
104  f_parameter_type.id()==ID_pointer ||
105  f_parameter_type.id()==ID_union) &&
106  (f_rhs_type.id()==ID_signedbv ||
107  f_rhs_type.id()==ID_unsignedbv ||
108  f_rhs_type.id()==ID_c_bit_field ||
109  f_rhs_type.id()==ID_c_enum_tag ||
110  f_rhs_type.id()==ID_bool ||
111  f_rhs_type.id()==ID_pointer ||
112  f_rhs_type.id()==ID_union))
113  {
114  rhs=
116  byte_extract_id(),
117  rhs,
118  from_integer(0, index_type()),
119  parameter_type);
120  }
121  else
122  {
123  std::ostringstream error;
124  error << "function call: parameter \"" << identifier
125  << "\" type mismatch: got " << rhs.type().pretty()
126  << ", expected " << parameter_type.pretty();
127  throw error.str();
128  }
129  }
130 
131  symex_assign_rec(state, code_assignt(lhs, rhs));
132  }
133 
134  if(it1!=arguments.end())
135  it1++;
136  }
137 
138  if(function_type.has_ellipsis())
139  {
140  // These are va_arg arguments; their types may differ from call to call
141  unsigned va_count=0;
142  const symbolt *va_sym=nullptr;
143  while(!ns.lookup(
144  id2string(function_identifier)+"::va_arg"+std::to_string(va_count),
145  va_sym))
146  ++va_count;
147 
148  for( ; it1!=arguments.end(); it1++, va_count++)
149  {
150  irep_idt id=
151  id2string(function_identifier)+"::va_arg"+std::to_string(va_count);
152 
153  // add to symbol table
154  symbolt symbol;
155  symbol.name=id;
156  symbol.base_name="va_arg"+std::to_string(va_count);
157  symbol.type=it1->type();
158 
159  new_symbol_table.move(symbol);
160 
161  symbol_exprt lhs=symbol_exprt(id, it1->type());
162 
163  symex_assign_rec(state, code_assignt(lhs, *it1));
164  }
165  }
166  else if(it1!=arguments.end())
167  {
168  // we got too many arguments, but we will just ignore them
169  }
170 }
171 
173  const goto_functionst &goto_functions,
174  statet &state,
175  const code_function_callt &code)
176 {
177  const exprt &function=code.function();
178 
179  if(function.id()==ID_symbol)
180  symex_function_call_symbol(goto_functions, state, code);
181  else if(function.id()==ID_if)
182  throw "symex_function_call can't do if";
183  else if(function.id()==ID_dereference)
184  throw "symex_function_call can't do dereference";
185  else
186  throw "unexpected function for symex_function_call: "+function.id_string();
187 }
188 
190  const goto_functionst &goto_functions,
191  statet &state,
192  const code_function_callt &code)
193 {
194  target.location(state.guard.as_expr(), state.source);
195 
196  assert(code.function().id()==ID_symbol);
197 
198  const irep_idt &identifier=
199  to_symbol_expr(code.function()).get_identifier();
200 
201  if(identifier=="CBMC_trace")
202  {
203  symex_trace(state, code);
204  }
205  else if(has_prefix(id2string(identifier), CPROVER_FKT_PREFIX))
206  {
207  symex_fkt(state, code);
208  }
209  else if(has_prefix(id2string(identifier), CPROVER_MACRO_PREFIX))
210  {
211  symex_macro(state, code);
212  }
213  else
214  symex_function_call_code(goto_functions, state, code);
215 }
216 
219  const goto_functionst &goto_functions,
220  statet &state,
221  const code_function_callt &call)
222 {
223  const irep_idt &identifier=
224  to_symbol_expr(call.function()).get_identifier();
225 
226  // find code in function map
227 
228  goto_functionst::function_mapt::const_iterator it=
229  goto_functions.function_map.find(identifier);
230 
231  if(it==goto_functions.function_map.end())
232  throw "failed to find `"+id2string(identifier)+"' in function_map";
233 
234  const goto_functionst::goto_functiont &goto_function=it->second;
235 
236  const bool stop_recursing=get_unwind_recursion(
237  identifier,
238  state.source.thread_nr,
239  state.top().loop_iterations[identifier].count);
240 
241  // see if it's too much
242  if(stop_recursing)
243  {
244  if(options.get_bool_option("partial-loops"))
245  {
246  // it's ok, ignore
247  }
248  else
249  {
250  if(options.get_bool_option("unwinding-assertions"))
251  vcc(false_exprt(), "recursion unwinding assertion", state);
252 
253  // add to state guard to prevent further assignments
254  state.guard.add(false_exprt());
255  }
256 
257  symex_transition(state);
258  return;
259  }
260 
261  // record the call
262  target.function_call(state.guard.as_expr(), identifier, state.source);
263 
264  if(!goto_function.body_available())
265  {
266  no_body(identifier);
267 
268  // record the return
269  target.function_return(state.guard.as_expr(), identifier, state.source);
270 
271  if(call.lhs().is_not_nil())
272  {
273  side_effect_expr_nondett rhs(call.lhs().type());
275  code_assignt code(call.lhs(), rhs);
276  symex_assign_rec(state, code);
277  }
278 
279  symex_transition(state);
280  return;
281  }
282 
283  // read the arguments -- before the locality renaming
284  exprt::operandst arguments=call.arguments();
285  for(unsigned i=0; i<arguments.size(); i++)
286  state.rename(arguments[i], ns);
287 
288  // produce a new frame
289  assert(!state.call_stack().empty());
290  goto_symex_statet::framet &frame=state.new_frame();
291 
292  // preserve locality of local variables
293  locality(identifier, state, goto_function);
294 
295  // assign actuals to formal parameters
296  parameter_assignments(identifier, goto_function, state, arguments);
297 
298  frame.end_of_function=--goto_function.body.instructions.end();
299  frame.return_value=call.lhs();
300  frame.calling_location=state.source;
301  frame.function_identifier=identifier;
302  frame.hidden_function=goto_function.is_hidden();
303 
304  const goto_symex_statet::framet &p_frame=state.previous_frame();
305  for(goto_symex_statet::framet::loop_iterationst::const_iterator
306  it=p_frame.loop_iterations.begin();
307  it!=p_frame.loop_iterations.end();
308  ++it)
309  if(it->second.is_recursion)
310  frame.loop_iterations.insert(*it);
311 
312  // increase unwinding counter
313  frame.loop_iterations[identifier].is_recursion=true;
314  frame.loop_iterations[identifier].count++;
315 
316  state.source.is_set=true;
317  symex_transition(state, goto_function.body.instructions.begin());
318 }
319 
322 {
323  assert(!state.call_stack().empty());
324 
325  {
326  statet::framet &frame=state.top();
327 
328  // restore program counter
329  symex_transition(state, frame.calling_location.pc);
330 
331  // restore L1 renaming
332  state.level1.restore_from(frame.old_level1);
333 
334  // clear function-locals from L2 renaming
335  assert(state.dirty);
336  for(goto_symex_statet::renaming_levelt::current_namest::iterator
337  c_it=state.level2.current_names.begin();
338  c_it!=state.level2.current_names.end();
339  ) // no ++c_it
340  {
341  const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
342  // could use iteration over local_objects as l1_o_id is prefix
343  if(frame.local_objects.find(l1_o_id)==frame.local_objects.end() ||
344  (state.threads.size()>1 &&
345  (*state.dirty)(c_it->second.first.get_object_name())))
346  {
347  ++c_it;
348  continue;
349  }
350  goto_symex_statet::renaming_levelt::current_namest::iterator
351  cur=c_it;
352  ++c_it;
353  state.level2.current_names.erase(cur);
354  }
355  }
356 
357  state.pop_frame();
358 }
359 
362 {
363  // first record the return
365  state.guard.as_expr(), state.source.pc->function, state.source);
366 
367  // then get rid of the frame
368  pop_frame(state);
369 }
370 
374  const irep_idt function_identifier,
375  statet &state,
376  const goto_functionst::goto_functiont &goto_function)
377 {
378  unsigned &frame_nr=
379  state.threads[state.source.thread_nr].function_frame[function_identifier];
380  frame_nr++;
381 
382  std::set<irep_idt> local_identifiers;
383 
384  get_local_identifiers(goto_function, local_identifiers);
385 
386  statet::framet &frame=state.top();
387 
388  for(std::set<irep_idt>::const_iterator
389  it=local_identifiers.begin();
390  it!=local_identifiers.end();
391  it++)
392  {
393  // get L0 name
394  ssa_exprt ssa(ns.lookup(*it).symbol_expr());
395  state.rename(ssa, ns, goto_symex_statet::L0);
396  const irep_idt l0_name=ssa.get_identifier();
397 
398  // save old L1 name for popping the frame
399  statet::level1t::current_namest::const_iterator c_it=
400  state.level1.current_names.find(l0_name);
401 
402  if(c_it!=state.level1.current_names.end())
403  frame.old_level1[l0_name]=c_it->second;
404 
405  // do L1 renaming -- these need not be unique, as
406  // identifiers may be shared among functions
407  // (e.g., due to inlining or other code restructuring)
408 
409  state.level1.current_names[l0_name]=
410  std::make_pair(ssa, frame_nr);
411  state.rename(ssa, ns, goto_symex_statet::L1);
412 
413  irep_idt l1_name=ssa.get_identifier();
414  unsigned offset=0;
415 
416  while(state.l1_history.find(l1_name)!=state.l1_history.end())
417  {
418  state.level1.increase_counter(l0_name);
419  ++offset;
420  ssa.set_level_1(frame_nr+offset);
421  l1_name=ssa.get_identifier();
422  }
423 
424  // now unique -- store
425  frame.local_objects.insert(l1_name);
426  state.l1_history.insert(l1_name);
427  }
428 }
429 
431 {
432  statet::framet &frame=state.top();
433 
434  const goto_programt::instructiont &instruction=*state.source.pc;
435  assert(instruction.is_return());
436  const code_returnt &code=to_code_return(instruction.code);
437 
438  target.location(state.guard.as_expr(), state.source);
439 
440  if(code.operands().size()==1)
441  {
442  exprt value=code.op0();
443 
444  if(frame.return_value.is_not_nil())
445  {
446  code_assignt assignment(frame.return_value, value);
447 
448  if(!base_type_eq(assignment.lhs().type(),
449  assignment.rhs().type(), ns))
450  throw
451  "goto_symext::return_assignment type mismatch at "+
452  instruction.source_location.as_string()+":\n"+
453  "assignment.lhs().type():\n"+assignment.lhs().type().pretty()+"\n"+
454  "assignment.rhs().type():\n"+assignment.rhs().type().pretty();
455 
456  symex_assign_rec(state, assignment);
457  }
458  }
459  else
460  {
461  if(frame.return_value.is_not_nil())
462  throw "return with unexpected value";
463  }
464 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
exprt as_expr() const
Definition: guard.h:43
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
symex_targett & target
Definition: goto_symex.h:105
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
virtual void location(const exprt &guard, const sourcet &source)=0
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
Variables whose address is taken.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
bool has_ellipsis() const
Definition: std_types.h:803
renaming_levelt::current_namest old_level1
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void symex_function_call_symbol(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
void get_local_identifiers(const goto_function_templatet< goto_programt > &goto_function, std::set< irep_idt > &dest)
virtual void symex_trace(statet &state, const code_function_callt &code)
std::vector< parametert > parameterst
Definition: std_types.h:829
void increase_counter(const irep_idt &identifier)
void parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
optionst options
Definition: goto_symex.h:96
loop_iterationst loop_iterations
void return_assignment(statet &state)
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
virtual void symex_macro(statet &state, const code_function_callt &code)
void locality(const irep_idt function_identifier, statet &state, const goto_functionst::goto_functiont &goto_function)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
void restore_from(const current_namest &other)
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)=0
goto_symex_statet::level2t level2
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
argumentst & arguments()
Definition: std_code.h:689
exprt & rhs()
Definition: std_code.h:162
Symbolic Execution.
virtual void symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)
Definition: symex_main.cpp:23
API to expression classes.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
irep_idt byte_extract_id()
virtual void symex_function_call(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:746
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
goto_symex_statet::level1t level1
A function call.
Definition: std_code.h:657
virtual void symex_end_of_function(statet &state)
do function call by inlining
bitvector_typet index_type()
Definition: c_types.cpp:15
goto_function_templatet< goto_programt > goto_functiont
Symbol table.
const framet & previous_frame()
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
The boolean constant false.
Definition: std_expr.h:3753
virtual void symex_fkt(statet &state, const code_function_callt &code)
void symex_assign_rec(statet &state, const code_assignt &code)
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const dirtyt * dirty
symbol_tablet & new_symbol_table
Definition: goto_symex.h:97
typet type
Type of symbol.
Definition: symbol.h:37
virtual void symex_function_call_code(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
do function call by inlining
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
#define CPROVER_FKT_PREFIX
l1_historyt l1_history
const parameterst & parameters() const
Definition: std_types.h:841
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)=0
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
call_stackt & call_stack()
const source_locationt & source_location() const
Definition: expr.h:142
virtual void vcc(const exprt &expr, const std::string &msg, statet &state)
Definition: symex_main.cpp:53
source_locationt & add_source_location()
Definition: expr.h:147
symex_targett::sourcet calling_location
Expression to hold a symbol (variable)
Definition: std_expr.h:82
#define CPROVER_MACRO_PREFIX
Return from a function.
Definition: std_code.h:714
virtual void no_body(const irep_idt &identifier)
Definition: goto_symex.h:213
Base Type Computation.
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const namespacet & ns
Definition: goto_symex.h:104
const irep_idt & get_identifier() const
Definition: std_types.h:782
bool empty() const
Definition: dstring.h:61
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Assignment.
Definition: std_code.h:144
void pop_frame(statet &state)
pop one call frame
void add(const exprt &expr)
Definition: guard.cpp:64
symex_targett::sourcet source