CBMC
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 
16 #include "path_storage.h"
17 
19 {
20  const goto_programt::instructiont &instruction=*state.source.pc;
21  symex_decl(state, instruction.decl_symbol());
22 }
23 
24 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
25 {
26  // each declaration introduces a new object, which we record as a fresh L1
27  // index
28 
29  // We use "1" as the first level-1 index, which is in line with doing so for
30  // level-2 indices (but it's an arbitrary choice, we have just always been
31  // doing it this way).
32  ssa_exprt ssa = state.add_object(
33  expr,
34  [this](const irep_idt &l0_name) {
35  return path_storage.get_unique_l1_index(l0_name, 1);
36  },
37  ns);
38 
39  ssa = state.declare(std::move(ssa), ns);
40 
41  // we hide the declaration of auxiliary variables
42  // and if the statement itself is hidden
43  bool hidden = ns.lookup(expr.get_identifier()).is_auxiliary ||
44  state.call_stack().top().hidden_function ||
45  state.source.pc->source_location().get_hide();
46 
47  target.decl(
48  state.guard.as_expr(),
49  ssa,
50  state.field_sensitivity.apply(ns, state, ssa, false),
51  state.source,
54 
55  if(path_storage.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
57  state.guard.as_expr(),
58  ssa,
59  state.atomic_section_id,
60  state.source);
61 
63 }
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:38
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
bool hidden_function
Definition: frame.h:40
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:228
guardt guard
Definition: goto_state.h:58
unsigned atomic_section_id
Threads.
Definition: goto_state.h:76
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:18
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:816
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:266
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
Definition: goto_symex.h:845
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:258
exprt as_expr() const
Definition: guard_expr.h:46
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
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
void symex_field_local_init(goto_symex_statet &state, const ssa_exprt &expr)
Initialize local-scope shadow memory for local variables and parameters.
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:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
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.
Storage of symbolic execution paths to resume.
API to expression classes.
goto_programt::const_targett pc
Definition: symex_target.h:42