cprover
ssa_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_SSA_EXPR_H
11 #define CPROVER_UTIL_SSA_EXPR_H
12 
13 #include "std_expr.h"
14 
17 class ssa_exprt:public symbol_exprt
18 {
19 public:
21  {
22  set(ID_C_SSA_symbol, true);
23  }
24 
28  explicit ssa_exprt(const exprt &expr):
29  symbol_exprt(expr.type())
30  {
31  set(ID_C_SSA_symbol, true);
32  add(ID_expression, expr);
34  }
35 
36  void update_type()
37  {
38  static_cast<exprt &>(add(ID_expression)).type()=type();
39  }
40 
41  const exprt &get_original_expr() const
42  {
43  return static_cast<const exprt &>(find(ID_expression));
44  }
45 
47  {
49  ode.object()=get_original_expr();
51  }
52 
53  const ssa_exprt get_l1_object() const
54  {
56  ode.object()=get_original_expr();
57 
58  ssa_exprt root(ode.root_object());
59  root.set(ID_L0, get(ID_L0));
60  root.set(ID_L1, get(ID_L1));
61  root.update_identifier();
62 
63  return root;
64  }
65 
67  {
68  #if 0
69  return get_l1_object().get_identifier();
70  #else
71  // the above is the clean version, this is the fast one, using
72  // an identifier cached during build_identifier
73  return get(ID_L1_object_identifier);
74  #endif
75  }
76 
78  {
80  return o.get_identifier();
81  }
82 
83  void set_level_0(unsigned i)
84  {
85  set(ID_L0, i);
87  }
88 
89  void set_level_1(unsigned i)
90  {
91  set(ID_L1, i);
93  }
94 
95  void set_level_2(unsigned i)
96  {
97  set(ID_L2, i);
99  }
100 
102  {
103  remove(ID_L2);
105  }
106 
107  const irep_idt get_level_0() const
108  {
109  return get(ID_L0);
110  }
111 
112  const irep_idt get_level_1() const
113  {
114  return get(ID_L1);
115  }
116 
117  const irep_idt get_level_2() const
118  {
119  return get(ID_L2);
120  }
121 
123  {
124  const irep_idt &l0=get_level_0();
125  const irep_idt &l1=get_level_1();
126  const irep_idt &l2=get_level_2();
127 
128  auto idpair=build_identifier(get_original_expr(), l0, l1, l2);
129  set_identifier(idpair.first);
130  set(ID_L1_object_identifier, idpair.second);
131  }
132 
133  static std::pair<irep_idt, irep_idt> build_identifier(
134  const exprt &src,
135  const irep_idt &l0,
136  const irep_idt &l1,
137  const irep_idt &l2);
138 
139  /* Used to determine whether or not an identifier can be built
140  * before trying and getting an exception */
141  static bool can_build_identifier(const exprt &src);
142 };
143 
154 inline const ssa_exprt &to_ssa_expr(const exprt &expr)
155 {
156  assert(expr.id()==ID_symbol &&
157  expr.get_bool(ID_C_SSA_symbol) &&
158  !expr.has_operands());
159  return static_cast<const ssa_exprt &>(expr);
160 }
161 
166 {
167  assert(expr.id()==ID_symbol &&
168  expr.get_bool(ID_C_SSA_symbol) &&
169  !expr.has_operands());
170  return static_cast<ssa_exprt &>(expr);
171 }
172 
173 inline bool is_ssa_expr(const exprt &expr)
174 {
175  return expr.id()==ID_symbol &&
176  expr.get_bool(ID_C_SSA_symbol);
177 }
178 
179 #endif // CPROVER_UTIL_SSA_EXPR_H
const ssa_exprt get_l1_object() const
Definition: ssa_expr.h:53
void update_identifier()
Definition: ssa_expr.h:122
ssa_exprt(const exprt &expr)
Constructor.
Definition: ssa_expr.h:28
void set_level_1(unsigned i)
Definition: ssa_expr.h:89
const irep_idt & get_identifier() const
Definition: std_expr.h:128
const exprt & root_object() const
Definition: std_expr.h:1966
typet & type()
Definition: expr.h:56
static std::pair< irep_idt, irep_idt > build_identifier(const exprt &src, const irep_idt &l0, const irep_idt &l1, const irep_idt &l2)
Definition: ssa_expr.cpp:87
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
ssa_exprt()
Definition: ssa_expr.h:20
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const irep_idt get_l1_object_identifier() const
Definition: ssa_expr.h:66
const irep_idt get_level_1() const
Definition: ssa_expr.h:112
const irep_idt & id() const
Definition: irep.h:189
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
void set_level_0(unsigned i)
Definition: ssa_expr.h:83
void remove_level_2()
Definition: ssa_expr.h:101
API to expression classes.
const irep_idt get_original_name() const
Definition: ssa_expr.h:77
static bool can_build_identifier(const exprt &src)
Definition: ssa_expr.cpp:76
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
const irep_idt get_level_0() const
Definition: ssa_expr.h:107
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
bool has_operands() const
Definition: expr.h:63
Base class for all expressions.
Definition: expr.h:42
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
void update_type()
Definition: ssa_expr.h:36
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:173
irept & add(const irep_namet &name)
Definition: irep.cpp:306
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:123
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const irep_idt get_level_2() const
Definition: ssa_expr.h:117
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214