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 <util/find_symbols.h>
15 #include <util/std_expr.h>
16 
18 
20 {
21  const goto_programt::instructiont &instruction=*state.source.pc;
22 
23  const code_deadt &code = instruction.get_dead();
24  symex_dead(state, code.symbol());
25 }
26 
27 void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
28 {
29  ssa_exprt to_rename = is_ssa_expr(symbol_expr) ? to_ssa_expr(symbol_expr)
30  : ssa_exprt{symbol_expr};
31  ssa_exprt ssa = state.rename_ssa<L1>(to_rename, ns).get();
32 
33  const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
34  find_symbols_sett fields_set;
35  find_symbols_or_nexts(fields, fields_set);
36 
37  for(const irep_idt &l1_identifier : fields_set)
38  {
39  // We cannot remove the object from the L1 renaming map, because L1 renaming
40  // information is not local to a path, but removing it from the propagation
41  // map and value-set is safe as 1) it is local to a path and 2) this
42  // instance can no longer appear.
43  state.value_set.values.erase_if_exists(l1_identifier);
44  state.propagation.erase_if_exists(l1_identifier);
45  // Remove from the local L2 renaming map; this means any reads from the dead
46  // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
47  // positive integers), which is never defined by any write, and will be
48  // dropped by `goto_symext::merge_goto` on merging with branches where the
49  // identifier is still live.
50  state.drop_l1_name(l1_identifier);
51  }
52 }
goto_programt::instructiont::get_dead
const code_deadt & get_dead() const
Get the dead statement for DEAD.
Definition: goto_program.h:213
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_symex_statet::drop_l1_name
void drop_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
Definition: goto_symex_state.h:238
L1
@ L1
Definition: renamed.h:18
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
find_symbols_or_nexts
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
Definition: find_symbols.cpp:18
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
sharing_mapt::erase_if_exists
void erase_if_exists(const key_type &k)
Erase element if it exists.
Definition: sharing_map.h:264
exprt
Base class for all expressions.
Definition: expr.h:53
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
goto_symex_statet::rename_ssa
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
goto_symext::symex_dead
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
Definition: symex_dead.cpp:19
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:63
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:128
find_symbols.h
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
goto_symex.h
Symbolic Execution.
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:473
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:467
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:124
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:256
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:22
field_sensitivityt::get_fields
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
Definition: field_sensitivity.cpp:147
add_failed_symbols.h
Pointer Dereferencing.
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
API to expression classes.
goto_statet::value_set
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:43
value_sett::values
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:329