Skip to content

Commit 23306ee

Browse files
tautschnigtautschnig
authored
Merge pull request #6612 from tautschnig/cleanup/c-library-overflow
Cleanup processing and use __builtin_X_overflow
2 parents 048b824 + 291c72a commit 23306ee

File tree

14 files changed

+199
-253
lines changed

14 files changed

+199
-253
lines changed

‎regression/cbmc/gcc_builtin_add_overflow/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,20 @@
11
#include <assert.h>
22
#include <limits.h>
33

4+
#ifndef __GNUC__
5+
_Bool __builtin_add_overflow();
6+
_Bool __builtin_add_overflow_p();
7+
_Bool __builtin_sadd_overflow(int, int, int *);
8+
_Bool __builtin_saddl_overflow(long, long, long *);
9+
_Bool __builtin_saddll_overflow(long long, long long, long long *);
10+
_Bool __builtin_uadd_overflow(unsigned int, unsigned int, unsigned int *);
11+
_Bool __builtin_uaddl_overflow(unsigned long, unsigned long, unsigned long *);
12+
_Bool __builtin_uaddll_overflow(
13+
unsigned long long,
14+
unsigned long long,
15+
unsigned long long *);
16+
#endif
17+
418
void check_int(void)
519
{
620
int const one = 1;

‎regression/cbmc/gcc_builtin_add_overflow/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE gcc-only
1+
CORE
22
main.c
33

44
\[check_int.assertion.1\] line \d+ assertion !__builtin_sadd_overflow\(one, one, &result\): SUCCESS

‎regression/cbmc/gcc_builtin_add_overflow/type-conflict-2.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
type-conflict.c
3+
4+
line 14 function main: __builtin_add_overflow takes exactly 3 arguments, but 2 were provided$
5+
^EXIT=6$
6+
^SIGNAL=0$

‎regression/cbmc/gcc_builtin_add_overflow/type-conflict.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
3+
#ifndef __GNUC__
4+
_Bool __builtin_add_overflow();
5+
_Bool __builtin_add_overflow_p();
6+
#endif
7+
8+
int main(void)
9+
{
10+
int a, b, c, d, r;
11+
#ifdef CONFLICT1
12+
assert(!__builtin_add_overflow(a, b, r));
13+
#endif
14+
assert(__builtin_add_overflow(c, d));
15+
}

‎regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
type-conflict.c
3+
-DCONFLICT1
4+
line 12 function main: __builtin_add_overflow has signature __builtin_add_overflow\(integral, integral, integral\*\), but argument 3 \(r\) has type `signed int`$
5+
^EXIT=6$
6+
^SIGNAL=0$

‎regression/cbmc/gcc_builtin_mul_overflow/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,20 @@
22
#include <limits.h>
33
#include <stdint.h>
44

5+
#ifndef __GNUC__
6+
_Bool __builtin_mul_overflow();
7+
_Bool __builtin_mul_overflow_p();
8+
_Bool __builtin_smul_overflow(int, int, int *);
9+
_Bool __builtin_smull_overflow(long, long, long *);
10+
_Bool __builtin_smulll_overflow(long long, long long, long long *);
11+
_Bool __builtin_umul_overflow(unsigned int, unsigned int, unsigned int *);
12+
_Bool __builtin_umull_overflow(unsigned long, unsigned long, unsigned long *);
13+
_Bool __builtin_umulll_overflow(
14+
unsigned long long,
15+
unsigned long long,
16+
unsigned long long *);
17+
#endif
18+
519
#define A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(T) \
620
(((T)(1)) << (sizeof(T) * CHAR_BIT) / 2 - 1)
721

‎regression/cbmc/gcc_builtin_mul_overflow/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE gcc-only
1+
CORE
22
main.c
33

44
\[check_int.assertion.1\] line \d+ assertion !__builtin_smul_overflow\(1, 1, &result\): SUCCESS

‎regression/cbmc/gcc_builtin_sub_overflow/main.c

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,20 @@
11
#include <assert.h>
22
#include <limits.h>
33

4+
#ifndef __GNUC__
5+
_Bool __builtin_sub_overflow();
6+
_Bool __builtin_sub_overflow_p();
7+
_Bool __builtin_ssub_overflow(int, int, int *);
8+
_Bool __builtin_ssubl_overflow(long, long, long *);
9+
_Bool __builtin_ssubll_overflow(long long, long long, long long *);
10+
_Bool __builtin_usub_overflow(unsigned int, unsigned int, unsigned int *);
11+
_Bool __builtin_usubl_overflow(unsigned long, unsigned long, unsigned long *);
12+
_Bool __builtin_usubll_overflow(
13+
unsigned long long,
14+
unsigned long long,
15+
unsigned long long *);
16+
#endif
17+
418
void check_int(void)
519
{
620
int result;
@@ -30,7 +44,16 @@ void check_long_long(void)
3044
assert(result == 0ll);
3145
assert(__builtin_ssubll_overflow(LLONG_MIN, 1ll, &result));
3246
assert(!__builtin_ssubll_overflow(LLONG_MIN / 2ll, LLONG_MAX / 2ll, &result));
47+
#if !defined(_WIN32)
48+
// Visual Studio x86/32 bit has an 8-byte "long long" type with corresponding
49+
// LLONG_MAX and LLONG_MIN constants (9223372036854775807i64 and
50+
// -9223372036854775807i64 - 1, respectively), but compiles these to 32-bit
51+
// values. The result is that -LLONG_MAX wraps around to the 32-bit value of
52+
// -LLONG_MIN (-2147483648), with the consequence that result == LLONG_MIN
53+
// after the above subtraction. Therefore, disable this assertion on Visual
54+
// Studio x86/32 bit.
3355
assert(result - 1ll == LLONG_MIN);
56+
#endif
3457
assert(0 && "reachability");
3558
}
3659

‎regression/cbmc/gcc_builtin_sub_overflow/test.desc

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE gcc-only
1+
CORE
22
main.c
33

44
\[check_int.assertion.1\] line \d+ assertion !__builtin_ssub_overflow\(1, 1, &result\): SUCCESS
@@ -17,8 +17,7 @@ main.c
1717
\[check_long_long.assertion.2\] line \d+ assertion result == 0ll: SUCCESS
1818
\[check_long_long.assertion.3\] line \d+ assertion __builtin_ssubll_overflow\(.*, 1ll, &result\): SUCCESS
1919
\[check_long_long.assertion.4\] line \d+ assertion !__builtin_ssubll_overflow\(.* / 2ll, .* / 2ll, &result\): SUCCESS
20-
\[check_long_long.assertion.5\] line \d+ assertion result - 1ll == .*: SUCCESS
21-
\[check_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
20+
\[check_long_long.assertion.[56]\] line \d+ assertion 0 && "reachability": FAILURE
2221
\[check_unsigned.assertion.1\] line \d+ assertion !__builtin_usub_overflow\(1u, 1u, &result\): SUCCESS
2322
\[check_unsigned.assertion.2\] line \d+ assertion result == 0u: SUCCESS
2423
\[check_unsigned.assertion.3\] line \d+ assertion __builtin_usub_overflow\(0u, 1u, &result\): SUCCESS
@@ -40,15 +39,17 @@ main.c
4039
\[check_unsigned_long_long.assertion.5\] line \d+ assertion result == 0ull: SUCCESS
4140
\[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_usubll_overflow\(.* / 2ull, .*, &result\): SUCCESS
4241
\[check_unsigned_long_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
43-
\[check_generic.assertion.1\] line 79 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS
44-
\[check_generic.assertion.2\] line 80 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS
45-
\[check_generic.assertion.3\] line 81 assertion big_result == -5ll: SUCCESS
46-
\[check_generic.assertion.4\] line 82 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS
47-
\[check_generic.assertion.5\] line 83 assertion small_result == 5: SUCCESS
48-
\[check_generic.assertion.6\] line 84 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS
49-
\[check_generic.assertion.7\] line 85 assertion big_result == 5ll: SUCCESS
50-
\[check_generic.assertion.8\] line 86 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS
51-
\[check_generic.assertion.9\] line 87 assertion big_result == 2ll \* .* \+ 1: SUCCESS
52-
\[check_generic.assertion.10\] line 88 assertion 0 && "reachability": FAILURE
42+
\[check_generic.assertion.1\] line 102 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS
43+
\[check_generic.assertion.2\] line 103 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS
44+
\[check_generic.assertion.3\] line 104 assertion big_result == -5ll: SUCCESS
45+
\[check_generic.assertion.4\] line 105 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS
46+
\[check_generic.assertion.5\] line 106 assertion small_result == 5: SUCCESS
47+
\[check_generic.assertion.6\] line 107 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS
48+
\[check_generic.assertion.7\] line 108 assertion big_result == 5ll: SUCCESS
49+
\[check_generic.assertion.8\] line 109 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS
50+
\[check_generic.assertion.9\] line 110 assertion big_result == 2ll \* .* \+ 1: SUCCESS
51+
\[check_generic.assertion.10\] line 111 assertion 0 && "reachability": FAILURE
5352
^EXIT=10$
5453
^SIGNAL=0$
54+
--
55+
\[check_long_long.assertion.5\] line \d+ assertion result - 1ll == .*: FAILURE

‎src/ansi-c/c_typecheck_base.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,9 @@ class c_typecheck_baset:
202202
virtual void typecheck_function_call_arguments(
203203
side_effect_expr_function_callt &expr);
204204
virtual exprt do_special_functions(side_effect_expr_function_callt &expr);
205+
exprt typecheck_builtin_overflow(
206+
side_effect_expr_function_callt &expr,
207+
const irep_idt &arith_op);
205208
virtual optionalt<symbol_exprt> typecheck_gcc_polymorphic_builtin(
206209
const irep_idt &identifier,
207210
const exprt::operandst &arguments,

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 89 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -3170,76 +3170,106 @@ exprt c_typecheck_baset::do_special_functions(
31703170
}
31713171
else if(
31723172
identifier == "__builtin_add_overflow" ||
3173+
identifier == "__builtin_sadd_overflow" ||
3174+
identifier == "__builtin_saddl_overflow" ||
3175+
identifier == "__builtin_saddll_overflow" ||
3176+
identifier == "__builtin_uadd_overflow" ||
3177+
identifier == "__builtin_uaddl_overflow" ||
3178+
identifier == "__builtin_uaddll_overflow" ||
3179+
identifier == "__builtin_add_overflow_p")
3180+
{
3181+
return typecheck_builtin_overflow(expr, ID_plus);
3182+
}
3183+
else if(
31733184
identifier == "__builtin_sub_overflow" ||
3185+
identifier == "__builtin_ssub_overflow" ||
3186+
identifier == "__builtin_ssubl_overflow" ||
3187+
identifier == "__builtin_ssubll_overflow" ||
3188+
identifier == "__builtin_usub_overflow" ||
3189+
identifier == "__builtin_usubl_overflow" ||
3190+
identifier == "__builtin_usubll_overflow" ||
3191+
identifier == "__builtin_sub_overflow_p")
3192+
{
3193+
return typecheck_builtin_overflow(expr, ID_minus);
3194+
}
3195+
else if(
31743196
identifier == "__builtin_mul_overflow" ||
3175-
identifier == "__builtin_add_overflow_p" ||
3176-
identifier == "__builtin_sub_overflow_p" ||
3197+
identifier == "__builtin_smul_overflow" ||
3198+
identifier == "__builtin_smull_overflow" ||
3199+
identifier == "__builtin_smulll_overflow" ||
3200+
identifier == "__builtin_umul_overflow" ||
3201+
identifier == "__builtin_umull_overflow" ||
3202+
identifier == "__builtin_umulll_overflow" ||
31773203
identifier == "__builtin_mul_overflow_p")
31783204
{
3179-
// check function signature
3180-
if(expr.arguments().size() != 3)
3181-
{
3182-
std::ostringstream error_message;
3183-
error_message << expr.source_location().as_string() << ": " << identifier
3184-
<< " takes exactly 3 arguments, but "
3185-
<< expr.arguments().size() << " were provided";
3186-
throw invalid_source_file_exceptiont{error_message.str()};
3187-
}
3205+
return typecheck_builtin_overflow(expr, ID_mult);
3206+
}
3207+
else
3208+
return nil_exprt();
3209+
// NOLINTNEXTLINE(readability/fn_size)
3210+
}
31883211

3189-
typecheck_function_call_arguments(expr);
3212+
exprt c_typecheck_baset::typecheck_builtin_overflow(
3213+
side_effect_expr_function_callt &expr,
3214+
const irep_idt &arith_op)
3215+
{
3216+
const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
31903217

3191-
auto lhs = expr.arguments()[0];
3192-
auto rhs = expr.arguments()[1];
3193-
auto result = expr.arguments()[2];
3194-
3195-
const bool is__p_variant = has_suffix(id2string(identifier), "_p");
3196-
3197-
{
3198-
auto const raise_wrong_argument_error =
3199-
[this, identifier](
3200-
const exprt &wrong_argument, std::size_t argument_number, bool _p) {
3201-
std::ostringstream error_message;
3202-
error_message << wrong_argument.source_location().as_string() << ": "
3203-
<< identifier << " has signature " << identifier
3204-
<< "(integral, integral, integral" << (_p ? "" : "*")
3205-
<< "), "
3206-
<< "but argument " << argument_number << " ("
3207-
<< expr2c(wrong_argument, *this) << ") has type `"
3208-
<< type2c(wrong_argument.type(), *this) << '`';
3209-
throw invalid_source_file_exceptiont{error_message.str()};
3210-
};
3211-
for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3212-
{
3213-
auto const &argument = expr.arguments()[arg_index];
3218+
// check function signature
3219+
if(expr.arguments().size() != 3)
3220+
{
3221+
std::ostringstream error_message;
3222+
error_message << expr.source_location().as_string() << ": " << identifier
3223+
<< " takes exactly 3 arguments, but "
3224+
<< expr.arguments().size() << " were provided";
3225+
throw invalid_source_file_exceptiont{error_message.str()};
3226+
}
32143227

3215-
if(!is_signed_or_unsigned_bitvector(argument.type()))
3216-
{
3217-
raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3218-
}
3219-
}
3220-
if(
3221-
!is__p_variant &&
3222-
(result.type().id() != ID_pointer ||
3223-
!is_signed_or_unsigned_bitvector(result.type().subtype())))
3228+
typecheck_function_call_arguments(expr);
3229+
3230+
auto lhs = expr.arguments()[0];
3231+
auto rhs = expr.arguments()[1];
3232+
auto result = expr.arguments()[2];
3233+
3234+
const bool is__p_variant = has_suffix(id2string(identifier), "_p");
3235+
3236+
{
3237+
auto const raise_wrong_argument_error =
3238+
[this, identifier](
3239+
const exprt &wrong_argument, std::size_t argument_number, bool _p) {
3240+
std::ostringstream error_message;
3241+
error_message << wrong_argument.source_location().as_string() << ": "
3242+
<< identifier << " has signature " << identifier
3243+
<< "(integral, integral, integral" << (_p ? "" : "*")
3244+
<< "), "
3245+
<< "but argument " << argument_number << " ("
3246+
<< expr2c(wrong_argument, *this) << ") has type `"
3247+
<< type2c(wrong_argument.type(), *this) << '`';
3248+
throw invalid_source_file_exceptiont{error_message.str()};
3249+
};
3250+
for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3251+
{
3252+
auto const &argument = expr.arguments()[arg_index];
3253+
3254+
if(!is_signed_or_unsigned_bitvector(argument.type()))
32243255
{
3225-
raise_wrong_argument_error(result, 3, is__p_variant);
3256+
raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
32263257
}
32273258
}
3228-
3229-
irep_idt kind =
3230-
has_prefix(id2string(identifier), "__builtin_add_overflow")
3231-
? ID_plus
3232-
: has_prefix(id2string(identifier), "__builtin_sub_overflow") ? ID_minus
3233-
: ID_mult;
3234-
3235-
return side_effect_expr_overflowt{kind,
3236-
std::move(lhs),
3237-
std::move(rhs),
3238-
std::move(result),
3239-
expr.source_location()};
3259+
if(
3260+
!is__p_variant &&
3261+
(result.type().id() != ID_pointer ||
3262+
!is_signed_or_unsigned_bitvector(result.type().subtype())))
3263+
{
3264+
raise_wrong_argument_error(result, 3, is__p_variant);
3265+
}
32403266
}
3241-
else
3242-
return nil_exprt();
3267+
3268+
return side_effect_expr_overflowt{arith_op,
3269+
std::move(lhs),
3270+
std::move(rhs),
3271+
std::move(result),
3272+
expr.source_location()};
32433273
}
32443274

32453275
/// Typecheck the parameters in a function call expression, and where

0 commit comments

Comments
 (0)