Skip to content

Commit ef623c2

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #5233 from hannes-steffenhagen-diffblue/feature/gcc_overflow_builtins
Add __builtin_add_overflow primitives
2 parents ff4e5f5 + 448906f commit ef623c2

File tree

4 files changed

+206
-1
lines changed

4 files changed

+206
-1
lines changed

‎regression/cbmc/gcc_builtin_add_overflow/main.c

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
#include <assert.h>
2+
#include <limits.h>
3+
4+
void check_int(void)
5+
{
6+
int const one = 1;
7+
int result;
8+
9+
assert(!__builtin_sadd_overflow(one, one, &result));
10+
assert(result == 2);
11+
assert(__builtin_sadd_overflow(one, INT_MAX, &result));
12+
assert(!__builtin_sadd_overflow(INT_MAX / 2, INT_MAX / 2, &result));
13+
assert(result + 1 == INT_MAX);
14+
assert(__builtin_sadd_overflow(INT_MAX / 2 + 2, INT_MAX / 2 + 2, &result));
15+
assert(__builtin_sadd_overflow(-one, INT_MIN, &result));
16+
assert(0 && "reachability");
17+
}
18+
19+
void check_long(void)
20+
{
21+
long const one = 1l;
22+
long result;
23+
24+
assert(!__builtin_saddl_overflow(one, one, &result));
25+
assert(result == 2l);
26+
assert(__builtin_saddl_overflow(one, LONG_MAX, &result));
27+
assert(!__builtin_saddl_overflow(LONG_MAX / 2l, LONG_MAX / 2l, &result));
28+
assert(result + 1l == LONG_MAX);
29+
assert(
30+
__builtin_saddl_overflow(LONG_MAX / 2l + 2l, LONG_MAX / 2l + 2l, &result));
31+
assert(__builtin_saddl_overflow(-one, LONG_MIN, &result));
32+
assert(0 && "reachability");
33+
}
34+
35+
void check_long_long(void)
36+
{
37+
long long const one = 1ll;
38+
long long result;
39+
40+
assert(!__builtin_saddll_overflow(one, one, &result));
41+
assert(result == 2ll);
42+
assert(__builtin_saddll_overflow(one, LLONG_MAX, &result));
43+
assert(!__builtin_saddll_overflow(LLONG_MAX / 2ll, LLONG_MAX / 2ll, &result));
44+
assert(result + 1ll == LLONG_MAX);
45+
assert(__builtin_saddll_overflow(
46+
LLONG_MAX / 2ll + 2ll, LLONG_MAX / 2ll + 2ll, &result));
47+
assert(__builtin_saddll_overflow(-one, LLONG_MIN, &result));
48+
assert(0 && "reachability");
49+
}
50+
51+
void check_unsigned(void)
52+
{
53+
unsigned const one = 1u;
54+
unsigned result;
55+
56+
assert(!__builtin_uadd_overflow(one, one, &result));
57+
assert(result == 2u);
58+
assert(!__builtin_uadd_overflow(UINT_MAX / 2, UINT_MAX / 2, &result));
59+
assert(result + 1u == UINT_MAX);
60+
assert(__builtin_uadd_overflow(UINT_MAX / 2 + 2, UINT_MAX / 2 + 2, &result));
61+
assert(__builtin_uadd_overflow(one, UINT_MAX, &result));
62+
assert(0 && "reachability");
63+
}
64+
65+
void check_unsigned_long(void)
66+
{
67+
unsigned long const one = 1ul;
68+
unsigned long result;
69+
70+
assert(!__builtin_uaddl_overflow(one, one, &result));
71+
assert(result == 2ul);
72+
assert(!__builtin_uaddl_overflow(ULONG_MAX / 2, ULONG_MAX / 2, &result));
73+
assert(result + 1ul == ULONG_MAX);
74+
assert(
75+
__builtin_uaddl_overflow(ULONG_MAX / 2 + 2, ULONG_MAX / 2 + 2, &result));
76+
assert(__builtin_uaddl_overflow(one, ULONG_MAX, &result));
77+
assert(0 && "reachability");
78+
}
79+
80+
void check_unsigned_long_long(void)
81+
{
82+
unsigned long long const one = 1ull;
83+
unsigned long long result;
84+
85+
assert(!__builtin_uaddl_overflow(one, one, &result));
86+
assert(result == 2ull);
87+
assert(!__builtin_uaddll_overflow(ULLONG_MAX / 2, ULLONG_MAX / 2, &result));
88+
assert(result + 1ull == ULLONG_MAX);
89+
assert(
90+
__builtin_uaddll_overflow(ULLONG_MAX / 2 + 2, ULLONG_MAX / 2 + 2, &result));
91+
assert(__builtin_uaddl_overflow(one, ULLONG_MAX, &result));
92+
assert(0 && "reachability");
93+
}
94+
95+
int main(void)
96+
{
97+
check_int();
98+
check_long();
99+
check_long_long();
100+
check_unsigned();
101+
check_unsigned_long();
102+
check_unsigned_long_long();
103+
}

‎regression/cbmc/gcc_builtin_add_overflow/test.desc

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
CORE gcc-only
2+
main.c
3+
4+
\[check_int.assertion.1\] line \d+ assertion !__builtin_sadd_overflow\(one, one, &result\): SUCCESS
5+
\[check_int.assertion.2\] line \d+ assertion result == 2: SUCCESS
6+
\[check_int.assertion.3\] line \d+ assertion __builtin_sadd_overflow\(one, .*, &result\): SUCCESS
7+
\[check_int.assertion.4\] line \d+ assertion !__builtin_sadd_overflow\(.* / 2, .* / 2, &result\): SUCCESS
8+
\[check_int.assertion.5\] line \d+ assertion result \+ 1 == .*: SUCCESS
9+
\[check_int.assertion.6\] line \d+ assertion __builtin_sadd_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS
10+
\[check_int.assertion.7\] line \d+ assertion __builtin_sadd_overflow\(-one, .*, &result\): SUCCESS
11+
\[check_int.assertion.8\] line \d+ assertion 0 && "reachability": FAILURE
12+
\[check_long.assertion.1\] line \d+ assertion !__builtin_saddl_overflow\(one, one, &result\): SUCCESS
13+
\[check_long.assertion.2\] line \d+ assertion result == 2l: SUCCESS
14+
\[check_long.assertion.3\] line \d+ assertion __builtin_saddl_overflow\(one, .*, &result\): SUCCESS
15+
\[check_long.assertion.4\] line \d+ assertion !__builtin_saddl_overflow\(.* / 2l, .* / 2l, &result\): SUCCESS
16+
\[check_long.assertion.5\] line \d+ assertion result \+ 1l == .*: SUCCESS
17+
\[check_long.assertion.6\] line \d+ assertion __builtin_saddl_overflow\(.* / 2l \+ 2l, .* / 2l \+ 2l, &result\): SUCCESS
18+
\[check_long.assertion.7\] line \d+ assertion __builtin_saddl_overflow\(-one, .*, &result\): SUCCESS
19+
\[check_long.assertion.8\] line \d+ assertion 0 && "reachability": FAILURE
20+
\[check_long_long.assertion.1\] line \d+ assertion !__builtin_saddll_overflow\(one, one, &result\): SUCCESS
21+
\[check_long_long.assertion.2\] line \d+ assertion result == 2ll: SUCCESS
22+
\[check_long_long.assertion.3\] line \d+ assertion __builtin_saddll_overflow\(one, .*, &result\): SUCCESS
23+
\[check_long_long.assertion.4\] line \d+ assertion !__builtin_saddll_overflow\(.* / 2ll, .* / 2ll, &result\): SUCCESS
24+
\[check_long_long.assertion.5\] line \d+ assertion result \+ 1ll == .*: SUCCESS
25+
\[check_long_long.assertion.6\] line \d+ assertion __builtin_saddll_overflow\(.* / 2ll \+ 2ll, .* / 2ll \+ 2ll, &result\): SUCCESS
26+
\[check_long_long.assertion.7\] line \d+ assertion __builtin_saddll_overflow\(-one, .*, &result\): SUCCESS
27+
\[check_long_long.assertion.8\] line \d+ assertion 0 && "reachability": FAILURE
28+
\[check_unsigned.assertion.1\] line \d+ assertion !__builtin_uadd_overflow\(one, one, &result\): SUCCESS
29+
\[check_unsigned.assertion.2\] line \d+ assertion result == 2u: SUCCESS
30+
\[check_unsigned.assertion.3\] line \d+ assertion !__builtin_uadd_overflow\(.* / 2, .* / 2, &result\): SUCCESS
31+
\[check_unsigned.assertion.4\] line \d+ assertion result \+ 1u == .*: SUCCESS
32+
\[check_unsigned.assertion.5\] line \d+ assertion __builtin_uadd_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS
33+
\[check_unsigned.assertion.6\] line \d+ assertion __builtin_uadd_overflow\(one, .*, &result\): SUCCESS
34+
\[check_unsigned.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
35+
\[check_unsigned_long.assertion.1\] line \d+ assertion !__builtin_uaddl_overflow\(one, one, &result\): SUCCESS
36+
\[check_unsigned_long.assertion.2\] line \d+ assertion result == 2ul: SUCCESS
37+
\[check_unsigned_long.assertion.3\] line \d+ assertion !__builtin_uaddl_overflow\(.* / 2, .* / 2, &result\): SUCCESS
38+
\[check_unsigned_long.assertion.4\] line \d+ assertion result \+ 1ul == .*: SUCCESS
39+
\[check_unsigned_long.assertion.5\] line \d+ assertion __builtin_uaddl_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS
40+
\[check_unsigned_long.assertion.6\] line \d+ assertion __builtin_uaddl_overflow\(one, .*, &result\): SUCCESS
41+
\[check_unsigned_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
42+
\[check_unsigned_long_long.assertion.1\] line \d+ assertion !__builtin_uaddl_overflow\(one, one, &result\): SUCCESS
43+
\[check_unsigned_long_long.assertion.2\] line \d+ assertion result == 2ull: SUCCESS
44+
\[check_unsigned_long_long.assertion.3\] line \d+ assertion !__builtin_uaddll_overflow\(.* / 2, .* / 2, &result\): SUCCESS
45+
\[check_unsigned_long_long.assertion.4\] line \d+ assertion result \+ 1ull == .*: SUCCESS
46+
\[check_unsigned_long_long.assertion.5\] line \d+ assertion __builtin_uaddll_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS
47+
\[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_uaddl_overflow\(one, .*, &result\): SUCCESS
48+
\[check_unsigned_long_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
49+
VERIFICATION FAILED
50+
^EXIT=10$
51+
^SIGNAL=0$

‎src/ansi-c/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ endforeach()
1313

1414
add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
1515
COMMAND converter < ${converter_input_path} > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
16-
DEPENDS converter
16+
DEPENDS converter ${converter_input_path}
1717
)
1818

1919
add_executable(file_converter file_converter.cpp)

‎src/ansi-c/library/math.c

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2299,5 +2299,56 @@ long double copysignl(long double x, long double y)
22992299
return (signbit(y)) ? -abs : abs;
23002300
}
23012301

2302+
/* FUNCTION: __builtin_sadd_overflow */
23022303

2304+
_Bool __builtin_sadd_overflow(int a, int b, int *res)
2305+
{
2306+
*res = a + b;
2307+
return __CPROVER_overflow_plus(a, b);
2308+
}
2309+
2310+
/* FUNCTION: __builtin_saddl_overflow */
2311+
2312+
_Bool __builtin_saddl_overflow(long a, long b, long *res)
2313+
{
2314+
*res = a + b;
2315+
return __CPROVER_overflow_plus(a, b);
2316+
}
2317+
2318+
/* FUNCTION: __builtin_saddll_overflow */
2319+
2320+
_Bool __builtin_saddll_overflow(long long a, long long b, long long *res)
2321+
{
2322+
*res = a + b;
2323+
return __CPROVER_overflow_plus(a, b);
2324+
}
2325+
2326+
/* FUNCTION: __builtin_uadd_overflow */
23032327

2328+
_Bool __builtin_uadd_overflow(unsigned a, unsigned b, unsigned *res)
2329+
{
2330+
*res = a + b;
2331+
return __CPROVER_overflow_plus(a, b);
2332+
}
2333+
2334+
/* FUNCTION: __builtin_uaddl_overflow */
2335+
2336+
_Bool __builtin_uaddl_overflow(
2337+
unsigned long a,
2338+
unsigned long b,
2339+
unsigned long *res)
2340+
{
2341+
*res = a + b;
2342+
return __CPROVER_overflow_plus(a, b);
2343+
}
2344+
2345+
/* FUNCTION: __builtin_uaddll_overflow */
2346+
2347+
_Bool __builtin_uaddll_overflow(
2348+
unsigned long long a,
2349+
unsigned long long b,
2350+
unsigned long long *res)
2351+
{
2352+
*res = a + b;
2353+
return __CPROVER_overflow_plus(a, b);
2354+
}

0 commit comments

Comments
 (0)