cprover
symex_builtin_functions.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 <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/cprover_prefix.h>
18 #include <util/std_types.h>
20 #include <util/symbol_table.h>
21 #include <util/std_expr.h>
22 #include <util/std_code.h>
23 #include <util/simplify_expr.h>
24 #include <util/prefix.h>
25 #include <util/string2int.h>
26 
27 #include <util/c_types.h>
28 
30 
31 #include "goto_symex_state.h"
32 
33 inline static typet c_sizeof_type_rec(const exprt &expr)
34 {
35  const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
36 
37  if(!sizeof_type.is_nil())
38  {
39  return static_cast<const typet &>(sizeof_type);
40  }
41  else if(expr.id()==ID_mult)
42  {
43  forall_operands(it, expr)
44  {
45  typet t=c_sizeof_type_rec(*it);
46  if(t.is_not_nil())
47  return t;
48  }
49  }
50 
51  return nil_typet();
52 }
53 
55  statet &state,
56  const exprt &lhs,
57  const side_effect_exprt &code)
58 {
59  if(code.operands().size()!=1)
60  throw "malloc expected to have one operand";
61 
62  if(lhs.is_nil())
63  return; // ignore
64 
66 
67  exprt size=code.op0();
68  typet object_type=nil_typet();
69 
70  // is the type given?
71  if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)
72  {
73  object_type=code.type().subtype();
74  }
75  else
76  {
77  exprt tmp_size=size;
78  state.rename(tmp_size, ns); // to allow constant propagation
79  simplify(tmp_size, ns);
80 
81  // special treatment for sizeof(T)*x
82  {
83  typet tmp_type=c_sizeof_type_rec(tmp_size);
84 
85  if(tmp_type.is_not_nil())
86  {
87  // Did the size get multiplied?
88  mp_integer elem_size=pointer_offset_size(tmp_type, ns);
89  mp_integer alloc_size;
90 
91  if(elem_size<0)
92  {
93  }
94  else if(to_integer(tmp_size, alloc_size) &&
95  tmp_size.id()==ID_mult &&
96  tmp_size.operands().size()==2 &&
97  (tmp_size.op0().is_constant() ||
98  tmp_size.op1().is_constant()))
99  {
100  exprt s=tmp_size.op0();
101  if(s.is_constant())
102  {
103  s=tmp_size.op1();
104  assert(c_sizeof_type_rec(tmp_size.op0())==tmp_type);
105  }
106  else
107  assert(c_sizeof_type_rec(tmp_size.op1())==tmp_type);
108 
109  object_type=array_typet(tmp_type, s);
110  }
111  else
112  {
113  if(alloc_size==elem_size)
114  object_type=tmp_type;
115  else
116  {
117  mp_integer elements=alloc_size/elem_size;
118 
119  if(elements*elem_size==alloc_size)
120  object_type=array_typet(
121  tmp_type, from_integer(elements, tmp_size.type()));
122  }
123  }
124  }
125  }
126 
127  if(object_type.is_nil())
128  object_type=array_typet(unsigned_char_type(), tmp_size);
129 
130  // we introduce a fresh symbol for the size
131  // to prevent any issues of the size getting ever changed
132 
133  if(object_type.id()==ID_array &&
134  !to_array_type(object_type).size().is_constant())
135  {
136  exprt &size=to_array_type(object_type).size();
137 
138  symbolt size_symbol;
139 
140  size_symbol.base_name=
141  "dynamic_object_size"+std::to_string(dynamic_counter);
142  size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
143  size_symbol.is_lvalue=true;
144  size_symbol.type=tmp_size.type();
145  size_symbol.mode=ID_C;
146 
147  new_symbol_table.add(size_symbol);
148 
149  code_assignt assignment(size_symbol.symbol_expr(), size);
150  size=assignment.lhs();
151 
152  symex_assign_rec(state, assignment);
153  }
154  }
155 
156  // value
157  symbolt value_symbol;
158 
159  value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
160  value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
161  value_symbol.is_lvalue=true;
162  value_symbol.type=object_type;
163  value_symbol.type.set("#dynamic", true);
164  value_symbol.mode=ID_C;
165 
166  new_symbol_table.add(value_symbol);
167 
168  address_of_exprt rhs;
169 
170  if(object_type.id()==ID_array)
171  {
172  rhs.type()=pointer_type(value_symbol.type.subtype());
173  index_exprt index_expr(value_symbol.type.subtype());
174  index_expr.array()=value_symbol.symbol_expr();
175  index_expr.index()=from_integer(0, index_type());
176  rhs.op0()=index_expr;
177  }
178  else
179  {
180  rhs.op0()=value_symbol.symbol_expr();
181  rhs.type()=pointer_type(value_symbol.type);
182  }
183 
184  if(rhs.type()!=lhs.type())
185  rhs.make_typecast(lhs.type());
186 
187  symex_assign_rec(state, code_assignt(lhs, rhs));
188 }
189 
191 {
192  if(src.id()==ID_typecast)
193  return get_symbol(to_typecast_expr(src).op());
194  else if(src.id()==ID_address_of)
195  {
196  exprt op=to_address_of_expr(src).object();
197  if(op.id()==ID_symbol &&
198  op.get_bool(ID_C_SSA_symbol))
199  return to_ssa_expr(op).get_object_name();
200  else
201  return irep_idt();
202  }
203  else
204  return irep_idt();
205 }
206 
208  statet &state,
209  const exprt &lhs,
210  const side_effect_exprt &code)
211 {
212  if(code.operands().size()!=1)
213  throw "va_arg_next expected to have one operand";
214 
215  if(lhs.is_nil())
216  return; // ignore
217 
218  exprt tmp=code.op0();
219  state.rename(tmp, ns); // to allow constant propagation
220  do_simplify(tmp);
221  irep_idt id=get_symbol(tmp);
222 
223  exprt rhs=zero_initializer(lhs.type(), code.source_location(), ns);
224 
225  if(!id.empty())
226  {
227  // strip last name off id to get function name
228  std::size_t pos=id2string(id).rfind("::");
229  if(pos!=std::string::npos)
230  {
231  irep_idt function_identifier=std::string(id2string(id), 0, pos);
232  std::string base=id2string(function_identifier)+"::va_arg";
233 
234  if(has_prefix(id2string(id), base))
235  id=base+std::to_string(
237  std::string(id2string(id), base.size(), std::string::npos))+1);
238  else
239  id=base+"0";
240 
241  const symbolt *symbol;
242  if(!ns.lookup(id, symbol))
243  {
244  exprt symbol_expr=symbol_exprt(symbol->name, symbol->type);
245  rhs=address_of_exprt(symbol_expr);
246  rhs.make_typecast(lhs.type());
247  }
248  }
249  }
250 
251  symex_assign_rec(state, code_assignt(lhs, rhs));
252 }
253 
255 {
256  if(src.id()==ID_typecast)
257  {
258  assert(src.operands().size()==1);
259  return get_string_argument_rec(src.op0());
260  }
261  else if(src.id()==ID_address_of)
262  {
263  assert(src.operands().size()==1);
264  if(src.op0().id()==ID_index)
265  {
266  assert(src.op0().operands().size()==2);
267 
268  if(src.op0().op0().id()==ID_string_constant &&
269  src.op0().op1().is_zero())
270  {
271  const exprt &fmt_str=src.op0().op0();
272  return fmt_str.get_string(ID_value);
273  }
274  }
275  }
276 
277  return "";
278 }
279 
281 {
282  exprt tmp=src;
283  simplify(tmp, ns);
284  return get_string_argument_rec(tmp);
285 }
286 
288  statet &state,
289  const exprt &lhs,
290  const exprt &rhs)
291 {
292  if(rhs.operands().empty())
293  throw "printf expected to have at least one operand";
294 
295  exprt tmp_rhs=rhs;
296  state.rename(tmp_rhs, ns);
297  do_simplify(tmp_rhs);
298 
299  const exprt::operandst &operands=tmp_rhs.operands();
300  std::list<exprt> args;
301 
302  for(unsigned i=1; i<operands.size(); i++)
303  args.push_back(operands[i]);
304 
305  const irep_idt format_string=
306  get_string_argument(operands[0], ns);
307 
308  if(format_string!="")
310  state.guard.as_expr(),
311  state.source, "printf", format_string, args);
312 }
313 
315  statet &state,
316  const codet &code)
317 {
318  if(code.operands().size()<2)
319  throw "input expected to have at least two operands";
320 
321  exprt id_arg=code.op0();
322 
323  state.rename(id_arg, ns);
324 
325  std::list<exprt> args;
326 
327  for(unsigned i=1; i<code.operands().size(); i++)
328  {
329  args.push_back(code.operands()[i]);
330  state.rename(args.back(), ns);
331  do_simplify(args.back());
332  }
333 
334  const irep_idt input_id=get_string_argument(id_arg, ns);
335 
336  target.input(state.guard.as_expr(), state.source, input_id, args);
337 }
338 
340  statet &state,
341  const codet &code)
342 {
343  if(code.operands().size()<2)
344  throw "output expected to have at least two operands";
345 
346  exprt id_arg=code.op0();
347 
348  state.rename(id_arg, ns);
349 
350  std::list<exprt> args;
351 
352  for(unsigned i=1; i<code.operands().size(); i++)
353  {
354  args.push_back(code.operands()[i]);
355  state.rename(args.back(), ns);
356  do_simplify(args.back());
357  }
358 
359  const irep_idt output_id=get_string_argument(id_arg, ns);
360 
361  target.output(state.guard.as_expr(), state.source, output_id, args);
362 }
363 
365  statet &state,
366  const exprt &lhs,
367  const side_effect_exprt &code)
368 {
369  bool do_array;
370 
371  if(code.type().id()!=ID_pointer)
372  throw "new expected to return pointer";
373 
374  do_array=(code.get(ID_statement)==ID_cpp_new_array);
375 
376  dynamic_counter++;
377 
378  const std::string count_string(std::to_string(dynamic_counter));
379 
380  // value
381  symbolt symbol;
382  symbol.base_name=
383  do_array?"dynamic_"+count_string+"_array":
384  "dynamic_"+count_string+"_value";
385  symbol.name="symex_dynamic::"+id2string(symbol.base_name);
386  symbol.is_lvalue=true;
387  symbol.mode=ID_cpp;
388 
389  if(do_array)
390  {
391  symbol.type=array_typet();
392  symbol.type.subtype()=code.type().subtype();
393  exprt size_arg=static_cast<const exprt&>(code.find(ID_size));
394  clean_expr(size_arg, state, false);
395  symbol.type.set(ID_size, size_arg);
396  }
397  else
398  symbol.type=code.type().subtype();
399 
400  // symbol.type.set("#active", symbol_expr(active_symbol));
401  symbol.type.set("#dynamic", true);
402 
403  new_symbol_table.add(symbol);
404 
405  // make symbol expression
406 
407  exprt rhs(ID_address_of, code.type());
408  rhs.type().subtype()=code.type().subtype();
409 
410  if(do_array)
411  {
412  exprt index_expr(ID_index, code.type().subtype());
413  index_expr.copy_to_operands(
414  symbol.symbol_expr(),
415  from_integer(0, index_type()));
416  rhs.move_to_operands(index_expr);
417  }
418  else
419  rhs.copy_to_operands(symbol.symbol_expr());
420 
421  symex_assign_rec(state, code_assignt(lhs, rhs));
422 }
423 
425  statet &state,
426  const codet &code)
427 {
428  // bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
429 }
430 
432  statet &state,
433  const code_function_callt &code)
434 {
435  if(code.arguments().size()<2)
436  // NOLINTNEXTLINE(readability/throw)
437  throw "symex_trace expects at least two arguments";
438 
439  int debug_thresh=unsafe_string2int(options.get_option("debug-level"));
440 
441  mp_integer debug_lvl;
442 
443  if(to_integer(code.arguments()[0], debug_lvl))
444  // NOLINTNEXTLINE(readability/throw)
445  throw "CBMC_trace expects constant as first argument";
446 
447  if(code.arguments()[1].id()!="implicit_address_of" ||
448  code.arguments()[1].operands().size()!=1 ||
449  code.arguments()[1].op0().id()!=ID_string_constant)
450  // NOLINTNEXTLINE(readability/throw)
451  throw "CBMC_trace expects string constant as second argument";
452 
453  if(mp_integer(debug_thresh)>=debug_lvl)
454  {
455  std::list<exprt> vars;
456 
457  irep_idt event=code.arguments()[1].op0().get(ID_value);
458 
459  for(unsigned j=2; j<code.arguments().size(); j++)
460  {
461  exprt var(code.arguments()[j]);
462  state.rename(var, ns);
463  vars.push_back(var);
464  }
465 
466  target.output(state.guard.as_expr(), state.source, event, vars);
467  }
468 }
469 
471  statet &state,
472  const code_function_callt &code)
473 {
474  #if 0
475  exprt new_fc(ID_function, fc.type());
476 
477  new_fc.reserve_operands(fc.operands().size()-1);
478 
479  bool first=true;
480 
481  Forall_operands(it, fc)
482  if(first)
483  first=false;
484  else
485  new_fc.move_to_operands(*it);
486 
487  new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
488 
489  fc.swap(new_fc);
490  #endif
491 }
492 
494  statet &state,
495  const code_function_callt &code)
496 {
497  const irep_idt &identifier=code.op0().get(ID_identifier);
498 
499  if(identifier==CPROVER_MACRO_PREFIX "waitfor")
500  {
501  #if 0
502  exprt new_fc("waitfor", fc.type());
503 
504  if(fc.operands().size()!=4)
505  throw "waitfor expected to have four operands";
506 
507  exprt &cycle_var=fc.op1();
508  exprt &bound=fc.op2();
509  exprt &predicate=fc.op3();
510 
511  if(cycle_var.id()!=ID_symbol)
512  throw "waitfor expects symbol as first operand but got "+
513  cycle_var.id();
514 
515  exprt new_cycle_var(cycle_var);
516  new_cycle_var.id("waitfor_symbol");
517  new_cycle_var.copy_to_operands(bound);
518 
519  replace_expr(cycle_var, new_cycle_var, predicate);
520 
521  new_fc.operands().resize(4);
522  new_fc.op0().swap(cycle_var);
523  new_fc.op1().swap(new_cycle_var);
524  new_fc.op2().swap(bound);
525  new_fc.op3().swap(predicate);
526 
527  fc.swap(new_fc);
528  #endif
529  }
530  else
531  throw "unknown macro: "+id2string(identifier);
532 }
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:19
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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
BigInt mp_integer
Definition: mp_arith.h:19
Linking: Zero Initialization.
symex_targett & target
Definition: goto_symex.h:105
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
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
irep_idt get_string_argument_rec(const exprt &src)
exprt & object()
Definition: std_expr.h:2608
exprt & op0()
Definition: expr.h:84
irep_idt mode
Language mode.
Definition: symbol.h:55
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
virtual void symex_gcc_builtin_va_arg_next(statet &state, const exprt &lhs, const side_effect_exprt &code)
virtual void symex_trace(statet &state, const code_function_callt &code)
literalt pos(literalt a)
Definition: literal.h:193
Symbolic Execution.
optionst options
Definition: goto_symex.h:96
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
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
exprt & op()
Definition: std_expr.h:1739
virtual void symex_macro(statet &state, const code_function_callt &code)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs)
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
argumentst & arguments()
Definition: std_code.h:689
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
static unsigned dynamic_counter
Definition: goto_symex.h:334
Symbolic Execution.
const std::string get_option(const std::string &option) const
Definition: options.cpp:60
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void symex_input(statet &state, const codet &code)
const exprt & size() const
Definition: std_types.h:915
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
irep_idt get_string_argument(const exprt &src, const namespacet &ns)
irep_idt get_symbol(const exprt &src)
bitvector_typet index_type()
Definition: c_types.cpp:15
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void clean_expr(exprt &expr, statet &state, bool write)
Symbol table.
Operator to return the address of an object.
Definition: std_expr.h:2593
static typet c_sizeof_type_rec(const exprt &expr)
virtual void symex_fkt(statet &state, const code_function_callt &code)
bool is_constant() const
Definition: expr.cpp:128
void symex_assign_rec(statet &state, const code_assignt &code)
std::vector< exprt > operandst
Definition: expr.h:49
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
Pointer Logic.
symbol_tablet & new_symbol_table
Definition: goto_symex.h:97
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:51
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)=0
virtual void symex_malloc(statet &state, const exprt &lhs, const side_effect_exprt &code)
Base class for all expressions.
Definition: expr.h:46
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)=0
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const source_locationt & source_location() const
Definition: expr.h:142
The NIL type.
Definition: std_types.h:43
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:236
arrays with given size
Definition: std_types.h:901
virtual void symex_cpp_delete(statet &state, const codet &code)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
dstringt irep_idt
Definition: irep.h:32
A statement in a programming language.
Definition: std_code.h:19
#define CPROVER_MACRO_PREFIX
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:134
const typet & subtype() const
Definition: type.h:31
virtual void symex_output(statet &state, const codet &code)
An expression containing a side effect.
Definition: std_code.h:997
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const namespacet & ns
Definition: goto_symex.h:104
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
exprt & array()
Definition: std_expr.h:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
bool simplify(exprt &expr, const namespacet &ns)
bool is_lvalue
Definition: symbol.h:71
array index operator
Definition: std_expr.h:1170
symex_targett::sourcet source
exprt & op3()
Definition: expr.h:93