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$ diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 6d5fb84fd93..8406b464d37 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -833,6 +833,127 @@ 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()); +} + +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()); +} + +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()); +} + +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 +1265,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); 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