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 code_deadt &code = to_code_dead(instruction.code);
25 
26  // We increase the L2 renaming to make these non-deterministic.
27  // We also prevent propagation of old values.
28 
29  ssa_exprt ssa(code.symbol());
30  state.rename(ssa, ns, goto_symex_statet::L1);
31 
32  // in case of pointers, put something into the value set
33  if(ns.follow(code.symbol().type()).id() == ID_pointer)
34  {
35  exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns);
36 
37  exprt rhs;
38 
39  if(failed.is_not_nil())
40  rhs = address_of_exprt(failed, to_pointer_type(code.symbol().type()));
41  else
42  rhs=exprt(ID_invalid);
43 
44  state.rename(rhs, ns, goto_symex_statet::L1);
45  state.value_set.assign(ssa, rhs, ns, true, false);
46  }
47 
48  ssa_exprt ssa_lhs=to_ssa_expr(ssa);
49  const irep_idt &l1_identifier=ssa_lhs.get_identifier();
50 
51  // prevent propagation
52  state.propagation.erase(l1_identifier);
53 
54  // L2 renaming
55  auto level2_it = state.level2.current_names.find(l1_identifier);
56  if(level2_it != state.level2.current_names.end())
58 }
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
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
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.
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
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
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 an exprt to a symbol_exprt.
Definition: std_expr.h:251
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
symbol_exprt & symbol()
Definition: std_code.h:432
Base class for all expressions.
Definition: expr.h:54
virtual void symex_dead(statet &)
Definition: symex_dead.cpp:20
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
symex_targett::sourcet source