SMT2: only typecast array index for fixed-width bitvector index types

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 << ")";
       }
     }

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]")