From fa1f359101b582f52beab03b71126ccac0f7197e Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 13 Feb 2020 13:09:28 +0000 Subject: [PATCH 1/2] Fix cprover_library.inc dependencies in CMake `cprover_library.inc` should depend on the *.c files, not just the converter itself. --- src/ansi-c/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt index a018bc5619a..e046697bd5f 100644 --- a/src/ansi-c/CMakeLists.txt +++ b/src/ansi-c/CMakeLists.txt @@ -13,7 +13,7 @@ endforeach() add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc" COMMAND converter < ${converter_input_path} > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc" - DEPENDS converter + DEPENDS converter ${converter_input_path} ) add_executable(file_converter file_converter.cpp) From 448906f8ed9cb3640539b9dbc8d408bc1d9b0d29 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 13 Feb 2020 13:53:14 +0000 Subject: [PATCH 2/2] Add support for GCCs __builtin_add_overflow primitives Note: Not the generic version. --- .../cbmc/gcc_builtin_add_overflow/main.c | 103 ++++++++++++++++++ .../cbmc/gcc_builtin_add_overflow/test.desc | 51 +++++++++ src/ansi-c/library/math.c | 51 +++++++++ 3 files changed, 205 insertions(+) create mode 100644 regression/cbmc/gcc_builtin_add_overflow/main.c create mode 100644 regression/cbmc/gcc_builtin_add_overflow/test.desc diff --git a/regression/cbmc/gcc_builtin_add_overflow/main.c b/regression/cbmc/gcc_builtin_add_overflow/main.c new file mode 100644 index 00000000000..dfc8a257960 --- /dev/null +++ b/regression/cbmc/gcc_builtin_add_overflow/main.c @@ -0,0 +1,103 @@ +#include +#include + +void check_int(void) +{ + int const one = 1; + int result; + + assert(!__builtin_sadd_overflow(one, one, &result)); + assert(result == 2); + assert(__builtin_sadd_overflow(one, INT_MAX, &result)); + assert(!__builtin_sadd_overflow(INT_MAX / 2, INT_MAX / 2, &result)); + assert(result + 1 == INT_MAX); + assert(__builtin_sadd_overflow(INT_MAX / 2 + 2, INT_MAX / 2 + 2, &result)); + assert(__builtin_sadd_overflow(-one, INT_MIN, &result)); + assert(0 && "reachability"); +} + +void check_long(void) +{ + long const one = 1l; + long result; + + assert(!__builtin_saddl_overflow(one, one, &result)); + assert(result == 2l); + assert(__builtin_saddl_overflow(one, LONG_MAX, &result)); + assert(!__builtin_saddl_overflow(LONG_MAX / 2l, LONG_MAX / 2l, &result)); + assert(result + 1l == LONG_MAX); + assert( + __builtin_saddl_overflow(LONG_MAX / 2l + 2l, LONG_MAX / 2l + 2l, &result)); + assert(__builtin_saddl_overflow(-one, LONG_MIN, &result)); + assert(0 && "reachability"); +} + +void check_long_long(void) +{ + long long const one = 1ll; + long long result; + + assert(!__builtin_saddll_overflow(one, one, &result)); + assert(result == 2ll); + assert(__builtin_saddll_overflow(one, LLONG_MAX, &result)); + assert(!__builtin_saddll_overflow(LLONG_MAX / 2ll, LLONG_MAX / 2ll, &result)); + assert(result + 1ll == LLONG_MAX); + assert(__builtin_saddll_overflow( + LLONG_MAX / 2ll + 2ll, LLONG_MAX / 2ll + 2ll, &result)); + assert(__builtin_saddll_overflow(-one, LLONG_MIN, &result)); + assert(0 && "reachability"); +} + +void check_unsigned(void) +{ + unsigned const one = 1u; + unsigned result; + + assert(!__builtin_uadd_overflow(one, one, &result)); + assert(result == 2u); + assert(!__builtin_uadd_overflow(UINT_MAX / 2, UINT_MAX / 2, &result)); + assert(result + 1u == UINT_MAX); + assert(__builtin_uadd_overflow(UINT_MAX / 2 + 2, UINT_MAX / 2 + 2, &result)); + assert(__builtin_uadd_overflow(one, UINT_MAX, &result)); + assert(0 && "reachability"); +} + +void check_unsigned_long(void) +{ + unsigned long const one = 1ul; + unsigned long result; + + assert(!__builtin_uaddl_overflow(one, one, &result)); + assert(result == 2ul); + assert(!__builtin_uaddl_overflow(ULONG_MAX / 2, ULONG_MAX / 2, &result)); + assert(result + 1ul == ULONG_MAX); + assert( + __builtin_uaddl_overflow(ULONG_MAX / 2 + 2, ULONG_MAX / 2 + 2, &result)); + assert(__builtin_uaddl_overflow(one, ULONG_MAX, &result)); + assert(0 && "reachability"); +} + +void check_unsigned_long_long(void) +{ + unsigned long long const one = 1ull; + unsigned long long result; + + assert(!__builtin_uaddl_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(0 && "reachability"); +} + +int main(void) +{ + check_int(); + check_long(); + check_long_long(); + check_unsigned(); + check_unsigned_long(); + check_unsigned_long_long(); +} diff --git a/regression/cbmc/gcc_builtin_add_overflow/test.desc b/regression/cbmc/gcc_builtin_add_overflow/test.desc new file mode 100644 index 00000000000..c6341909287 --- /dev/null +++ b/regression/cbmc/gcc_builtin_add_overflow/test.desc @@ -0,0 +1,51 @@ +CORE gcc-only +main.c + +\[check_int.assertion.1\] line \d+ assertion !__builtin_sadd_overflow\(one, one, &result\): SUCCESS +\[check_int.assertion.2\] line \d+ assertion result == 2: SUCCESS +\[check_int.assertion.3\] line \d+ assertion __builtin_sadd_overflow\(one, .*, &result\): SUCCESS +\[check_int.assertion.4\] line \d+ assertion !__builtin_sadd_overflow\(.* / 2, .* / 2, &result\): SUCCESS +\[check_int.assertion.5\] line \d+ assertion result \+ 1 == .*: SUCCESS +\[check_int.assertion.6\] line \d+ assertion __builtin_sadd_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS +\[check_int.assertion.7\] line \d+ assertion __builtin_sadd_overflow\(-one, .*, &result\): SUCCESS +\[check_int.assertion.8\] line \d+ assertion 0 && "reachability": FAILURE +\[check_long.assertion.1\] line \d+ assertion !__builtin_saddl_overflow\(one, one, &result\): SUCCESS +\[check_long.assertion.2\] line \d+ assertion result == 2l: SUCCESS +\[check_long.assertion.3\] line \d+ assertion __builtin_saddl_overflow\(one, .*, &result\): SUCCESS +\[check_long.assertion.4\] line \d+ assertion !__builtin_saddl_overflow\(.* / 2l, .* / 2l, &result\): SUCCESS +\[check_long.assertion.5\] line \d+ assertion result \+ 1l == .*: SUCCESS +\[check_long.assertion.6\] line \d+ assertion __builtin_saddl_overflow\(.* / 2l \+ 2l, .* / 2l \+ 2l, &result\): SUCCESS +\[check_long.assertion.7\] line \d+ assertion __builtin_saddl_overflow\(-one, .*, &result\): SUCCESS +\[check_long.assertion.8\] line \d+ assertion 0 && "reachability": FAILURE +\[check_long_long.assertion.1\] line \d+ assertion !__builtin_saddll_overflow\(one, one, &result\): SUCCESS +\[check_long_long.assertion.2\] line \d+ assertion result == 2ll: SUCCESS +\[check_long_long.assertion.3\] line \d+ assertion __builtin_saddll_overflow\(one, .*, &result\): SUCCESS +\[check_long_long.assertion.4\] line \d+ assertion !__builtin_saddll_overflow\(.* / 2ll, .* / 2ll, &result\): SUCCESS +\[check_long_long.assertion.5\] line \d+ assertion result \+ 1ll == .*: SUCCESS +\[check_long_long.assertion.6\] line \d+ assertion __builtin_saddll_overflow\(.* / 2ll \+ 2ll, .* / 2ll \+ 2ll, &result\): SUCCESS +\[check_long_long.assertion.7\] line \d+ assertion __builtin_saddll_overflow\(-one, .*, &result\): SUCCESS +\[check_long_long.assertion.8\] line \d+ assertion 0 && "reachability": FAILURE +\[check_unsigned.assertion.1\] line \d+ assertion !__builtin_uadd_overflow\(one, one, &result\): SUCCESS +\[check_unsigned.assertion.2\] line \d+ assertion result == 2u: SUCCESS +\[check_unsigned.assertion.3\] line \d+ assertion !__builtin_uadd_overflow\(.* / 2, .* / 2, &result\): SUCCESS +\[check_unsigned.assertion.4\] line \d+ assertion result \+ 1u == .*: SUCCESS +\[check_unsigned.assertion.5\] line \d+ assertion __builtin_uadd_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS +\[check_unsigned.assertion.6\] line \d+ assertion __builtin_uadd_overflow\(one, .*, &result\): SUCCESS +\[check_unsigned.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE +\[check_unsigned_long.assertion.1\] line \d+ assertion !__builtin_uaddl_overflow\(one, one, &result\): SUCCESS +\[check_unsigned_long.assertion.2\] line \d+ assertion result == 2ul: SUCCESS +\[check_unsigned_long.assertion.3\] line \d+ assertion !__builtin_uaddl_overflow\(.* / 2, .* / 2, &result\): SUCCESS +\[check_unsigned_long.assertion.4\] line \d+ assertion result \+ 1ul == .*: SUCCESS +\[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.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.7\] line \d+ assertion 0 && "reachability": FAILURE +VERIFICATION FAILED +^EXIT=10$ +^SIGNAL=0$ diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index 332c8baaffb..41c89213420 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -2299,5 +2299,56 @@ long double copysignl(long double x, long double y) return (signbit(y)) ? -abs : abs; } +/* FUNCTION: __builtin_sadd_overflow */ +_Bool __builtin_sadd_overflow(int a, int b, int *res) +{ + *res = a + b; + return __CPROVER_overflow_plus(a, b); +} + +/* FUNCTION: __builtin_saddl_overflow */ + +_Bool __builtin_saddl_overflow(long a, long b, long *res) +{ + *res = a + b; + return __CPROVER_overflow_plus(a, b); +} + +/* FUNCTION: __builtin_saddll_overflow */ + +_Bool __builtin_saddll_overflow(long long a, long long b, long long *res) +{ + *res = a + b; + return __CPROVER_overflow_plus(a, b); +} + +/* FUNCTION: __builtin_uadd_overflow */ +_Bool __builtin_uadd_overflow(unsigned a, unsigned b, unsigned *res) +{ + *res = a + b; + return __CPROVER_overflow_plus(a, b); +} + +/* FUNCTION: __builtin_uaddl_overflow */ + +_Bool __builtin_uaddl_overflow( + unsigned long a, + unsigned long b, + unsigned long *res) +{ + *res = a + b; + return __CPROVER_overflow_plus(a, b); +} + +/* FUNCTION: __builtin_uaddll_overflow */ + +_Bool __builtin_uaddll_overflow( + unsigned long long a, + unsigned long long b, + unsigned long long *res) +{ + *res = a + b; + return __CPROVER_overflow_plus(a, b); +}