Skip to content

Commit 5258eba

Browse files
thomasspriggsthomasspriggs
committed
Add encoding of with_exprt
1 parent 9527c69 commit 5258eba

File tree

2 files changed

+225
-0
lines changed

2 files changed

+225
-0
lines changed

‎src/solvers/smt2_incremental/encoding/struct_encoding.cpp‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,57 @@ typet struct_encodingt::encode(typet type) const
5050
return type;
5151
}
5252

53+
/// \brief Extracts the component/field names and new values from a `with_exprt`
54+
/// which expresses a new struct value where one or more members of a
55+
/// struct have had their values substituted with new values.
56+
/// \note This is implemented using direct access to the operands and other
57+
/// underlying irept interfaces, because the interface for `with_exprt`
58+
/// only supports a single `where` / `new_value` pair and does not
59+
/// support extracting the name from the `where` operand.
60+
static std::unordered_map<irep_idt, exprt>
61+
extricate_updates(const with_exprt &struct_expr)
62+
{
63+
std::unordered_map<irep_idt, exprt> pairs;
64+
auto current_operand = struct_expr.operands().begin();
65+
// Skip the struct being updated in order to begin with the pairs.
66+
current_operand++;
67+
while(current_operand != struct_expr.operands().end())
68+
{
69+
INVARIANT(
70+
current_operand->id() == ID_member_name,
71+
"operand is expected to be the name of a member");
72+
auto name = current_operand->find(ID_component_name).id();
73+
++current_operand;
74+
INVARIANT(
75+
current_operand != struct_expr.operands().end(),
76+
"every name is expected to be followed by a paired value");
77+
pairs[name] = *current_operand;
78+
++current_operand;
79+
}
80+
POSTCONDITION(!pairs.empty());
81+
return pairs;
82+
}
83+
84+
static exprt encode(const with_exprt &with, const namespacet &ns)
85+
{
86+
const auto tag_type = type_checked_cast<struct_tag_typet>(with.type());
87+
const auto struct_type =
88+
type_checked_cast<struct_typet>(ns.follow(with.type()));
89+
const auto updates = extricate_updates(with);
90+
const auto components =
91+
make_range(struct_type.components())
92+
.map([&](const struct_union_typet::componentt &component) -> exprt {
93+
const auto &update = updates.find(component.get_name());
94+
if(update != updates.end())
95+
return update->second;
96+
else
97+
return member_exprt{
98+
with.old(), component.get_name(), component.type()};
99+
})
100+
.collect<exprt::operandst>();
101+
return struct_exprt{components, tag_type};
102+
}
103+
53104
static exprt encode(const struct_exprt &struct_expr)
54105
{
55106
INVARIANT(
@@ -111,6 +162,11 @@ exprt struct_encodingt::encode(exprt expr) const
111162
{
112163
exprt &current = *work_queue.front();
113164
work_queue.pop();
165+
// Note that "with" expressions are handled before type encoding in order to
166+
// facilitate checking that they are applied to structs rather than arrays.
167+
if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(current))
168+
if(can_cast_type<struct_tag_typet>(current.type()))
169+
current = ::encode(*with_expr, ns);
114170
current.type() = encode(current.type());
115171
if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(current))
116172
current = ::encode(*struct_expr);

‎unit/solvers/smt2_incremental/encoding/struct_encoding.cpp‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,13 @@ TEST_CASE("struct encoding of types", "[core][smt2_incremental]")
7171
}
7272
}
7373

74+
exprt make_member_name_expression(const irep_idt component_name)
75+
{
76+
exprt result{ID_member_name};
77+
result.set(ID_component_name, component_name);
78+
return result;
79+
}
80+
7481
TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
7582
{
7683
const struct_union_typet::componentst component_types{
@@ -150,6 +157,168 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
150157
REQUIRE(test.struct_encoding.encode(input) == expected);
151158
}
152159
}
160+
SECTION("with expression producing new struct with substituted member")
161+
{
162+
SECTION("First member")
163+
{
164+
const with_exprt with{
165+
symbol_expr,
166+
make_member_name_expression("green"),
167+
from_integer(0, signedbv_typet{32})};
168+
const concatenation_exprt expected{
169+
{from_integer(0, signedbv_typet{32}),
170+
extractbits_exprt{symbol_expr_as_bv, 39, 24, unsignedbv_typet{16}},
171+
extractbits_exprt{symbol_expr_as_bv, 23, 0, signedbv_typet{24}}},
172+
bv_typet{72}};
173+
REQUIRE(test.struct_encoding.encode(with) == expected);
174+
}
175+
SECTION("Second member")
176+
{
177+
const with_exprt with{
178+
symbol_expr,
179+
make_member_name_expression("eggs"),
180+
from_integer(0, unsignedbv_typet{16})};
181+
const concatenation_exprt expected{
182+
{extractbits_exprt{symbol_expr_as_bv, 71, 40, signedbv_typet{32}},
183+
from_integer(0, unsignedbv_typet{16}),
184+
extractbits_exprt{symbol_expr_as_bv, 23, 0, signedbv_typet{24}}},
185+
bv_typet{72}};
186+
REQUIRE(test.struct_encoding.encode(with) == expected);
187+
}
188+
SECTION("Third member")
189+
{
190+
const with_exprt with{
191+
symbol_expr,
192+
make_member_name_expression("ham"),
193+
from_integer(0, signedbv_typet{24})};
194+
const concatenation_exprt expected{
195+
{extractbits_exprt{symbol_expr_as_bv, 71, 40, signedbv_typet{32}},
196+
extractbits_exprt{symbol_expr_as_bv, 39, 24, unsignedbv_typet{16}},
197+
from_integer(0, signedbv_typet{24})},
198+
bv_typet{72}};
199+
REQUIRE(test.struct_encoding.encode(with) == expected);
200+
}
201+
SECTION("First and second members")
202+
{
203+
const concatenation_exprt expected{
204+
{from_integer(0, signedbv_typet{32}),
205+
from_integer(1, unsignedbv_typet{16}),
206+
extractbits_exprt{symbol_expr_as_bv, 23, 0, signedbv_typet{24}}},
207+
bv_typet{72}};
208+
SECTION("Operands in field order")
209+
{
210+
with_exprt with_in_order{
211+
symbol_expr,
212+
make_member_name_expression("green"),
213+
from_integer(0, signedbv_typet{32})};
214+
with_in_order.operands().push_back(make_member_name_expression("eggs"));
215+
with_in_order.operands().push_back(
216+
from_integer(1, unsignedbv_typet{16}));
217+
REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
218+
}
219+
SECTION("Operands in reverse order vs fields")
220+
{
221+
with_exprt with_reversed{
222+
symbol_expr,
223+
make_member_name_expression("eggs"),
224+
from_integer(1, unsignedbv_typet{16})};
225+
with_reversed.operands().push_back(
226+
make_member_name_expression("green"));
227+
with_reversed.operands().push_back(from_integer(0, signedbv_typet{32}));
228+
REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
229+
}
230+
}
231+
SECTION("First and third members")
232+
{
233+
const concatenation_exprt expected{
234+
{from_integer(0, signedbv_typet{32}),
235+
extractbits_exprt{symbol_expr_as_bv, 39, 24, unsignedbv_typet{16}},
236+
from_integer(1, signedbv_typet{24})},
237+
bv_typet{72}};
238+
SECTION("Operands in field order")
239+
{
240+
with_exprt with_in_order{
241+
symbol_expr,
242+
make_member_name_expression("green"),
243+
from_integer(0, signedbv_typet{32})};
244+
with_in_order.operands().push_back(make_member_name_expression("ham"));
245+
with_in_order.operands().push_back(from_integer(1, signedbv_typet{24}));
246+
REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
247+
}
248+
SECTION("Operands in reverse order vs fields")
249+
{
250+
with_exprt with_reversed{
251+
symbol_expr,
252+
make_member_name_expression("ham"),
253+
from_integer(1, signedbv_typet{24})};
254+
with_reversed.operands().push_back(
255+
make_member_name_expression("green"));
256+
with_reversed.operands().push_back(from_integer(0, signedbv_typet{32}));
257+
REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
258+
}
259+
}
260+
SECTION("Second and third members")
261+
{
262+
const concatenation_exprt expected{
263+
{extractbits_exprt{symbol_expr_as_bv, 71, 40, signedbv_typet{32}},
264+
from_integer(0, unsignedbv_typet{16}),
265+
from_integer(1, signedbv_typet{24})},
266+
bv_typet{72}};
267+
SECTION("Operands in field order")
268+
{
269+
with_exprt with_in_order{
270+
symbol_expr,
271+
make_member_name_expression("eggs"),
272+
from_integer(0, unsignedbv_typet{16})};
273+
with_in_order.operands().push_back(make_member_name_expression("ham"));
274+
with_in_order.operands().push_back(from_integer(1, signedbv_typet{24}));
275+
REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
276+
}
277+
SECTION("Operands in reverse order vs fields")
278+
{
279+
with_exprt with_reversed{
280+
symbol_expr,
281+
make_member_name_expression("ham"),
282+
from_integer(1, signedbv_typet{24})};
283+
with_reversed.operands().push_back(make_member_name_expression("eggs"));
284+
with_reversed.operands().push_back(
285+
from_integer(0, unsignedbv_typet{16}));
286+
REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
287+
}
288+
}
289+
SECTION("All members")
290+
{
291+
const concatenation_exprt expected{
292+
{from_integer(1, signedbv_typet{32}),
293+
from_integer(2, unsignedbv_typet{16}),
294+
from_integer(3, signedbv_typet{24})},
295+
bv_typet{72}};
296+
SECTION("Operands in field order")
297+
{
298+
with_exprt with{
299+
symbol_expr,
300+
make_member_name_expression("green"),
301+
from_integer(1, signedbv_typet{32})};
302+
with.operands().push_back(make_member_name_expression("eggs"));
303+
with.operands().push_back(from_integer(2, unsignedbv_typet{16}));
304+
with.operands().push_back(make_member_name_expression("ham"));
305+
with.operands().push_back(from_integer(3, signedbv_typet{24}));
306+
REQUIRE(test.struct_encoding.encode(with) == expected);
307+
}
308+
SECTION("Operands out of order vs fields")
309+
{
310+
with_exprt with{
311+
symbol_expr,
312+
make_member_name_expression("eggs"),
313+
from_integer(2, unsignedbv_typet{16})};
314+
with.operands().push_back(make_member_name_expression("ham"));
315+
with.operands().push_back(from_integer(3, signedbv_typet{24}));
316+
with.operands().push_back(make_member_name_expression("green"));
317+
with.operands().push_back(from_integer(1, signedbv_typet{32}));
318+
REQUIRE(test.struct_encoding.encode(with) == expected);
319+
}
320+
}
321+
}
153322
}
154323

155324
TEST_CASE(

0 commit comments

Comments
 (0)