diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 8188e629d5d8..376717b9b767 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1894,11 +1894,22 @@ exprt lower_address_of_array_index(exprt expr) expr_try_dynamic_cast(address_of_expr->object()); if(!array_index_expr) return; - expr = plus_exprt{ - address_of_exprt{ - array_index_expr->array(), - type_checked_cast(address_of_expr->type())}, - array_index_expr->index()}; + // The pointer type of the new address_of must be a pointer to the + // array element type so that pointer arithmetic scales by the + // correct element size. For nested arrays like int a[3][4], + // &a[1] gets type int(*)[4] so that +1 adds sizeof(int[4]) = 16. + // The result is typecast back to the original address_of type to + // keep the types of enclosing expressions consistent. + const auto &outer_ptr_type = + type_checked_cast(address_of_expr->type()); + const pointer_typet element_pointer_type( + array_index_expr->type(), outer_ptr_type.get_width()); + exprt lowered = plus_exprt( + address_of_exprt(array_index_expr->array(), element_pointer_type), + array_index_expr->index()); + if(element_pointer_type != outer_ptr_type) + lowered = typecast_exprt(std::move(lowered), outer_ptr_type); + expr = std::move(lowered); }); return expr; } diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 2817ba012fea..184afcce4128 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -416,16 +416,21 @@ smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr) define_index_identifiers(expr); const exprt substituted = substitute_defined_padding( substitute_identifiers(expr, expression_identifiers)); - track_expression_objects(substituted, ns, object_map); + // Lower address-of-array-index before scanning for pointer sizes, so + // that any new pointer types introduced by the lowering (e.g. a + // pointer to a row type in a nested array) are registered in the + // pointer size map. + const exprt lowered = lower_address_of_array_index(substituted); + track_expression_objects(lowered, ns, object_map); associate_pointer_sizes( - substituted, + lowered, ns, pointer_sizes_map, object_map, object_size_function.make_application, is_dynamic_object_function.make_application); return ::convert_expr_to_smt( - substituted, + lowered, object_map, pointer_sizes_map, object_size_function.make_application, diff --git a/unit/solvers/smt2_incremental/nested_array_addr.cpp b/unit/solvers/smt2_incremental/nested_array_addr.cpp new file mode 100644 index 000000000000..70cdee1e2b8c --- /dev/null +++ b/unit/solvers/smt2_incremental/nested_array_addr.cpp @@ -0,0 +1,87 @@ +// Author: Michael Tautschnig + +/// \file +/// Unit tests for lower_address_of_array_index with nested array indices. + +#include +#include +#include +#include +#include +#include +#include + +#include +#include + +TEST_CASE( + "lower_address_of_array_index nested array uses correct element pointer type", + "[core][smt2_incremental]") +{ + // For int a[3][4], &a[i][j] is lowered by two passes of + // lower_address_of_array_index: + // &a[i][j] -> &(a[i])[j] -> (int*)&(a[i]) + j + // &(a[i]) -> (int(*)[4])&a + i + // The inner &(a[i]) must get pointer-to-element type int(*)[4], not + // int* (which is the outer address_of type). Using int* makes +i + // scale by sizeof(int)=4 instead of sizeof(int[4])=16. + + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); + + const signedbv_typet int_type{32}; + const unsignedbv_typet idx_type{64}; + const array_typet inner_array_type{ + int_type, from_integer(4, signed_size_type())}; + const array_typet outer_array_type{ + inner_array_type, from_integer(3, signed_size_type())}; + + const symbol_exprt a{"a", outer_array_type}; + const exprt i = from_integer(1, idx_type); + const exprt j = from_integer(2, idx_type); + + // Build &a[i][j]: address_of(index(index(a, i), j)) + const index_exprt a_i{a, i}; + const index_exprt a_i_j{a_i, j}; + const address_of_exprt addr_a_i_j{a_i_j}; + + // The outer pointer type is int* (pointer to int_type). + const pointer_typet outer_ptr_type = + type_checked_cast(addr_a_i_j.type()); + REQUIRE(outer_ptr_type.base_type() == int_type); + + const exprt lowered = lower_address_of_array_index(addr_a_i_j); + + // After lowering, the result should be: + // (int*)( (int(*)[4])&a + i ) + j + // i.e., a plus_exprt with: + // - lhs: typecast from (int(*)[4])&a+i to int* + // - rhs: j + // The key check: the inner plus must use pointer-to-inner_array_type, + // not pointer-to-int_type. + + // The top-level should be a plus of something and j. + const auto *top_plus = expr_try_dynamic_cast(lowered); + REQUIRE(top_plus != nullptr); + CHECK(top_plus->op1() == j); + + // The lhs should be a typecast (because the inner element pointer type + // differs from the outer pointer type). + const auto *cast = expr_try_dynamic_cast(top_plus->op0()); + REQUIRE(cast != nullptr); + CHECK(cast->type() == outer_ptr_type); + + // Inside the typecast: a plus of address_of(a) with element pointer + // type and i. + const auto *inner_plus = expr_try_dynamic_cast(cast->op()); + REQUIRE(inner_plus != nullptr); + CHECK(inner_plus->op1() == i); + + const auto *inner_addr = + expr_try_dynamic_cast(inner_plus->op0()); + REQUIRE(inner_addr != nullptr); + // The inner address_of must have pointer-to-inner_array_type. + const auto &inner_ptr_type = + type_checked_cast(inner_addr->type()); + CHECK(inner_ptr_type.base_type() == inner_array_type); +}