cprover
symex_decl.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <util/std_expr.h>
15 
17 {
18  const goto_programt::instructiont &instruction=*state.source.pc;
19  symex_decl(state, instruction.decl_symbol());
20 }
21 
22 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
23 {
24  // each declaration introduces a new object, which we record as a fresh L1
25  // index
26 
27  // We use "1" as the first level-1 index, which is in line with doing so for
28  // level-2 indices (but it's an arbitrary choice, we have just always been
29  // doing it this way).
30  ssa_exprt ssa = state.add_object(
31  expr,
32  [this](const irep_idt &l0_name) {
33  return path_storage.get_unique_l1_index(l0_name, 1);
34  },
35  ns);
36 
37  ssa = state.declare(std::move(ssa), ns);
38 
39  // we hide the declaration of auxiliary variables
40  // and if the statement itself is hidden
41  bool hidden = ns.lookup(expr.get_identifier()).is_auxiliary ||
42  state.call_stack().top().hidden_function ||
43  state.source.pc->source_location.get_hide();
44 
45  target.decl(
46  state.guard.as_expr(),
47  ssa,
48  state.field_sensitivity.apply(ns, state, ssa, false),
49  state.source,
52 
53  if(path_storage.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
55  state.guard.as_expr(),
56  ssa,
57  state.atomic_section_id,
58  state.source);
59 }
framet & top()
Definition: call_stack.h:17
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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.
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:212
guardt guard
Definition: goto_state.h:54
unsigned atomic_section_id
Threads.
Definition: goto_state.h:72
Central data structure: state.
ssa_exprt declare(ssa_exprt ssa, const namespacet &ns)
Add invalid (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of sy...
ssa_exprt add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
Instantiate the object expr.
call_stackt & call_stack()
field_sensitivityt field_sensitivity
symex_targett::sourcet source
virtual void symex_decl(statet &state)
Symbolically execute a DECL instruction.
Definition: symex_decl.cpp:16
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:797
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:264
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:256
exprt as_expr() const
Definition: guard_expr.h:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
Definition: path_storage.h:116
std::size_t get_unique_l1_index(const irep_idt &id, std::size_t minimum_index)
Provide a unique L1 index for a given id, starting from minimum_index.
Definition: path_storage.h:104
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
irep_idt get_object_name() const
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
Symbolic Execution.
API to expression classes.
bool hidden_function
Definition: frame.h:34
goto_programt::const_targett pc
Definition: symex_target.h:43