Implement incremental SMT2 support for bswap_exprt

Implements byte swapping in the incremental SMT2 decision procedure and
adds unit tests. Regression test `gcc_bswap1` now passes.

Fixes: #8064

Author: tautschnig

regression/cbmc/gcc_bswap1/test.desc

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

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1432,9 +1432,60 @@ static smt_termt convert_expr_to_smt(
   const bswap_exprt &byte_swap,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for byte swap expression: " +
-    byte_swap.pretty());
+  const auto operand_term = converted.at(byte_swap.op());
+  const auto &operand_type = byte_swap.op().type();
+
+  if(!can_cast_type<bitvector_typet>(operand_type))
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for byte swap of non-bitvector type: " +
+      byte_swap.pretty());
+  }
+
+  const auto &bv_type = to_bitvector_type(operand_type);
+  const std::size_t width = bv_type.get_width();
+  const std::size_t byte_bits = byte_swap.get_bits_per_byte();
+
+  // Width must be multiple of byte_bits
+  if(width % byte_bits != 0)
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for byte swap with width not multiple of byte "
+      "size: " +
+      byte_swap.pretty());
+  }
+
+  const std::size_t num_bytes = width / byte_bits;
+
+  // If only one byte, no swapping needed
+  if(num_bytes == 1)
+    return operand_term;
+
+  // Extract each byte from the operand
+  // byte_terms[i] will contain bits [(i+1)*byte_bits-1 : i*byte_bits]
+  std::vector<smt_termt> byte_terms;
+  byte_terms.reserve(num_bytes);
+
+  for(std::size_t byte_idx = 0; byte_idx < num_bytes; ++byte_idx)
+  {
+    const std::size_t high_bit = (byte_idx + 1) * byte_bits - 1;
+    const std::size_t low_bit = byte_idx * byte_bits;
+
+    byte_terms.push_back(
+      smt_bit_vector_theoryt::extract(high_bit, low_bit)(operand_term));
+  }
+
+  // Concatenate bytes in reverse order
+  // SMT concat(a, b) makes 'a' the most significant bits
+  // So to reverse bytes, we start with byte 0 (originally least significant)
+  // and make it most significant in the result
+  smt_termt result = byte_terms[0];
+  for(std::size_t i = 1; i < num_bytes; ++i)
+  {
+    result = smt_bit_vector_theoryt::concat(result, byte_terms[i]);
+  }
+
+  return result;
 }
 
 static smt_termt convert_expr_to_smt(

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1776,3 +1776,77 @@ TEST_CASE(
     CHECK(test.convert(assignment) == expected);
   }
 }
+
+TEST_CASE(
+  "expr to smt conversion for bswap_exprt expressions",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  SECTION("16-bit byte swap")
+  {
+    const symbol_exprt operand{"my_value", unsignedbv_typet{16}};
+    const bswap_exprt byte_swap{operand, 8, unsignedbv_typet{16}};
+    INFO("Expression being converted: " + byte_swap.pretty(2, 0));
+    const smt_identifier_termt operand_smt{
+      "my_value", smt_bit_vector_sortt{16}};
+    // For 16-bit bswap, we extract [7:0] and [15:8], then concat in reverse
+    // order
+    // concat([7:0], [15:8]) puts [7:0] as most significant
+    const smt_termt expected = smt_bit_vector_theoryt::concat(
+      smt_bit_vector_theoryt::extract(7, 0)(operand_smt),
+      smt_bit_vector_theoryt::extract(15, 8)(operand_smt));
+    CHECK(test.convert(byte_swap) == expected);
+  }
+  SECTION("32-bit byte swap")
+  {
+    const symbol_exprt operand{"my_value", unsignedbv_typet{32}};
+    const bswap_exprt byte_swap{operand, 8, unsignedbv_typet{32}};
+    INFO("Expression being converted: " + byte_swap.pretty(2, 0));
+    const smt_identifier_termt operand_smt{
+      "my_value", smt_bit_vector_sortt{32}};
+    // For 32-bit bswap, we extract 4 bytes and concat in reverse order
+    const smt_termt expected = smt_bit_vector_theoryt::concat(
+      smt_bit_vector_theoryt::concat(
+        smt_bit_vector_theoryt::concat(
+          smt_bit_vector_theoryt::extract(7, 0)(operand_smt),
+          smt_bit_vector_theoryt::extract(15, 8)(operand_smt)),
+        smt_bit_vector_theoryt::extract(23, 16)(operand_smt)),
+      smt_bit_vector_theoryt::extract(31, 24)(operand_smt));
+    CHECK(test.convert(byte_swap) == expected);
+  }
+  SECTION("64-bit byte swap")
+  {
+    const symbol_exprt operand{"my_value", unsignedbv_typet{64}};
+    const bswap_exprt byte_swap{operand, 8, unsignedbv_typet{64}};
+    INFO("Expression being converted: " + byte_swap.pretty(2, 0));
+    const smt_identifier_termt operand_smt{
+      "my_value", smt_bit_vector_sortt{64}};
+    // For 64-bit bswap, we extract 8 bytes and concat in reverse order
+    const smt_termt expected = smt_bit_vector_theoryt::concat(
+      smt_bit_vector_theoryt::concat(
+        smt_bit_vector_theoryt::concat(
+          smt_bit_vector_theoryt::concat(
+            smt_bit_vector_theoryt::concat(
+              smt_bit_vector_theoryt::concat(
+                smt_bit_vector_theoryt::concat(
+                  smt_bit_vector_theoryt::extract(7, 0)(operand_smt),
+                  smt_bit_vector_theoryt::extract(15, 8)(operand_smt)),
+                smt_bit_vector_theoryt::extract(23, 16)(operand_smt)),
+              smt_bit_vector_theoryt::extract(31, 24)(operand_smt)),
+            smt_bit_vector_theoryt::extract(39, 32)(operand_smt)),
+          smt_bit_vector_theoryt::extract(47, 40)(operand_smt)),
+        smt_bit_vector_theoryt::extract(55, 48)(operand_smt)),
+      smt_bit_vector_theoryt::extract(63, 56)(operand_smt));
+    CHECK(test.convert(byte_swap) == expected);
+  }
+  SECTION("Single byte (no swap needed)")
+  {
+    const symbol_exprt operand{"my_value", unsignedbv_typet{8}};
+    const bswap_exprt byte_swap{operand, 8, unsignedbv_typet{8}};
+    INFO("Expression being converted: " + byte_swap.pretty(2, 0));
+    const smt_identifier_termt operand_smt{"my_value", smt_bit_vector_sortt{8}};
+    // Single byte should return operand unchanged
+    CHECK(test.convert(byte_swap) == operand_smt);
+  }
+}