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=to_code(instruction.code);
27 
28  if(code.operands().size()==2)
29  throw "two-operand decl not supported here";
30 
31  if(code.operands().size()!=1)
32  throw "decl expects one operand";
33 
34  if(code.op0().id()!=ID_symbol)
35  throw "decl expects symbol as first operand";
36 
37  symex_decl(state, to_symbol_expr(code.op0()));
38 }
39 
40 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
41 {
42  // We increase the L2 renaming to make these non-deterministic.
43  // We also prevent propagation of old values.
44 
45  ssa_exprt ssa(expr);
46  state.rename(ssa, ns, goto_symex_statet::L1);
47  const irep_idt &l1_identifier=ssa.get_identifier();
48 
49  // rename type to L2
50  state.rename(ssa.type(), l1_identifier, ns);
51  ssa.update_type();
52 
53  // in case of pointers, put something into the value set
54  if(ns.follow(expr.type()).id()==ID_pointer)
55  {
56  exprt failed=
57  get_failed_symbol(expr, ns);
58 
59  exprt rhs;
60 
61  if(failed.is_not_nil())
62  rhs=address_of_exprt(failed, to_pointer_type(expr.type()));
63  else
64  rhs=exprt(ID_invalid);
65 
66  state.rename(rhs, ns, goto_symex_statet::L1);
67  state.value_set.assign(ssa, rhs, ns, true, false);
68  }
69 
70  // prevent propagation
71  state.propagation.remove(l1_identifier);
72 
73  // L2 renaming
74  // inlining may yield multiple declarations of the same identifier
75  // within the same L1 context
76  if(state.level2.current_names.find(l1_identifier)==
77  state.level2.current_names.end())
78  state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
79  state.level2.increase_counter(l1_identifier);
80  const bool record_events=state.record_events;
81  state.record_events=false;
82  state.rename(ssa, ns);
83  state.record_events=record_events;
84 
85  // we hide the declaration of auxiliary variables
86  // and if the statement itself is hidden
87  bool hidden=
88  ns.lookup(expr.get_identifier()).is_auxiliary ||
89  state.top().hidden_function ||
90  state.source.pc->source_location.get_hide();
91 
92  target.decl(
93  state.guard.as_expr(),
94  ssa,
95  state.source,
96  hidden?
99 
100  if(state.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
102  state.guard.as_expr(),
103  ssa,
104  state.atomic_section_id,
105  state.source);
106 }
exprt as_expr() const
Definition: guard.h:43
bool is_not_nil() const
Definition: irep.h:103
goto_programt::const_targett pc
Definition: symex_target.h:32
class goto_symex_statet::propagationt propagation
exprt & op0()
Definition: expr.h:72
Variables whose address is taken.
void remove(const irep_idt &identifier)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
Definition: std_expr.h:128
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:1088
void increase_counter(const irep_idt &identifier)
typet & type()
Definition: expr.h:56
Pointer Dereferencing.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
write to a sharedvariable
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
goto_symex_statet::level2t level2
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:237
const irep_idt & id() const
Definition: irep.h:189
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:238
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
incremental_dirtyt dirty
const typet & follow(const typet &) const
Definition: namespace.cpp:55
Operator to return the address of an object.
Definition: std_expr.h:3170
Base class for all expressions.
Definition: expr.h:42
irep_idt get_object_name() const
Definition: ssa_expr.h:46
void update_type()
Definition: ssa_expr.h:36
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
A statement in a programming language.
Definition: std_code.h:21
operandst & operands()
Definition: expr.h:66
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 namespace_baset::lookup().
Definition: namespace.cpp:130
symex_targett::sourcet source