cprover
symex_dereference.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/byte_operators.h>
16 #include <util/c_types.h>
17 #include <util/exception_utils.h>
18 #include <util/expr_iterator.h>
19 #include <util/expr_util.h>
20 #include <util/fresh_symbol.h>
21 #include <util/invariant.h>
23 
25 
26 #include "expr_skeleton.h"
27 #include "symex_assign.h"
29 
44  const exprt &expr,
45  statet &state,
46  bool keep_array)
47 {
48  exprt result;
49 
50  if(expr.id()==ID_byte_extract_little_endian ||
51  expr.id()==ID_byte_extract_big_endian)
52  {
53  // address_of(byte_extract(op, offset, t)) is
54  // address_of(op) + offset with adjustments for arrays
55 
57 
58  // recursive call
59  result = address_arithmetic(be.op(), state, keep_array);
60 
61  if(be.op().type().id() == ID_array && result.id() == ID_address_of)
62  {
64 
65  // turn &a of type T[i][j] into &(a[0][0])
66  for(const typet *t = &(a.type().subtype());
67  t->id() == ID_array && expr.type() != *t;
68  t = &(t->subtype()))
70  }
71 
72  // do (expr.type() *)(((char *)op)+offset)
73  result=typecast_exprt(result, pointer_type(char_type()));
74 
75  // there could be further dereferencing in the offset
76  exprt offset=be.offset();
77  dereference_rec(offset, state, false, false);
78 
79  result=plus_exprt(result, offset);
80 
81  // treat &array as &array[0]
82  const typet &expr_type = expr.type();
83  typet dest_type_subtype;
84 
85  if(expr_type.id()==ID_array && !keep_array)
86  dest_type_subtype=expr_type.subtype();
87  else
88  dest_type_subtype=expr_type;
89 
90  result=typecast_exprt(result, pointer_type(dest_type_subtype));
91  }
92  else if(expr.id()==ID_index ||
93  expr.id()==ID_member)
94  {
96  ode.build(expr, ns);
97 
98  const byte_extract_exprt be(
99  byte_extract_id(), ode.root_object(), ode.offset(), expr.type());
100 
101  // recursive call
102  result = address_arithmetic(be, state, keep_array);
103 
104  do_simplify(result);
105  }
106  else if(expr.id()==ID_dereference)
107  {
108  // ANSI-C guarantees &*p == p no matter what p is,
109  // even if it's complete garbage
110  // just grab the pointer, but be wary of further dereferencing
111  // in the pointer itself
112  result=to_dereference_expr(expr).pointer();
113  dereference_rec(result, state, false, false);
114  }
115  else if(expr.id()==ID_if)
116  {
117  if_exprt if_expr=to_if_expr(expr);
118 
119  // the condition is not an address
120  dereference_rec(if_expr.cond(), state, false, false);
121 
122  // recursive call
123  if_expr.true_case() =
124  address_arithmetic(if_expr.true_case(), state, keep_array);
125  if_expr.false_case() =
126  address_arithmetic(if_expr.false_case(), state, keep_array);
127 
128  result=if_expr;
129  }
130  else if(expr.id()==ID_symbol ||
131  expr.id()==ID_string_constant ||
132  expr.id()==ID_label ||
133  expr.id()==ID_array)
134  {
135  // give up, just dereference
136  result=expr;
137  dereference_rec(result, state, false, false);
138 
139  // turn &array into &array[0]
140  if(result.type().id() == ID_array && !keep_array)
141  result=index_exprt(result, from_integer(0, index_type()));
142 
143  // handle field-sensitive SSA symbol
144  mp_integer offset=0;
145  if(is_ssa_expr(expr))
146  {
147  auto offset_opt = compute_pointer_offset(expr, ns);
148  PRECONDITION(offset_opt.has_value());
149  offset = *offset_opt;
150  }
151 
152  if(offset>0)
153  {
154  const byte_extract_exprt be(
155  byte_extract_id(),
156  to_ssa_expr(expr).get_l1_object(),
157  from_integer(offset, index_type()),
158  expr.type());
159 
160  result = address_arithmetic(be, state, keep_array);
161 
162  do_simplify(result);
163  }
164  else
165  result=address_of_exprt(result);
166  }
167  else if(expr.id() == ID_typecast)
168  {
169  const typecast_exprt &tc_expr = to_typecast_expr(expr);
170 
171  result = address_arithmetic(tc_expr.op(), state, keep_array);
172 
173  // treat &array as &array[0]
174  const typet &expr_type = expr.type();
175  typet dest_type_subtype;
176 
177  if(expr_type.id() == ID_array && !keep_array)
178  dest_type_subtype = expr_type.subtype();
179  else
180  dest_type_subtype = expr_type;
181 
182  result = typecast_exprt(result, pointer_type(dest_type_subtype));
183  }
184  else
186  "goto_symext::address_arithmetic does not handle " + expr.id_string());
187 
188  const typet &expr_type = expr.type();
189  INVARIANT(
190  (expr_type.id() == ID_array && !keep_array) ||
191  pointer_type(expr_type) == result.type(),
192  "either non-persistent array or pointer to result");
193 
194  return result;
195 }
196 
198 goto_symext::cache_dereference(exprt &dereference_result, statet &state)
199 {
200  auto const cache_key = [&] {
201  auto cache_key =
202  state.field_sensitivity.apply(ns, state, dereference_result, false);
203  if(auto let_expr = expr_try_dynamic_cast<let_exprt>(dereference_result))
204  {
205  let_expr->value() = state.rename<L2>(let_expr->value(), ns).get();
206  }
207  else
208  {
209  cache_key = state.rename<L2>(cache_key, ns).get();
210  }
211  return cache_key;
212  }();
213 
214  if(auto cached = state.dereference_cache.find(cache_key))
215  {
216  return *cached;
217  }
218 
219  auto const &cache_symbol = get_fresh_aux_symbol(
220  cache_key.type(),
221  "symex",
222  "dereference_cache",
223  dereference_result.source_location(),
225  ns,
226  state.symbol_table);
227 
228  // we need to lift possible lets
229  // (come from the value set to avoid repeating complex pointer comparisons)
230  auto cache_value = cache_key;
231  lift_lets(state, cache_value);
232 
233  auto assign = symex_assignt{
235 
236  auto cache_symbol_expr = cache_symbol.symbol_expr();
237  assign.assign_symbol(
238  to_ssa_expr(state.rename<L1>(cache_symbol_expr, ns).get()),
239  expr_skeletont{},
240  cache_value,
241  {});
242 
243  state.dereference_cache.insert(cache_key, cache_symbol_expr);
244  return cache_symbol_expr;
245 }
246 
259  exprt &expr,
260  statet &state,
261  bool write,
262  bool is_in_quantifier)
263 {
264  if(expr.id()==ID_dereference)
265  {
266  bool expr_is_not_null = false;
267 
268  if(state.threads.size() == 1)
269  {
270  const irep_idt &expr_function = state.source.function_id;
271  if(!expr_function.empty())
272  {
273  const dereference_exprt to_check =
275 
276  expr_is_not_null = path_storage.safe_pointers.at(expr_function)
277  .is_safe_dereference(to_check, state.source.pc);
278  }
279  }
280 
281  exprt tmp1;
282  tmp1.swap(to_dereference_expr(expr).pointer());
283 
284  // first make sure there are no dereferences in there
285  dereference_rec(tmp1, state, false, is_in_quantifier);
286 
287  // Depending on the nature of the pointer expression, the recursive deref
288  // operation might have introduced a construct such as
289  // (x == &o1 ? o1 : o2).field, in which case we should simplify to push the
290  // member operator inside the if, then apply field-sensitivity to yield
291  // (x == &o1 ? o1..field : o2..field). value_set_dereferencet can then
292  // apply the dereference operation to each of o1..field and o2..field
293  // independently, as it special-cases the ternary conditional operator.
294  // There may also be index operators in tmp1 which can now be resolved to
295  // constant array cell references, so we replace symbols with constants
296  // first, hoping for a transformation such as
297  // (x == &o1 ? o1 : o2)[idx] =>
298  // (x == &o1 ? o1 : o2)[2] =>
299  // (x == &o1 ? o1[[2]] : o2[[2]])
300  // Note we don't L2 rename non-constant symbols at this point, because the
301  // value-set works in terms of L1 names and we don't want to ask it to
302  // dereference an L2 pointer, which it would not have an entry for.
303 
304  tmp1 = state.rename<L1_WITH_CONSTANT_PROPAGATION>(tmp1, ns).get();
305 
306  do_simplify(tmp1);
307 
309  {
310  // make sure simplify has not re-introduced any dereferencing that
311  // had previously been cleaned away
312  INVARIANT(
313  !has_subexpr(tmp1, ID_dereference),
314  "simplify re-introduced dereferencing");
315  }
316 
317  tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), false);
318 
319  // we need to set up some elaborate call-backs
320  symex_dereference_statet symex_dereference_state(state, ns);
321 
323  ns,
324  state.symbol_table,
325  symex_dereference_state,
327  expr_is_not_null,
328  log);
329 
330  // std::cout << "**** " << format(tmp1) << '\n';
331  exprt tmp2 =
332  dereference.dereference(tmp1, symex_config.show_points_to_sets);
333  // std::cout << "**** " << format(tmp2) << '\n';
334 
335 
336  // this may yield a new auto-object
337  trigger_auto_object(tmp2, state);
338 
339  // Check various conditions for when we should try to cache the expression.
340  // 1. Caching dereferences must be enabled.
341  // 2. Do not cache inside LHS of writes.
342  // 3. Do not cache inside quantifiers (references variables outside their
343  // scope).
344  // 4. Only cache "complicated" expressions, i.e. of the form
345  // [let p = <expr> in ]
346  // (p == &something ? something : ...))
347  // Otherwise we should just return it unchanged.
348  if(
349  symex_config.cache_dereferences && !write && !is_in_quantifier &&
350  (tmp2.id() == ID_if || tmp2.id() == ID_let))
351  {
352  expr = cache_dereference(tmp2, state);
353  }
354  else
355  {
356  expr = std::move(tmp2);
357  }
358  }
359  else if(
360  expr.id() == ID_index && to_index_expr(expr).array().id() == ID_member &&
361  to_array_type(to_index_expr(expr).array().type()).size().is_zero())
362  {
363  // This is an expression of the form x.a[i],
364  // where a is a zero-sized array. This gets
365  // re-written into *(&x.a+i)
366 
367  index_exprt index_expr=to_index_expr(expr);
368 
369  address_of_exprt address_of_expr(index_expr.array());
370  address_of_expr.type()=pointer_type(expr.type());
371 
372  dereference_exprt tmp{plus_exprt{address_of_expr, index_expr.index()}};
374 
375  // recursive call
376  dereference_rec(tmp, state, write, is_in_quantifier);
377 
378  expr.swap(tmp);
379  }
380  else if(expr.id()==ID_index &&
381  to_index_expr(expr).array().type().id()==ID_pointer)
382  {
383  // old stuff, will go away
384  UNREACHABLE;
385  }
386  else if(expr.id()==ID_address_of)
387  {
388  address_of_exprt &address_of_expr=to_address_of_expr(expr);
389 
390  exprt &object=address_of_expr.object();
391 
392  expr = address_arithmetic(
393  object,
394  state,
395  to_pointer_type(expr.type()).subtype().id() == ID_array);
396  }
397  else if(expr.id()==ID_typecast)
398  {
399  exprt &tc_op=to_typecast_expr(expr).op();
400 
401  // turn &array into &array[0] when casting to pointer-to-element-type
402  if(
403  tc_op.id() == ID_address_of &&
404  to_address_of_expr(tc_op).object().type().id() == ID_array &&
405  expr.type() ==
406  pointer_type(to_address_of_expr(tc_op).object().type().subtype()))
407  {
408  expr=
410  index_exprt(
411  to_address_of_expr(tc_op).object(),
412  from_integer(0, index_type())));
413 
414  dereference_rec(expr, state, write, is_in_quantifier);
415  }
416  else
417  {
418  dereference_rec(tc_op, state, write, is_in_quantifier);
419  }
420  }
421  else
422  {
423  bool is_quantifier = expr.id() == ID_forall || expr.id() == ID_exists;
424  Forall_operands(it, expr)
425  dereference_rec(*it, state, write, is_in_quantifier || is_quantifier);
426  }
427 }
428 
429 static exprt
430 apply_to_objects_in_dereference(exprt e, const std::function<exprt(exprt)> &f)
431 {
432  if(auto deref = expr_try_dynamic_cast<dereference_exprt>(e))
433  {
434  deref->op() = f(std::move(deref->op()));
435  return *deref;
436  }
437 
438  for(auto &sub : e.operands())
439  sub = apply_to_objects_in_dereference(std::move(sub), f);
440  return e;
441 }
442 
480 void goto_symext::dereference(exprt &expr, statet &state, bool write)
481 {
482  PRECONDITION(!state.call_stack().empty());
483 
484  // Symbols whose address is taken need to be renamed to level 1
485  // in order to distinguish addresses of local variables
486  // from different frames.
487  expr = apply_to_objects_in_dereference(std::move(expr), [&](exprt e) {
488  return state.field_sensitivity.apply(
489  ns, state, state.rename<L1>(std::move(e), ns).get(), false);
490  });
491 
492  // start the recursion!
493  dereference_rec(expr, state, write, false);
494  // dereferencing may introduce new symbol_exprt
495  // (like __CPROVER_memory)
496  expr = state.rename<L1>(std::move(expr), ns).get();
497 
498  // Dereferencing is likely to introduce new member-of-if constructs --
499  // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field."
500  // Run expression simplification, which converts that to
501  // (x == &o1 ? o1.field : o2.field))
502  // before applying field sensitivity. Field sensitivity can then turn such
503  // field-of-symbol expressions into atomic SSA expressions instead of having
504  // to rewrite all of 'o1' otherwise.
505  // Even without field sensitivity this can be beneficial: for example,
506  // "(b ? s1 : s2).member := X" results in
507  // (b ? s1 : s2) := (b ? s1 : s2) with (member := X)
508  // and then
509  // s1 := b ? ((b ? s1 : s2) with (member := X)) : s1
510  // when all we need is
511  // s1 := s1 with (member := X) [and guard b]
512  // s2 := s2 with (member := X) [and guard !b]
513  do_simplify(expr);
514 
516  {
517  // make sure simplify has not re-introduced any dereferencing that
518  // had previously been cleaned away
519  INVARIANT(
520  !has_subexpr(expr, ID_dereference),
521  "simplify re-introduced dereferencing");
522  }
523 
524  expr = state.field_sensitivity.apply(ns, state, std::move(expr), write);
525 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
exception_utils.h
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.
goto_statet::dereference_cache
sharing_mapt< exprt, symbol_exprt, false, irep_hash > dereference_cache
This is used for eliminating repeated complicated dereferences.
Definition: goto_state.h:43
goto_symext::cache_dereference
symbol_exprt cache_dereference(exprt &dereference_result, statet &state)
Definition: symex_dereference.cpp:198
L2
@ L2
Definition: renamed.h:20
typet::subtype
const typet & subtype() const
Definition: type.h:47
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:141
symex_assign.h
Symbolic Execution of assignments.
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
arith_tools.h
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: pointer_expr.cpp:108
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:339
L1
@ L1
Definition: renamed.h:18
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:442
typet
The type of an expression, extends irept.
Definition: type.h:28
goto_symext::address_arithmetic
exprt address_arithmetic(const exprt &, statet &, bool keep_array)
Transforms an lvalue expression by replacing any dereference operations it contains with explicit ref...
Definition: symex_dereference.cpp:43
fresh_symbol.h
Fresh auxiliary symbol creation.
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
expr_skeleton.h
Expression skeleton.
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
goto_symext::target
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:264
value_set_dereference.h
Pointer Dereferencing.
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
goto_symext::path_storage
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:802
symex_configt::cache_dereferences
bool cache_dereferences
Whether or not to replace multiple occurrences of the same dereference with a single symbol that cont...
Definition: symex_config.h:64
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:144
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:147
invariant.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
symex_assignt
Functor for symex assignment.
Definition: symex_assign.h:26
goto_symext::trigger_auto_object
void trigger_auto_object(const exprt &, statet &)
Definition: auto_objects.cpp:77
symex_dereference_state.h
Symbolic Execution of ANSI-C.
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
object_descriptor_exprt::root_object
static const exprt & root_object(const exprt &expr)
Definition: pointer_expr.cpp:125
symex_targett::assignment_typet::STATE
@ STATE
goto_symext::log
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:276
compute_pointer_offset
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:500
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:198
byte_operators.h
Expression classes for byte-level operators.
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:147
symex_configt::show_points_to_sets
bool show_points_to_sets
Definition: symex_config.h:49
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
goto_symext::dereference
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
Definition: symex_dereference.cpp:480
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
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:399
goto_symex.h
Symbolic Execution.
goto_symext::dereference_rec
void dereference_rec(exprt &expr, statet &state, bool write, bool is_in_quantifier)
If expr is a dereference_exprt, replace it with explicit references to the objects it may point to.
Definition: symex_dereference.cpp:258
symex_dereference_statet
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Definition: symex_dereference_state.h:26
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
irept::swap
void swap(irept &irep)
Definition: irep.h:453
get_original_name
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Definition: renaming_level.cpp:156
irept::id
const irep_idt & id() const
Definition: irep.h:407
dstringt::empty
bool empty() const
Definition: dstring.h:88
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
L1_WITH_CONSTANT_PROPAGATION
@ L1_WITH_CONSTANT_PROPAGATION
Definition: renamed.h:19
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:33
sharing_mapt::insert
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
Definition: sharing_map.h:1346
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:124
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
value_set_dereferencet
Wrapper for a function dereferencing pointer expressions using a value set.
Definition: value_set_dereference.h:28
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
expr_util.h
Deprecated expression utility functions.
apply_to_objects_in_dereference
static exprt apply_to_objects_in_dereference(exprt e, const std::function< exprt(exprt)> &f)
Definition: symex_dereference.cpp:430
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
goto_symext::language_mode
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition: goto_symex.h:239
path_storaget::safe_pointers
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
Definition: path_storage.h:100
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2103
goto_symext::lift_lets
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
Definition: symex_clean_expr.cpp:204
goto_symext::symex_config
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:183
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
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...
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:367
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1242
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
symex_configt::run_validation_checks
bool run_validation_checks
Should the additional validation checks be run? If this flag is set the checks for renaming (both lev...
Definition: symex_config.h:44
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
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
expr_skeletont
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
sharing_mapt::find
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1449
object_descriptor_exprt::offset
exprt & offset()
Definition: pointer_expr.h:189