CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_decl.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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
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) {
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
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,
60 state.source);
61
63}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
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.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition goto_symex.h:810
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:839
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().
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
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.
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
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