From 00d968c88d10178fbfd70240c6e071d34d9e53a5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 21:14:12 +0000 Subject: [PATCH] SMT2: only typecast array index for fixed-width bitvector index types When converting an array store/select, the index was unconditionally typecast to the array's index type, which is wrong once that index type is a mathematical integer or a struct (e.g. a map key): the cast is unnecessary (the sorts already match) and, for struct keys, ill-formed. Coerce the index to the array's declared index type only when that type is a fixed-width bitvector and differs from the index expression's type; otherwise emit the index unchanged. The decision is keyed on the *destination* (array) index type so that an integer- or differently-sized-bitvector-sourced index is still coerced when the array's index type is a bitvector -- in particular when array_typet::index_type() falls back to c_index_type() for an array without an ID_C_index_type annotation, which would otherwise feed an integer-sorted index into a bitvector-sorted store/select (ill-sorted SMT). A DATA_INVARIANT makes the remaining assumption explicit: a bitvector index requires the array's index type to be a bitvector too. The selection logic (previously duplicated verbatim in convert_with and convert_index) is factored into a single cast_array_index() helper. Enum and enum-tag index types are treated as bitvector-like; convert_typecast resolves an enum-tag destination via ns.follow_tag, so the emission stays valid. A unit test (unit/solvers/smt2/smt2_conv.cpp) pins the serialization for all three cases -- mathematical-integer index, matching-width bitvector index, and differing-width bitvector index -- for both select and store. Co-authored-by: Kiro --- src/solvers/smt2/smt2_conv.cpp | 42 ++++++++++++++++++++-- unit/solvers/smt2/smt2_conv.cpp | 64 +++++++++++++++++++++++++++++++++ 2 files changed, 103 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e5a7d4ff0f2..0d0b5f2d511 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -4538,6 +4538,36 @@ void smt2_convt::convert_floatbv_fma(const floatbv_fma_exprt &expr) convert_floatbv(expr); } +/// Coerce \p index to the array's declared index type \p array_index_type when +/// the array uses a fixed-width bitvector-like index sort and the index does +/// not already have that type; otherwise (mathematical-integer or struct / +/// map-key index sorts, which are expected to match already) emit it unchanged. +/// convert_typecast coerces an integer or differently-sized bitvector source. +static exprt cast_array_index(exprt index, const typet &array_index_type) +{ + const auto is_bv = [](const typet &t) + { + return t.id() == ID_unsignedbv || t.id() == ID_signedbv || + t.id() == ID_c_bool || t.id() == ID_c_enum || + t.id() == ID_c_enum_tag; + }; + + if(array_index_type != index.type() && is_bv(array_index_type)) + return typecast_exprt(std::move(index), array_index_type); + + // Emitting the index unchanged is only well-sorted when the sorts already + // match. In particular a fixed-width bitvector index requires the array's + // index type to be a bitvector too; array_typet::index_type() falls back to + // c_index_type() (a bitvector) for arrays without an ID_C_index_type + // annotation, so an integer-sorted index into such an array is handled by + // the cast above rather than slipping through here. + DATA_INVARIANT( + array_index_type == index.type() || !is_bv(index.type()), + "a bitvector array index requires a bitvector array index type"); + + return index; +} + void smt2_convt::convert_with(const with_exprt &expr) { INVARIANT( @@ -4552,10 +4582,13 @@ void smt2_convt::convert_with(const with_exprt &expr) if(use_array_theory(expr)) { + const exprt where = + cast_array_index(expr.where(), array_type.index_type()); + out << "(store "; convert_expr(expr.old()); out << " "; - convert_expr(typecast_exprt(expr.where(), array_type.index_type())); + convert_expr(where); out << " "; convert_expr(expr.new_value()); out << ")"; @@ -4768,13 +4801,16 @@ void smt2_convt::convert_index(const index_exprt &expr) if(use_array_theory(expr.array())) { + const exprt index = + cast_array_index(expr.index(), array_type.index_type()); + if(expr.is_boolean() && !use_array_of_bool) { out << "(= "; out << "(select "; convert_expr(expr.array()); out << " "; - convert_expr(typecast_exprt(expr.index(), array_type.index_type())); + convert_expr(index); out << ")"; out << " #b1)"; } @@ -4783,7 +4819,7 @@ void smt2_convt::convert_index(const index_exprt &expr) out << "(select "; convert_expr(expr.array()); out << " "; - convert_expr(typecast_exprt(expr.index(), array_type.index_type())); + convert_expr(index); out << ")"; } } diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index 80ebbcffcad..8654dece49a 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/unit/solvers/smt2/smt2_conv.cpp @@ -115,6 +115,70 @@ TEST_CASE("smt2_convt reduction operators", "[core][solvers][smt2]") } } +TEST_CASE("smt2_convt array index typecast", "[core][solvers][smt2]") +{ + // The array store/select index is only typecast to the array's declared + // index type when that index type is a fixed-width bitvector and differs + // from the index expression's type. Mathematical-integer (and struct / + // map-key) index sorts are emitted unchanged; differing-width bitvector + // indices are coerced. + const unsignedbv_typet u8{8}; + const unsignedbv_typet u32{32}; + + SECTION("mathematical-integer index is emitted without a typecast") + { + array_typet array_type{u8, from_integer(10, size_type())}; + array_type.index_type_nonconst() = integer_typet(); + const symbol_exprt a{"a", array_type}; + const symbol_exprt i{"i", integer_typet()}; + + // select + REQUIRE( + get_assert(equal_exprt{index_exprt{a, i}, from_integer(0, u8)}) == + "(assert (= (select a i) (_ bv0 8)))"); + + // store + const with_exprt store{a, i, from_integer(0, u8)}; + REQUIRE( + get_assert(equal_exprt{store, a}) == + "(assert (= (store a i (_ bv0 8)) a))"); + } + + SECTION("matching-width bitvector index is emitted without a typecast") + { + array_typet array_type{u8, from_integer(10, u32)}; + array_type.index_type_nonconst() = u32; + const symbol_exprt a{"a", array_type}; + const symbol_exprt i{"i", u32}; + + REQUIRE( + get_assert(equal_exprt{index_exprt{a, i}, from_integer(0, u8)}) == + "(assert (= (select a i) (_ bv0 8)))"); + } + + SECTION("differing-width bitvector index is coerced to the array index type") + { + array_typet array_type{u8, from_integer(10, u32)}; + array_type.index_type_nonconst() = u32; + const symbol_exprt a{"a", array_type}; + const symbol_exprt i{"i", u8}; // narrower than the u32 array index type + + // select: i must be widened to 32 bits before indexing + const std::string select_assert = + get_assert(equal_exprt{index_exprt{a, i}, from_integer(0, u8)}); + INFO("select: " << select_assert); + REQUIRE(select_assert.find("(select a i)") == std::string::npos); + REQUIRE(select_assert.find("(select a ((_ ") != std::string::npos); + + // store: likewise + const with_exprt store{a, i, from_integer(0, u8)}; + const std::string store_assert = get_assert(equal_exprt{store, a}); + INFO("store: " << store_assert); + REQUIRE(store_assert.find("(store a i ") == std::string::npos); + REQUIRE(store_assert.find("(store a ((_ ") != std::string::npos); + } +} + TEST_CASE( "smt2_convt no unary concat for zero-width operand", "[core][solvers][smt2]")