1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
|
/*******************************************************************\
Module: Unit test for ssa_expr.h/ssa_expr.cpp
Author: Romain Brenguier, romain.brenguier@diffblue.com
\*******************************************************************/
#include <testing-utils/use_catch.h>
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/ssa_expr.h>
TEST_CASE("Constructor of ssa_exprt", "[unit][util][ssa_expr]")
{
GIVEN("An expression containing member access, array access and a symbol")
{
const signedbv_typet int_type{32};
const array_typet array_type{int_type, from_integer(10, int_type)};
std::vector<struct_typet::componentt> components;
components.emplace_back("array_field", array_type);
const struct_typet struct_type{components};
const symbol_exprt symbol{"sym", struct_type};
const index_exprt index{member_exprt{symbol, components.back()},
from_integer(9, int_type)};
WHEN("construct an ssa_exprt from `sym.array_field[9]`")
{
const ssa_exprt ssa{index};
THEN("the ssa_exprt has identifier 'sym..array_field[[9]]'")
{
REQUIRE(ssa.get_identifier() == "sym..array_field[[9]]");
REQUIRE(ssa.get_l1_object_identifier() == "sym..array_field[[9]]");
}
THEN("the ssa_exprt has no level set")
{
REQUIRE(ssa.get_level_0() == irep_idt{});
REQUIRE(ssa.get_level_1() == irep_idt{});
REQUIRE(ssa.get_level_2() == irep_idt{});
}
}
}
}
TEST_CASE("Set level", "[unit][util][ssa_expr]")
{
GIVEN("An SSA expression constructed from a symbol")
{
const signedbv_typet int_type{32};
const symbol_exprt symbol{"sym", int_type};
ssa_exprt ssa(symbol);
WHEN("set_level_0")
{
ssa.set_level_0(1);
REQUIRE(ssa.get_level_0() == "1");
REQUIRE(ssa.get_level_1() == irep_idt{});
REQUIRE(ssa.get_level_2() == irep_idt{});
REQUIRE(ssa.get_original_expr() == symbol);
REQUIRE(ssa.get_identifier() == "sym!1");
REQUIRE(ssa.get_l1_object_identifier() == "sym!1");
}
WHEN("set_level_1")
{
ssa.set_level_1(3);
REQUIRE(ssa.get_level_0() == irep_idt{});
REQUIRE(ssa.get_level_1() == "3");
REQUIRE(ssa.get_level_2() == irep_idt{});
REQUIRE(ssa.get_original_expr() == symbol);
REQUIRE(ssa.get_identifier() == "sym@3");
REQUIRE(ssa.get_l1_object_identifier() == "sym@3");
}
WHEN("set_level_2")
{
ssa.set_level_2(7);
REQUIRE(ssa.get_level_0() == irep_idt{});
REQUIRE(ssa.get_level_1() == irep_idt{});
REQUIRE(ssa.get_level_2() == "7");
REQUIRE(ssa.get_original_expr() == symbol);
REQUIRE(ssa.get_identifier() == "sym#7");
REQUIRE(ssa.get_l1_object_identifier() == "sym");
}
}
}
TEST_CASE("Set expression", "[unit][util][ssa_expr]")
{
GIVEN("An SSA expression constructed from a symbol")
{
const signedbv_typet int_type{32};
const array_typet array_type{int_type, from_integer(10, int_type)};
const symbol_exprt symbol{"sym", array_type};
const index_exprt index{symbol, from_integer(9, int_type)};
ssa_exprt ssa(symbol);
ssa.set_level_0(1);
ssa.set_level_1(3);
ssa.set_level_2(7);
WHEN("call set_expression with an index_exprt")
{
ssa.set_expression(index);
THEN("Indices are preserved")
{
REQUIRE(ssa.get_level_0() == "1");
REQUIRE(ssa.get_level_1() == "3");
REQUIRE(ssa.get_level_2() == "7");
}
THEN("The underlying expression has been replaced")
{
REQUIRE(ssa.get_original_expr() == index);
}
THEN("The identifiers are updated")
{
REQUIRE(ssa.get_identifier() == "sym!1@3#7[[9]]");
REQUIRE(ssa.get_l1_object_identifier() == "sym!1@3[[9]]");
}
}
}
}
TEST_CASE("ssa_exprt::get_object_name", "[unit][util][ssa_expr]")
{
GIVEN("An ssa_exprt constructed from a symbol")
{
const signedbv_typet int_type{32};
const symbol_exprt symbol{"sym", int_type};
const ssa_exprt ssa{symbol};
THEN("The object name is the same as the symbol name")
{
REQUIRE(ssa.get_object_name() == "sym");
}
}
GIVEN("An expression containing member access, array access and a symbol")
{
const signedbv_typet int_type{32};
const array_typet array_type{int_type, from_integer(10, int_type)};
std::vector<struct_typet::componentt> components;
components.emplace_back("array_field", array_type);
const struct_typet struct_type{components};
const symbol_exprt symbol{"sym", struct_type};
const index_exprt index{member_exprt{symbol, components.back()},
from_integer(9, int_type)};
const ssa_exprt ssa{symbol};
THEN("The object name is the same as the symbol")
{
REQUIRE(ssa.get_object_name() == "sym");
}
}
}
TEST_CASE("ssa_exprt::get_l1_object", "[unit][util][ssa_expr]")
{
const signedbv_typet int_type{32};
const array_typet array_type{int_type, from_integer(10, int_type)};
GIVEN("An ssa_exprt obtained from a symbol")
{
const symbol_exprt symbol{"sym", int_type};
ssa_exprt ssa{symbol};
ssa.set_level_0(1);
ssa.set_level_1(3);
ssa.set_level_2(7);
// Check we have constructed the desired SSA expression
REQUIRE(ssa.get_identifier() == "sym!1@3#7");
WHEN("get_l1_object is called on the SSA expression")
{
const ssa_exprt l1_object = ssa.get_l1_object();
THEN("level 0 and level 1 are the same, l2 is removed")
{
REQUIRE(l1_object.get_level_0() == "1");
REQUIRE(l1_object.get_level_1() == "3");
REQUIRE(l1_object.get_level_2() == irep_idt{});
REQUIRE(l1_object.get_identifier() == "sym!1@3");
}
}
}
GIVEN("An ssa_exprt containing member access, array access and a symbol")
{
std::vector<struct_typet::componentt> components;
components.emplace_back("array_field", array_type);
const struct_typet struct_type{components};
const symbol_exprt symbol{"sym", struct_type};
const index_exprt index{member_exprt{symbol, components.back()},
from_integer(9, int_type)};
ssa_exprt ssa{index};
ssa.set_level_0(1);
ssa.set_level_1(3);
ssa.set_level_2(7);
// Check we have constructed the desired SSA expression
REQUIRE(ssa.get_identifier() == "sym!1@3#7..array_field[[9]]");
WHEN("get_l1_object is called on the SSA expression")
{
const ssa_exprt l1_object = ssa.get_l1_object();
THEN("level 0 and level 1 are the same, l2 is removed")
{
REQUIRE(l1_object.get_level_0() == "1");
REQUIRE(l1_object.get_level_1() == "3");
REQUIRE(l1_object.get_level_2() == irep_idt{});
REQUIRE(l1_object.get_identifier() == "sym!1@3");
}
}
}
GIVEN("An ssa_exprt with its L2 index set")
{
const symbol_exprt symbol{"sym", int_type};
ssa_exprt ssa{symbol};
ssa.set_level_2(7);
WHEN("Its L1 object is taken")
{
const ssa_exprt l1_object = ssa.get_l1_object();
THEN("It should compare equal to the base symbol")
{
REQUIRE(l1_object == ssa_exprt{symbol});
}
}
}
}
|
