Skip to content

Commit 0b8c742

Browse files
Merge pull request #4736 from romainbrenguier/clean-up/ssa_exprt
Clean-up ssa-exprt
2 parents a613337 + 926c7c0 commit 0b8c742

File tree

2 files changed

+144
-85
lines changed

2 files changed

+144
-85
lines changed

src/util/ssa_expr.cpp

Lines changed: 128 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,43 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/arith_tools.h>
1515

16+
/// If \p expr is:
17+
/// - a symbol_exprt "s" add "s" to the stream \p os
18+
/// - a member_exprt, apply recursively and add "..component_name"
19+
/// - an index_exprt where the index is a constant, apply recursively on the
20+
/// array and add "[[index]]"
21+
/// \return the stream \p os
22+
static std::ostream &
23+
initialize_ssa_identifier(std::ostream &os, const exprt &expr)
24+
{
25+
if(auto member = expr_try_dynamic_cast<member_exprt>(expr))
26+
{
27+
return initialize_ssa_identifier(os, member->struct_op())
28+
<< ".." << member->get_component_name();
29+
}
30+
if(auto index = expr_try_dynamic_cast<index_exprt>(expr))
31+
{
32+
const auto idx =
33+
numeric_cast_v<mp_integer>(to_constant_expr(index->index()));
34+
return initialize_ssa_identifier(os, index->array()) << "[[" << idx << "]]";
35+
}
36+
if(auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
37+
return os << symbol->get_identifier();
38+
39+
UNREACHABLE;
40+
}
41+
42+
ssa_exprt::ssa_exprt(const exprt &expr) : symbol_exprt(expr.type())
43+
{
44+
set(ID_C_SSA_symbol, true);
45+
add(ID_expression, expr);
46+
std::ostringstream os;
47+
initialize_ssa_identifier(os, expr);
48+
const std::string id = os.str();
49+
set_identifier(id);
50+
set(ID_L1_object_identifier, id);
51+
}
52+
1653
/// If \p expr is a symbol "s" add to \p os "s!l0@l1#l2" and to \p l1_object_os
1754
/// "s!l0@l1".
1855
/// If \p expr is a member or index expression, recursively apply the procedure
@@ -75,20 +112,6 @@ static void build_ssa_identifier_rec(
75112
UNREACHABLE;
76113
}
77114

78-
/* Used to determine whether or not an identifier can be built
79-
* before trying and getting an exception */
80-
bool ssa_exprt::can_build_identifier(const exprt &expr)
81-
{
82-
if(expr.id()==ID_symbol)
83-
return true;
84-
else if(expr.id() == ID_member)
85-
return can_build_identifier(to_member_expr(expr).compound());
86-
else if(expr.id() == ID_index)
87-
return can_build_identifier(to_index_expr(expr).array());
88-
else
89-
return false;
90-
}
91-
92115
static std::pair<irep_idt, irep_idt> build_identifier(
93116
const exprt &expr,
94117
const irep_idt &l0,
@@ -103,13 +126,97 @@ static std::pair<irep_idt, irep_idt> build_identifier(
103126
return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str()));
104127
}
105128

106-
void ssa_exprt::update_identifier()
129+
static void update_identifier(ssa_exprt &ssa)
130+
{
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+
}
139+
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)
107182
{
108-
const irep_idt &l0 = get_level_0();
109-
const irep_idt &l1 = get_level_1();
110-
const irep_idt &l2 = get_level_2();
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+
}
111192

112-
auto idpair = build_identifier(get_original_expr(), l0, l1, l2);
113-
set_identifier(idpair.first);
114-
set(ID_L1_object_identifier, idpair.second);
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);
115222
}

src/util/ssa_expr.h

Lines changed: 16 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -17,13 +17,13 @@ class ssa_exprt:public symbol_exprt
1717
{
1818
public:
1919
/// Constructor
20-
/// \param expr: Expression to be converted to SSA symbol
21-
explicit ssa_exprt(const exprt &expr) : symbol_exprt(expr.type())
22-
{
23-
set(ID_C_SSA_symbol, true);
24-
add(ID_expression, expr);
25-
update_identifier();
26-
}
20+
/// \param expr: Expression to be converted to SSA symbol. A valid argument
21+
/// must be one of these:
22+
/// - a symbol_exprt
23+
/// - a member_exprt where the accessed struct would be a valid argument
24+
/// - an index_exprt where the index is a constant and the array would be
25+
/// a valid argument
26+
explicit ssa_exprt(const exprt &expr);
2727

2828
void update_type()
2929
{
@@ -38,76 +38,27 @@ class ssa_exprt:public symbol_exprt
3838
/// Replace the underlying, original expression by \p expr while maintaining
3939
/// SSA indices.
4040
/// \param expr: expression to store
41-
void set_expression(const exprt &expr)
42-
{
43-
type() = expr.type();
44-
add(ID_expression, expr);
45-
update_identifier();
46-
}
47-
48-
irep_idt get_object_name() const
49-
{
50-
const exprt &original_expr = get_original_expr();
51-
52-
if(original_expr.id() == ID_symbol)
53-
return to_symbol_expr(original_expr).get_identifier();
54-
55-
object_descriptor_exprt ode(original_expr);
56-
return to_symbol_expr(ode.root_object()).get_identifier();
57-
}
58-
59-
const ssa_exprt get_l1_object() const
60-
{
61-
object_descriptor_exprt ode(get_original_expr());
41+
void set_expression(const exprt &expr);
6242

63-
ssa_exprt root(ode.root_object());
64-
root.set(ID_L0, get(ID_L0));
65-
root.set(ID_L1, get(ID_L1));
66-
root.update_identifier();
43+
irep_idt get_object_name() const;
6744

68-
return root;
69-
}
45+
const ssa_exprt get_l1_object() const;
7046

71-
const irep_idt get_l1_object_identifier() const
72-
{
73-
#if 0
74-
return get_l1_object().get_identifier();
75-
#else
76-
// the above is the clean version, this is the fast one, using
77-
// an identifier cached during build_identifier
78-
return get(ID_L1_object_identifier);
79-
#endif
80-
}
47+
const irep_idt get_l1_object_identifier() const;
8148

8249
const irep_idt get_original_name() const
8350
{
8451
ssa_exprt o(get_original_expr());
8552
return o.get_identifier();
8653
}
8754

88-
void set_level_0(unsigned i)
89-
{
90-
set(ID_L0, i);
91-
update_identifier();
92-
}
55+
void set_level_0(unsigned i);
9356

94-
void set_level_1(unsigned i)
95-
{
96-
set(ID_L1, i);
97-
update_identifier();
98-
}
57+
void set_level_1(unsigned i);
9958

100-
void set_level_2(unsigned i)
101-
{
102-
set(ID_L2, i);
103-
update_identifier();
104-
}
59+
void set_level_2(unsigned i);
10560

106-
void remove_level_2()
107-
{
108-
remove(ID_L2);
109-
set_identifier(get_l1_object_identifier());
110-
}
61+
void remove_level_2();
11162

11263
const irep_idt get_level_0() const
11364
{
@@ -124,6 +75,7 @@ class ssa_exprt:public symbol_exprt
12475
return get(ID_L2);
12576
}
12677

78+
DEPRECATED(SINCE(2019, 05, 29, "Should only be used internally"))
12779
void update_identifier();
12880

12981
/// Used to determine whether or not an identifier can be built before trying

0 commit comments

Comments
 (0)