diff --git a/regression/cbmc/gcc_bswap1/test.desc b/regression/cbmc/gcc_bswap1/test.desc index b38684cc270..2f839efe54a 100644 --- a/regression/cbmc/gcc_bswap1/test.desc +++ b/regression/cbmc/gcc_bswap1/test.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c ^EXIT=10$ diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index d5910628470..e95fd320f03 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/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(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 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( diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 4a70592f67c..e9580acdeae 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/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); + } +}