From b78ca4597a669d2fdbfb08fd7456ff57af7c9719 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 8 Mar 2022 12:58:31 +0000 Subject: [PATCH 1/6] Add dispatch of overflow expression to smt conversions --- .../smt2_incremental/convert_expr_to_smt.cpp | 48 +++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 6d5fb84fd93..54ab23399b0 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -833,6 +833,34 @@ static smt_termt convert_expr_to_smt(const isnormal_exprt &is_normal_expr) is_normal_expr.pretty()); } +static smt_termt convert_expr_to_smt(const plus_overflow_exprt &plus_overflow) +{ + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for plus overflow expression: " + + plus_overflow.pretty()); +} + +static smt_termt convert_expr_to_smt(const minus_overflow_exprt &minus_overflow) +{ + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for minus overflow expression: " + + minus_overflow.pretty()); +} + +static smt_termt convert_expr_to_smt(const mult_overflow_exprt &mult_overflow) +{ + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for multiply overflow expression: " + + mult_overflow.pretty()); +} + +static smt_termt convert_expr_to_smt(const shl_overflow_exprt &shl_overflow) +{ + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for shift left overflow expression: " + + shl_overflow.pretty()); +} + static smt_termt convert_expr_to_smt(const array_exprt &array_construction) { UNIMPLEMENTED_FEATURE( @@ -1144,6 +1172,26 @@ smt_termt convert_expr_to_smt(const exprt &expr) { return convert_expr_to_smt(*is_normal_expr); } + if( + const auto plus_overflow = expr_try_dynamic_cast(expr)) + { + return convert_expr_to_smt(*plus_overflow); + } + if( + const auto minus_overflow = + expr_try_dynamic_cast(expr)) + { + return convert_expr_to_smt(*minus_overflow); + } + if( + const auto mult_overflow = expr_try_dynamic_cast(expr)) + { + return convert_expr_to_smt(*mult_overflow); + } + if(const auto shl_overflow = expr_try_dynamic_cast(expr)) + { + return convert_expr_to_smt(*shl_overflow); + } if(const auto array_construction = expr_try_dynamic_cast(expr)) { return convert_expr_to_smt(*array_construction); From bf20fc9f9b17ab3c825ae7dad982a4adfd00ba64 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 8 Mar 2022 20:37:00 +0000 Subject: [PATCH 2/6] Implement plus overflow to smt terms conversion --- .../smt2_incremental/convert_expr_to_smt.cpp | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 54ab23399b0..092be8fce7a 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -833,8 +833,44 @@ static smt_termt convert_expr_to_smt(const isnormal_exprt &is_normal_expr) is_normal_expr.pretty()); } +/// \brief +/// Constructs a term which is true if the most significant bit of \p input +/// is set. +static smt_termt most_significant_bit_is_set(const smt_termt &input) +{ + const auto bit_vector_sort = input.get_sort().cast(); + INVARIANT( + bit_vector_sort, + "Most significant bit can only be extracted from bit vector terms."); + const size_t most_significant_bit_index = bit_vector_sort->bit_width() - 1; + const auto extract_most_significant_bit = smt_bit_vector_theoryt::extract( + most_significant_bit_index, most_significant_bit_index); + return smt_core_theoryt::equal( + extract_most_significant_bit(input), smt_bit_vector_constant_termt{1, 1}); +} + static smt_termt convert_expr_to_smt(const plus_overflow_exprt &plus_overflow) { + const smt_termt left = convert_expr_to_smt(plus_overflow.lhs()); + const smt_termt right = convert_expr_to_smt(plus_overflow.rhs()); + if(operands_are_of_type(plus_overflow)) + { + const auto add_carry_bit = smt_bit_vector_theoryt::zero_extend(1); + return most_significant_bit_is_set( + smt_bit_vector_theoryt::add(add_carry_bit(left), add_carry_bit(right))); + } + if(operands_are_of_type(plus_overflow)) + { + // Overflow has occurred if the operands have the same sign and adding them + // gives a result of the opposite sign. + const smt_termt msb_left = most_significant_bit_is_set(left); + const smt_termt msb_right = most_significant_bit_is_set(right); + return smt_core_theoryt::make_and( + smt_core_theoryt::equal(msb_left, msb_right), + smt_core_theoryt::distinct( + msb_left, + most_significant_bit_is_set(smt_bit_vector_theoryt::add(left, right)))); + } UNIMPLEMENTED_FEATURE( "Generation of SMT formula for plus overflow expression: " + plus_overflow.pretty()); From 45653593472e844fcb293a330179dffd28c563c5 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 8 Mar 2022 20:38:34 +0000 Subject: [PATCH 3/6] Implement minus overflow to smt terms conversion --- .../smt2_incremental/convert_expr_to_smt.cpp | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 092be8fce7a..09a30ec9a5a 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -878,6 +878,29 @@ static smt_termt convert_expr_to_smt(const plus_overflow_exprt &plus_overflow) static smt_termt convert_expr_to_smt(const minus_overflow_exprt &minus_overflow) { + const smt_termt left = convert_expr_to_smt(minus_overflow.lhs()); + const smt_termt right = convert_expr_to_smt(minus_overflow.rhs()); + if(operands_are_of_type(minus_overflow)) + { + return smt_bit_vector_theoryt::unsigned_less_than(left, right); + } + if(operands_are_of_type(minus_overflow)) + { + // Overflow has occurred if the operands have the opposing signs and + // subtracting them gives a result having the same signedness as the + // right-hand operand. For example the following would be overflow for cases + // for 8 bit wide bit vectors - + // -128 - 1 == 127 + // 127 - (-1) == -128 + const smt_termt msb_left = most_significant_bit_is_set(left); + const smt_termt msb_right = most_significant_bit_is_set(right); + return smt_core_theoryt::make_and( + smt_core_theoryt::distinct(msb_left, msb_right), + smt_core_theoryt::equal( + msb_right, + most_significant_bit_is_set( + smt_bit_vector_theoryt::subtract(left, right)))); + } UNIMPLEMENTED_FEATURE( "Generation of SMT formula for minus overflow expression: " + minus_overflow.pretty()); From 02e53cb1a67e86ebbde6256ef1a8ba002f2cae9d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 9 Mar 2022 19:35:00 +0000 Subject: [PATCH 4/6] Document `smt_bit_vector_theoryt::negate` --- src/solvers/smt2_incremental/smt_bit_vector_theory.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.h b/src/solvers/smt2_incremental/smt_bit_vector_theory.h index 20c42bdd2b9..03388d04006 100644 --- a/src/solvers/smt2_incremental/smt_bit_vector_theory.h +++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.h @@ -245,6 +245,7 @@ class smt_bit_vector_theoryt static smt_sortt return_sort(const smt_termt &operand); static void validate(const smt_termt &operand); }; + /// \brief Arithmetic negation in two's complement. static const smt_function_application_termt::factoryt negate; // Shift operations From 4aac3acf66c1503da7484f0f6b7b50966f2143cf Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 9 Mar 2022 19:35:50 +0000 Subject: [PATCH 5/6] Implement multiplication overflow to smt terms conversion --- .../smt2_incremental/convert_expr_to_smt.cpp | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 09a30ec9a5a..8406b464d37 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -908,6 +908,40 @@ static smt_termt convert_expr_to_smt(const minus_overflow_exprt &minus_overflow) static smt_termt convert_expr_to_smt(const mult_overflow_exprt &mult_overflow) { + PRECONDITION(mult_overflow.lhs().type() == mult_overflow.rhs().type()); + const auto &operand_type = mult_overflow.lhs().type(); + const smt_termt left = convert_expr_to_smt(mult_overflow.lhs()); + const smt_termt right = convert_expr_to_smt(mult_overflow.rhs()); + if( + const auto unsigned_type = + type_try_dynamic_cast(operand_type)) + { + const std::size_t width = unsigned_type->get_width(); + const auto extend = smt_bit_vector_theoryt::zero_extend(width); + return smt_bit_vector_theoryt::unsigned_greater_than_or_equal( + smt_bit_vector_theoryt::multiply(extend(left), extend(right)), + smt_bit_vector_constant_termt{power(2, width), width * 2}); + } + if( + const auto signed_type = + type_try_dynamic_cast(operand_type)) + { + const smt_termt msb_left = most_significant_bit_is_set(left); + const smt_termt msb_right = most_significant_bit_is_set(right); + const std::size_t width = signed_type->get_width(); + const auto extend = smt_bit_vector_theoryt::sign_extend(width); + const auto multiplication = + smt_bit_vector_theoryt::multiply(extend(left), extend(right)); + const auto too_large = smt_bit_vector_theoryt::signed_greater_than_or_equal( + multiplication, + smt_bit_vector_constant_termt{power(2, width - 1), width * 2}); + const auto too_small = smt_bit_vector_theoryt::signed_less_than( + multiplication, + smt_bit_vector_theoryt::negate( + smt_bit_vector_constant_termt{power(2, width - 1), width * 2})); + return smt_core_theoryt::if_then_else( + smt_core_theoryt::equal(msb_left, msb_right), too_large, too_small); + } UNIMPLEMENTED_FEATURE( "Generation of SMT formula for multiply overflow expression: " + mult_overflow.pretty()); From efd4635b8367bf3b129e7b7f65ebf64c7bd0b5e9 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 10 Mar 2022 17:19:36 +0000 Subject: [PATCH 6/6] Enable SMT2 tests which pass with the overflow implementation --- .../cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc | 2 +- regression/cbmc/overflow/leftshift_overflow-c89.desc | 2 +- regression/cbmc/overflow/leftshift_overflow-c99.desc | 2 +- regression/cbmc/overflow/mod_overflow.desc | 2 +- regression/cbmc/overflow/signed_addition_overflow1.desc | 2 +- regression/cbmc/overflow/signed_addition_overflow2.desc | 2 +- regression/cbmc/overflow/signed_addition_overflow3.desc | 2 +- regression/cbmc/overflow/signed_addition_overflow4.desc | 2 +- regression/cbmc/overflow/signed_multiplication1.desc | 2 +- regression/cbmc/overflow/signed_subtraction1.desc | 2 +- regression/cbmc/overflow/unary_minus_overflow.desc | 2 +- regression/cbmc/pragma_cprover2/test.desc | 2 +- regression/cbmc/set-property-inline1/test.desc | 2 +- regression/contracts/variant_init_inside_loop/test.desc | 2 +- 14 files changed, 14 insertions(+), 14 deletions(-) diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc index cd36ec1f882..9c561b2433b 100644 --- a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc +++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE signed_overflow.c --incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace ^VERIFICATION FAILED$ diff --git a/regression/cbmc/overflow/leftshift_overflow-c89.desc b/regression/cbmc/overflow/leftshift_overflow-c89.desc index 78ccc75aa8a..0e7b71047b8 100644 --- a/regression/cbmc/overflow/leftshift_overflow-c89.desc +++ b/regression/cbmc/overflow/leftshift_overflow-c89.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend leftshift_overflow.c --signed-overflow-check --c89 ^EXIT=10$ diff --git a/regression/cbmc/overflow/leftshift_overflow-c99.desc b/regression/cbmc/overflow/leftshift_overflow-c99.desc index 5104954ed84..6bd817096c3 100644 --- a/regression/cbmc/overflow/leftshift_overflow-c99.desc +++ b/regression/cbmc/overflow/leftshift_overflow-c99.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend leftshift_overflow.c --signed-overflow-check --c99 ^EXIT=10$ diff --git a/regression/cbmc/overflow/mod_overflow.desc b/regression/cbmc/overflow/mod_overflow.desc index fd1ab486ff6..3dd44700a71 100644 --- a/regression/cbmc/overflow/mod_overflow.desc +++ b/regression/cbmc/overflow/mod_overflow.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend mod_overflow.c --signed-overflow-check ^EXIT=10$ diff --git a/regression/cbmc/overflow/signed_addition_overflow1.desc b/regression/cbmc/overflow/signed_addition_overflow1.desc index 0db00fffad6..8f0a19c0056 100644 --- a/regression/cbmc/overflow/signed_addition_overflow1.desc +++ b/regression/cbmc/overflow/signed_addition_overflow1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend signed_addition_overflow1.c --signed-overflow-check ^EXIT=10$ diff --git a/regression/cbmc/overflow/signed_addition_overflow2.desc b/regression/cbmc/overflow/signed_addition_overflow2.desc index 2e02a2230df..c5cd82b695d 100644 --- a/regression/cbmc/overflow/signed_addition_overflow2.desc +++ b/regression/cbmc/overflow/signed_addition_overflow2.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend signed_addition_overflow2.c --signed-overflow-check ^EXIT=10$ diff --git a/regression/cbmc/overflow/signed_addition_overflow3.desc b/regression/cbmc/overflow/signed_addition_overflow3.desc index 9710d0ad847..f4a7e139afc 100644 --- a/regression/cbmc/overflow/signed_addition_overflow3.desc +++ b/regression/cbmc/overflow/signed_addition_overflow3.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend signed_addition_overflow3.c --signed-overflow-check --conversion-check ^EXIT=10$ diff --git a/regression/cbmc/overflow/signed_addition_overflow4.desc b/regression/cbmc/overflow/signed_addition_overflow4.desc index b532dbb788e..85044403a64 100644 --- a/regression/cbmc/overflow/signed_addition_overflow4.desc +++ b/regression/cbmc/overflow/signed_addition_overflow4.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend signed_addition_overflow4.c --signed-overflow-check --conversion-check ^EXIT=10$ diff --git a/regression/cbmc/overflow/signed_multiplication1.desc b/regression/cbmc/overflow/signed_multiplication1.desc index 3e243e13501..65f1aba2329 100644 --- a/regression/cbmc/overflow/signed_multiplication1.desc +++ b/regression/cbmc/overflow/signed_multiplication1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend signed_multiplication1.c --signed-overflow-check ^EXIT=0$ diff --git a/regression/cbmc/overflow/signed_subtraction1.desc b/regression/cbmc/overflow/signed_subtraction1.desc index fad1fa02144..cc170ec9e4d 100644 --- a/regression/cbmc/overflow/signed_subtraction1.desc +++ b/regression/cbmc/overflow/signed_subtraction1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend signed_subtraction1.c --signed-overflow-check ^EXIT=0$ diff --git a/regression/cbmc/overflow/unary_minus_overflow.desc b/regression/cbmc/overflow/unary_minus_overflow.desc index 2766431e519..78ba903c155 100644 --- a/regression/cbmc/overflow/unary_minus_overflow.desc +++ b/regression/cbmc/overflow/unary_minus_overflow.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend unary_minus_overflow.c --signed-overflow-check --unsigned-overflow-check ^EXIT=10$ diff --git a/regression/cbmc/pragma_cprover2/test.desc b/regression/cbmc/pragma_cprover2/test.desc index fc1f888dfcf..e55c0ab42e1 100644 --- a/regression/cbmc/pragma_cprover2/test.desc +++ b/regression/cbmc/pragma_cprover2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --signed-overflow-check ^\[main.overflow\.1\] line 21 arithmetic overflow on signed \+ in n \+ n: FAILURE$ diff --git a/regression/cbmc/set-property-inline1/test.desc b/regression/cbmc/set-property-inline1/test.desc index de76ddc5e98..501f959f369 100644 --- a/regression/cbmc/set-property-inline1/test.desc +++ b/regression/cbmc/set-property-inline1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --property inc.overflow.1 --property inc.overflow.2 --slice-formula --signed-overflow-check --conversion-check ^EXIT=10$ diff --git a/regression/contracts/variant_init_inside_loop/test.desc b/regression/contracts/variant_init_inside_loop/test.desc index b67e30c23df..05abef9b977 100644 --- a/regression/contracts/variant_init_inside_loop/test.desc +++ b/regression/contracts/variant_init_inside_loop/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --apply-loop-contracts _ --unsigned-overflow-check ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$