@@ -50,71 +50,6 @@ ssa_exprt::ssa_exprt(const exprt &expr) : symbol_exprt(expr.type())
50
50
set (ID_L1_object_identifier, id);
51
51
}
52
52
53
- void ssa_exprt::set_expression (const exprt &expr)
54
- {
55
- type () = expr.type ();
56
- add (ID_expression, expr);
57
- update_identifier ();
58
- }
59
-
60
- irep_idt ssa_exprt::get_object_name () const
61
- {
62
- const exprt &original_expr = get_original_expr ();
63
-
64
- if (original_expr.id () == ID_symbol)
65
- return to_symbol_expr (original_expr).get_identifier ();
66
-
67
- object_descriptor_exprt ode (original_expr);
68
- return to_symbol_expr (ode.root_object ()).get_identifier ();
69
- }
70
-
71
- const ssa_exprt ssa_exprt::get_l1_object () const
72
- {
73
- object_descriptor_exprt ode (get_original_expr ());
74
-
75
- ssa_exprt root (ode.root_object ());
76
- root.set (ID_L0, get (ID_L0));
77
- root.set (ID_L1, get (ID_L1));
78
- root.update_identifier ();
79
-
80
- return root;
81
- }
82
-
83
- const irep_idt ssa_exprt::get_l1_object_identifier () const
84
- {
85
- #if 0
86
- return get_l1_object().get_identifier();
87
- #else
88
- // the above is the clean version, this is the fast one, using
89
- // an identifier cached during build_identifier
90
- return get (ID_L1_object_identifier);
91
- #endif
92
- }
93
-
94
- void ssa_exprt::set_level_0 (unsigned i)
95
- {
96
- set (ID_L0, i);
97
- update_identifier ();
98
- }
99
-
100
- void ssa_exprt::set_level_1 (unsigned i)
101
- {
102
- set (ID_L1, i);
103
- update_identifier ();
104
- }
105
-
106
- void ssa_exprt::set_level_2 (unsigned i)
107
- {
108
- set (ID_L2, i);
109
- update_identifier ();
110
- }
111
-
112
- void ssa_exprt::remove_level_2 ()
113
- {
114
- remove (ID_L2);
115
- set_identifier (get_l1_object_identifier ());
116
- }
117
-
118
53
// / If \p expr is a symbol "s" add to \p os "s!l0@l1#l2" and to \p l1_object_os
119
54
// / "s!l0@l1".
120
55
// / If \p expr is a member or index expression, recursively apply the procedure
@@ -177,20 +112,6 @@ static void build_ssa_identifier_rec(
177
112
UNREACHABLE;
178
113
}
179
114
180
- /* Used to determine whether or not an identifier can be built
181
- * before trying and getting an exception */
182
- bool ssa_exprt::can_build_identifier (const exprt &expr)
183
- {
184
- if (expr.id ()==ID_symbol)
185
- return true ;
186
- else if (expr.id () == ID_member)
187
- return can_build_identifier (to_member_expr (expr).compound ());
188
- else if (expr.id () == ID_index)
189
- return can_build_identifier (to_index_expr (expr).array ());
190
- else
191
- return false ;
192
- }
193
-
194
115
static std::pair<irep_idt, irep_idt> build_identifier (
195
116
const exprt &expr,
196
117
const irep_idt &l0,
@@ -205,13 +126,97 @@ static std::pair<irep_idt, irep_idt> build_identifier(
205
126
return std::make_pair (irep_idt (oss.str ()), irep_idt (l1_object_oss.str ()));
206
127
}
207
128
208
- void ssa_exprt:: update_identifier ()
129
+ static void update_identifier (ssa_exprt &ssa )
209
130
{
210
- const irep_idt &l0 = get_level_0 ();
211
- const irep_idt &l1 = get_level_1 ();
212
- const irep_idt &l2 = get_level_2 ();
131
+ const irep_idt &l0 = ssa.get_level_0 ();
132
+ const irep_idt &l1 = ssa.get_level_1 ();
133
+ const irep_idt &l2 = ssa.get_level_2 ();
134
+
135
+ auto idpair = build_identifier (ssa.get_original_expr (), l0, l1, l2);
136
+ ssa.set_identifier (idpair.first );
137
+ ssa.set (ID_L1_object_identifier, idpair.second );
138
+ }
213
139
214
- auto idpair = build_identifier (get_original_expr (), l0, l1, l2);
215
- set_identifier (idpair.first );
216
- set (ID_L1_object_identifier, idpair.second );
140
+ void ssa_exprt::set_expression (const exprt &expr)
141
+ {
142
+ type () = expr.type ();
143
+ add (ID_expression, expr);
144
+ ::update_identifier (*this );
145
+ }
146
+
147
+ irep_idt ssa_exprt::get_object_name () const
148
+ {
149
+ const exprt &original_expr = get_original_expr ();
150
+
151
+ if (original_expr.id () == ID_symbol)
152
+ return to_symbol_expr (original_expr).get_identifier ();
153
+
154
+ object_descriptor_exprt ode (original_expr);
155
+ return to_symbol_expr (ode.root_object ()).get_identifier ();
156
+ }
157
+
158
+ const ssa_exprt ssa_exprt::get_l1_object () const
159
+ {
160
+ object_descriptor_exprt ode (get_original_expr ());
161
+
162
+ ssa_exprt root (ode.root_object ());
163
+ root.set (ID_L0, get (ID_L0));
164
+ root.set (ID_L1, get (ID_L1));
165
+ ::update_identifier (root);
166
+
167
+ return root;
168
+ }
169
+
170
+ const irep_idt ssa_exprt::get_l1_object_identifier () const
171
+ {
172
+ #if 0
173
+ return get_l1_object().get_identifier();
174
+ #else
175
+ // the above is the clean version, this is the fast one, using
176
+ // an identifier cached during build_identifier
177
+ return get (ID_L1_object_identifier);
178
+ #endif
179
+ }
180
+
181
+ void ssa_exprt::set_level_0 (unsigned i)
182
+ {
183
+ set (ID_L0, i);
184
+ ::update_identifier (*this );
185
+ }
186
+
187
+ void ssa_exprt::set_level_1 (unsigned i)
188
+ {
189
+ set (ID_L1, i);
190
+ ::update_identifier (*this );
191
+ }
192
+
193
+ void ssa_exprt::set_level_2 (unsigned i)
194
+ {
195
+ set (ID_L2, i);
196
+ ::update_identifier (*this );
197
+ }
198
+
199
+ void ssa_exprt::remove_level_2 ()
200
+ {
201
+ remove (ID_L2);
202
+ set_identifier (get_l1_object_identifier ());
203
+ }
204
+
205
+ /* Used to determine whether or not an identifier can be built
206
+ * before trying and getting an exception */
207
+ bool ssa_exprt::can_build_identifier (const exprt &expr)
208
+ {
209
+ if (expr.id () == ID_symbol)
210
+ return true ;
211
+ else if (expr.id () == ID_member)
212
+ return can_build_identifier (to_member_expr (expr).compound ());
213
+ else if (expr.id () == ID_index)
214
+ return can_build_identifier (to_index_expr (expr).array ());
215
+ else
216
+ return false ;
217
+ }
218
+
219
+ void ssa_exprt::update_identifier ()
220
+ {
221
+ ::update_identifier (*this );
217
222
}
0 commit comments