diff --git a/regression/cbmc/gcc_builtin_add_overflow/main.c b/regression/cbmc/gcc_builtin_add_overflow/main.c index ba074369e04..a9559865a97 100644 --- a/regression/cbmc/gcc_builtin_add_overflow/main.c +++ b/regression/cbmc/gcc_builtin_add_overflow/main.c @@ -110,6 +110,26 @@ void check_generic(void) assert(0 && "reachability"); } +void check_generic_p(void) +{ + unsigned char small_result = 0; + signed long long big_result = 0; + assert(!__builtin_add_overflow_p(17, 25, small_result)); + assert(small_result == 0); + assert(!__builtin_add_overflow_p(17, 25, big_result)); + assert(big_result == 0); + assert(0 && "reachability"); +} + +void check_non_const() +{ + int a, b, c, d, r; + // this may overflow (negated assertion fails) + assert(!__builtin_add_overflow(a, b, &r)); + // but need not overflow (assertion fails) + assert(__builtin_add_overflow(c, d, &c)); +} + int main(void) { check_int(); @@ -119,4 +139,6 @@ int main(void) check_unsigned_long(); check_unsigned_long_long(); check_generic(); + check_generic_p(); + check_non_const(); } diff --git a/regression/cbmc/gcc_builtin_add_overflow/test.desc b/regression/cbmc/gcc_builtin_add_overflow/test.desc index 6555c307d1d..134a33337ac 100644 --- a/regression/cbmc/gcc_builtin_add_overflow/test.desc +++ b/regression/cbmc/gcc_builtin_add_overflow/test.desc @@ -57,6 +57,13 @@ main.c \[check_generic.assertion.9\] line \d+ assertion big_result == 2ll \* .*: SUCCESS \[check_generic.assertion.10\] line \d+ assertion __builtin_add_overflow\(.* / 2 \+ 1, .*/ 2 \+ 1, &big_result\): SUCCESS \[check_generic.assertion.11\] line \d+ assertion 0 && "reachability": FAILURE +\[check_generic_p.assertion.1\] line \d+ assertion !__builtin_add_overflow_p\(17, 25, small_result\): SUCCESS +\[check_generic_p.assertion.2\] line \d+ assertion small_result == 0: SUCCESS +\[check_generic_p.assertion.3\] line \d+ assertion !__builtin_add_overflow_p\(17, 25, big_result\): SUCCESS +\[check_generic_p.assertion.4\] line \d+ assertion big_result == 0: SUCCESS +\[check_generic_p.assertion.5\] line \d+ assertion 0 && "reachability": FAILURE +\[check_non_const\.assertion\.1\] line \d+ assertion !__builtin_add_overflow\(a, b, &r\): FAILURE +\[check_non_const\.assertion\.2\] line \d+ assertion __builtin_add_overflow\(c, d, &c\): FAILURE VERIFICATION FAILED ^EXIT=10$ ^SIGNAL=0$ diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h index 49e8c814694..5061d8fccf8 100644 --- a/src/ansi-c/c_expr.h +++ b/src/ansi-c/c_expr.h @@ -108,9 +108,9 @@ inline shuffle_vector_exprt &to_shuffle_vector_expr(exprt &expr) } /// \brief A Boolean expression returning true, iff the result of performing -/// operation \c kind on operands \c lhs and \c rhs in infinite-precision -/// arithmetic cannot be represented in the type of the object that \c result -/// points to. +/// operation \c kind on operands \c a and \c b in infinite-precision arithmetic +/// cannot be represented in the type of the object that \c result points to (or +/// the type of \c result, if it is not a pointer). /// If \c result is a pointer, the result of the operation is stored in the /// object pointed to by \c result. class side_effect_expr_overflowt : public side_effect_exprt diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index f268ac4ee0e..267e336e148 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -3012,7 +3013,10 @@ exprt c_typecheck_baset::do_special_functions( else if( identifier == "__builtin_add_overflow" || identifier == "__builtin_sub_overflow" || - identifier == "__builtin_mul_overflow") + identifier == "__builtin_mul_overflow" || + identifier == "__builtin_add_overflow_p" || + identifier == "__builtin_sub_overflow_p" || + identifier == "__builtin_mul_overflow_p") { // check function signature if(expr.arguments().size() != 3) @@ -3028,47 +3032,52 @@ exprt c_typecheck_baset::do_special_functions( auto lhs = expr.arguments()[0]; auto rhs = expr.arguments()[1]; - auto result_ptr = expr.arguments()[2]; + auto result = expr.arguments()[2]; + + const bool is__p_variant = has_suffix(id2string(identifier), "_p"); { auto const raise_wrong_argument_error = - [this, - identifier](const exprt &wrong_argument, std::size_t argument_number) { + [this, identifier]( + const exprt &wrong_argument, std::size_t argument_number, bool _p) { std::ostringstream error_message; error_message << wrong_argument.source_location().as_string() << ": " << identifier << " has signature " << identifier - << "(integral, integral, integral*), " + << "(integral, integral, integral" << (_p ? "" : "*") + << "), " << "but argument " << argument_number << " (" << expr2c(wrong_argument, *this) << ") has type `" << type2c(wrong_argument.type(), *this) << '`'; throw invalid_source_file_exceptiont{error_message.str()}; }; - for(auto const arg_index : {0, 1}) + for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index) { auto const &argument = expr.arguments()[arg_index]; if(!is_signed_or_unsigned_bitvector(argument.type())) { - raise_wrong_argument_error(argument, arg_index + 1); + raise_wrong_argument_error(argument, arg_index + 1, is__p_variant); } } if( - result_ptr.type().id() != ID_pointer || - !is_signed_or_unsigned_bitvector(result_ptr.type().subtype())) + !is__p_variant && + (result.type().id() != ID_pointer || + !is_signed_or_unsigned_bitvector(result.type().subtype()))) { - raise_wrong_argument_error(result_ptr, 3); + raise_wrong_argument_error(result, 3, is__p_variant); } } irep_idt kind = - (identifier == "__builtin_add_overflow") + has_prefix(id2string(identifier), "__builtin_add_overflow") ? ID_plus - : (identifier == "__builtin_sub_overflow") ? ID_minus : ID_mult; + : has_prefix(id2string(identifier), "__builtin_sub_overflow") ? ID_minus + : ID_mult; return side_effect_expr_overflowt{kind, std::move(lhs), std::move(rhs), - std::move(result_ptr), + std::move(result), expr.source_location()}; } else diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 78f9a988050..f86c8506aec 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -599,48 +599,89 @@ void goto_convertt::remove_overflow( const irep_idt &statement = expr.get_statement(); const exprt &lhs = expr.lhs(); const exprt &rhs = expr.rhs(); - const exprt &result_ptr = expr.result(); + const exprt &result = expr.result(); - // actual logic implementing the operators + // actual logic implementing the operators: perform operations on signed + // bitvector types of sufficiently large size to hold the result auto const make_operation = [&statement](exprt lhs, exprt rhs) -> exprt { + std::size_t lhs_ssize = to_bitvector_type(lhs.type()).get_width(); + if(lhs.type().id() == ID_unsignedbv) + ++lhs_ssize; + std::size_t rhs_ssize = to_bitvector_type(rhs.type()).get_width(); + if(rhs.type().id() == ID_unsignedbv) + ++rhs_ssize; + if(statement == ID_overflow_plus) { - return plus_exprt{lhs, rhs}; + std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1; + integer_bitvector_typet ssize_type{ID_signedbv, ssize}; + return plus_exprt{typecast_exprt{lhs, ssize_type}, + typecast_exprt{rhs, ssize_type}}; } else if(statement == ID_overflow_minus) { - return minus_exprt{lhs, rhs}; + std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1; + integer_bitvector_typet ssize_type{ID_signedbv, ssize}; + return minus_exprt{typecast_exprt{lhs, ssize_type}, + typecast_exprt{rhs, ssize_type}}; } else { INVARIANT( statement == ID_overflow_mult, "the three overflow operations are add, sub and mul"); - return mult_exprt{lhs, rhs}; + std::size_t ssize = lhs_ssize + rhs_ssize; + integer_bitvector_typet ssize_type{ID_signedbv, ssize}; + return mult_exprt{typecast_exprt{lhs, ssize_type}, + typecast_exprt{rhs, ssize_type}}; } }; - // we’re basically generating this expression - // (*result = (result_type)((integer)lhs OP (integer)rhs)), - // ((integer)result == (integer)lhs OP (integer)rhs) - // i.e. perform the operation (+, -, *) on arbitrary length integer, - // cast to result type, check if the casted result is still equivalent - // to the arbitrary length result. - auto operation = make_operation( - typecast_exprt{lhs, integer_typet{}}, typecast_exprt{rhs, integer_typet{}}); - - typecast_exprt operation_result{operation, result_ptr.type().subtype()}; - - code_assignt assign{dereference_exprt{result_ptr}, - std::move(operation_result), - expr.source_location()}; - convert_assign(assign, dest, mode); + // Generating the following sequence of statements: + // large_signedbv tmp = (large_signedbv)lhs OP (large_signedbv)rhs; + // *result = (result_type)tmp; // only if result is a pointer + // (large_signedbv)(result_type)tmp != tmp; + // This performs the operation (+, -, *) on a signed bitvector type of + // sufficiently large width to store the precise result, cast to result + // type, check if the cast result is not equivalent to the full-length + // result. + auto operation = make_operation(lhs, rhs); + // Disable overflow checks as the operation cannot overflow on the larger + // type + operation.add_source_location() = expr.source_location(); + operation.add_source_location().add_pragma("disable:signed-overflow-check"); + + make_temp_symbol(operation, "large_bv", dest, mode); + + optionalt result_type; + if(result.type().id() == ID_pointer) + { + result_type = to_pointer_type(result.type()).subtype(); + code_assignt result_assignment{dereference_exprt{result}, + typecast_exprt{operation, *result_type}, + expr.source_location()}; + convert_assign(result_assignment, dest, mode); + } + else + { + result_type = result.type(); + // evaluate side effects + exprt tmp = result; + clean_expr(tmp, dest, mode, false); // result _not_ used + } if(result_is_used) { - notequal_exprt overflow_check{ - typecast_exprt{dereference_exprt{result_ptr}, integer_typet{}}, - operation}; + typecast_exprt inner_tc{operation, *result_type}; + inner_tc.add_source_location() = expr.source_location(); + inner_tc.add_source_location().add_pragma("disable:conversion-check"); + typecast_exprt outer_tc{inner_tc, operation.type()}; + outer_tc.add_source_location() = expr.source_location(); + outer_tc.add_source_location().add_pragma("disable:conversion-check"); + + notequal_exprt overflow_check{outer_tc, operation}; + overflow_check.add_source_location() = expr.source_location(); + expr.swap(overflow_check); } else