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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
goto_symext::symex_dead
virtual void symex_dead(statet &)
Definition: symex_dead.cpp:20
value_sett::assign
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
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:41
goto_symex_statet
Definition: goto_symex_state.h:34
goto_symex_statet::L1
@ L1
Definition: goto_symex_state.h:72
goto_symex_statet::rename
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Definition: goto_symex_state.cpp:273
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symex_statet::value_set
value_sett value_set
Definition: goto_symex_state.h:109
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:58
symex_renaming_levelt::increase_counter
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
Definition: renaming_level.h:41
get_failed_symbol
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
Definition: add_failed_symbols.cpp:94
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
goto_symex_statet::propagation
std::map< irep_idt, exprt > propagation
Definition: goto_symex_state.h:69
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
goto_symex.h
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:432
irept::id
const irep_idt & id() const
Definition: irep.h:259
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
add_failed_symbols.h
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
goto_symex_statet::level2
symex_level2t level2
Definition: goto_symex_state.h:66
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
symex_renaming_levelt::current_names
current_namest current_names
Definition: renaming_level.h:31