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 &,
22  const unsigned,
23  unsigned)
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 
76  parameter_type, state.source.pc->source_location);
77  }
78  else
79  rhs=*it1;
80 
81  if(rhs.is_nil())
82  {
83  // 'nil' argument doesn't get assigned
84  }
85  else
86  {
87  // It should be the same exact type.
88  if(!base_type_eq(parameter_type, rhs.type(), ns))
89  {
90  const typet &f_parameter_type=ns.follow(parameter_type);
91  const typet &f_rhs_type=ns.follow(rhs.type());
92 
93  // But we are willing to do some limited conversion.
94  // This is highly dubious, obviously.
95  if((f_parameter_type.id()==ID_signedbv ||
96  f_parameter_type.id()==ID_unsignedbv ||
97  f_parameter_type.id()==ID_c_enum_tag ||
98  f_parameter_type.id()==ID_bool ||
99  f_parameter_type.id()==ID_pointer ||
100  f_parameter_type.id()==ID_union) &&
101  (f_rhs_type.id()==ID_signedbv ||
102  f_rhs_type.id()==ID_unsignedbv ||
103  f_rhs_type.id()==ID_c_bit_field ||
104  f_rhs_type.id()==ID_c_enum_tag ||
105  f_rhs_type.id()==ID_bool ||
106  f_rhs_type.id()==ID_pointer ||
107  f_rhs_type.id()==ID_union))
108  {
109  rhs=
111  byte_extract_id(),
112  rhs,
113  from_integer(0, index_type()),
114  parameter_type);
115  }
116  else
117  {
118  std::ostringstream error;
119  error << "function call: parameter \"" << identifier
120  << "\" type mismatch: got " << rhs.type().pretty()
121  << ", expected " << parameter_type.pretty();
122  throw error.str();
123  }
124  }
125 
126  symex_assign(state, code_assignt(lhs, rhs));
127  }
128 
129  if(it1!=arguments.end())
130  it1++;
131  }
132 
133  if(function_type.has_ellipsis())
134  {
135  // These are va_arg arguments; their types may differ from call to call
136  std::size_t va_count=0;
137  const symbolt *va_sym=nullptr;
138  while(!ns.lookup(
139  id2string(function_identifier)+"::va_arg"+std::to_string(va_count),
140  va_sym))
141  ++va_count;
142 
143  for( ; it1!=arguments.end(); it1++, va_count++)
144  {
145  irep_idt id=
146  id2string(function_identifier)+"::va_arg"+std::to_string(va_count);
147 
148  // add to symbol table
149  symbolt symbol;
150  symbol.name=id;
151  symbol.base_name="va_arg"+std::to_string(va_count);
152  symbol.mode=ID_C;
153  symbol.type=it1->type();
154 
155  state.symbol_table.insert(std::move(symbol));
156 
157  symbol_exprt lhs=symbol_exprt(id, it1->type());
158 
159  symex_assign(state, code_assignt(lhs, *it1));
160  }
161  }
162  else if(it1!=arguments.end())
163  {
164  // we got too many arguments, but we will just ignore them
165  }
166 }
167 
169  const get_goto_functiont &get_goto_function,
170  statet &state,
171  const code_function_callt &code)
172 {
173  const exprt &function=code.function();
174 
175  if(function.id()==ID_symbol)
176  symex_function_call_symbol(get_goto_function, state, code);
177  else if(function.id()==ID_if)
178  throw "symex_function_call can't do if";
179  else if(function.id()==ID_dereference)
180  throw "symex_function_call can't do dereference";
181  else
182  throw "unexpected function for symex_function_call: "+function.id_string();
183 }
184 
186  const get_goto_functiont &get_goto_function,
187  statet &state,
188  const code_function_callt &code)
189 {
190  target.location(state.guard.as_expr(), state.source);
191 
192  PRECONDITION(code.function().id() == ID_symbol);
193 
194  const irep_idt &identifier=
195  to_symbol_expr(code.function()).get_identifier();
196 
197  if(identifier=="CBMC_trace")
198  {
199  symex_trace(state, code);
200  }
201  else if(has_prefix(id2string(identifier), CPROVER_FKT_PREFIX))
202  {
203  symex_fkt(state, code);
204  }
205  else if(has_prefix(id2string(identifier), CPROVER_MACRO_PREFIX))
206  {
207  symex_macro(state, code);
208  }
209  else
210  symex_function_call_code(get_goto_function, state, code);
211 }
212 
215  const get_goto_functiont &get_goto_function,
216  statet &state,
217  const code_function_callt &call)
218 {
219  const irep_idt &identifier=
220  to_symbol_expr(call.function()).get_identifier();
221 
222  const goto_functionst::goto_functiont &goto_function =
223  get_goto_function(identifier);
224 
225  state.dirty.populate_dirty_for_function(identifier, goto_function);
226 
227  auto emplace_safe_pointers_result =
228  safe_pointers.emplace(identifier, local_safe_pointerst{ns});
229  if(emplace_safe_pointers_result.second)
230  emplace_safe_pointers_result.first->second(goto_function.body);
231 
232  const bool stop_recursing=get_unwind_recursion(
233  identifier,
234  state.source.thread_nr,
235  state.top().loop_iterations[identifier].count);
236 
237  // see if it's too much
238  if(stop_recursing)
239  {
240  if(options.get_bool_option("partial-loops"))
241  {
242  // it's ok, ignore
243  }
244  else
245  {
246  if(options.get_bool_option("unwinding-assertions"))
247  vcc(false_exprt(), "recursion unwinding assertion", state);
248 
249  // add to state guard to prevent further assignments
250  state.guard.add(false_exprt());
251  }
252 
253  symex_transition(state);
254  return;
255  }
256 
257  // record the call
258  target.function_call(state.guard.as_expr(), identifier, state.source);
259 
260  if(!goto_function.body_available())
261  {
262  no_body(identifier);
263 
264  // record the return
265  target.function_return(state.guard.as_expr(), identifier, state.source);
266 
267  if(call.lhs().is_not_nil())
268  {
269  const auto rhs =
271  code_assignt code(call.lhs(), rhs);
272  symex_assign(state, code);
273  }
274 
275  symex_transition(state);
276  return;
277  }
278 
279  // read the arguments -- before the locality renaming
280  exprt::operandst arguments=call.arguments();
281  for(auto &a : arguments)
282  state.rename(a, ns);
283 
284  // produce a new frame
285  PRECONDITION(!state.call_stack().empty());
286  goto_symex_statet::framet &frame=state.new_frame();
287 
288  // preserve locality of local variables
289  locality(identifier, state, goto_function);
290 
291  // assign actuals to formal parameters
292  parameter_assignments(identifier, goto_function, state, arguments);
293 
294  frame.end_of_function=--goto_function.body.instructions.end();
295  frame.return_value=call.lhs();
296  frame.calling_location=state.source;
297  frame.function_identifier=identifier;
298  frame.hidden_function=goto_function.is_hidden();
299 
300  const goto_symex_statet::framet &p_frame=state.previous_frame();
301  for(goto_symex_statet::framet::loop_iterationst::const_iterator
302  it=p_frame.loop_iterations.begin();
303  it!=p_frame.loop_iterations.end();
304  ++it)
305  if(it->second.is_recursion)
306  frame.loop_iterations.insert(*it);
307 
308  // increase unwinding counter
309  frame.loop_iterations[identifier].is_recursion=true;
310  frame.loop_iterations[identifier].count++;
311 
312  state.source.is_set=true;
313  symex_transition(state, goto_function.body.instructions.begin());
314 }
315 
318 {
319  PRECONDITION(!state.call_stack().empty());
320 
321  {
322  statet::framet &frame=state.top();
323 
324  // restore program counter
325  symex_transition(state, frame.calling_location.pc);
326 
327  // restore L1 renaming
328  state.level1.restore_from(frame.old_level1);
329 
330  // clear function-locals from L2 renaming
331  for(goto_symex_statet::renaming_levelt::current_namest::iterator
332  c_it=state.level2.current_names.begin();
333  c_it!=state.level2.current_names.end();
334  ) // no ++c_it
335  {
336  const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
337  // could use iteration over local_objects as l1_o_id is prefix
338  if(
339  frame.local_objects.find(l1_o_id) == frame.local_objects.end() ||
340  (state.threads.size() > 1 &&
341  state.dirty(c_it->second.first.get_object_name())))
342  {
343  ++c_it;
344  continue;
345  }
346  goto_symex_statet::renaming_levelt::current_namest::iterator
347  cur=c_it;
348  ++c_it;
349  state.level2.current_names.erase(cur);
350  }
351  }
352 
353  state.pop_frame();
354 }
355 
358 {
359  // first record the return
361  state.guard.as_expr(), state.source.pc->function, state.source);
362 
363  // then get rid of the frame
364  pop_frame(state);
365 }
366 
370  const irep_idt function_identifier,
371  statet &state,
372  const goto_functionst::goto_functiont &goto_function)
373 {
374  unsigned &frame_nr=
375  state.threads[state.source.thread_nr].function_frame[function_identifier];
376  frame_nr++;
377 
378  std::set<irep_idt> local_identifiers;
379 
380  get_local_identifiers(goto_function, local_identifiers);
381 
382  statet::framet &frame=state.top();
383 
384  for(std::set<irep_idt>::const_iterator
385  it=local_identifiers.begin();
386  it!=local_identifiers.end();
387  it++)
388  {
389  // get L0 name
390  ssa_exprt ssa(ns.lookup(*it).symbol_expr());
391  state.rename(ssa, ns, goto_symex_statet::L0);
392  const irep_idt l0_name=ssa.get_identifier();
393 
394  // save old L1 name for popping the frame
395  statet::level1t::current_namest::const_iterator c_it=
396  state.level1.current_names.find(l0_name);
397 
398  if(c_it!=state.level1.current_names.end())
399  frame.old_level1[l0_name]=c_it->second;
400 
401  // do L1 renaming -- these need not be unique, as
402  // identifiers may be shared among functions
403  // (e.g., due to inlining or other code restructuring)
404 
405  state.level1.current_names[l0_name]=
406  std::make_pair(ssa, frame_nr);
407  state.rename(ssa, ns, goto_symex_statet::L1);
408 
409  irep_idt l1_name=ssa.get_identifier();
410  unsigned offset=0;
411 
412  while(state.l1_history.find(l1_name)!=state.l1_history.end())
413  {
414  state.level1.increase_counter(l0_name);
415  ++offset;
416  ssa.set_level_1(frame_nr+offset);
417  l1_name=ssa.get_identifier();
418  }
419 
420  // now unique -- store
421  frame.local_objects.insert(l1_name);
422  state.l1_history.insert(l1_name);
423  }
424 }
425 
427 {
428  statet::framet &frame=state.top();
429 
430  const goto_programt::instructiont &instruction=*state.source.pc;
431  PRECONDITION(instruction.is_return());
432  const code_returnt &code=to_code_return(instruction.code);
433 
434  target.location(state.guard.as_expr(), state.source);
435 
436  if(code.operands().size()==1)
437  {
438  exprt value=code.op0();
439 
440  if(frame.return_value.is_not_nil())
441  {
442  code_assignt assignment(frame.return_value, value);
443 
444  if(!base_type_eq(assignment.lhs().type(),
445  assignment.rhs().type(), ns))
446  throw
447  "goto_symext::return_assignment type mismatch at "+
448  instruction.source_location.as_string()+":\n"+
449  "assignment.lhs().type():\n"+assignment.lhs().type().pretty()+"\n"+
450  "assignment.rhs().type():\n"+assignment.rhs().type().pretty();
451 
452  symex_assign(state, assignment);
453  }
454  }
455  else
456  {
457  if(frame.return_value.is_not_nil())
458  throw "return with unexpected value";
459  }
460 }
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:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
virtual void no_body(const irep_idt &)
Definition: goto_symex.h:341
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 &)
irep_idt mode
Language mode.
Definition: symbol.h:52
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:86
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:239
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
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:890
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Definition: goto_symex.h:472
exprt & rhs()
Definition: std_code.h:214
Symbolic Execution.
messaget log
Definition: goto_symex.h:243
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
symex_target_equationt & target
Definition: goto_symex.h:240
irep_idt byte_extract_id()
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:963
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
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:858
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:4497
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:204
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:878
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
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
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:923
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:73
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:136
Assignment.
Definition: std_code.h:196
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