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 {
19  const goto_programt::instructiont &instruction=*state.source.pc;
20  symex_dead(state, instruction.dead_symbol());
21 }
22 
23 void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
24 {
25  ssa_exprt to_rename = is_ssa_expr(symbol_expr) ? to_ssa_expr(symbol_expr)
26  : ssa_exprt{symbol_expr};
27  ssa_exprt ssa = state.rename_ssa<L1>(to_rename, ns).get();
28 
29  const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
30  find_symbols_sett fields_set;
31  find_symbols_or_nexts(fields, fields_set);
32 
33  for(const irep_idt &l1_identifier : fields_set)
34  {
35  // We cannot remove the object from the L1 renaming map, because L1 renaming
36  // information is not local to a path, but removing it from the propagation
37  // map and value-set is safe as 1) it is local to a path and 2) this
38  // instance can no longer appear.
39  state.value_set.values.erase_if_exists(l1_identifier);
40  state.propagation.erase_if_exists(l1_identifier);
41  // Remove from the local L2 renaming map; this means any reads from the dead
42  // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
43  // positive integers), which is never defined by any write, and will be
44  // dropped by `goto_symext::merge_goto` on merging with branches where the
45  // identifier is still live.
46  state.drop_l1_name(l1_identifier);
47  }
48 }
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:234
L1
@ L1
Definition: renamed.h:24
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:42
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:42
sharing_mapt::erase_if_exists
void erase_if_exists(const key_type &k)
Erase element if it exists.
Definition: sharing_map.h:274
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:60
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:17
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:71
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:125
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:145
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:295
goto_symex.h
Symbolic Execution.
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:120
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:243
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
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:156
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
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:51
value_sett::values
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:292