Skip to content

Commit 8878f15

Browse files
author
Enrico Steffinlongo
committed
Add support for array_of of array index_exprt
1 parent 175a609 commit 8878f15

File tree

2 files changed

+27
-2
lines changed

2 files changed

+27
-2
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 22 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1813,6 +1813,25 @@ at_scope_exitt<functiont> at_scope_exit(functiont exit_function)
18131813
}
18141814
#endif
18151815

1816+
exprt lower_address_of_array_index(exprt expr)
1817+
{
1818+
expr.visit_pre([](exprt &expr) {
1819+
const auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr);
1820+
if(!address_of_expr)
1821+
return;
1822+
const auto array_index_expr =
1823+
expr_try_dynamic_cast<index_exprt>(address_of_expr->object());
1824+
if(!array_index_expr)
1825+
return;
1826+
expr = plus_exprt{
1827+
address_of_exprt{
1828+
array_index_expr->array(),
1829+
type_checked_cast<pointer_typet>(address_of_expr->type())},
1830+
array_index_expr->index()};
1831+
});
1832+
return expr;
1833+
}
1834+
18161835
smt_termt convert_expr_to_smt(
18171836
const exprt &expr,
18181837
const smt_object_mapt &object_map,
@@ -1830,13 +1849,14 @@ smt_termt convert_expr_to_smt(
18301849
const auto end_conversion = at_scope_exit([&]() { in_conversion = false; });
18311850
#endif
18321851
sub_expression_mapt sub_expression_map;
1833-
expr.visit_post([&](const exprt &expr) {
1852+
const auto lowered_expr = lower_address_of_array_index(expr);
1853+
lowered_expr.visit_post([&](const exprt &expr) {
18341854
const auto find_result = sub_expression_map.find(expr);
18351855
if(find_result != sub_expression_map.cend())
18361856
return;
18371857
smt_termt term = dispatch_expr_to_smt_conversion(
18381858
expr, sub_expression_map, object_map, pointer_sizes, object_size);
18391859
sub_expression_map.emplace_hint(find_result, expr, std::move(term));
18401860
});
1841-
return std::move(sub_expression_map.at(expr));
1861+
return std::move(sub_expression_map.at(lowered_expr));
18421862
}

src/solvers/smt2_incremental/convert_expr_to_smt.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,11 @@ class typet;
1616
/// stored as sort ast (abstract syntax tree).
1717
smt_sortt convert_type_to_smt_sort(const typet &type);
1818

19+
/// \brief Lower the `address_of(array[idx])` sub expressions in \p expr to
20+
/// `idx + address_of(array)`, so that it can be fed to
21+
/// `convert_expr_to_smt`.
22+
exprt lower_address_of_array_index(exprt expr);
23+
1924
/// \brief Converts the \p expression to an smt encoding of the same expression
2025
/// stored as term ast (abstract syntax tree).
2126
smt_termt convert_expr_to_smt(

0 commit comments

Comments
 (0)