CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_dead.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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
24 const exprt &l1_expr,
25 const namespacet &ns)
26{
28 {
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 {
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.
50 }
51 else if(
52 l1_expr.type().id() == ID_array || l1_expr.type().id() == ID_struct ||
53 l1_expr.type().id() == ID_struct_tag || l1_expr.type().id() == ID_union ||
54 l1_expr.type().id() == ID_union_tag)
55 {
56 for(const auto &op : l1_expr.operands())
57 remove_l1_object_rec(state, op, ns);
58 }
59 else
61}
62
63void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
64{
65 ssa_exprt to_rename = is_ssa_expr(symbol_expr) ? to_ssa_expr(symbol_expr)
66 : ssa_exprt{symbol_expr};
67 ssa_exprt ssa = state.rename_ssa<L1>(to_rename, ns).get();
68
69 const exprt fields =
70 state.field_sensitivity.get_fields(ns, state, ssa, false);
71 remove_l1_object_rec(state, fields, ns);
72}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr, bool disjoined_fields_only) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
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.
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
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
std::vector< threadt > threads
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:258
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.
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Expression to hold a symbol (variable)
Definition std_expr.h:131
valuest values
Stores the LHS ID -> RHS expression set map.
Definition value_set.h:296
Symbolic Execution.
@ L1
Definition renamed.h:24
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
API to expression classes.
goto_programt::const_targett pc
static void remove_l1_object_rec(goto_symext::statet &state, const exprt &l1_expr, const namespacet &ns)