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/std_expr.h>
15 
17 {
18  const goto_programt::instructiont &instruction=*state.source.pc;
19  symex_dead(state, instruction.dead_symbol());
20 }
21 
23  goto_symext::statet &state,
24  const exprt &l1_expr,
25  const namespacet &ns)
26 {
27  if(is_ssa_expr(l1_expr))
28  {
29  const ssa_exprt &l1_ssa = to_ssa_expr(l1_expr);
30  const irep_idt &l1_identifier = l1_ssa.get_identifier();
31 
32  // We cannot remove the object from the L1 renaming map, because L1 renaming
33  // information is not local to a path, but removing it from the propagation
34  // map and value-set is safe as 1) it is local to a path and 2) this
35  // instance can no longer appear (unless shared across threads).
36  if(
37  state.threads.size() <= 1 ||
38  state.write_is_shared(l1_ssa, ns) ==
40  {
41  state.value_set.values.erase_if_exists(l1_identifier);
42  }
43  state.propagation.erase_if_exists(l1_identifier);
44  // Remove from the local L2 renaming map; this means any reads from the dead
45  // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
46  // positive integers), which is never defined by any write, and will be
47  // dropped by `goto_symext::merge_goto` on merging with branches where the
48  // identifier is still live.
49  state.drop_l1_name(l1_identifier);
50  }
51  else if(l1_expr.id() == ID_array || l1_expr.id() == ID_struct)
52  {
53  for(const auto &op : l1_expr.operands())
54  remove_l1_object_rec(state, op, ns);
55  }
56  else
58 }
59 
60 void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
61 {
62  ssa_exprt to_rename = is_ssa_expr(symbol_expr) ? to_ssa_expr(symbol_expr)
63  : ssa_exprt{symbol_expr};
64  ssa_exprt ssa = state.rename_ssa<L1>(to_rename, ns).get();
65 
66  const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
67  remove_l1_object_rec(state, fields, ns);
68 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
operandst & operands()
Definition: expr.h:92
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 ...
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:71
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
Central data structure: state.
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
void drop_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
field_sensitivityt field_sensitivity
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
symex_targett::sourcet source
std::vector< threadt > threads
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
Definition: symex_dead.cpp:16
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:243
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
void erase_if_exists(const key_type &k)
Erase element if it exists.
Definition: sharing_map.h:274
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:292
Symbolic Execution.
@ L1
Definition: renamed.h:24
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
API to expression classes.
goto_programt::const_targett pc
Definition: symex_target.h:42
static void remove_l1_object_rec(goto_symext::statet &state, const exprt &l1_expr, const namespacet &ns)
Definition: symex_dead.cpp:22