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