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/rename.h>
17 #include <util/std_expr.h>
18 
20 
21 #include <analyses/dirty.h>
22 
24 {
25  const goto_programt::instructiont &instruction=*state.source.pc;
26 
27  const codet &code=to_code(instruction.code);
28 
29  if(code.operands().size()==2)
30  throw "two-operand decl not supported here";
31 
32  if(code.operands().size()!=1)
33  throw "decl expects one operand";
34 
35  if(code.op0().id()!=ID_symbol)
36  throw "decl expects symbol as first operand";
37 
38  symex_decl(state, to_symbol_expr(code.op0()));
39 }
40 
41 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
42 {
43  // We increase the L2 renaming to make these non-deterministic.
44  // We also prevent propagation of old values.
45 
46  ssa_exprt ssa(expr);
47  state.rename(ssa, ns, goto_symex_statet::L1);
48  const irep_idt &l1_identifier=ssa.get_identifier();
49 
50  // rename type to L2
51  state.rename(ssa.type(), l1_identifier, ns);
52  ssa.update_type();
53 
54  // in case of pointers, put something into the value set
55  if(ns.follow(expr.type()).id()==ID_pointer)
56  {
57  exprt failed=
58  get_failed_symbol(expr, ns);
59 
60  exprt rhs;
61 
62  if(failed.is_not_nil())
63  {
64  address_of_exprt address_of_expr;
65  address_of_expr.object()=failed;
66  address_of_expr.type()=expr.type();
67  rhs=address_of_expr;
68  }
69  else
70  rhs=exprt(ID_invalid);
71 
72  state.rename(rhs, ns, goto_symex_statet::L1);
73  state.value_set.assign(ssa, rhs, ns, true, false);
74  }
75 
76  // prevent propagation
77  state.propagation.remove(l1_identifier);
78 
79  // L2 renaming
80  // inlining may yield multiple declarations of the same identifier
81  // within the same L1 context
82  if(state.level2.current_names.find(l1_identifier)==
83  state.level2.current_names.end())
84  state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
85  state.level2.increase_counter(l1_identifier);
86  const bool record_events=state.record_events;
87  state.record_events=false;
88  state.rename(ssa, ns);
89  state.record_events=record_events;
90 
91  // we hide the declaration of auxiliary variables
92  // and if the statement itself is hidden
93  bool hidden=
94  ns.lookup(expr.get_identifier()).is_auxiliary ||
95  state.top().hidden_function ||
96  state.source.pc->source_location.get_hide();
97 
98  target.decl(
99  state.guard.as_expr(),
100  ssa,
101  state.source,
102  hidden?
105 
106  assert(state.dirty);
107  if((*state.dirty)(ssa.get_object_name()) &&
108  state.atomic_section_id==0)
110  state.guard.as_expr(),
111  ssa,
112  state.atomic_section_id,
113  state.source);
114 }
exprt as_expr() const
Definition: guard.h:43
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
symex_targett & target
Definition: goto_symex.h:105
bool is_not_nil() const
Definition: irep.h:104
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt & object()
Definition: std_expr.h:2608
class goto_symex_statet::propagationt propagation
exprt & op0()
Definition: expr.h:84
Variables whose address is taken.
void remove(const irep_idt &identifier)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void symex_decl(statet &state)
Definition: symex_decl.cpp:23
const irep_idt & get_identifier() const
Definition: std_expr.h:120
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Definition: value_set.cpp:1089
void increase_counter(const irep_idt &identifier)
typet & type()
Definition: expr.h:60
Pointer Dereferencing.
goto_symex_statet::level2t level2
const irep_idt & id() const
Definition: irep.h:189
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Symbolic Execution.
API to expression classes.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
Operator to return the address of an object.
Definition: std_expr.h:2593
const dirtyt * dirty
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
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:49
Expression to hold a symbol (variable)
Definition: std_expr.h:82
A statement in a programming language.
Definition: std_code.h:19
operandst & operands()
Definition: expr.h:70
const namespacet & ns
Definition: goto_symex.h:104
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0
symex_targett::sourcet source