From 612f33a42ab6bc20f551ff19429939e27758b05e Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 8 Nov 2022 17:30:08 +0000 Subject: [PATCH 1/4] Create correct number of index id when with_exprt As `with_exprt` can be used as a multy-ary operatior (with more than 3 arguments) we need to introduce an index smt_identifier_termt for each index used by the expression. --- .../smt2_incremental_decision_procedure.cpp | 26 +++++--- .../smt2_incremental_decision_procedure.cpp | 65 +++++++++++++++++++ 2 files changed, 82 insertions(+), 9 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index adfadfb4976..cc78f30b52a 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -283,15 +283,23 @@ void smt2_incremental_decision_proceduret::define_index_identifiers( return; if(const auto with_expr = expr_try_dynamic_cast(expr_node)) { - const auto index_expr = with_expr->where(); - const auto index_term = convert_expr_to_smt(index_expr); - const auto index_identifier = "index_" + std::to_string(index_sequence()); - const auto index_definition = - smt_define_function_commandt{index_identifier, {}, index_term}; - expression_identifiers.emplace(index_expr, index_definition.identifier()); - identifier_table.emplace(index_identifier, index_definition.identifier()); - solver_process->send( - smt_define_function_commandt{index_identifier, {}, index_term}); + for(auto operand_ite = ++with_expr->operands().begin(); + operand_ite != with_expr->operands().end(); + operand_ite += 2) + { + const auto index_expr = *operand_ite; + const auto index_term = convert_expr_to_smt(index_expr); + const auto index_identifier = + "index_" + std::to_string(index_sequence()); + const auto index_definition = + smt_define_function_commandt{index_identifier, {}, index_term}; + expression_identifiers.emplace( + index_expr, index_definition.identifier()); + identifier_table.emplace( + index_identifier, index_definition.identifier()); + solver_process->send( + smt_define_function_commandt{index_identifier, {}, index_term}); + } } }); } diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 17e13c88a98..d644576a76a 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -669,3 +669,68 @@ TEST_CASE( REQUIRE(test.sent_commands == expected_commands); } } + +TEST_CASE( + "smt2_incremental_decision_proceduret multi-ary with_exprt introduces " + "correct number of indexes.", + "[core][smt2_incremental]") +{ + auto test = decision_procedure_test_environmentt::make(); + const signedbv_typet index_type{32}; + const signedbv_typet value_type{8}; + const array_typet array_type{value_type, from_integer(3, index_type)}; + const auto original_array_symbol = + make_test_symbol("original_array", array_type); + const auto result_array_symbol = make_test_symbol("result_array", array_type); + with_exprt with_expr{ + original_array_symbol.symbol_expr(), + from_integer(0, index_type), + from_integer(0, value_type)}; + with_expr.add_to_operands( + from_integer(1, index_type), from_integer(1, value_type)); + with_expr.add_to_operands( + from_integer(2, index_type), from_integer(2, value_type)); + const equal_exprt equal_expr{result_array_symbol.symbol_expr(), with_expr}; + test.sent_commands.clear(); + test.procedure.set_to(equal_expr, true); + + const smt_bit_vector_sortt smt_index_sort{32}; + const smt_bit_vector_sortt smt_value_sort{8}; + const smt_array_sortt smt_array_sort{smt_index_sort, smt_value_sort}; + const smt_identifier_termt smt_original_array_term{ + "original_array", smt_array_sort}; + const smt_identifier_termt smt_result_array_term{ + "result_array", smt_array_sort}; + const smt_identifier_termt index_0_term{"index_0", smt_index_sort}; + const smt_identifier_termt index_1_term{"index_1", smt_index_sort}; + const smt_identifier_termt index_2_term{"index_2", smt_index_sort}; + const smt_termt store_term = smt_array_theoryt::store( + smt_array_theoryt::store( + smt_array_theoryt::store( + smt_original_array_term, + index_0_term, + smt_bit_vector_constant_termt{0, smt_value_sort}), + index_1_term, + smt_bit_vector_constant_termt{1, smt_value_sort}), + index_2_term, + smt_bit_vector_constant_termt{2, smt_value_sort}); + const auto smt_assertion = smt_assert_commandt{ + smt_core_theoryt::equal(smt_result_array_term, store_term)}; + const std::vector expected_commands{ + smt_declare_function_commandt(smt_result_array_term, {}), + smt_declare_function_commandt(smt_original_array_term, {}), + smt_define_function_commandt{ + index_0_term.identifier(), + {}, + smt_bit_vector_constant_termt{0, smt_index_sort}}, + smt_define_function_commandt{ + index_1_term.identifier(), + {}, + smt_bit_vector_constant_termt{1, smt_index_sort}}, + smt_define_function_commandt{ + index_2_term.identifier(), + {}, + smt_bit_vector_constant_termt{2, smt_index_sort}}, + smt_assertion}; + REQUIRE(test.sent_commands == expected_commands); +} From 8c8839255563e7540ff92b3a4d99fec3cbe3ec51 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Thu, 3 Nov 2022 17:44:24 +0000 Subject: [PATCH 2/4] Relax type of bitwise operations to any bitvector Lowering of the byte extraction and byte update expressions can yield non-integer bitvector typed operands. Because we do not require a numeric interpretation of them we can relax the requirement of integer-typed operands for bitwise operators. --- .../smt2_incremental/convert_expr_to_smt.cpp | 15 ++--- .../smt2_incremental/convert_expr_to_smt.cpp | 65 +++++++++++-------- 2 files changed, 42 insertions(+), 38 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 628d1a4da86..37d664bb85b 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -367,7 +367,7 @@ static smt_termt convert_expr_to_smt( const bitand_exprt &bitwise_and_expr, const sub_expression_mapt &converted) { - if(operands_are_of_type(bitwise_and_expr)) + if(operands_are_of_type(bitwise_and_expr)) { return convert_multiary_operator_to_terms( bitwise_and_expr, converted, smt_bit_vector_theoryt::make_and); @@ -384,7 +384,7 @@ static smt_termt convert_expr_to_smt( const bitor_exprt &bitwise_or_expr, const sub_expression_mapt &converted) { - if(operands_are_of_type(bitwise_or_expr)) + if(operands_are_of_type(bitwise_or_expr)) { return convert_multiary_operator_to_terms( bitwise_or_expr, converted, smt_bit_vector_theoryt::make_or); @@ -401,7 +401,7 @@ static smt_termt convert_expr_to_smt( const bitxor_exprt &bitwise_xor, const sub_expression_mapt &converted) { - if(operands_are_of_type(bitwise_xor)) + if(operands_are_of_type(bitwise_xor)) { return convert_multiary_operator_to_terms( bitwise_xor, converted, smt_bit_vector_theoryt::make_xor); @@ -418,10 +418,7 @@ static smt_termt convert_expr_to_smt( const bitnot_exprt &bitwise_not, const sub_expression_mapt &converted) { - const bool operand_is_bitvector = - can_cast_type(bitwise_not.op().type()); - - if(operand_is_bitvector) + if(can_cast_type(bitwise_not.op().type())) { return smt_bit_vector_theoryt::make_not(converted.at(bitwise_not.op())); } @@ -436,9 +433,7 @@ static smt_termt convert_expr_to_smt( const unary_minus_exprt &unary_minus, const sub_expression_mapt &converted) { - const bool operand_is_bitvector = - can_cast_type(unary_minus.op().type()); - if(operand_is_bitvector) + if(can_cast_type(unary_minus.op().type())) { return smt_bit_vector_theoryt::negate(converted.at(unary_minus.op())); } diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 3b59f09ebf4..3ebc3f1097c 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -727,20 +727,23 @@ TEST_CASE( } } -SCENARIO( +TEMPLATE_TEST_CASE( "Bitwise \"AND\" expressions are converted to SMT terms", - "[core][smt2_incremental]") + "[core][smt2_incrzmental]", + signedbv_typet, + unsignedbv_typet, + bv_typet) { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386); - GIVEN("three integer bitvectors and their smt-term equivalents") + GIVEN("three bitvectors and their smt-term equivalents") { const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8}; const smt_termt smt_term_three = smt_bit_vector_constant_termt{3, 8}; const smt_termt smt_term_five = smt_bit_vector_constant_termt{5, 8}; - const auto one_bvint = from_integer(1, signedbv_typet{8}); - const auto three_bvint = from_integer(3, signedbv_typet{8}); - const auto five_bvint = from_integer(5, signedbv_typet{8}); + const auto one_bvint = from_integer(1, TestType{8}); + const auto three_bvint = from_integer(3, TestType{8}); + const auto five_bvint = from_integer(5, TestType{8}); WHEN("a bitand_exprt with two of them as arguments is converted") { @@ -766,8 +769,7 @@ SCENARIO( // support direct construction with multiple operands - so we have to // construct its parent class and downcast it. const exprt::operandst and_operands{one_bvint, three_bvint, five_bvint}; - const multi_ary_exprt first_step{ - ID_bitand, and_operands, signedbv_typet{8}}; + const multi_ary_exprt first_step{ID_bitand, and_operands, TestType{8}}; const auto bitand_expr = to_bitand_expr(first_step); const auto constructed_term = test.convert(bitand_expr); @@ -800,20 +802,23 @@ SCENARIO( } } -SCENARIO( +TEMPLATE_TEST_CASE( "Bitwise \"OR\" expressions are converted to SMT terms", - "[core][smt2_incremental]") + "[core][smt2_incremental]", + signedbv_typet, + unsignedbv_typet, + bv_typet) { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386); - GIVEN("three integer bitvectors and their smt-term equivalents") + GIVEN("three bitvectors and their smt-term equivalents") { const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8}; const smt_termt smt_term_three = smt_bit_vector_constant_termt{3, 8}; const smt_termt smt_term_five = smt_bit_vector_constant_termt{5, 8}; - const auto one_bvint = from_integer(1, signedbv_typet{8}); - const auto three_bvint = from_integer(3, signedbv_typet{8}); - const auto five_bvint = from_integer(5, signedbv_typet{8}); + const auto one_bvint = from_integer(1, TestType{8}); + const auto three_bvint = from_integer(3, TestType{8}); + const auto five_bvint = from_integer(5, TestType{8}); WHEN("a bitor_exprt with two of them as arguments is converted") { @@ -840,8 +845,7 @@ SCENARIO( WHEN("a ternary bitor_exprt gets connverted to smt terms") { const exprt::operandst or_operands{one_bvint, three_bvint, five_bvint}; - const multi_ary_exprt first_step{ - ID_bitor, or_operands, signedbv_typet{8}}; + const multi_ary_exprt first_step{ID_bitor, or_operands, TestType{8}}; const auto bitor_expr = to_bitor_expr(first_step); const auto constructed_term = test.convert(bitor_expr); @@ -877,20 +881,23 @@ SCENARIO( } } -SCENARIO( +TEMPLATE_TEST_CASE( "Bitwise \"XOR\" expressions are converted to SMT terms", - "[core][smt2_incremental]") + "[core][smt2_incremental]", + signedbv_typet, + unsignedbv_typet, + bv_typet) { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386); - GIVEN("three integer bitvectors and their smt-term equivalents") + GIVEN("three bitvectors and their smt-term equivalents") { const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8}; const smt_termt smt_term_three = smt_bit_vector_constant_termt{3, 8}; const smt_termt smt_term_five = smt_bit_vector_constant_termt{5, 8}; - const auto one_bvint = from_integer(1, signedbv_typet{8}); - const auto three_bvint = from_integer(3, signedbv_typet{8}); - const auto five_bvint = from_integer(5, signedbv_typet{8}); + const auto one_bvint = from_integer(1, TestType{8}); + const auto three_bvint = from_integer(3, TestType{8}); + const auto five_bvint = from_integer(5, TestType{8}); WHEN("a bitxor_exprt with two of them as arguments is converted") { @@ -913,8 +920,7 @@ SCENARIO( WHEN("a ternary bitxor_exprt gets connverted to smt terms") { const exprt::operandst xor_operands{one_bvint, three_bvint, five_bvint}; - const multi_ary_exprt first_step{ - ID_bitxor, xor_operands, signedbv_typet{8}}; + const multi_ary_exprt first_step{ID_bitxor, xor_operands, TestType{8}}; const auto bitxor_expr = to_bitxor_expr(first_step); const auto constructed_term = test.convert(bitxor_expr); @@ -949,14 +955,17 @@ SCENARIO( } } -SCENARIO( +TEMPLATE_TEST_CASE( "Bitwise \"NOT\" expressions are converted to SMT terms (1's complement)", - "[core][smt2_incremental]") + "[core][smt2_incremental]", + signedbv_typet, + unsignedbv_typet, + bv_typet) { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386); - GIVEN("An integer bitvector") + GIVEN("An bitvector") { - const auto one_bvint = from_integer(1, signedbv_typet{8}); + const auto one_bvint = from_integer(1, TestType{8}); WHEN("A bitnot_exprt is constructed and converted to an SMT term") { From 455cf807356f958e8e989e9e3c1c51fd34ffa374 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Thu, 3 Nov 2022 17:43:00 +0000 Subject: [PATCH 3/4] Add lowering for byte extraction and update When the input program includes non-aligned memory accesses the decision procedure is passed expressions including byte_extract and byte_update operators. To support such programs in the decision procedure we need to lower such operators to operators we support. --- .../smt2_incremental_decision_procedure.cpp | 30 ++-- .../smt2_incremental_decision_procedure.cpp | 165 ++++++++++++++++++ 2 files changed, 184 insertions(+), 11 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index cc78f30b52a..f1d0d2e52c4 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -11,6 +11,7 @@ #include #include +#include #include #include #include @@ -257,19 +258,23 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret( } void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined( - const exprt &expr) + const exprt &in_expr) { if( - expression_handle_identifiers.find(expr) != + expression_handle_identifiers.find(in_expr) != expression_handle_identifiers.cend()) { return; } - define_dependent_functions(expr); + const exprt lowered_expr = lower_byte_operators(in_expr, ns); + + define_dependent_functions(lowered_expr); smt_define_function_commandt function{ - "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)}; - expression_handle_identifiers.emplace(expr, function.identifier()); + "B" + std::to_string(handle_sequence()), + {}, + convert_expr_to_smt(lowered_expr)}; + expression_handle_identifiers.emplace(in_expr, function.identifier()); identifier_table.emplace( function.identifier().identifier(), function.identifier()); solver_process->send(function); @@ -484,22 +489,25 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const return number_of_solver_calls; } -void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value) +void smt2_incremental_decision_proceduret::set_to( + const exprt &in_expr, + bool value) { - PRECONDITION(can_cast_type(expr.type())); + const exprt lowered_expr = lower_byte_operators(in_expr, ns); + PRECONDITION(can_cast_type(lowered_expr.type())); log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) { debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n " - << expr.pretty(2, 0) << messaget::eom; + << lowered_expr.pretty(2, 0) << messaget::eom; }); - define_dependent_functions(expr); + define_dependent_functions(lowered_expr); auto converted_term = [&]() -> smt_termt { const auto expression_handle_identifier = - expression_handle_identifiers.find(expr); + expression_handle_identifiers.find(lowered_expr); if(expression_handle_identifier != expression_handle_identifiers.cend()) return expression_handle_identifier->second; else - return convert_expr_to_smt(expr); + return convert_expr_to_smt(lowered_expr); }(); if(!value) converted_term = smt_core_theoryt::make_not(converted_term); diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index d644576a76a..7c560cda794 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -15,6 +15,7 @@ #include #include #include +#include #include #include #include @@ -23,6 +24,8 @@ // means that we get error messages showing the smt formula expressed as SMT2 // strings instead of `{?}` being printed. It works because catch uses the // appropriate overload of `operator<<` where it exists. +#include + #include #include @@ -734,3 +737,165 @@ TEST_CASE( smt_assertion}; REQUIRE(test.sent_commands == expected_commands); } + +TEST_CASE( + "smt2_incremental_decision_proceduret byte update-extract commands.", + "[core][smt2_incremental]") +{ + auto test = decision_procedure_test_environmentt::make(); + SECTION("byte_extract - byte from int correctly extracted.") + { + const auto int64_type = signedbv_typet(64); + const auto byte_type = signedbv_typet(8); + const auto extracted_byte_symbol = + make_test_symbol("extracted_byte", byte_type); + const auto original_int_symbol = + make_test_symbol("original_int", int64_type); + const auto byte_extract = make_byte_extract( + original_int_symbol.symbol_expr(), + from_integer(1, int64_type), + byte_type); + const typecast_exprt typecast_expr{byte_extract, byte_type}; + const equal_exprt equal_expr{ + extracted_byte_symbol.symbol_expr(), typecast_expr}; + test.sent_commands.clear(); + test.procedure.set_to(equal_expr, true); + const smt_bit_vector_sortt smt_int64_type{64}; + const smt_bit_vector_sortt smt_byte_type{8}; + const smt_identifier_termt extracted_byte_term{ + "extracted_byte", smt_byte_type}; + const smt_identifier_termt original_int{"original_int", smt_int64_type}; + const smt_termt smt_equal_term = smt_core_theoryt::equal( + extracted_byte_term, + smt_bit_vector_theoryt::extract(15, 8)(original_int)); + const auto smt_assertion = smt_assert_commandt{smt_equal_term}; + const std::vector expected_commands{ + smt_declare_function_commandt(extracted_byte_term, {}), + smt_declare_function_commandt(original_int, {}), + smt_assertion}; + REQUIRE(test.sent_commands == expected_commands); + } + SECTION("byte_extract - int from byte correctly extracted.") + { + const auto byte_type = signedbv_typet(8); + const auto int16_type = signedbv_typet(16); + const auto ptr_type = signedbv_typet(32); + const auto extracted_int_symbol = + make_test_symbol("extracted_int", int16_type); + const auto original_byte_array_symbol = make_test_symbol( + "original_byte_array", array_typet(byte_type, from_integer(2, ptr_type))); + const auto byte_extract = make_byte_extract( + original_byte_array_symbol.symbol_expr(), + from_integer(0, ptr_type), + int16_type); + const equal_exprt equal_expr{ + extracted_int_symbol.symbol_expr(), byte_extract}; + test.sent_commands.clear(); + test.procedure.set_to(equal_expr, true); + const smt_bit_vector_sortt smt_int16_type{16}; + const smt_bit_vector_sortt smt_ptr_type{32}; + const smt_bit_vector_sortt smt_byte_type{8}; + const smt_identifier_termt extracted_int_term{ + "extracted_int", smt_int16_type}; + const smt_identifier_termt original_byte_array_term{ + "original_byte_array", smt_array_sortt{smt_ptr_type, smt_byte_type}}; + const smt_termt smt_equal_term = smt_core_theoryt::equal( + extracted_int_term, + smt_bit_vector_theoryt::concat( + smt_array_theoryt::select( + original_byte_array_term, + smt_bit_vector_constant_termt{1, smt_ptr_type}), + smt_array_theoryt::select( + original_byte_array_term, + smt_bit_vector_constant_termt{0, smt_ptr_type}))); + const auto smt_assertion = smt_assert_commandt{smt_equal_term}; + const std::vector expected_commands{ + smt_declare_function_commandt(extracted_int_term, {}), + smt_declare_function_commandt(original_byte_array_term, {}), + smt_assertion}; + REQUIRE(test.sent_commands == expected_commands); + } + SECTION("byte_update - write bytes into int.") + { + const auto int64_type = signedbv_typet(64); + const auto byte_type = signedbv_typet(8); + const auto result_int_symbol = make_test_symbol("result_int", int64_type); + const auto original_int_symbol = + make_test_symbol("original_int", int64_type); + const auto byte_update = make_byte_update( + original_int_symbol.symbol_expr(), + from_integer(1, int64_type), + from_integer(0x0B, byte_type)); + const equal_exprt equal_expr{result_int_symbol.symbol_expr(), byte_update}; + test.sent_commands.clear(); + test.procedure.set_to(equal_expr, true); + const smt_bit_vector_sortt smt_value_type{64}; + const smt_identifier_termt result_int_term{"result_int", smt_value_type}; + const smt_identifier_termt original_int_term{ + "original_int", smt_value_type}; + const smt_termt smt_equal_term = smt_core_theoryt::equal( + result_int_term, + smt_bit_vector_theoryt::make_or( + smt_bit_vector_theoryt::make_and( + original_int_term, + smt_bit_vector_constant_termt{0xFFFFFFFFFFFF00FF, 64}), + smt_bit_vector_constant_termt{0x0B00, 64})); + const auto smt_assertion = smt_assert_commandt{smt_equal_term}; + const std::vector expected_commands{ + smt_declare_function_commandt{result_int_term, {}}, + smt_declare_function_commandt{original_int_term, {}}, + smt_assertion}; + REQUIRE(test.sent_commands == expected_commands); + } + SECTION("byte_update - writes int into byte array.") + { + const auto int32_type = signedbv_typet(32); + const auto int16_type = signedbv_typet(16); + const auto byte_type = signedbv_typet(8); + const array_typet byte_array_type{byte_type, from_integer(2, int32_type)}; + const auto result_array_symbol = + make_test_symbol("result_array", byte_array_type); + const auto original_array_symbol = + make_test_symbol("original_array", byte_array_type); + const auto byte_update = make_byte_update( + original_array_symbol.symbol_expr(), + from_integer(0, int32_type), + from_integer(0x0102, int16_type)); + const equal_exprt equal_expr{ + result_array_symbol.symbol_expr(), byte_update}; + test.sent_commands.clear(); + test.procedure.set_to(equal_expr, true); + const smt_bit_vector_sortt smt_byte_type{8}; + const smt_bit_vector_sortt smt_index_type{32}; + const smt_array_sortt smt_array_type{smt_index_type, smt_byte_type}; + const smt_identifier_termt result_array_term{ + "result_array", smt_array_type}; + const smt_identifier_termt original_array_term{ + "original_array", smt_array_type}; + const smt_identifier_termt index_0_term{"index_0", smt_index_type}; + const smt_identifier_termt index_1_term{"index_1", smt_index_type}; + const smt_termt smt_equal_term = smt_core_theoryt::equal( + result_array_term, + smt_array_theoryt::store( + smt_array_theoryt::store( + original_array_term, + index_0_term, + smt_bit_vector_constant_termt{2, smt_byte_type}), + index_1_term, + smt_bit_vector_constant_termt{1, smt_byte_type})); + const auto smt_assertion = smt_assert_commandt{smt_equal_term}; + const std::vector expected_commands{ + smt_declare_function_commandt{result_array_term, {}}, + smt_declare_function_commandt{original_array_term, {}}, + smt_define_function_commandt{ + index_0_term.identifier(), + {}, + smt_bit_vector_constant_termt{0, smt_index_type}}, + smt_define_function_commandt{ + index_1_term.identifier(), + {}, + smt_bit_vector_constant_termt{1, smt_index_type}}, + smt_assertion}; + REQUIRE(test.sent_commands == expected_commands); + } +} From 424bed5ec14f84258eb6bf9f9c2170772d87c862 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Wed, 28 Sep 2022 18:28:24 +0100 Subject: [PATCH 4/4] Add regression tests for byte extraction/update --- .../array-misalign-between.c | 18 ++++++++++++++++++ .../array-misalign-between.desc | 12 ++++++++++++ .../array-misalign.c | 16 ++++++++++++++++ .../array-misalign.desc | 11 +++++++++++ .../byte-extract-small.c | 12 ++++++++++++ .../byte-extract-small.desc | 8 ++++++++ .../bitvector-bitwise-operators/byte-extract.c | 9 +++++++++ .../byte-extract.desc | 8 ++++++++ .../byte-update-small.c | 13 +++++++++++++ .../byte-update-small.desc | 9 +++++++++ .../bitvector-bitwise-operators/byte-update.c | 10 ++++++++++ .../byte-update.desc | 8 ++++++++ 12 files changed, 134 insertions(+) create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.c create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.c create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.c create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.desc create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.c create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.desc create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.c create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.c create mode 100644 regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.c new file mode 100644 index 00000000000..3f88e447d25 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.c @@ -0,0 +1,18 @@ +#include +#include + +int main() +{ + uint16_t x[3]; + x[0] = 0; + x[1] = 0; + x[2] = 0; + uint8_t *c = x; + c[1] = 1; + assert(x[0] == 256); + assert(x[0] == 0); + assert(x[1] == 0); + assert(x[2] == 0); + uint16_t between = c[1]; + assert(between == 1); +} diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc new file mode 100644 index 00000000000..65d08a7a3f5 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc @@ -0,0 +1,12 @@ +CORE +array-misalign-between.c +--slice-formula +\[main\.assertion\.1\] line \d+ assertion x\[0\] == 256: SUCCESS +\[main\.assertion\.2\] line \d+ assertion x\[0\] == 0: FAILURE +\[main\.assertion\.3\] line \d+ assertion x\[1\] == 0: SUCCESS +\[main\.assertion\.4\] line \d+ assertion x\[2\] == 0: SUCCESS +\[main\.assertion\.5\] line \d+ assertion between == 1: SUCCESS +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.c new file mode 100644 index 00000000000..314d713d1e4 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.c @@ -0,0 +1,16 @@ +#include +#include + +int main() +{ + uint16_t x[3]; + x[0] = 0; + x[1] = 0; + x[2] = 0; + uint8_t *c = x; + c[1] = 1; + assert(x[0] == 256ul); + assert(x[0] == 0ul); + assert(x[1] == 0ul); + assert(x[2] == 0ul); +} diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc new file mode 100644 index 00000000000..ebf12032610 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc @@ -0,0 +1,11 @@ +CORE +array-misalign.c +--slice-formula +\[main.assertion\.1\] line \d+ assertion x\[0\] == 256ul: SUCCESS +\[main.assertion\.2\] line \d+ assertion x\[0\] == 0ul: FAILURE +\[main.assertion\.3\] line \d+ assertion x\[1\] == 0ul: SUCCESS +\[main.assertion\.4\] line \d+ assertion x\[2\] == 0ul: SUCCESS +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.c new file mode 100644 index 00000000000..3a3b7ee37d5 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.c @@ -0,0 +1,12 @@ +#include +#include + +int main() +{ + uint8_t x[2]; + x[0] = 1u; + x[1] = 1u; + uint16_t *y = x; + uint16_t z = *y; + assert(z == 257); +} diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.desc new file mode 100644 index 00000000000..351ef6fd938 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.desc @@ -0,0 +1,8 @@ +CORE +byte-extract-small.c +--slice-formula +\[main.assertion\.1\] line \d+ assertion z == 257: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.c new file mode 100644 index 00000000000..a16820e1f14 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.c @@ -0,0 +1,9 @@ +#include +#include + +int main() +{ + uint16_t x; + uint8_t *y = &x; + assert(y[0] == 0); +} diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.desc new file mode 100644 index 00000000000..d0ce61f1ab5 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.desc @@ -0,0 +1,8 @@ +CORE +byte-extract.c +--slice-formula +\[main.assertion\.1\] line \d+ assertion y\[0\] == 0: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.c new file mode 100644 index 00000000000..60400f48b51 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.c @@ -0,0 +1,13 @@ +#include +#include + +int main() +{ + uint8_t x[2]; + x[0] = 0; + x[1] = 0; + uint16_t *y = x; + *y = 258; + assert(x[0] == 2); + assert(x[1] == 1); +} diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc new file mode 100644 index 00000000000..2b297829663 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc @@ -0,0 +1,9 @@ +CORE +byte-update-small.c +--slice-formula +\[main\.assertion\.1\] line \d+ assertion x\[0\] == 2: SUCCESS +\[main\.assertion\.2\] line \d+ assertion x\[1\] == 1: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.c new file mode 100644 index 00000000000..061dc87c587 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.c @@ -0,0 +1,10 @@ +#include +#include + +int main() +{ + uint16_t x = 0; + uint8_t *y = &x; + y[1] = 1; + assert(x == 256); +} diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc new file mode 100644 index 00000000000..47a0e05d468 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc @@ -0,0 +1,8 @@ +CORE +byte-update.c +--slice-formula +\[main\.assertion\.1\] line \d+ assertion x == 256: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +--