SMT2 Incremental: support array-to-array typecasts

regression/cbmc/SIMD1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend no-new-smt
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -258,6 +258,15 @@ static smt_termt convert_expr_to_smt(
   const auto &from_term = converted.at(cast.op());
   const typet &from_type = cast.op().type();
   const typet &to_type = cast.type();
+  // Array-to-array typecasts are handled by the decision procedure
+  // (define_array_typecast_function) and the expression should have been
+  // substituted before reaching this point.
+  if(
+    can_cast_type<array_typet>(to_type) &&
+    can_cast_type<array_typet>(from_type))
+  {
+    UNHANDLED_CASE;
+  }
   if(type_try_dynamic_cast<bool_typet>(to_type))
     return make_not_zero(from_term, cast.op().type());
   if(const auto c_bool_type = type_try_dynamic_cast<c_bool_typet>(to_type))

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -4,6 +4,7 @@
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/range.h>
@@ -20,6 +21,7 @@
 #include <solvers/smt2_incremental/encoding/nondet_padding.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
+#include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 
@@ -81,12 +83,18 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
   {
     const exprt &expr_node = *stack.top();
     stack.pop();
+    const bool is_array_typecast = [&]()
+    {
+      const auto *typecast = expr_try_dynamic_cast<typecast_exprt>(expr_node);
+      return typecast && can_cast_type<array_typet>(typecast->type()) &&
+             can_cast_type<array_typet>(typecast->op().type());
+    }();
     if(
       can_cast_expr<symbol_exprt>(expr_node) ||
       can_cast_expr<array_exprt>(expr_node) ||
       can_cast_expr<array_of_exprt>(expr_node) ||
       can_cast_expr<nondet_symbol_exprt>(expr_node) ||
-      can_cast_expr<string_constantt>(expr_node))
+      can_cast_expr<string_constantt>(expr_node) || is_array_typecast)
     {
       dependent_expressions.push_back(expr_node);
     }
@@ -162,6 +170,90 @@ void smt2_incremental_decision_proceduret::define_array_function(
   expression_identifiers.emplace(array, array_identifier);
 }
 
+/// \brief Defines a function of array sort for a typecast between two
+///   array types and asserts element-by-element reinterpretation constraints.
+/// \details The target array elements are computed from the source array
+///   elements by concatenating or extracting bit vector values as needed.
+///   Higher-indexed source elements occupy the more significant bit
+///   positions when widening elements.
+void smt2_incremental_decision_proceduret::define_array_typecast_function(
+  const typecast_exprt &typecast)
+{
+  const auto &source_array_type =
+    type_checked_cast<array_typet>(typecast.op().type());
+  const auto &target_array_type =
+    type_checked_cast<array_typet>(typecast.type());
+
+  const smt_sortt target_sort = convert_type_to_smt_sort(target_array_type);
+  const smt_identifier_termt array_id{
+    "array_" + std::to_string(array_sequence()), target_sort};
+  solver_process->send(smt_declare_function_commandt{array_id, {}});
+  identifier_table.emplace(array_id.identifier(), array_id);
+
+  const smt_termt source_term = convert_expr_to_smt(typecast.op());
+
+  const auto source_elem_width =
+    to_bitvector_type(source_array_type.element_type()).get_width();
+  const auto target_elem_width =
+    to_bitvector_type(target_array_type.element_type()).get_width();
+  const auto target_size =
+    numeric_cast_v<std::size_t>(to_constant_expr(target_array_type.size()));
+
+  const auto &target_index_type = target_array_type.index_type();
+  const auto &source_index_type = source_array_type.index_type();
+
+  for(std::size_t i = 0; i < target_size; ++i)
+  {
+    const smt_termt index =
+      convert_expr_to_smt(from_integer(i, target_index_type));
+    smt_termt element_value = [&]() -> smt_termt
+    {
+      if(target_elem_width == source_elem_width)
+      {
+        const smt_termt src_index =
+          convert_expr_to_smt(from_integer(i, source_index_type));
+        return smt_array_theoryt::select(source_term, src_index);
+      }
+      else if(target_elem_width > source_elem_width)
+      {
+        // Widening: combine multiple source elements via concatenation.
+        const std::size_t ratio = target_elem_width / source_elem_width;
+        // Start with the least significant source element.
+        smt_termt result = smt_array_theoryt::select(
+          source_term,
+          convert_expr_to_smt(from_integer(i * ratio, source_index_type)));
+        // Higher-indexed source elements go in the more significant
+        // bit positions.
+        for(std::size_t j = 1; j < ratio; ++j)
+        {
+          smt_termt src_elem = smt_array_theoryt::select(
+            source_term,
+            convert_expr_to_smt(
+              from_integer(i * ratio + j, source_index_type)));
+          result = smt_bit_vector_theoryt::concat(src_elem, result);
+        }
+        return result;
+      }
+      else
+      {
+        // Narrowing: extract portion of a source element.
+        const std::size_t ratio = source_elem_width / target_elem_width;
+        const std::size_t src_idx = i / ratio;
+        const std::size_t offset = (i % ratio) * target_elem_width;
+        smt_termt src_elem = smt_array_theoryt::select(
+          source_term,
+          convert_expr_to_smt(from_integer(src_idx, source_index_type)));
+        return smt_bit_vector_theoryt::extract(
+          offset + target_elem_width - 1, offset)(src_elem);
+      }
+    }();
+    solver_process->send(smt_assert_commandt{smt_core_theoryt::equal(
+      smt_array_theoryt::select(array_id, index), element_value)});
+  }
+
+  expression_identifiers.emplace(typecast, array_id);
+}
+
 void send_function_definition(
   const exprt &expr,
   const irep_idt &symbol_identifier,
@@ -228,6 +320,16 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
     {
       define_array_function(*string);
     }
+    else if(
+      const auto typecast = expr_try_dynamic_cast<typecast_exprt>(current))
+    {
+      if(
+        can_cast_type<array_typet>(typecast->type()) &&
+        can_cast_type<array_typet>(typecast->op().type()))
+      {
+        define_array_typecast_function(*typecast);
+      }
+    }
     else if(
       const auto nondet_symbol =
         expr_try_dynamic_cast<nondet_symbol_exprt>(current))

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -23,6 +23,7 @@
 class namespacet;
 class smt_base_solver_processt; // IWYU pragma: keep
 class string_constantt;
+class typecast_exprt;
 class union_tag_typet;
 
 class smt2_incremental_decision_proceduret final
@@ -77,6 +78,10 @@ class smt2_incremental_decision_proceduret final
   /// `array_of_exprt`.
   template <typename t_exprt>
   void define_array_function(const t_exprt &array);
+  /// \brief Defines a function of array sort for a typecast between two
+  ///   array types and asserts element-by-element reinterpretation
+  ///   constraints.
+  void define_array_typecast_function(const typecast_exprt &typecast);
   /// \brief Generate and send to the SMT solver clauses asserting that each
   /// array element is as specified by \p array.
   void initialize_array_elements(

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1465,6 +1465,34 @@ TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
   }
 }
 
+TEST_CASE(
+  "Array to array typecast in convert_expr_to_smt",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  const auto source_type =
+    array_typet{signedbv_typet{32}, from_integer(4, c_index_type())};
+  const auto target_type =
+    array_typet{signedbv_typet{64}, from_integer(2, c_index_type())};
+  const symbol_exprt source_array{"src_array", source_type};
+  const typecast_exprt cast{source_array, target_type};
+  const cbmc_invariants_should_throwt invariants_throw;
+  SECTION("Array to array typecast is not handled directly")
+  {
+    CHECK_THROWS(test.convert(cast));
+  }
+  SECTION("Sort conversion for array types")
+  {
+    CHECK(
+      convert_type_to_smt_sort(source_type) ==
+      smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{32}});
+    CHECK(
+      convert_type_to_smt_sort(target_type) ==
+      smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{64}});
+  }
+}
+
 TEST_CASE(
   "expr to smt conversion for address of operator",
   "[core][smt2_incremental]")