diff --git a/regression/cbmc/gcc_builtin_add_overflow/main.c b/regression/cbmc/gcc_builtin_add_overflow/main.c index dfc8a257960..ba074369e04 100644 --- a/regression/cbmc/gcc_builtin_add_overflow/main.c +++ b/regression/cbmc/gcc_builtin_add_overflow/main.c @@ -82,13 +82,31 @@ void check_unsigned_long_long(void) unsigned long long const one = 1ull; unsigned long long result; - assert(!__builtin_uaddl_overflow(one, one, &result)); + assert(!__builtin_uaddll_overflow(one, one, &result)); assert(result == 2ull); assert(!__builtin_uaddll_overflow(ULLONG_MAX / 2, ULLONG_MAX / 2, &result)); assert(result + 1ull == ULLONG_MAX); assert( __builtin_uaddll_overflow(ULLONG_MAX / 2 + 2, ULLONG_MAX / 2 + 2, &result)); - assert(__builtin_uaddl_overflow(one, ULLONG_MAX, &result)); + assert(__builtin_uaddll_overflow(one, ULLONG_MAX, &result)); + assert(0 && "reachability"); +} + +void check_generic(void) +{ + unsigned char small_result; + signed long long big_result; + assert(!__builtin_add_overflow(17, 25, &small_result)); + assert(small_result == 42); + assert(!__builtin_add_overflow(17, 25, &big_result)); + assert(big_result == 42ll); + assert(__builtin_add_overflow(216, 129, &small_result)); + assert(!__builtin_add_overflow(216, 129, &big_result)); + assert(big_result == 345); + assert(!__builtin_add_overflow(INT_MAX, INT_MAX, &big_result)); + assert(big_result == 2ll * INT_MAX); + assert( + __builtin_add_overflow(LLONG_MAX / 2 + 1, LLONG_MAX / 2 + 1, &big_result)); assert(0 && "reachability"); } @@ -100,4 +118,5 @@ int main(void) check_unsigned(); check_unsigned_long(); check_unsigned_long_long(); + check_generic(); } diff --git a/regression/cbmc/gcc_builtin_add_overflow/test.desc b/regression/cbmc/gcc_builtin_add_overflow/test.desc index c6341909287..6555c307d1d 100644 --- a/regression/cbmc/gcc_builtin_add_overflow/test.desc +++ b/regression/cbmc/gcc_builtin_add_overflow/test.desc @@ -39,13 +39,24 @@ main.c \[check_unsigned_long.assertion.5\] line \d+ assertion __builtin_uaddl_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS \[check_unsigned_long.assertion.6\] line \d+ assertion __builtin_uaddl_overflow\(one, .*, &result\): SUCCESS \[check_unsigned_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE -\[check_unsigned_long_long.assertion.1\] line \d+ assertion !__builtin_uaddl_overflow\(one, one, &result\): SUCCESS +\[check_unsigned_long_long.assertion.1\] line \d+ assertion !__builtin_uaddll_overflow\(one, one, &result\): SUCCESS \[check_unsigned_long_long.assertion.2\] line \d+ assertion result == 2ull: SUCCESS \[check_unsigned_long_long.assertion.3\] line \d+ assertion !__builtin_uaddll_overflow\(.* / 2, .* / 2, &result\): SUCCESS \[check_unsigned_long_long.assertion.4\] line \d+ assertion result \+ 1ull == .*: SUCCESS \[check_unsigned_long_long.assertion.5\] line \d+ assertion __builtin_uaddll_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS -\[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_uaddl_overflow\(one, .*, &result\): SUCCESS +\[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_uaddll_overflow\(one, .*, &result\): SUCCESS \[check_unsigned_long_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE +\[check_generic.assertion.1\] line \d+ assertion !__builtin_add_overflow\(17, 25, &small_result\): SUCCESS +\[check_generic.assertion.2\] line \d+ assertion small_result == 42: SUCCESS +\[check_generic.assertion.3\] line \d+ assertion !__builtin_add_overflow\(17, 25, &big_result\): SUCCESS +\[check_generic.assertion.4\] line \d+ assertion big_result == 42ll: SUCCESS +\[check_generic.assertion.5\] line \d+ assertion __builtin_add_overflow\(216, 129, &small_result\): SUCCESS +\[check_generic.assertion.6\] line \d+ assertion !__builtin_add_overflow\(216, 129, &big_result\): SUCCESS +\[check_generic.assertion.7\] line \d+ assertion big_result == 345: SUCCESS +\[check_generic.assertion.8\] line \d+ assertion !__builtin_add_overflow\(.*, .*, &big_result\): SUCCESS +\[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 VERIFICATION FAILED ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/gcc_builtin_mul_overflow/main.c b/regression/cbmc/gcc_builtin_mul_overflow/main.c index 4d7fd6ec218..30373710042 100644 --- a/regression/cbmc/gcc_builtin_mul_overflow/main.c +++ b/regression/cbmc/gcc_builtin_mul_overflow/main.c @@ -104,6 +104,22 @@ void check_unsigned_long_long(void) assert(0 && "reachability"); } +void check_generic(void) +{ + unsigned char small_result; + long long big_result; + + assert(__builtin_mul_overflow(100, 100, &small_result)); + assert(!__builtin_mul_overflow(100, 100, &big_result)); + assert(big_result == 10000); + assert(!__builtin_mul_overflow(10, 10, &small_result)); + assert(small_result == 100); + assert(!__builtin_mul_overflow(INT_MAX, INT_MAX, &big_result)); + assert(big_result == 4611686014132420609ll); + assert(__builtin_mul_overflow(INT_MAX * 2ll, INT_MAX * 2ll, &big_result)); + assert(0 && "reachability"); +} + int main(void) { check_int(); @@ -112,5 +128,6 @@ int main(void) check_unsigned(); check_unsigned_long(); check_unsigned_long_long(); + check_generic(); return 0; } diff --git a/regression/cbmc/gcc_builtin_mul_overflow/test.desc b/regression/cbmc/gcc_builtin_mul_overflow/test.desc index e045d26c089..7f0f9a1f25d 100644 --- a/regression/cbmc/gcc_builtin_mul_overflow/test.desc +++ b/regression/cbmc/gcc_builtin_mul_overflow/test.desc @@ -37,5 +37,14 @@ main.c \[check_unsigned_long_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_unsigned_long_long_max \* lt_isqrt_of_unsigned_long_long_max: SUCCESS \[check_unsigned_long_long.assertion.5\] line \d+ assertion __builtin_umulll_overflow\( lt_isqrt_of_unsigned_long_long_max << 1, lt_isqrt_of_unsigned_long_long_max << 1, &result\): SUCCESS \[check_unsigned_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE +\[check_generic.assertion.1\] line \d+ assertion __builtin_mul_overflow\(100, 100, &small_result\): SUCCESS +\[check_generic.assertion.2\] line \d+ assertion !__builtin_mul_overflow\(100, 100, &big_result\): SUCCESS +\[check_generic.assertion.3\] line \d+ assertion big_result == 10000: SUCCESS +\[check_generic.assertion.4\] line \d+ assertion !__builtin_mul_overflow\(10, 10, &small_result\): SUCCESS +\[check_generic.assertion.5\] line \d+ assertion small_result == 100: SUCCESS +\[check_generic.assertion.6\] line \d+ assertion !__builtin_mul_overflow\(.*, .*, &big_result\): SUCCESS +\[check_generic.assertion.7\] line \d+ assertion big_result == 4611686014132420609ll: SUCCESS +\[check_generic.assertion.8\] line \d+ assertion __builtin_mul_overflow\(.* \* 2ll, .* \* 2ll, &big_result\): SUCCESS +\[check_generic.assertion.9\] line \d+ assertion 0 && "reachability": FAILURE ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/gcc_builtin_sub_overflow/main.c b/regression/cbmc/gcc_builtin_sub_overflow/main.c index cf474be25d1..091e19d2a47 100644 --- a/regression/cbmc/gcc_builtin_sub_overflow/main.c +++ b/regression/cbmc/gcc_builtin_sub_overflow/main.c @@ -71,6 +71,23 @@ void check_unsigned_long_long(void) assert(0 && "reachability"); } +void check_generic(void) +{ + unsigned char small_result; + long long big_result; + + assert(__builtin_sub_overflow(5, 10, &small_result)); + assert(!__builtin_sub_overflow(5, 10, &big_result)); + assert(big_result == -5ll); + assert(!__builtin_sub_overflow(10, 5, &small_result)); + assert(small_result == 5); + assert(!__builtin_sub_overflow(10, 5, &big_result)); + assert(big_result == 5ll); + assert(!__builtin_sub_overflow(INT_MIN, INT_MAX, &big_result)); + assert(big_result == 2ll * INT_MIN + 1); + assert(0 && "reachability"); +} + int main(void) { check_int(); @@ -79,4 +96,5 @@ int main(void) check_unsigned(); check_unsigned_long(); check_unsigned_long_long(); + check_generic(); } diff --git a/regression/cbmc/gcc_builtin_sub_overflow/test.desc b/regression/cbmc/gcc_builtin_sub_overflow/test.desc index 3de0e65d7da..8dadd397961 100644 --- a/regression/cbmc/gcc_builtin_sub_overflow/test.desc +++ b/regression/cbmc/gcc_builtin_sub_overflow/test.desc @@ -40,5 +40,15 @@ main.c \[check_unsigned_long_long.assertion.5\] line \d+ assertion result == 0ull: SUCCESS \[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_usubll_overflow\(.* / 2ull, .*, &result\): SUCCESS \[check_unsigned_long_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE +\[check_generic.assertion.1\] line 79 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS +\[check_generic.assertion.2\] line 80 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS +\[check_generic.assertion.3\] line 81 assertion big_result == -5ll: SUCCESS +\[check_generic.assertion.4\] line 82 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS +\[check_generic.assertion.5\] line 83 assertion small_result == 5: SUCCESS +\[check_generic.assertion.6\] line 84 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS +\[check_generic.assertion.7\] line 85 assertion big_result == 5ll: SUCCESS +\[check_generic.assertion.8\] line 86 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS +\[check_generic.assertion.9\] line 87 assertion big_result == 2ll \* .* \+ 1: SUCCESS +\[check_generic.assertion.10\] line 88 assertion 0 && "reachability": FAILURE ^EXIT=10$ ^SIGNAL=0$ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index fa50f159086..eb081c8c13c 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_typecheck_base.h" #include +#include #include #include @@ -33,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "builtin_factory.h" #include "c_qualifiers.h" #include "c_typecast.h" +#include "expr2c.h" #include "padding.h" #include "type2name.h" @@ -2801,6 +2803,102 @@ exprt c_typecheck_baset::do_special_functions( overflow.type() = bool_typet{}; return overflow; } + else if( + identifier == "__builtin_add_overflow" || + identifier == "__builtin_sub_overflow" || + identifier == "__builtin_mul_overflow") + { + // check function signature + if(expr.arguments().size() != 3) + { + std::ostringstream error_message; + error_message << expr.source_location().as_string() << ": " << identifier + << " takes exactly 3 arguments, but " + << expr.arguments().size() << " were provided"; + throw invalid_source_file_exceptiont{error_message.str()}; + } + + auto lhs = expr.arguments()[0]; + auto rhs = expr.arguments()[1]; + auto result_ptr = expr.arguments()[2]; + + typecheck_expr(lhs); + typecheck_expr(rhs); + typecheck_expr(result_ptr); + + { + auto const raise_wrong_argument_error = + [this, + identifier](const exprt &wrong_argument, std::size_t argument_number) { + std::ostringstream error_message; + error_message << wrong_argument.source_location().as_string() << ": " + << identifier << " has signature " << identifier + << "(integral, integral, integral*), " + << "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}) + { + auto const &argument = expr.arguments()[arg_index]; + + if(!is_signed_or_unsigned_bitvector(argument.type())) + { + raise_wrong_argument_error(argument, arg_index + 1); + } + } + if( + result_ptr.type().id() != ID_pointer || + !is_signed_or_unsigned_bitvector(result_ptr.type().subtype())) + { + raise_wrong_argument_error(result_ptr, 3); + } + } + + // actual logic implementing the operators + auto const make_operation = [&identifier](exprt lhs, exprt rhs) -> exprt { + if(identifier == "__builtin_add_overflow") + { + return plus_exprt{lhs, rhs}; + } + else if(identifier == "__builtin_sub_overflow") + { + return minus_exprt{lhs, rhs}; + } + else + { + INVARIANT( + identifier == "__builtin_mul_overflow", + "the three overflow operations are add, sub and mul"); + return mult_exprt{lhs, rhs}; + } + }; + + // 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{}}); + + auto operation_result = + typecast_exprt{operation, result_ptr.type().subtype()}; + typecheck_expr_typecast(operation_result); + auto overflow_check = notequal_exprt{ + typecast_exprt{dereference_exprt{result_ptr}, integer_typet{}}, + operation}; + typecheck_expr(overflow_check); + return exprt{ID_comma, + bool_typet{}, + {side_effect_expr_assignt{dereference_exprt{result_ptr}, + operation_result, + expr.source_location()}, + overflow_check}}; + } else return nil_exprt(); }