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 <cassert>
15 
16 #include <util/std_expr.h>
17 
19 
20 #include <analyses/dirty.h>
21 
23 {
24  const goto_programt::instructiont &instruction=*state.source.pc;
25 
26  const codet &code = instruction.code;
27 
28  // two-operand decl not supported here
29  // we handle the decl with only one operand
30  PRECONDITION(code.operands().size() == 1);
31 
32  symex_decl(state, to_code_decl(code).symbol());
33 }
34 
35 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
36 {
37  // We increase the L2 renaming to make these non-deterministic.
38  // We also prevent propagation of old values.
39 
40  ssa_exprt ssa(expr);
41  state.rename(ssa, ns, goto_symex_statet::L1);
42  const irep_idt &l1_identifier=ssa.get_identifier();
43 
44  // rename type to L2
45  state.rename(ssa.type(), l1_identifier, ns);
46  ssa.update_type();
47 
48  // in case of pointers, put something into the value set
49  if(ns.follow(expr.type()).id()==ID_pointer)
50  {
51  exprt failed=
52  get_failed_symbol(expr, ns);
53 
54  exprt rhs;
55 
56  if(failed.is_not_nil())
57  rhs=address_of_exprt(failed, to_pointer_type(expr.type()));
58  else
59  rhs=exprt(ID_invalid);
60 
61  state.rename(rhs, ns, goto_symex_statet::L1);
62  state.value_set.assign(ssa, rhs, ns, true, false);
63  }
64 
65  // prevent propagation
66  state.propagation.erase(l1_identifier);
67 
68  // L2 renaming
69  // inlining may yield multiple declarations of the same identifier
70  // within the same L1 context
71  const auto level2_it =
72  state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 0))
73  .first;
75  const bool record_events=state.record_events;
76  state.record_events=false;
77  state.rename(ssa, ns);
78  state.record_events=record_events;
79 
80  // we hide the declaration of auxiliary variables
81  // and if the statement itself is hidden
82  bool hidden=
83  ns.lookup(expr.get_identifier()).is_auxiliary ||
84  state.top().hidden_function ||
85  state.source.pc->source_location.get_hide();
86 
87  target.decl(
88  state.guard.as_expr(),
89  ssa,
90  state.source,
91  hidden?
94 
95  if(state.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
97  state.guard.as_expr(),
98  ssa,
99  state.atomic_section_id,
100  state.source);
101 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
dirty.h
goto_symex_statet::guard
guardt guard
Definition: goto_symex_state.h:57
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
value_sett::assign
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it.
Definition: value_set.cpp:1151
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:41
goto_symext::target
symex_target_equationt & target
Definition: goto_symex.h:216
goto_symex_statet
Definition: goto_symex_state.h:34
goto_symex_statet::L1
@ L1
Definition: goto_symex_state.h:72
goto_symext::symex_decl
virtual void symex_decl(statet &)
Definition: symex_decl.cpp:22
goto_symex_statet::rename
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Definition: goto_symex_state.cpp:273
exprt
Base class for all expressions.
Definition: expr.h:54
ssa_exprt::get_object_name
irep_idt get_object_name() const
Definition: ssa_expr.h:46
goto_symex_statet::value_set
value_sett value_set
Definition: goto_symex_state.h:109
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:58
symex_renaming_levelt::increase_counter
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
Definition: renaming_level.h:41
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
symex_target_equationt::decl
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
Definition: symex_target_equation.cpp:156
get_failed_symbol
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
Definition: add_failed_symbols.cpp:94
symex_targett::assignment_typet::STATE
@ STATE
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
goto_symex_statet::propagation
std::map< irep_idt, exprt > propagation
Definition: goto_symex_state.h:69
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
goto_symex_statet::dirty
incremental_dirtyt dirty
Definition: goto_symex_state.h:258
goto_symex_statet::record_events
bool record_events
Definition: goto_symex_state.h:257
ssa_exprt::update_type
void update_type()
Definition: ssa_expr.h:36
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
goto_symex_statet::atomic_section_id
unsigned atomic_section_id
Definition: goto_symex_state.h:234
goto_symex_statet::top
framet & top()
Definition: goto_symex_state.h:215
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
goto_symex.h
goto_symex_statet::framet::hidden_function
bool hidden_function
Definition: goto_symex_state.h:183
irept::id
const irep_idt & id() const
Definition: irep.h:259
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
symex_target_equationt::shared_write
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...
Definition: symex_target_equation.cpp:49
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:215
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
guardt::as_expr
exprt as_expr() const
Definition: guard.h:41
exprt::operands
operandst & operands()
Definition: expr.h:78
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
add_failed_symbols.h
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
goto_symex_statet::level2
symex_level2t level2
Definition: goto_symex_state.h:66
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
symex_renaming_levelt::current_names
current_namest current_names
Definition: renaming_level.h:31
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34