diff --git a/regression/cbmc/Overflow_Leftshift1/main.c b/regression/cbmc/Overflow_Leftshift1/main.c index 70dd6e5c478..cdc26ac2ef3 100644 --- a/regression/cbmc/Overflow_Leftshift1/main.c +++ b/regression/cbmc/Overflow_Leftshift1/main.c @@ -1,11 +1,24 @@ int main() { unsigned char x; + + // signed, owing to promotion, and may overflow unsigned r=x << ((sizeof(unsigned)-1)*8); + + // signed, owing to promotion, and cannot overflow r=x << ((sizeof(unsigned)-1)*8-1); + + // unsigned r=(unsigned)x << ((sizeof(unsigned)-1)*8); - int s=-1 << ((sizeof(int)-1)*8); - s=-256 << ((sizeof(int)-1)*8); + // negative value or zero, not an overflow + int s = -x << ((sizeof(int) - 1) * 8); + + // overflow + s = 1 << x; + + // distance too far, not an overflow + s = s << 100; + return 0; } diff --git a/regression/cbmc/Overflow_Leftshift1/test.desc b/regression/cbmc/Overflow_Leftshift1/test.desc index da481b5cb6d..c7b2f8119c0 100644 --- a/regression/cbmc/Overflow_Leftshift1/test.desc +++ b/regression/cbmc/Overflow_Leftshift1/test.desc @@ -3,8 +3,13 @@ main.c --signed-overflow-check ^EXIT=10$ ^SIGNAL=0$ -^\[.*\] .* arithmetic overflow on signed shl in .*: FAILURE$ -^\*\* 2 of 4 failed +^\[.*\] line 6 arithmetic overflow on signed shl in .*: FAILURE$ +^\[.*\] line 9 arithmetic overflow on signed shl in .*: SUCCESS$ +^\[.*\] line 15 arithmetic overflow on signed shl in .*: SUCCESS$ +^\[.*\] line 18 arithmetic overflow on signed shl in .*: FAILURE$ +^\*\* 2 of 5 failed ^VERIFICATION FAILED$ -- ^warning: ignoring +^\[.*\] line 12 arithmetic overflow on signed shl in .*: .* +^\[.*\] line 21 arithmetic overflow on signed shl in .*: .* diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index cba0a131902..94ac5785860 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -37,8 +37,6 @@ rm Linking7/test.desc rm Linking7/member-name-mismatch.desc rm Malloc23/test.desc rm Multi_Dimensional_Array2/test.desc -rm Overflow_Leftshift1/test.desc -rm Overflow_Subtraction1/test.desc rm Pointer_Arithmetic11/test.desc rm Pointer_byte_extract2/test.desc rm Pointer_byte_extract5/no-simplify.desc diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index fe073af66a0..c674aa39449 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -589,6 +589,81 @@ void goto_checkt::integer_overflow_check( return; } + else if(expr.id() == ID_shl) + { + if(type.id() == ID_signedbv) + { + const auto &shl_expr = to_shl_expr(expr); + const auto &op = shl_expr.op(); + const auto &op_type = to_signedbv_type(type); + const auto op_width = op_type.get_width(); + const auto &distance = shl_expr.distance(); + const auto &distance_type = distance.type(); + + // a left shift of a negative value is undefined; + // yet this isn't an overflow + exprt neg_value_shift; + + if(op_type.id() == ID_unsignedbv) + neg_value_shift = false_exprt(); + else + neg_value_shift = + binary_relation_exprt(op, ID_lt, from_integer(0, op_type)); + + // a shift with negative distance is undefined; + // yet this isn't an overflow + exprt neg_dist_shift; + + if(distance_type.id() == ID_unsignedbv) + neg_dist_shift = false_exprt(); + else + neg_dist_shift = + binary_relation_exprt(op, ID_lt, from_integer(0, distance_type)); + + // shifting a non-zero value by more than its width is undefined; + // yet this isn't an overflow + const exprt dist_too_large = binary_predicate_exprt( + distance, ID_gt, from_integer(op_width, distance_type)); + + const exprt op_zero = equal_exprt(op, from_integer(0, op_type)); + + auto new_type = to_bitvector_type(op_type); + new_type.set_width(op_width * 2); + + const exprt op_ext = typecast_exprt(op, new_type); + + const exprt op_ext_shifted = shl_exprt(op_ext, distance); + + // get top bits of the shifted operand + const exprt top_bits = extractbits_exprt( + op_ext_shifted, + new_type.get_width() - 1, + op_width - 1, + unsignedbv_typet(op_width + 1)); + + const exprt top_bits_zero = + equal_exprt(top_bits, from_integer(0, top_bits.type())); + + // a negative distance shift isn't an overflow; + // a negative value shift isn't an overflow; + // a shift that's too far isn't an overflow; + // a shift of zero isn't overflow; + // else check the top bits + add_guarded_claim( + disjunction({neg_value_shift, + neg_dist_shift, + dist_too_large, + op_zero, + top_bits_zero}), + "arithmetic overflow on signed shl", + "overflow", + expr.find_source_location(), + expr, + guard); + } + + return; + } exprt overflow("overflow-"+expr.id_string(), bool_typet()); overflow.operands()=expr.operands(); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 5d6d692ddd7..52876ca6012 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2960,6 +2960,29 @@ class shl_exprt:public shift_exprt } }; +/// \brief Cast an exprt to a \ref shl_exprt +/// +/// \a expr must be known to be \ref shl_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref shl_exprt +inline const shl_exprt &to_shl_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_shl); + DATA_INVARIANT( + expr.operands().size() == 2, "Bit-wise shl must have two operands"); + return static_cast(expr); +} + +/// \copydoc to_shl_expr(const exprt &) +inline shl_exprt &to_shl_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_shl); + DATA_INVARIANT( + expr.operands().size() == 2, "Bit-wise shl must have two operands"); + return static_cast(expr); +} + /// \brief Arithmetic right shift class ashr_exprt:public shift_exprt {