Skip to content

Commit 5beb73b

Browse files
Add support for gccs __builtin_mul_overflow
Not the generic version
1 parent d33d348 commit 5beb73b

File tree

3 files changed

+211
-0
lines changed

3 files changed

+211
-0
lines changed

Diff for: regression/cbmc/gcc_builtin_mul_overflow/main.c

+116
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
#include <assert.h>
2+
#include <limits.h>
3+
#include <stdint.h>
4+
5+
#define A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(T) \
6+
(((T)(1)) << (sizeof(T) * CHAR_BIT) / 2 - 1)
7+
8+
void check_int(void)
9+
{
10+
int result;
11+
assert(!__builtin_smul_overflow(1, 1, &result));
12+
assert(result == 1);
13+
int const lt_isqrt_of_int_max =
14+
A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(int);
15+
assert(!__builtin_smul_overflow(
16+
lt_isqrt_of_int_max, lt_isqrt_of_int_max, &result));
17+
assert(result == lt_isqrt_of_int_max * lt_isqrt_of_int_max);
18+
assert(__builtin_smul_overflow(
19+
lt_isqrt_of_int_max << 1, lt_isqrt_of_int_max << 1, &result));
20+
assert(0 && "reachability");
21+
}
22+
23+
void check_long(void)
24+
{
25+
long result;
26+
assert(!__builtin_smull_overflow(1l, 1l, &result));
27+
assert(result == 1l);
28+
long const lt_isqrt_of_long_max =
29+
A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(long);
30+
assert(!__builtin_smull_overflow(
31+
lt_isqrt_of_long_max, lt_isqrt_of_long_max, &result));
32+
assert(result == lt_isqrt_of_long_max * lt_isqrt_of_long_max);
33+
assert(__builtin_smull_overflow(
34+
lt_isqrt_of_long_max << 1, lt_isqrt_of_long_max << 1, &result));
35+
assert(0 && "reachability");
36+
}
37+
38+
void check_long_long(void)
39+
{
40+
long long result;
41+
assert(!__builtin_smulll_overflow(1ll, 1ll, &result));
42+
assert(result == 1ll);
43+
long long const lt_isqrt_of_long_long_max =
44+
A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(long long);
45+
assert(!__builtin_smulll_overflow(
46+
lt_isqrt_of_long_long_max, lt_isqrt_of_long_long_max, &result));
47+
assert(result == lt_isqrt_of_long_long_max * lt_isqrt_of_long_long_max);
48+
assert(__builtin_smulll_overflow(
49+
lt_isqrt_of_long_long_max << 1, lt_isqrt_of_long_long_max << 1, &result));
50+
assert(0 && "reachability");
51+
}
52+
53+
void check_unsigned(void)
54+
{
55+
unsigned result;
56+
assert(!__builtin_umul_overflow(1u, 1u, &result));
57+
assert(result == 1u);
58+
unsigned const lt_isqrt_of_unsigned_max =
59+
A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(unsigned);
60+
assert(!__builtin_umul_overflow(
61+
lt_isqrt_of_unsigned_max, lt_isqrt_of_unsigned_max, &result));
62+
assert(result == lt_isqrt_of_unsigned_max * lt_isqrt_of_unsigned_max);
63+
assert(__builtin_umul_overflow(
64+
lt_isqrt_of_unsigned_max << 1, lt_isqrt_of_unsigned_max << 1, &result));
65+
assert(0 && "reachability");
66+
}
67+
68+
void check_unsigned_long(void)
69+
{
70+
unsigned long result;
71+
assert(!__builtin_umull_overflow(1ul, 1ul, &result));
72+
assert(result == 1ul);
73+
unsigned long const lt_isqrt_of_unsigned_long_max =
74+
A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(unsigned long);
75+
assert(!__builtin_umull_overflow(
76+
lt_isqrt_of_unsigned_long_max, lt_isqrt_of_unsigned_long_max, &result));
77+
assert(
78+
result == lt_isqrt_of_unsigned_long_max * lt_isqrt_of_unsigned_long_max);
79+
assert(__builtin_umull_overflow(
80+
lt_isqrt_of_unsigned_long_max << 1,
81+
lt_isqrt_of_unsigned_long_max << 1,
82+
&result));
83+
assert(0 && "reachability");
84+
}
85+
86+
void check_unsigned_long_long(void)
87+
{
88+
unsigned long long result;
89+
assert(!__builtin_umulll_overflow(1ull, 1ull, &result));
90+
assert(result == 1ull);
91+
unsigned long long const lt_isqrt_of_unsigned_long_long_max =
92+
A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(unsigned long long);
93+
assert(!__builtin_umulll_overflow(
94+
lt_isqrt_of_unsigned_long_long_max,
95+
lt_isqrt_of_unsigned_long_long_max,
96+
&result));
97+
assert(
98+
result ==
99+
lt_isqrt_of_unsigned_long_long_max * lt_isqrt_of_unsigned_long_long_max);
100+
assert(__builtin_umulll_overflow(
101+
lt_isqrt_of_unsigned_long_long_max << 1,
102+
lt_isqrt_of_unsigned_long_long_max << 1,
103+
&result));
104+
assert(0 && "reachability");
105+
}
106+
107+
int main(void)
108+
{
109+
check_int();
110+
check_long();
111+
check_long_long();
112+
check_unsigned();
113+
check_unsigned_long();
114+
check_unsigned_long_long();
115+
return 0;
116+
}

Diff for: regression/cbmc/gcc_builtin_mul_overflow/test.desc

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
CORE gcc-only
2+
main.c
3+
4+
\[check_int.assertion.1\] line \d+ assertion !__builtin_smul_overflow\(1, 1, &result\): SUCCESS
5+
\[check_int.assertion.2\] line \d+ assertion result == 1: SUCCESS
6+
\[check_int.assertion.3\] line \d+ assertion !__builtin_smul_overflow\( lt_isqrt_of_int_max, lt_isqrt_of_int_max, &result\): SUCCESS
7+
\[check_int.assertion.4\] line \d+ assertion result == lt_isqrt_of_int_max \* lt_isqrt_of_int_max: SUCCESS
8+
\[check_int.assertion.5\] line \d+ assertion __builtin_smul_overflow\( lt_isqrt_of_int_max << 1, lt_isqrt_of_int_max << 1, &result\): SUCCESS
9+
\[check_int.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
10+
\[check_long.assertion.1\] line \d+ assertion !__builtin_smull_overflow\(1l, 1l, &result\): SUCCESS
11+
\[check_long.assertion.2\] line \d+ assertion result == 1l: SUCCESS
12+
\[check_long.assertion.3\] line \d+ assertion !__builtin_smull_overflow\( lt_isqrt_of_long_max, lt_isqrt_of_long_max, &result\): SUCCESS
13+
\[check_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_long_max \* lt_isqrt_of_long_max: SUCCESS
14+
\[check_long.assertion.5\] line \d+ assertion __builtin_smull_overflow\( lt_isqrt_of_long_max << 1, lt_isqrt_of_long_max << 1, &result\): SUCCESS
15+
\[check_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
16+
\[check_long_long.assertion.1\] line \d+ assertion !__builtin_smulll_overflow\(1ll, 1ll, &result\): SUCCESS
17+
\[check_long_long.assertion.2\] line \d+ assertion result == 1ll: SUCCESS
18+
\[check_long_long.assertion.3\] line \d+ assertion !__builtin_smulll_overflow\( lt_isqrt_of_long_long_max, lt_isqrt_of_long_long_max, &result\): SUCCESS
19+
\[check_long_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_long_long_max \* lt_isqrt_of_long_long_max: SUCCESS
20+
\[check_long_long.assertion.5\] line \d+ assertion __builtin_smulll_overflow\( lt_isqrt_of_long_long_max << 1, lt_isqrt_of_long_long_max << 1, &result\): SUCCESS
21+
\[check_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
22+
\[check_unsigned.assertion.1\] line \d+ assertion !__builtin_umul_overflow\(1u, 1u, &result\): SUCCESS
23+
\[check_unsigned.assertion.2\] line \d+ assertion result == 1u: SUCCESS
24+
\[check_unsigned.assertion.3\] line \d+ assertion !__builtin_umul_overflow\( lt_isqrt_of_unsigned_max, lt_isqrt_of_unsigned_max, &result\): SUCCESS
25+
\[check_unsigned.assertion.4\] line \d+ assertion result == lt_isqrt_of_unsigned_max \* lt_isqrt_of_unsigned_max: SUCCESS
26+
\[check_unsigned.assertion.5\] line \d+ assertion __builtin_umul_overflow\( lt_isqrt_of_unsigned_max << 1, lt_isqrt_of_unsigned_max << 1, &result\): SUCCESS
27+
\[check_unsigned.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
28+
\[check_unsigned_long.assertion.1\] line \d+ assertion !__builtin_umull_overflow\(1ul, 1ul, &result\): SUCCESS
29+
\[check_unsigned_long.assertion.2\] line \d+ assertion result == 1ul: SUCCESS
30+
\[check_unsigned_long.assertion.3\] line \d+ assertion !__builtin_umull_overflow\( lt_isqrt_of_unsigned_long_max, lt_isqrt_of_unsigned_long_max, &result\): SUCCESS
31+
\[check_unsigned_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_unsigned_long_max \* lt_isqrt_of_unsigned_long_max: SUCCESS
32+
\[check_unsigned_long.assertion.5\] line \d+ assertion __builtin_umull_overflow\( lt_isqrt_of_unsigned_long_max << 1, lt_isqrt_of_unsigned_long_max << 1, &result\): SUCCESS
33+
\[check_unsigned_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
34+
\[check_unsigned_long_long.assertion.1\] line \d+ assertion !__builtin_umulll_overflow\(1ull, 1ull, &result\): SUCCESS
35+
\[check_unsigned_long_long.assertion.2\] line \d+ assertion result == 1ull: SUCCESS
36+
\[check_unsigned_long_long.assertion.3\] line \d+ assertion !__builtin_umulll_overflow\( lt_isqrt_of_unsigned_long_long_max, lt_isqrt_of_unsigned_long_long_max, &result\): SUCCESS
37+
\[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
38+
\[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
39+
\[check_unsigned_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
40+
^EXIT=10$
41+
^SIGNAL=0$

Diff for: src/ansi-c/library/math.c

+54
Original file line numberDiff line numberDiff line change
@@ -2406,3 +2406,57 @@ _Bool __builtin_usubll_overflow(
24062406
*res = a - b;
24072407
return __CPROVER_overflow_minus(a, b);
24082408
}
2409+
2410+
/* FUNCTION: __builtin_smul_overflow */
2411+
2412+
_Bool __builtin_smul_overflow(int a, int b, int *res)
2413+
{
2414+
*res = a * b;
2415+
return __CPROVER_overflow_mult(a, b);
2416+
}
2417+
2418+
/* FUNCTION: __builtin_smull_overflow */
2419+
2420+
_Bool __builtin_smull_overflow(long a, long b, long *res)
2421+
{
2422+
*res = a * b;
2423+
return __CPROVER_overflow_mult(a, b);
2424+
}
2425+
2426+
/* FUNCTION: __builtin_smulll_overflow */
2427+
2428+
_Bool __builtin_smulll_overflow(long long a, long long b, long long *res)
2429+
{
2430+
*res = a * b;
2431+
return __CPROVER_overflow_mult(a, b);
2432+
}
2433+
2434+
/* FUNCTION: __builtin_umul_overflow */
2435+
2436+
_Bool __builtin_umul_overflow(unsigned a, unsigned b, unsigned *res)
2437+
{
2438+
*res = a * b;
2439+
return __CPROVER_overflow_mult(a, b);
2440+
}
2441+
2442+
/* FUNCTION: __builtin_umull_overflow */
2443+
2444+
_Bool __builtin_umull_overflow(
2445+
unsigned long a,
2446+
unsigned long b,
2447+
unsigned long *res)
2448+
{
2449+
*res = a * b;
2450+
return __CPROVER_overflow_mult(a, b);
2451+
}
2452+
2453+
/* FUNCTION: __builtin_umulll_overflow */
2454+
2455+
_Bool __builtin_umulll_overflow(
2456+
unsigned long long a,
2457+
unsigned long long b,
2458+
unsigned long long *res)
2459+
{
2460+
*res = a * b;
2461+
return __CPROVER_overflow_mult(a, b);
2462+
}

0 commit comments

Comments
 (0)