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 }
exprt as_expr() const
Definition: guard.h:41
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
bool is_not_nil() const
Definition: irep.h:173
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
goto_programt::const_targett pc
Definition: symex_target.h:41
Variables whose address is taken.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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
typet & type()
Return the type of the expression.
Definition: expr.h:68
Pointer Dereferencing.
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...
std::map< irep_idt, exprt > propagation
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
Symbolic Execution.
virtual void symex_decl(statet &)
Definition: symex_decl.cpp:22
API to expression classes.
symex_target_equationt & target
Definition: goto_symex.h:216
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
incremental_dirtyt dirty
current_namest current_names
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
symex_level2t level2
Base class for all expressions.
Definition: expr.h:54
irep_idt get_object_name() const
Definition: ssa_expr.h:46
void update_type()
Definition: ssa_expr.h:36
Expression to hold a symbol (variable)
Definition: std_expr.h:143
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
operandst & operands()
Definition: expr.h:78
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
symex_targett::sourcet source