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