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  auto array_size_rhs = array_size;
154  array_size = size_symbol.symbol_expr();
155 
156  symex_assign(state, size_symbol.symbol_expr(), array_size_rhs);
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  symex_assign(state, value_symbol.symbol_expr(), *zero_value);
185  }
186  else
187  {
188  auto lhs = value_symbol.symbol_expr();
189  auto rhs =
190  path_storage.build_symex_nondet(*object_type, code.source_location());
191  symex_assign(state, lhs, rhs);
192  }
193 
194  exprt rhs;
195 
196  if(object_type->id() == ID_array)
197  {
198  const auto &array_type = to_array_type(*object_type);
199  index_exprt index_expr(
200  value_symbol.symbol_expr(), from_integer(0, index_type()));
201  rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
202  }
203  else
204  {
205  rhs=address_of_exprt(
206  value_symbol.symbol_expr(), pointer_type(value_symbol.type));
207  }
208 
209  symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
210 }
211 
216  const irep_idt &parameter,
217  const pointer_typet &lhs_type,
218  const namespacet &ns)
219 {
220  static const pointer_typet void_ptr_type = pointer_type(empty_typet{});
221 
222  symbol_exprt parameter_expr = ns.lookup(parameter).symbol_expr();
223 
224  // Visual Studio has va_list == char* and stores parameters of size no
225  // greater than the size of a pointer as immediate values
226  if(lhs_type.subtype().id() != ID_pointer)
227  {
228  auto parameter_size = size_of_expr(parameter_expr.type(), ns);
229  CHECK_RETURN(parameter_size.has_value());
230 
231  binary_predicate_exprt fits_slot{
232  *parameter_size,
233  ID_le,
234  from_integer(lhs_type.get_width(), parameter_size->type())};
235 
236  return if_exprt{
237  fits_slot,
238  typecast_exprt::conditional_cast(parameter_expr, void_ptr_type),
240  address_of_exprt{parameter_expr}, void_ptr_type)};
241  }
242  else
243  {
245  address_of_exprt{std::move(parameter_expr)}, void_ptr_type);
246  }
247 }
248 
250  statet &state,
251  const exprt &lhs,
252  const side_effect_exprt &code)
253 {
254  PRECONDITION(code.operands().size() == 1);
255 
256  if(lhs.is_nil())
257  return; // ignore
258 
259  // create an array holding pointers to the parameters, starting after the
260  // parameter that the operand points to
261  const exprt &op = skip_typecast(to_unary_expr(code).op());
262  // this must be the address of a symbol
263  const irep_idt start_parameter =
265 
266  exprt::operandst va_arg_operands;
267  bool parameter_id_found = false;
268  for(auto &parameter : state.call_stack().top().parameter_names)
269  {
270  if(!parameter_id_found)
271  {
272  parameter_id_found = parameter == start_parameter;
273  continue;
274  }
275 
276  va_arg_operands.push_back(
277  va_list_entry(parameter, to_pointer_type(lhs.type()), ns));
278  }
279  const std::size_t va_arg_size = va_arg_operands.size();
280  exprt array =
281  array_exprt{std::move(va_arg_operands),
283  from_integer(va_arg_size, size_type())}};
284 
285  symbolt &va_array = get_fresh_aux_symbol(
286  array.type(),
288  "va_args",
289  state.source.pc->source_location,
290  ns.lookup(state.source.function_id).mode,
291  state.symbol_table);
292  va_array.value = array;
293 
294  array = clean_expr(std::move(array), state, false);
295  array = state.rename(std::move(array), ns).get();
296  do_simplify(array);
297  symex_assign(state, va_array.symbol_expr(), std::move(array));
298 
299  exprt rhs = address_of_exprt{
300  index_exprt{va_array.symbol_expr(), from_integer(0, index_type())}};
301  rhs = state.rename(std::move(rhs), ns).get();
302  symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
303 }
304 
306 {
307  if(src.id()==ID_typecast)
308  {
309  return get_string_argument_rec(to_typecast_expr(src).op());
310  }
311  else if(src.id()==ID_address_of)
312  {
313  const exprt &object = to_address_of_expr(src).object();
314 
315  if(object.id() == ID_index)
316  {
317  const auto &index_expr = to_index_expr(object);
318 
319  if(
320  index_expr.array().id() == ID_string_constant &&
321  index_expr.index().is_zero())
322  {
323  const exprt &fmt_str = index_expr.array();
324  return to_string_constant(fmt_str).get_value();
325  }
326  }
327  else if(object.id() == ID_string_constant)
328  {
329  return to_string_constant(object).get_value();
330  }
331  }
332 
333  return irep_idt();
334 }
335 
336 static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
337 {
338  exprt tmp=src;
339  simplify(tmp, ns);
340  return get_string_argument_rec(tmp);
341 }
342 
346 {
347  if(operands.size() != 2)
348  return {};
349 
350  const exprt &second_op = skip_typecast(operands.back());
351  if(second_op.id() != ID_address_of)
352  return {};
353 
354  if(second_op.type() != pointer_type(pointer_type(empty_typet{})))
355  return {};
356 
357  const exprt &object = to_address_of_expr(second_op).object();
358  if(object.id() != ID_index)
359  return {};
360 
361  const index_exprt &index_expr = to_index_expr(object);
362  if(!index_expr.index().is_zero())
363  return {};
364  else
365  return index_expr.array();
366 }
367 
369  statet &state,
370  const exprt &rhs)
371 {
372  PRECONDITION(!rhs.operands().empty());
373 
374  exprt tmp_rhs = rhs;
375  clean_expr(tmp_rhs, state, false);
376  tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
377  do_simplify(tmp_rhs);
378 
379  const exprt::operandst &operands=tmp_rhs.operands();
380  std::list<exprt> args;
381 
382  // we either have any number of operands or a va_list as second operand
383  optionalt<exprt> va_args = get_va_args(operands);
384 
385  if(!va_args.has_value())
386  {
387  args.insert(args.end(), std::next(operands.begin()), operands.end());
388  }
389  else
390  {
391  clean_expr(*va_args, state, false);
392  *va_args = state.field_sensitivity.apply(ns, state, *va_args, false);
393  *va_args = state.rename(*va_args, ns).get();
394  if(va_args->id() != ID_array)
395  {
396  // we were not able to constant-propagate va_args, and thus don't have
397  // sufficient information to generate printf -- give up
398  return;
399  }
400 
401  for(const auto &op : va_args->operands())
402  {
403  exprt parameter = skip_typecast(op);
404  if(parameter.id() == ID_address_of)
405  parameter = to_address_of_expr(parameter).object();
406  clean_expr(parameter, state, false);
407  parameter = state.rename(std::move(parameter), ns).get();
408  do_simplify(parameter);
409 
410  args.push_back(std::move(parameter));
411  }
412  }
413 
414  const irep_idt format_string=
415  get_string_argument(operands[0], ns);
416 
417  if(!format_string.empty())
419  state.guard.as_expr(),
420  state.source, "printf", format_string, args);
421 }
422 
424  statet &state,
425  const codet &code)
426 {
427  PRECONDITION(code.operands().size() >= 2);
428 
429  exprt id_arg = state.rename(code.op0(), ns).get();
430 
431  std::list<exprt> args;
432 
433  for(std::size_t i=1; i<code.operands().size(); i++)
434  {
435  exprt l2_arg = state.rename(code.operands()[i], ns).get();
436  do_simplify(l2_arg);
437  args.emplace_back(std::move(l2_arg));
438  }
439 
440  const irep_idt input_id=get_string_argument(id_arg, ns);
441 
442  target.input(state.guard.as_expr(), state.source, input_id, args);
443 }
444 
446  statet &state,
447  const codet &code)
448 {
449  PRECONDITION(code.operands().size() >= 2);
450  exprt id_arg = state.rename(code.op0(), ns).get();
451 
452  std::list<renamedt<exprt, L2>> args;
453 
454  for(std::size_t i=1; i<code.operands().size(); i++)
455  {
456  renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
458  l2_arg.simplify(ns);
459  args.emplace_back(l2_arg);
460  }
461 
462  const irep_idt output_id=get_string_argument(id_arg, ns);
463 
464  target.output(state.guard.as_expr(), state.source, output_id, args);
465 }
466 
473  statet &state,
474  const exprt &lhs,
475  const side_effect_exprt &code)
476 {
477  bool do_array;
478 
479  PRECONDITION(code.type().id() == ID_pointer);
480 
481  const auto &pointer_type = to_pointer_type(code.type());
482 
483  do_array =
484  (code.get(ID_statement) == ID_cpp_new_array ||
485  code.get(ID_statement) == ID_java_new_array_data);
486 
487  dynamic_counter++;
488 
489  const std::string count_string(std::to_string(dynamic_counter));
490 
491  // value
492  symbolt symbol;
493  symbol.base_name=
494  do_array?"dynamic_"+count_string+"_array":
495  "dynamic_"+count_string+"_value";
496  symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name);
497  symbol.is_lvalue=true;
498  if(code.get(ID_statement)==ID_cpp_new_array ||
499  code.get(ID_statement)==ID_cpp_new)
500  symbol.mode=ID_cpp;
501  else if(code.get(ID_statement) == ID_java_new_array_data)
502  symbol.mode=ID_java;
503  else
504  INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
505 
506  if(do_array)
507  {
508  exprt size_arg =
509  clean_expr(static_cast<const exprt &>(code.find(ID_size)), state, false);
510  symbol.type = array_typet(pointer_type.subtype(), size_arg);
511  }
512  else
513  symbol.type = pointer_type.subtype();
514 
515  symbol.type.set(ID_C_dynamic, true);
516 
517  state.symbol_table.add(symbol);
518 
519  // make symbol expression
520 
521  exprt rhs(ID_address_of, pointer_type);
522 
523  if(do_array)
524  {
525  rhs.add_to_operands(
527  }
528  else
529  rhs.copy_to_operands(symbol.symbol_expr());
530 
531  symex_assign(state, lhs, rhs);
532 }
533 
535  statet &,
536  const codet &)
537 {
538  // TODO
539  #if 0
540  bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
541  #endif
542 }
543 
545  statet &,
546  const code_function_callt &)
547 {
548  // TODO: uncomment this line when TG-4667 is done
549  // UNREACHABLE;
550  #if 0
551  exprt new_fc(ID_function, fc.type());
552 
553  new_fc.reserve_operands(fc.operands().size()-1);
554 
555  bool first=true;
556 
557  Forall_operands(it, fc)
558  if(first)
559  first=false;
560  else
561  new_fc.add_to_operands(std::move(*it));
562 
563  new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
564 
565  fc.swap(new_fc);
566  #endif
567 }
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:133
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:233
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:1789
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
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:218
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
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:103
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:209
goto_symext::dynamic_counter
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
Definition: goto_symex.h:789
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
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:368
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
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:797
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:2087
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:544
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:472
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:54
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:345
irep_idt
dstringt irep_idt
Definition: irep.h:37
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:147
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:81
field_sensitivityt::apply
NODISCARD 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:33
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
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:56
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
array_typet::size
const exprt & size() const
Definition: std_types.h:976
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:82
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:1215
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:961
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:145
get_string_argument_rec
static irep_idt get_string_argument_rec(const exprt &src)
Definition: symex_builtin_functions.cpp:305
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:534
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:644
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:767
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:249
goto_symex.h
Symbolic Execution.
goto_statet::guard
guardt guard
Definition: goto_state.h:54
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
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:423
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:215
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2524
index_exprt::index
exprt & index()
Definition: std_expr.h:1269
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
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:1533
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:33
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:1048
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
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:237
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:968
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:431
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:1815
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
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:336
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
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:140
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:278
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:383
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
exprt::operands
operandst & operands()
Definition: expr.h:96
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
index_exprt
Array index operator.
Definition: std_expr.h:1243
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:761
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:128
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:30
goto_symext::symex_assign
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:39
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1382
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:445
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:1898
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:256
dstringt::size
size_t size() const
Definition: dstring.h:104
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
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:220
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35