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 <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/expr_initializer.h>
17 #include <util/expr_util.h>
18 #include <util/fresh_symbol.h>
19 #include <util/invariant_utils.h>
20 #include <util/optional.h>
23 #include <util/prefix.h>
24 #include <util/simplify_expr.h>
25 #include <util/string2int.h>
26 #include <util/string_constant.h>
27 
28 inline static optionalt<typet> c_sizeof_type_rec(const exprt &expr)
29 {
30  const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
31 
32  if(!sizeof_type.is_nil())
33  {
34  return static_cast<const typet &>(sizeof_type);
35  }
36  else if(expr.id()==ID_mult)
37  {
38  forall_operands(it, expr)
39  {
40  const auto t = c_sizeof_type_rec(*it);
41  if(t.has_value())
42  return t;
43  }
44  }
45 
46  return {};
47 }
48 
50  statet &state,
51  const exprt &lhs,
52  const side_effect_exprt &code)
53 {
54  PRECONDITION(code.operands().size() == 2);
55 
56  if(lhs.is_nil())
57  return; // ignore
58 
60 
61  exprt size = to_binary_expr(code).op0();
62  optionalt<typet> object_type;
63  auto function_symbol = outer_symbol_table.lookup(state.source.function_id);
64  INVARIANT(function_symbol, "function associated with allocation not found");
65  const irep_idt &mode = function_symbol->mode;
66 
67  // is the type given?
68  if(
69  code.type().id() == ID_pointer &&
70  to_pointer_type(code.type()).subtype().id() != ID_empty)
71  {
72  object_type = to_pointer_type(code.type()).subtype();
73  }
74  else
75  {
76  // to allow constant propagation
77  exprt tmp_size = state.rename(size, ns).get();
78  simplify(tmp_size, ns);
79 
80  // special treatment for sizeof(T)*x
81  {
82  const auto tmp_type = c_sizeof_type_rec(tmp_size);
83 
84  if(tmp_type.has_value())
85  {
86  // Did the size get multiplied?
87  auto elem_size = pointer_offset_size(*tmp_type, ns);
88  const auto alloc_size = numeric_cast<mp_integer>(tmp_size);
89 
90  if(!elem_size.has_value() || *elem_size==0)
91  {
92  }
93  else if(
94  !alloc_size.has_value() && tmp_size.id() == ID_mult &&
95  tmp_size.operands().size() == 2 &&
96  (to_mult_expr(tmp_size).op0().is_constant() ||
97  to_mult_expr(tmp_size).op1().is_constant()))
98  {
99  exprt s = to_mult_expr(tmp_size).op0();
100  if(s.is_constant())
101  {
102  s = to_mult_expr(tmp_size).op1();
103  PRECONDITION(
104  *c_sizeof_type_rec(to_mult_expr(tmp_size).op0()) == *tmp_type);
105  }
106  else
107  PRECONDITION(
108  *c_sizeof_type_rec(to_mult_expr(tmp_size).op1()) == *tmp_type);
109 
110  object_type = array_typet(*tmp_type, s);
111  }
112  else if(alloc_size.has_value())
113  {
114  if(*alloc_size == *elem_size)
115  object_type = *tmp_type;
116  else
117  {
118  mp_integer elements = *alloc_size / (*elem_size);
119 
120  if(elements * (*elem_size) == *alloc_size)
121  object_type =
122  array_typet(*tmp_type, from_integer(elements, tmp_size.type()));
123  }
124  }
125  }
126  }
127 
128  if(!object_type.has_value())
129  object_type=array_typet(unsigned_char_type(), tmp_size);
130 
131  // we introduce a fresh symbol for the size
132  // to prevent any issues of the size getting ever changed
133 
134  if(
135  object_type->id() == ID_array &&
136  !to_array_type(*object_type).size().is_constant())
137  {
138  exprt &array_size = to_array_type(*object_type).size();
139 
140  auxiliary_symbolt size_symbol;
141 
142  size_symbol.base_name=
143  "dynamic_object_size"+std::to_string(dynamic_counter);
144  size_symbol.name =
146  size_symbol.type=tmp_size.type();
147  size_symbol.mode = mode;
148  size_symbol.type.set(ID_C_constant, true);
149  size_symbol.value = array_size;
150 
151  state.symbol_table.add(size_symbol);
152 
153  code_assignt assignment(size_symbol.symbol_expr(), array_size);
154  array_size = assignment.lhs();
155 
156  symex_assign(state, assignment);
157  }
158  }
159 
160  // value
161  symbolt value_symbol;
162 
163  value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
164  value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name);
165  value_symbol.is_lvalue=true;
166  value_symbol.type = *object_type;
167  value_symbol.type.set(ID_C_dynamic, true);
168  value_symbol.mode = mode;
169 
170  state.symbol_table.add(value_symbol);
171 
172  // to allow constant propagation
173  exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get();
174  simplify(zero_init, ns);
175 
176  INVARIANT(
177  zero_init.is_constant(), "allocate expects constant as second argument");
178 
179  if(!zero_init.is_zero() && !zero_init.is_false())
180  {
181  const auto zero_value =
182  zero_initializer(*object_type, code.source_location(), ns);
183  CHECK_RETURN(zero_value.has_value());
184  code_assignt assignment(value_symbol.symbol_expr(), *zero_value);
185  symex_assign(state, assignment);
186  }
187  else
188  {
189  const code_assignt assignment{
190  value_symbol.symbol_expr(),
191  path_storage.build_symex_nondet(*object_type, code.source_location())};
192  symex_assign(state, assignment);
193  }
194 
195  exprt rhs;
196 
197  if(object_type->id() == ID_array)
198  {
199  const auto &array_type = to_array_type(*object_type);
200  index_exprt index_expr(
201  value_symbol.symbol_expr(), from_integer(0, index_type()));
202  rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
203  }
204  else
205  {
206  rhs=address_of_exprt(
207  value_symbol.symbol_expr(), pointer_type(value_symbol.type));
208  }
209 
210  symex_assign(
211  state,
213 }
214 
219  const irep_idt &parameter,
220  const pointer_typet &lhs_type,
221  const namespacet &ns)
222 {
223  static const pointer_typet void_ptr_type = pointer_type(empty_typet{});
224 
225  symbol_exprt parameter_expr = ns.lookup(parameter).symbol_expr();
226 
227  // Visual Studio has va_list == char* and stores parameters of size no
228  // greater than the size of a pointer as immediate values
229  if(lhs_type.subtype().id() != ID_pointer)
230  {
231  auto parameter_size = size_of_expr(parameter_expr.type(), ns);
232  CHECK_RETURN(parameter_size.has_value());
233 
234  binary_predicate_exprt fits_slot{
235  *parameter_size,
236  ID_le,
237  from_integer(lhs_type.get_width(), parameter_size->type())};
238 
239  return if_exprt{
240  fits_slot,
241  typecast_exprt::conditional_cast(parameter_expr, void_ptr_type),
243  address_of_exprt{parameter_expr}, void_ptr_type)};
244  }
245  else
246  {
248  address_of_exprt{std::move(parameter_expr)}, void_ptr_type);
249  }
250 }
251 
253  statet &state,
254  const exprt &lhs,
255  const side_effect_exprt &code)
256 {
257  PRECONDITION(code.operands().size() == 1);
258 
259  if(lhs.is_nil())
260  return; // ignore
261 
262  // create an array holding pointers to the parameters, starting after the
263  // parameter that the operand points to
264  const exprt &op = skip_typecast(to_unary_expr(code).op());
265  // this must be the address of a symbol
266  const irep_idt start_parameter =
268 
269  exprt::operandst va_arg_operands;
270  bool parameter_id_found = false;
271  for(auto &parameter : state.call_stack().top().parameter_names)
272  {
273  if(!parameter_id_found)
274  {
275  parameter_id_found = parameter == start_parameter;
276  continue;
277  }
278 
279  va_arg_operands.push_back(
280  va_list_entry(parameter, to_pointer_type(lhs.type()), ns));
281  }
282  const std::size_t va_arg_size = va_arg_operands.size();
283  exprt array =
284  array_exprt{std::move(va_arg_operands),
286  from_integer(va_arg_size, size_type())}};
287 
288  symbolt &va_array = get_fresh_aux_symbol(
289  array.type(),
291  "va_args",
292  state.source.pc->source_location,
293  ns.lookup(state.source.function_id).mode,
294  state.symbol_table);
295  va_array.value = array;
296 
297  array = clean_expr(std::move(array), state, false);
298  array = state.rename(std::move(array), ns).get();
299  do_simplify(array);
300  symex_assign(state, code_assignt{va_array.symbol_expr(), std::move(array)});
301 
302  exprt rhs = address_of_exprt{
303  index_exprt{va_array.symbol_expr(), from_integer(0, index_type())}};
304  rhs = state.rename(std::move(rhs), ns).get();
305  symex_assign(
306  state,
308 }
309 
311 {
312  if(src.id()==ID_typecast)
313  {
314  return get_string_argument_rec(to_typecast_expr(src).op());
315  }
316  else if(src.id()==ID_address_of)
317  {
318  const exprt &object = to_address_of_expr(src).object();
319 
320  if(object.id() == ID_index)
321  {
322  const auto &index_expr = to_index_expr(object);
323 
324  if(
325  index_expr.array().id() == ID_string_constant &&
326  index_expr.index().is_zero())
327  {
328  const exprt &fmt_str = index_expr.array();
329  return to_string_constant(fmt_str).get_value();
330  }
331  }
332  else if(object.id() == ID_string_constant)
333  {
334  return to_string_constant(object).get_value();
335  }
336  }
337 
338  return irep_idt();
339 }
340 
341 static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
342 {
343  exprt tmp=src;
344  simplify(tmp, ns);
345  return get_string_argument_rec(tmp);
346 }
347 
351 {
352  if(operands.size() != 2)
353  return {};
354 
355  const exprt &second_op = skip_typecast(operands.back());
356  if(second_op.id() != ID_address_of)
357  return {};
358 
359  if(second_op.type() != pointer_type(pointer_type(empty_typet{})))
360  return {};
361 
362  const exprt &object = to_address_of_expr(second_op).object();
363  if(object.id() != ID_index)
364  return {};
365 
366  const index_exprt &index_expr = to_index_expr(object);
367  if(!index_expr.index().is_zero())
368  return {};
369  else
370  return index_expr.array();
371 }
372 
374  statet &state,
375  const exprt &rhs)
376 {
377  PRECONDITION(!rhs.operands().empty());
378 
379  exprt tmp_rhs = rhs;
380  clean_expr(tmp_rhs, state, false);
381  tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
382  do_simplify(tmp_rhs);
383 
384  const exprt::operandst &operands=tmp_rhs.operands();
385  std::list<exprt> args;
386 
387  // we either have any number of operands or a va_list as second operand
388  optionalt<exprt> va_args = get_va_args(operands);
389 
390  if(!va_args.has_value())
391  {
392  args.insert(args.end(), std::next(operands.begin()), operands.end());
393  }
394  else
395  {
396  clean_expr(*va_args, state, false);
397  *va_args = state.field_sensitivity.apply(ns, state, *va_args, false);
398  *va_args = state.rename(*va_args, ns).get();
399  if(va_args->id() != ID_array)
400  {
401  // we were not able to constant-propagate va_args, and thus don't have
402  // sufficient information to generate printf -- give up
403  return;
404  }
405 
406  for(const auto &op : va_args->operands())
407  {
408  exprt parameter = skip_typecast(op);
409  if(parameter.id() == ID_address_of)
410  parameter = to_address_of_expr(parameter).object();
411  clean_expr(parameter, state, false);
412  parameter = state.rename(std::move(parameter), ns).get();
413  do_simplify(parameter);
414 
415  args.push_back(std::move(parameter));
416  }
417  }
418 
419  const irep_idt format_string=
420  get_string_argument(operands[0], ns);
421 
422  if(!format_string.empty())
424  state.guard.as_expr(),
425  state.source, "printf", format_string, args);
426 }
427 
429  statet &state,
430  const codet &code)
431 {
432  PRECONDITION(code.operands().size() >= 2);
433 
434  exprt id_arg = state.rename(code.op0(), ns).get();
435 
436  std::list<exprt> args;
437 
438  for(std::size_t i=1; i<code.operands().size(); i++)
439  {
440  exprt l2_arg = state.rename(code.operands()[i], ns).get();
441  do_simplify(l2_arg);
442  args.emplace_back(std::move(l2_arg));
443  }
444 
445  const irep_idt input_id=get_string_argument(id_arg, ns);
446 
447  target.input(state.guard.as_expr(), state.source, input_id, args);
448 }
449 
451  statet &state,
452  const codet &code)
453 {
454  PRECONDITION(code.operands().size() >= 2);
455  exprt id_arg = state.rename(code.op0(), ns).get();
456 
457  std::list<renamedt<exprt, L2>> args;
458 
459  for(std::size_t i=1; i<code.operands().size(); i++)
460  {
461  renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
463  l2_arg.simplify(ns);
464  args.emplace_back(l2_arg);
465  }
466 
467  const irep_idt output_id=get_string_argument(id_arg, ns);
468 
469  target.output(state.guard.as_expr(), state.source, output_id, args);
470 }
471 
478  statet &state,
479  const exprt &lhs,
480  const side_effect_exprt &code)
481 {
482  bool do_array;
483 
484  PRECONDITION(code.type().id() == ID_pointer);
485 
486  const auto &pointer_type = to_pointer_type(code.type());
487 
488  do_array =
489  (code.get(ID_statement) == ID_cpp_new_array ||
490  code.get(ID_statement) == ID_java_new_array_data);
491 
492  dynamic_counter++;
493 
494  const std::string count_string(std::to_string(dynamic_counter));
495 
496  // value
497  symbolt symbol;
498  symbol.base_name=
499  do_array?"dynamic_"+count_string+"_array":
500  "dynamic_"+count_string+"_value";
501  symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name);
502  symbol.is_lvalue=true;
503  if(code.get(ID_statement)==ID_cpp_new_array ||
504  code.get(ID_statement)==ID_cpp_new)
505  symbol.mode=ID_cpp;
506  else if(code.get(ID_statement) == ID_java_new_array_data)
507  symbol.mode=ID_java;
508  else
509  INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
510 
511  if(do_array)
512  {
513  exprt size_arg =
514  clean_expr(static_cast<const exprt &>(code.find(ID_size)), state, false);
515  symbol.type = array_typet(pointer_type.subtype(), size_arg);
516  }
517  else
518  symbol.type = pointer_type.subtype();
519 
520  symbol.type.set(ID_C_dynamic, true);
521 
522  state.symbol_table.add(symbol);
523 
524  // make symbol expression
525 
526  exprt rhs(ID_address_of, pointer_type);
527 
528  if(do_array)
529  {
530  rhs.add_to_operands(
532  }
533  else
534  rhs.copy_to_operands(symbol.symbol_expr());
535 
536  symex_assign(state, code_assignt(lhs, rhs));
537 }
538 
540  statet &,
541  const codet &)
542 {
543  // TODO
544  #if 0
545  bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
546  #endif
547 }
548 
550  statet &,
551  const code_function_callt &)
552 {
553  // TODO: uncomment this line when TG-4667 is done
554  // UNREACHABLE;
555  #if 0
556  exprt new_fc(ID_function, fc.type());
557 
558  new_fc.reserve_operands(fc.operands().size()-1);
559 
560  bool first=true;
561 
562  Forall_operands(it, fc)
563  if(first)
564  first=false;
565  else
566  new_fc.add_to_operands(std::move(*it));
567 
568  new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
569 
570  fc.swap(new_fc);
571  #endif
572 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:229
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
path_storaget::build_symex_nondet
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
Definition: path_storage.h:91
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:102
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
goto_symext::dynamic_counter
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
Definition: goto_symex.h:788
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
Fresh auxiliary symbol creation.
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
goto_symext::symex_printf
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
Definition: symex_builtin_functions.cpp:373
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
goto_symext::target
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:264
optional.h
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symext::path_storage
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:796
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
pointer_predicates.h
Various predicates over pointers in programs.
renamedt::simplify
void simplify(const namespacet &ns)
Definition: renamed.h:39
goto_symext::symex_fkt
virtual void symex_fkt(statet &state, const code_function_callt &code)
Symbolically execute a FUNCTION_CALL instruction for a function whose name starts with CPROVER_FKT_PR...
Definition: symex_builtin_functions.cpp:549
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
goto_symext::symex_cpp_new
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has a CPP new or new array or a Java new array on...
Definition: symex_builtin_functions.cpp:477
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
ssa_exprt::get_object_name
irep_idt get_object_name() const
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
get_va_args
static optionalt< exprt > get_va_args(const exprt::operandst &operands)
Return an expression if operands fulfills all criteria that we expect of the expression to be a varia...
Definition: symex_builtin_functions.cpp:350
irep_idt
dstringt irep_idt
Definition: irep.h:32
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:160
unsigned_char_type
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
field_sensitivityt::apply
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
Definition: field_sensitivity.cpp:21
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
goto_symext::symex_assign
void symex_assign(statet &state, const code_assignt &code)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:38
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
framet::parameter_names
std::vector< irep_idt > parameter_names
Definition: frame.h:30
expr_initializer.h
Expression Initialization.
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:147
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:46
goto_symext::outer_symbol_table
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition: goto_symex.h:247
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1011
call_stackt::top
framet & top()
Definition: call_stack.h:17
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
get_string_argument_rec
static irep_idt get_string_argument_rec(const exprt &src)
Definition: symex_builtin_functions.cpp:310
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_symex_statet::symbol_table
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
Definition: goto_symex_state.h:69
goto_symext::symex_cpp_delete
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
Definition: symex_builtin_functions.cpp:539
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
c_sizeof_type_rec
static optionalt< typet > c_sizeof_type_rec(const exprt &expr)
Definition: symex_builtin_functions.cpp:28
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
SYMEX_DYNAMIC_PREFIX
#define SYMEX_DYNAMIC_PREFIX
Definition: pointer_predicates.h:17
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:817
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
goto_symext::symex_allocate
virtual void symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has an allocate on the right hand side.
Definition: symex_builtin_functions.cpp:49
goto_symext::symex_va_start
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
Definition: symex_builtin_functions.cpp:252
goto_symex.h
Symbolic Execution.
goto_statet::guard
guardt guard
Definition: goto_state.h:50
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
goto_symext::symex_input
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
Definition: symex_builtin_functions.cpp:428
symex_configt::simplify_opt
bool simplify_opt
Definition: symex_config.h:31
va_list_entry
static exprt va_list_entry(const irep_idt &parameter, const pointer_typet &lhs_type, const namespacet &ns)
Construct an entry for the var args array.
Definition: symex_builtin_functions.cpp:218
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:32
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:124
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:256
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
expr_util.h
Deprecated expression utility functions.
invariant_utils.h
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symex_target_equationt::output_fmt
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
Definition: symex_target_equation.cpp:235
pointer_offset_size
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition: pointer_offset_size.cpp:89
array_typet
Arrays with given size.
Definition: std_types.h:965
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
goto_symext::symex_config
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:183
get_string_argument
static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
Definition: symex_builtin_functions.cpp:341
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:157
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
goto_symex_statet::rename
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
exprt::operands
operandst & operands()
Definition: expr.h:95
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:127
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:30
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
c_types.h
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_symext::symex_output
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
Definition: symex_builtin_functions.cpp:450
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
string_constantt::get_value
const irep_idt & get_value() const
Definition: string_constant.h:22
INVARIANT_WITH_IREP
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
Definition: invariant_utils.h:29
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
symex_target_equationt::input
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
Definition: symex_target_equation.cpp:254
dstringt::size
size_t size() const
Definition: dstring.h:104
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
validation_modet::INVARIANT
@ INVARIANT
symex_target_equationt::output
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
Definition: symex_target_equation.cpp:218
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35