CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/symex_dead.cpp Source File

16 void goto_symext::symex_dead(statet &state)

17{

18 const goto_programt::instructiont &instruction=*state.source.pc;

19 symex_dead(state, instruction.dead_symbol());

20}

22 static void remove_l1_object_rec(

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.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) ==

39 goto_symex_statet::write_is_shared_resultt::NOT_SHARED)

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(

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

60 UNREACHABLE;

61}

63 void 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

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

dstringt

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

exprt

Base class for all expressions.

Definition expr.h:57

field_sensitivityt::get_fields

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 ...

Definition field_sensitivity.cpp:293

goto_programt::instructiont

This class represents an instruction in the GOTO intermediate representation.

Definition goto_program.h:180

goto_programt::instructiont::dead_symbol

const symbol_exprt & dead_symbol() const

Get the symbol for DEAD.

Definition goto_program.h:243

goto_statet::propagation

sharing_mapt< irep_idt, exprt > propagation

Definition goto_state.h:71

goto_statet::value_set

value_sett value_set

Uses level 1 names, and is used to do dereferencing.

Definition goto_state.h:51

goto_symex_statet

Central data structure: state.

Definition goto_symex_state.h:42

goto_symex_statet::write_is_shared_resultt::NOT_SHARED

@ NOT_SHARED

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:239

goto_symex_statet::field_sensitivity

field_sensitivityt field_sensitivity

Definition goto_symex_state.h:122

goto_symex_statet::write_is_shared

write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const

Definition goto_symex_state.cpp:514

goto_symex_statet::source

symex_targett::sourcet source

Definition goto_symex_state.h:62

goto_symex_statet::rename_ssa

renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)

Version of rename which is specialized for SSA exprt.

Definition goto_symex_state.cpp:144

goto_symex_statet::threads

std::vector< threadt > threads

Definition goto_symex_state.h:199

goto_symext::symex_dead

virtual void symex_dead(statet &state)

Symbolically execute a DEAD instruction.

Definition symex_dead.cpp:16

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

namespacet

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

Definition namespace.h:91

sharing_mapt::erase_if_exists

void erase_if_exists(const key_type &k)

Erase element if it exists.

Definition sharing_map.h:274

ssa_exprt

Expression providing an SSA-renamed symbol of expressions.

Definition ssa_expr.h:17

symbol_exprt

Expression to hold a symbol (variable)

Definition std_expr.h:132

value_sett::values

valuest values

Stores the LHS ID -> RHS expression set map.

Definition value_set.h:281

goto_symex.h

Symbolic Execution.

L1

@ L1

Definition renamed.h:24

UNREACHABLE

#define UNREACHABLE

This should be used to mark dead code.

Definition invariant.h:525

is_ssa_expr

bool is_ssa_expr(const exprt &expr)

Definition ssa_expr.h:125

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

std_expr.h

API to expression classes.

symex_targett::sourcet::pc

goto_programt::const_targett pc

Definition symex_target.h:42

remove_l1_object_rec

static void remove_l1_object_rec(goto_symext::statet &state, const exprt &l1_expr, const namespacet &ns)

Definition symex_dead.cpp:22