cprover
symex_dead.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 
22 {
23  const goto_programt::instructiont &instruction=*state.source.pc;
24 
25  const codet &code=to_code(instruction.code);
26 
27  if(code.operands().size()!=1)
28  throw "dead expects one operand";
29 
30  if(code.op0().id()!=ID_symbol)
31  throw "dead expects symbol as first operand";
32 
33  // We increase the L2 renaming to make these non-deterministic.
34  // We also prevent propagation of old values.
35 
36  ssa_exprt ssa(to_symbol_expr(code.op0()));
37  state.rename(ssa, ns, goto_symex_statet::L1);
38 
39  // in case of pointers, put something into the value set
40  if(ns.follow(code.op0().type()).id()==ID_pointer)
41  {
42  exprt failed=
44 
45  exprt rhs;
46 
47  if(failed.is_not_nil())
48  {
49  address_of_exprt address_of_expr;
50  address_of_expr.object()=failed;
51  address_of_expr.type()=code.op0().type();
52  rhs=address_of_expr;
53  }
54  else
55  rhs=exprt(ID_invalid);
56 
57  state.rename(rhs, ns, goto_symex_statet::L1);
58  state.value_set.assign(ssa, rhs, ns, true, false);
59  }
60 
61  ssa_exprt ssa_lhs=to_ssa_expr(ssa);
62  const irep_idt &l1_identifier=ssa_lhs.get_identifier();
63 
64  // prevent propagation
65  state.propagation.remove(l1_identifier);
66 
67  // L2 renaming
68  if(state.level2.current_names.find(l1_identifier)!=
69  state.level2.current_names.end())
70  state.level2.increase_counter(l1_identifier);
71 }
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
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
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: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)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
Symbolic Execution.
API to expression classes.
Operator to return the address of an object.
Definition: std_expr.h:2593
virtual void symex_dead(statet &state)
Definition: symex_dead.cpp:21
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
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
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
symex_targett::sourcet source