From 1ffb4056d4ccce2cec1cb150e1e783e4ea43c4b9 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 16 Feb 2022 14:29:53 +0000 Subject: [PATCH 1/8] Move static function `convert_multiary_operator_to_terms` to top of file. The rationale for that is that it's going to be used by functions that need to see it defined within the translation unit, and at its current location it's invisible to some of the functions defined above that. --- .../smt2_incremental/convert_expr_to_smt.cpp | 56 +++++++++---------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 07e71c1abca..28d8637edf3 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -21,6 +21,34 @@ #include #include +/// \brief Converts operator expressions with 2 or more operands to terms +/// expressed as binary operator application. +/// \param expr: The expression to convert. +/// \param factory: The factory function which makes applications of the +/// relevant smt term, when applied to the term operands. +/// \details The conversion used is left associative for instances with 3 or +/// more operands. The SMT standard / core theory version 2.6 actually +/// supports applying the `and`, `or` and `xor` to 3 or more operands. +/// However our internal `smt_core_theoryt` does not support this currently +/// and converting to binary application has the advantage of making the order +/// of evaluation explicit. +template +static smt_termt convert_multiary_operator_to_terms( + const multi_ary_exprt &expr, + const factoryt &factory) +{ + PRECONDITION(expr.operands().size() >= 2); + const auto operand_terms = + make_range(expr.operands()).map([](const exprt &expr) { + return convert_expr_to_smt(expr); + }); + return std::accumulate( + ++operand_terms.begin(), + operand_terms.end(), + *operand_terms.begin(), + factory); +} + static smt_sortt convert_type_to_smt_sort(const bool_typet &type) { return smt_bool_sortt{}; @@ -191,34 +219,6 @@ static smt_termt convert_expr_to_smt(const if_exprt &if_expression) convert_expr_to_smt(if_expression.false_case())); } -/// \brief Converts operator expressions with 2 or more operands to terms -/// expressed as binary operator application. -/// \param expr: The expression to convert. -/// \param factory: The factory function which makes applications of the -/// relevant smt term, when applied to the term operands. -/// \details The conversion used is left associative for instances with 3 or -/// more operands. The SMT standard / core theory version 2.6 actually -/// supports applying the `and`, `or` and `xor` to 3 or more operands. -/// However our internal `smt_core_theoryt` does not support this currently -/// and converting to binary application has the advantage of making the order -/// of evaluation explicit. -template -static smt_termt convert_multiary_operator_to_terms( - const multi_ary_exprt &expr, - const factoryt &factory) -{ - PRECONDITION(expr.operands().size() >= 2); - const auto operand_terms = - make_range(expr.operands()).map([](const exprt &expr) { - return convert_expr_to_smt(expr); - }); - return std::accumulate( - ++operand_terms.begin(), - operand_terms.end(), - *operand_terms.begin(), - factory); -} - static smt_termt convert_expr_to_smt(const and_exprt &and_expression) { return convert_multiary_operator_to_terms( From 8b35bf7d4b55410fe1193f1bba58a7e1cb9e2003 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 16 Feb 2022 14:31:52 +0000 Subject: [PATCH 2/8] Conversion of `bitwise and` expressions to SMT terms. --- .../smt2_incremental/convert_expr_to_smt.cpp | 19 ++++- .../smt2_incremental/convert_expr_to_smt.cpp | 85 +++++++++++++++++-- 2 files changed, 95 insertions(+), 9 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 28d8637edf3..92076e1dfd5 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -154,9 +154,22 @@ static smt_termt convert_expr_to_smt(const concatenation_exprt &concatenation) static smt_termt convert_expr_to_smt(const bitand_exprt &bitwise_and_expr) { - UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for bitwise and expression: " + - bitwise_and_expr.pretty()); + if(std::all_of( + bitwise_and_expr.operands().cbegin(), + bitwise_and_expr.operands().cend(), + [](exprt operand) { + return can_cast_type(operand.type()); + })) + { + return convert_multiary_operator_to_terms( + bitwise_and_expr, smt_bit_vector_theoryt::make_and); + } + else + { + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for bitwise and expression: " + + bitwise_and_expr.pretty()); + } } static smt_termt convert_expr_to_smt(const bitor_exprt &bitwise_or_expr) diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index f7939f97da6..bcacae00adc 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1,16 +1,16 @@ // Author: Diffblue Ltd. -#include +#include +#include +#include +#include +#include #include #include #include #include - -#include -#include -#include -#include +#include TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]") { @@ -416,3 +416,76 @@ TEST_CASE( REQUIRE_THROWS(convert_expr_to_smt(unary_minus_exprt{true_exprt{}})); } } + +SCENARIO( + "Bitwise \"AND\" expressions are converted to SMT terms", + "[core][smt2_incremental]") +{ + GIVEN("three integer 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}); + + WHEN("a bitand_exprt with two of them as arguments is converted") + { + const auto constructed_term = + convert_expr_to_smt(bitand_exprt{one_bvint, three_bvint}); + + THEN( + "it should be equivalent to a \"bvand\" term with the operands " + "converted as well") + { + const auto expected_term = + smt_bit_vector_theoryt::make_and(smt_term_one, smt_term_three); + + CHECK(constructed_term == expected_term); + } + } + + // bitand_exprt derives from multiary exprt, so we need to be able to handle + // expressions with more than 2 operands. + WHEN("a ternary bitand_exprt gets connverted to smt terms") + { + // We need to jump through a bit of a hoop because bitand_exprt doesn't + // 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 auto bitand_expr = to_bitand_expr(first_step); + + const auto constructed_term = convert_expr_to_smt(bitand_expr); + + THEN( + "it should be converted to an appropriate number of nested binary " + "\"bvand\" terms") + { + const auto expected_term = smt_bit_vector_theoryt::make_and( + smt_bit_vector_theoryt::make_and(smt_term_one, smt_term_three), + smt_term_five); + CHECK(constructed_term == expected_term); + } + } + + // Both of the above tests have been testing the positive case so far - + // where everything goes more or less how we expect. Let's see how it + // does with a negative case - where one of the terms is bad or otherwise + // unsuitable for expression. + WHEN("a bitand_exprt with operands of different types gets converted") + { + const cbmc_invariants_should_throwt invariants_throw; + THEN( + "convert_expr_to_smt should throw an exception because bvand requires" + "operands of the same sort") + { + CHECK_THROWS( + convert_expr_to_smt(bitand_exprt{one_bvint, true_exprt{}})); + } + } + } +} From f09c9f937055cfaff22ebf7209661c5eff81872c Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 16 Feb 2022 15:14:57 +0000 Subject: [PATCH 3/8] Conversion of `bitor_exprt` to `bvor`. --- .../smt2_incremental/convert_expr_to_smt.cpp | 19 ++++- .../smt2_incremental/convert_expr_to_smt.cpp | 76 +++++++++++++++++++ 2 files changed, 92 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 92076e1dfd5..02d715e488d 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -174,9 +174,22 @@ static smt_termt convert_expr_to_smt(const bitand_exprt &bitwise_and_expr) static smt_termt convert_expr_to_smt(const bitor_exprt &bitwise_or_expr) { - UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for bitwise or expression: " + - bitwise_or_expr.pretty()); + if(std::all_of( + bitwise_or_expr.operands().cbegin(), + bitwise_or_expr.operands().cend(), + [](exprt operand) { + return can_cast_type(operand.type()); + })) + { + return convert_multiary_operator_to_terms( + bitwise_or_expr, smt_bit_vector_theoryt::make_or); + } + else + { + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for bitwise or expression: " + + bitwise_or_expr.pretty()); + } } static smt_termt convert_expr_to_smt(const bitxor_exprt &bitwise_xor) diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index bcacae00adc..5e0e2593df6 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -489,3 +489,79 @@ SCENARIO( } } } + +SCENARIO( + "Bitwise \"OR\" expressions are converted to SMT terms", + "[core][smt2_incremental]") +{ + GIVEN("three integer 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}); + + WHEN("a bitor_exprt with two of them as arguments is converted") + { + const auto constructed_term = + convert_expr_to_smt(bitor_exprt{one_bvint, three_bvint}); + + THEN( + "it should be equivalent to a \"bvor\" term with the operands " + "converted as well") + { + const auto expected_term = + smt_bit_vector_theoryt::make_or(smt_term_one, smt_term_three); + + CHECK(constructed_term == expected_term); + } + } + + // bitor_exprt is similar to bitand_exprt in that it derives from multiary + // exprt, so we need to be able to handle expressions with more than 2 + // operands. We're going to follow the same format and construct a + // multiary_exprt as if it was a bitor_exprt, then cast it to one, finally + // passing it on to convert_expt_to_smt to convert it to an appropriate SMT + // term. + 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 auto bitor_expr = to_bitor_expr(first_step); + + const auto constructed_term = convert_expr_to_smt(bitor_expr); + + THEN( + "it should be converted to an appropriate number of nested binary " + "\"bvor\" terms") + { + // In QF_BV, bvor is defined as a binary function, so we need to + // construct bvor terms with arity > 2 in terms of nested bvor + // constructs. + const auto expected_term = smt_bit_vector_theoryt::make_or( + smt_bit_vector_theoryt::make_or(smt_term_one, smt_term_three), + smt_term_five); + CHECK(constructed_term == expected_term); + } + } + + // Both of the above tests have been testing the positive case so far - + // where everything goes more or less how we expect. Let's see how it does + // with a negative case - where one of the terms is bad or otherwise + // unsuitable for expression. + WHEN("a bitor_exprt with operands of different types gets converted") + { + const cbmc_invariants_should_throwt invariants_throw; + THEN( + "convert_expr_to_smt should throw an exception because bvor requires" + "operands of the same sort") + { + CHECK_THROWS(convert_expr_to_smt(bitor_exprt{one_bvint, true_exprt{}})); + } + } + } +} From f6a832f99877c2b9621bdb40aa1c6cd3b2b254ac Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 16 Feb 2022 15:26:04 +0000 Subject: [PATCH 4/8] Conversion of `bitxor_expr` to `bvxor` SMT terms. --- .../smt2_incremental/convert_expr_to_smt.cpp | 19 ++++- .../smt2_incremental/convert_expr_to_smt.cpp | 72 +++++++++++++++++++ 2 files changed, 88 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 02d715e488d..edb9c1c534e 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -194,9 +194,22 @@ static smt_termt convert_expr_to_smt(const bitor_exprt &bitwise_or_expr) static smt_termt convert_expr_to_smt(const bitxor_exprt &bitwise_xor) { - UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for bitwise xor expression: " + - bitwise_xor.pretty()); + if(std::all_of( + bitwise_xor.operands().cbegin(), + bitwise_xor.operands().cend(), + [](exprt operand) { + return can_cast_type(operand.type()); + })) + { + return convert_multiary_operator_to_terms( + bitwise_xor, smt_bit_vector_theoryt::make_xor); + } + else + { + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for bitwise xor expression: " + + bitwise_xor.pretty()); + } } static smt_termt convert_expr_to_smt(const bitnot_exprt &bitwise_not) diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 5e0e2593df6..02296159f84 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -565,3 +565,75 @@ SCENARIO( } } } + +SCENARIO( + "Bitwise \"XOR\" expressions are converted to SMT terms", + "[core][smt2_incremental]") +{ + GIVEN("three integer 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}); + + WHEN("a bitxor_exprt with two of them as arguments is converted") + { + const auto constructed_term = + convert_expr_to_smt(bitxor_exprt{one_bvint, three_bvint}); + + THEN( + "it should be equivalent to a \"bvxor\" term with the operands " + "converted as well") + { + const auto expected_term = + smt_bit_vector_theoryt::make_xor(smt_term_one, smt_term_three); + + CHECK(constructed_term == expected_term); + } + } + + // bitxor_exprt is similar to bitand_exprt and bitor_exprt, so we need + // to handle the case where we need to convert expressions with arity > 2. + 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 auto bitxor_expr = to_bitxor_expr(first_step); + + const auto constructed_term = convert_expr_to_smt(bitxor_expr); + + THEN( + "it should be converted to an appropriate number of nested binary " + "\"bvxor\" terms") + { + // We handle this in much the same way as we do bvand and bvor. + // See the corresponding comments there. + const auto expected_term = smt_bit_vector_theoryt::make_xor( + smt_bit_vector_theoryt::make_xor(smt_term_one, smt_term_three), + smt_term_five); + CHECK(constructed_term == expected_term); + } + } + + // Both of the above tests have been testing the positive case so far - + // where everything goes more or less how we expect. Let's see how it does + // with a negative case - where one of the terms is bad or otherwise + // unsuitable for expression. + WHEN("a bitxor_exprt with operands of different types gets converted") + { + const cbmc_invariants_should_throwt invariants_throw; + THEN( + "convert_expr_to_smt should throw an exception because bvxor requires" + "operands of the same sort") + { + CHECK_THROWS( + convert_expr_to_smt(bitxor_exprt{one_bvint, true_exprt{}})); + } + } + } +} From 67c25037ebdf1e05c2bbe59712e917359d8cc413 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 16 Feb 2022 16:05:22 +0000 Subject: [PATCH 5/8] Conversion of `bitnot_exprt` to `bvnot` SMT terms. --- .../smt2_incremental/convert_expr_to_smt.cpp | 16 +++++++-- .../smt2_incremental/convert_expr_to_smt.cpp | 35 +++++++++++++++++++ 2 files changed, 48 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index edb9c1c534e..ddd77d4d309 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -214,9 +214,19 @@ static smt_termt convert_expr_to_smt(const bitxor_exprt &bitwise_xor) static smt_termt convert_expr_to_smt(const bitnot_exprt &bitwise_not) { - UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for bitwise not expression: " + - bitwise_not.pretty()); + const bool operand_is_bitvector = + can_cast_type(bitwise_not.op().type()); + + if(operand_is_bitvector) + { + return smt_bit_vector_theoryt::make_not( + convert_expr_to_smt(bitwise_not.op())); + } + else + { + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for bitnot_exprt: " + bitwise_not.pretty()); + } } static smt_termt convert_expr_to_smt(const unary_minus_exprt &unary_minus) diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 02296159f84..064e8a9eb7e 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -637,3 +637,38 @@ SCENARIO( } } } + +SCENARIO( + "Bitwise \"NOT\" expressions are converted to SMT terms (1's complement)", + "[core][smt2_incremental]") +{ + GIVEN("An integer bitvector") + { + const auto one_bvint = from_integer(1, signedbv_typet{8}); + + WHEN("A bitnot_exprt is constructed and converted to an SMT term") + { + const auto constructed_term = + convert_expr_to_smt(bitnot_exprt{one_bvint}); + THEN("it should be converted to bvnot smt term") + { + const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8}; + const auto expected_term = + smt_bit_vector_theoryt::make_not(smt_term_one); + + REQUIRE(constructed_term == expected_term); + } + } + + WHEN("A bitnot_exprt is constructed with a false expression and converted") + { + const cbmc_invariants_should_throwt invariants_throw; + THEN( + "convert_expr_to_smt should throw an exception and not allow " + "construction") + { + REQUIRE_THROWS(convert_expr_to_smt(bitnot_exprt{false_exprt{}})); + } + } + } +} From 98783dacadc366794d4f1acc78aa69346a05f17b Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 16 Feb 2022 17:02:57 +0000 Subject: [PATCH 6/8] Conversion of left bit shift expression to `bvshl`. --- .../smt2_incremental/convert_expr_to_smt.cpp | 8 ++++ src/util/bitvector_expr.h | 6 +++ .../smt2_incremental/convert_expr_to_smt.cpp | 42 +++++++++++++++++++ 3 files changed, 56 insertions(+) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index ddd77d4d309..c0495f0de26 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -547,6 +547,14 @@ static smt_termt convert_expr_to_smt(const index_exprt &index) static smt_termt convert_expr_to_smt(const shift_exprt &shift) { + // TODO: Dispatch into different types of shifting + if(const auto left_shift = expr_try_dynamic_cast(shift)) + { + return smt_bit_vector_theoryt::shift_left( + convert_expr_to_smt(left_shift->op0()), + convert_expr_to_smt(left_shift->op1())); + } + // TODO: split into functions for separate types of shift including rotate. UNIMPLEMENTED_FEATURE( "Generation of SMT formula for shift expression: " + shift.pretty()); diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index 220a9e5cae7..b7bfb3d23c6 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -305,6 +305,12 @@ class shl_exprt : public shift_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_shl; +} + /// \brief Cast an exprt to a \ref shl_exprt /// /// \a expr must be known to be \ref shl_exprt. diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 064e8a9eb7e..7bab9f6d2e9 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -672,3 +672,45 @@ SCENARIO( } } } + +SCENARIO( + "Left-shift expressions are converted to SMT terms", + "[core][smt2_incremental]") +{ + GIVEN("An integer bitvector and the number of places we're going to shift") + { + // This is going to act as both the value to be shifted, and a value + // signifying the places to the left we're shifting. + const auto one_bvint = from_integer(1, signedbv_typet{8}); + + WHEN("We construct a shl_exprt and convert it to an SMT term") + { + const auto shift_expr = shl_exprt{one_bvint, one_bvint}; + const auto constructed_term = convert_expr_to_smt(shift_expr); + + THEN("It should be equivalent to a bvshl term") + { + const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8}; + const auto expected_term = smt_bit_vector_theoryt::shift_left( + /* term */ + smt_term_one, + /* distance */ + smt_term_one); + } + } + + WHEN( + "We construct a malformed shl_exprt and attempt to convert it to an SMT " + "term") + { + const cbmc_invariants_should_throwt invariants_throw; + THEN( + "convert_expr_to_smt should throw an exception because of validation " + "failure") + { + REQUIRE_THROWS( + convert_expr_to_smt(shl_exprt{one_bvint, false_exprt{}})); + } + } + } +} From 0652b4eff695e36937ff03f3f530998dfea3a0e7 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 16 Feb 2022 18:24:43 +0000 Subject: [PATCH 7/8] Conversion of logical and arithmetic right shift expressions to SMT. --- .../smt2_incremental/convert_expr_to_smt.cpp | 27 +++-- src/util/bitvector_expr.h | 12 +++ .../smt2_incremental/convert_expr_to_smt.cpp | 100 ++++++++++++++++++ 3 files changed, 133 insertions(+), 6 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index c0495f0de26..b0e9e1343dd 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -548,16 +548,31 @@ static smt_termt convert_expr_to_smt(const index_exprt &index) static smt_termt convert_expr_to_smt(const shift_exprt &shift) { // TODO: Dispatch into different types of shifting + const auto &first_operand = shift.op0(); + const auto &second_operand = shift.op1(); + if(const auto left_shift = expr_try_dynamic_cast(shift)) { return smt_bit_vector_theoryt::shift_left( - convert_expr_to_smt(left_shift->op0()), - convert_expr_to_smt(left_shift->op1())); + convert_expr_to_smt(first_operand), convert_expr_to_smt(second_operand)); + } + else if( + const auto right_logical_shift = expr_try_dynamic_cast(shift)) + { + return smt_bit_vector_theoryt::logical_shift_right( + convert_expr_to_smt(first_operand), convert_expr_to_smt(second_operand)); + } + else if( + const auto right_arith_shift = expr_try_dynamic_cast(shift)) + { + return smt_bit_vector_theoryt::arithmetic_shift_right( + convert_expr_to_smt(first_operand), convert_expr_to_smt(second_operand)); + } + else + { + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for shift expression: " + shift.pretty()); } - - // TODO: split into functions for separate types of shift including rotate. - UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for shift expression: " + shift.pretty()); } static smt_termt convert_expr_to_smt(const with_exprt &with) diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index b7bfb3d23c6..22c203bffa9 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -349,6 +349,12 @@ class ashr_exprt : public shift_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_ashr; +} + /// \brief Logical right shift class lshr_exprt : public shift_exprt { @@ -364,6 +370,12 @@ class lshr_exprt : public shift_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_lshr; +} + /// \brief Extracts a single bit of a bit-vector operand class extractbit_exprt : public binary_predicate_exprt { diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 7bab9f6d2e9..ab9642601b3 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -714,3 +714,103 @@ SCENARIO( } } } + +SCENARIO( + "Logical Right-shift expressions are converted to SMT terms", + "[core][smt2_incremental]") +{ + GIVEN("Two integer bitvectors, one for the value and one for the places") + { + const auto to_be_shifted = from_integer(1, signedbv_typet{8}); + const auto places = from_integer(2, signedbv_typet{8}); + + WHEN("We construct a lshr_exprt and convert it to an SMT term") + { + const auto shift_expr = lshr_exprt{to_be_shifted, places}; + const auto constructed_term = convert_expr_to_smt(shift_expr); + + THEN("We should get an logical shift right SMT term") + { + const smt_termt smt_term_value = smt_bit_vector_constant_termt{1, 8}; + const smt_termt smt_term_places = smt_bit_vector_constant_termt{2, 8}; + const auto expected_term = smt_bit_vector_theoryt::logical_shift_right( + smt_term_value, smt_term_places); + REQUIRE(constructed_term == expected_term); + } + } + + WHEN( + "We construct a malformed lshr_exprt and attempt to convert it to an SMT" + " term") + { + const cbmc_invariants_should_throwt invariants_throw; + THEN( + "convert_expr_to_smt should throw an exception because of validation " + "failure") + { + REQUIRE_THROWS( + convert_expr_to_smt(lshr_exprt{to_be_shifted, false_exprt{}})); + } + } + } +} + +SCENARIO( + "Arithmetic Right-shift expressions are converted to SMT terms", + "[core][smt2_incremental]") +{ + GIVEN("Two integer bitvectors, one for the value and one for the places") + { + const auto to_be_shifted = from_integer(1, signedbv_typet{8}); + const auto places = from_integer(2, signedbv_typet{8}); + + WHEN("We construct a ashr_exprt and convert it to an SMT term") + { + const auto shift_expr = ashr_exprt{to_be_shifted, places}; + const auto constructed_term = convert_expr_to_smt(shift_expr); + + THEN("We should get an arithmetic shift-right SMT term") + { + const smt_termt smt_term_value = smt_bit_vector_constant_termt{1, 8}; + const smt_termt smt_term_places = smt_bit_vector_constant_termt{2, 8}; + const auto expected_term = + smt_bit_vector_theoryt::arithmetic_shift_right( + smt_term_value, smt_term_places); + REQUIRE(constructed_term == expected_term); + } + } + + WHEN("We construct an ashr_exprt and with a shift of 0 places") + { + const auto zero_places = from_integer(0, signedbv_typet{8}); + const auto shift_expr = ashr_exprt{to_be_shifted, zero_places}; + const auto constructed_term = convert_expr_to_smt(shift_expr); + + THEN( + "When we convert it, we should be getting an arithmetic shift-right " + "term") + { + const smt_termt smt_term_value = smt_bit_vector_constant_termt{1, 8}; + const smt_termt smt_term_places = smt_bit_vector_constant_termt{0, 8}; + const auto expected_term = + smt_bit_vector_theoryt::arithmetic_shift_right( + smt_term_value, smt_term_places); + REQUIRE(constructed_term == expected_term); + } + } + + WHEN( + "We construct a malformed ashr_exprt and attempt to convert it to an SMT " + "term") + { + const cbmc_invariants_should_throwt invariants_throw; + THEN( + "convert_expr_to_smt should throw an exception because of validation " + "failure") + { + REQUIRE_THROWS( + convert_expr_to_smt(ashr_exprt{to_be_shifted, false_exprt{}})); + } + } + } +} From 05e1fd68792c4af7de9ce7882e4ce87be914df62 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 23 Feb 2022 09:24:41 +0000 Subject: [PATCH 8/8] Refactor the `std::all_of` checks in several bitwise operators into a function. --- .../smt2_incremental/convert_expr_to_smt.cpp | 34 +++++++++---------- 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index b0e9e1343dd..990a9e5f589 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -49,6 +49,19 @@ static smt_termt convert_multiary_operator_to_terms( factory); } +/// \brief Ensures that all operands of the argument expression have related +/// types. +/// \param expr: The expression of which the operands we evaluate for type +/// equality. +template +static bool operands_are_of_type(const exprt &expr) +{ + return std::all_of( + expr.operands().cbegin(), expr.operands().cend(), [](const exprt &operand) { + return can_cast_type(operand.type()); + }); +} + static smt_sortt convert_type_to_smt_sort(const bool_typet &type) { return smt_bool_sortt{}; @@ -154,12 +167,7 @@ static smt_termt convert_expr_to_smt(const concatenation_exprt &concatenation) static smt_termt convert_expr_to_smt(const bitand_exprt &bitwise_and_expr) { - if(std::all_of( - bitwise_and_expr.operands().cbegin(), - bitwise_and_expr.operands().cend(), - [](exprt operand) { - return can_cast_type(operand.type()); - })) + if(operands_are_of_type(bitwise_and_expr)) { return convert_multiary_operator_to_terms( bitwise_and_expr, smt_bit_vector_theoryt::make_and); @@ -174,12 +182,7 @@ static smt_termt convert_expr_to_smt(const bitand_exprt &bitwise_and_expr) static smt_termt convert_expr_to_smt(const bitor_exprt &bitwise_or_expr) { - if(std::all_of( - bitwise_or_expr.operands().cbegin(), - bitwise_or_expr.operands().cend(), - [](exprt operand) { - return can_cast_type(operand.type()); - })) + if(operands_are_of_type(bitwise_or_expr)) { return convert_multiary_operator_to_terms( bitwise_or_expr, smt_bit_vector_theoryt::make_or); @@ -194,12 +197,7 @@ static smt_termt convert_expr_to_smt(const bitor_exprt &bitwise_or_expr) static smt_termt convert_expr_to_smt(const bitxor_exprt &bitwise_xor) { - if(std::all_of( - bitwise_xor.operands().cbegin(), - bitwise_xor.operands().cend(), - [](exprt operand) { - return can_cast_type(operand.type()); - })) + if(operands_are_of_type(bitwise_xor)) { return convert_multiary_operator_to_terms( bitwise_xor, smt_bit_vector_theoryt::make_xor);