From 71be4901c37741b97cf999b31da01b6a3e29dfb4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 28 Jan 2026 08:16:15 -0800 Subject: [PATCH] fix: do not compile with `-fwrapv` (#12132) This PR removes the requirement that libraries compiled against the lean headers must use `-fwrapv`. clang [documents](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html#:~:text=Note%20that%20checks%20are%20still%20added%20even%20when%20%2Dfwrapv%20is%20enabled) that `-fwrapv` does not automatically turn off the integer overflow sanitizer; and so overflow should still be avoided in normal execution. This is a retry of #12098 after it was reverted in #12125. --- src/CMakeLists.txt | 4 - src/include/lean/lean.h | 192 ++++++++++++++++------------------------ 2 files changed, 75 insertions(+), 121 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0c14ac0453..3d57848dd3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -180,10 +180,6 @@ endif() # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection string(APPEND LEANC_EXTRA_CC_FLAGS " -fstack-clash-protection") -# This makes signed integer overflow guaranteed to match 2's complement. -string(APPEND CMAKE_CXX_FLAGS " -fwrapv") -string(APPEND LEANC_EXTRA_CC_FLAGS " -fwrapv") - if(NOT MULTI_THREAD) message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel") set(AUTO_THREAD_FINALIZATION OFF) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 69ca8df7d4..5138fefddc 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1808,7 +1808,7 @@ static inline uint8_t lean_uint8_of_nat_mk(lean_obj_arg a) { uint8_t r = lean_ui static inline lean_obj_res lean_uint8_to_nat(uint8_t a) { return lean_usize_to_nat((size_t)a); } static inline uint8_t lean_uint8_add(uint8_t a1, uint8_t a2) { return a1+a2; } static inline uint8_t lean_uint8_sub(uint8_t a1, uint8_t a2) { return a1-a2; } -static inline uint8_t lean_uint8_mul(uint8_t a1, uint8_t a2) { return a1*a2; } +static inline uint8_t lean_uint8_mul(uint8_t a1, uint8_t a2) { return 1U*a1*a2; } static inline uint8_t lean_uint8_div(uint8_t a1, uint8_t a2) { return a2 == 0 ? 0 : a1/a2; } static inline uint8_t lean_uint8_mod(uint8_t a1, uint8_t a2) { return a2 == 0 ? a1 : a1%a2; } static inline uint8_t lean_uint8_land(uint8_t a, uint8_t b) { return a & b; } @@ -1846,7 +1846,7 @@ static inline uint16_t lean_uint16_of_nat_mk(lean_obj_arg a) { uint16_t r = lean static inline lean_obj_res lean_uint16_to_nat(uint16_t a) { return lean_usize_to_nat((size_t)a); } static inline uint16_t lean_uint16_add(uint16_t a1, uint16_t a2) { return a1+a2; } static inline uint16_t lean_uint16_sub(uint16_t a1, uint16_t a2) { return a1-a2; } -static inline uint16_t lean_uint16_mul(uint16_t a1, uint16_t a2) { return a1*a2; } +static inline uint16_t lean_uint16_mul(uint16_t a1, uint16_t a2) { return 1U*a1*a2; } static inline uint16_t lean_uint16_div(uint16_t a1, uint16_t a2) { return a2 == 0 ? 0 : a1/a2; } static inline uint16_t lean_uint16_mod(uint16_t a1, uint16_t a2) { return a2 == 0 ? a1 : a1%a2; } static inline uint16_t lean_uint16_land(uint16_t a, uint16_t b) { return a & b; } @@ -1883,7 +1883,7 @@ static inline uint32_t lean_uint32_of_nat_mk(lean_obj_arg a) { uint32_t r = lean static inline lean_obj_res lean_uint32_to_nat(uint32_t a) { return lean_usize_to_nat((size_t)a); } static inline uint32_t lean_uint32_add(uint32_t a1, uint32_t a2) { return a1+a2; } static inline uint32_t lean_uint32_sub(uint32_t a1, uint32_t a2) { return a1-a2; } -static inline uint32_t lean_uint32_mul(uint32_t a1, uint32_t a2) { return a1*a2; } +static inline uint32_t lean_uint32_mul(uint32_t a1, uint32_t a2) { return 1U*a1*a2; } static inline uint32_t lean_uint32_div(uint32_t a1, uint32_t a2) { return a2 == 0 ? 0 : a1/a2; } static inline uint32_t lean_uint32_mod(uint32_t a1, uint32_t a2) { return a2 == 0 ? a1 : a1%a2; } static inline uint32_t lean_uint32_land(uint32_t a, uint32_t b) { return a & b; } @@ -1920,7 +1920,7 @@ static inline uint64_t lean_uint64_of_nat(b_lean_obj_arg a) { return lean_is_sca static inline uint64_t lean_uint64_of_nat_mk(lean_obj_arg a) { uint64_t r = lean_uint64_of_nat(a); lean_dec(a); return r; } static inline uint64_t lean_uint64_add(uint64_t a1, uint64_t a2) { return a1+a2; } static inline uint64_t lean_uint64_sub(uint64_t a1, uint64_t a2) { return a1-a2; } -static inline uint64_t lean_uint64_mul(uint64_t a1, uint64_t a2) { return a1*a2; } +static inline uint64_t lean_uint64_mul(uint64_t a1, uint64_t a2) { return 1U*a1*a2; } static inline uint64_t lean_uint64_div(uint64_t a1, uint64_t a2) { return a2 == 0 ? 0 : a1/a2; } static inline uint64_t lean_uint64_mod(uint64_t a1, uint64_t a2) { return a2 == 0 ? a1 : a1%a2; } static inline uint64_t lean_uint64_land(uint64_t a, uint64_t b) { return a & b; } @@ -1989,10 +1989,18 @@ static inline uint32_t lean_usize_to_uint32(size_t a) { return ((uint32_t)a); } static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); } /* - * Note that we compile all files with -frwapv so in the following section all potential UB that - * may arise from signed overflow is forced to match 2's complement behavior. + * Previously we compiled all files with -fwrapv so in the following section all potential UB that + * may arise from signed overflow is forced to match 2's complement behavior. However, this requires + * everyone including `lean.h` to also compile with this setting to avoid violating the one + * definition rule, and also makes it impossible to run the clang sanitizer (which considers + * -fwrapv a feature for graceful failures, not to mark things as intended). * - * We furthermore rely on the implementation defined behavior of gcc/clang to apply reduction mod + * To avoid integer promotion from small unsigned types to `int` in the `mul` functions, we add a + * `1U *` term as recommended by https://stackoverflow.com/a/31083928/102441. This is optimized out, + * but forces a cast to _at least_ `unsigned int`, without having to implicitly assume that this is + * `uint32_t`. + * + * We rely on the implementation defined behavior of gcc/clang to apply reduction mod * 2^N when casting to an integer type of size N: * https://gcc.gnu.org/onlinedocs/gcc/Integers-implementation.html#Integers-implementation * Unfortunately LLVM does not yet document their implementation defined behavior but it is @@ -2032,30 +2040,23 @@ static inline lean_obj_res lean_int8_to_int(uint8_t a) { } static inline uint8_t lean_int8_neg(uint8_t a) { - int8_t arg = (int8_t)a; - - return (uint8_t)(-arg); + // do not cast to `int8_t`, as there underflow is undefined behavior + return -a; } static inline uint8_t lean_int8_add(uint8_t a1, uint8_t a2) { - int8_t lhs = (int8_t)a1; - int8_t rhs = (int8_t)a2; - - return (uint8_t)(lhs + rhs); + // do not cast to `int8_t`, as there overflow is undefined behavior + return a1 + a2; } static inline uint8_t lean_int8_sub(uint8_t a1, uint8_t a2) { - int8_t lhs = (int8_t)a1; - int8_t rhs = (int8_t)a2; - - return (uint8_t)(lhs - rhs); + // do not cast to `int8_t`, as there overflow is undefined behavior + return a1 - a2; } static inline uint8_t lean_int8_mul(uint8_t a1, uint8_t a2) { - int8_t lhs = (int8_t)a1; - int8_t rhs = (int8_t)a2; - - return (uint8_t)(lhs * rhs); + // do not cast to `int8_t`, as there overflow is undefined behavior + return 1U * a1 * a2; } static inline uint8_t lean_int8_div(uint8_t a1, uint8_t a2) { @@ -2103,10 +2104,10 @@ static inline uint8_t lean_int8_shift_right(uint8_t a1, uint8_t a2) { } static inline uint8_t lean_int8_shift_left(uint8_t a1, uint8_t a2) { - int8_t lhs = (int8_t)a1; int8_t rhs = (((int8_t)a2 % 8) + 8) % 8; // this is smod 8 - return (uint8_t)(lhs << rhs); + // do not cast to `int8_t`, as there negative `a1` is undefined behavior + return a1 << (uint8_t)rhs; } static inline uint8_t lean_int8_complement(uint8_t a) { @@ -2116,11 +2117,8 @@ static inline uint8_t lean_int8_complement(uint8_t a) { } static inline uint8_t lean_int8_abs(uint8_t a) { - int8_t arg = (int8_t)a; - - // Recall that we are compiling with -fwrapv so this is guaranteed to - // map INT8_MIN to INT8_MIN - return (uint8_t)(arg < 0 ? -arg : arg); + // do not cast to `int8_t` to negate, as there underflow is undefined behavior + return (int8_t)a < 0 ? -a : a; } static inline uint8_t lean_int8_dec_eq(uint8_t a1, uint8_t a2) { @@ -2183,30 +2181,23 @@ static inline lean_obj_res lean_int16_to_int(uint16_t a) { } static inline uint16_t lean_int16_neg(uint16_t a) { - int16_t arg = (int16_t)a; - - return (uint16_t)(-arg); + // do not cast to `int16_t`, as there underflow is undefined behavior + return -a; } static inline uint16_t lean_int16_add(uint16_t a1, uint16_t a2) { - int16_t lhs = (int16_t)a1; - int16_t rhs = (int16_t)a2; - - return (uint16_t)(lhs + rhs); + // do not cast to `int16_t`, as there overflow is undefined behavior + return a1 + a2; } static inline uint16_t lean_int16_sub(uint16_t a1, uint16_t a2) { - int16_t lhs = (int16_t)a1; - int16_t rhs = (int16_t)a2; - - return (uint16_t)(lhs - rhs); + // do not cast to `int16_t`, as there overflow is undefined behavior + return a1 - a2; } static inline uint16_t lean_int16_mul(uint16_t a1, uint16_t a2) { - int16_t lhs = (int16_t)a1; - int16_t rhs = (int16_t)a2; - - return (uint16_t)(lhs * rhs); + // do not cast to `int16_t`, as there overflow is undefined behavior + return 1U * a1 * a2; } static inline uint16_t lean_int16_div(uint16_t a1, uint16_t a2) { @@ -2254,10 +2245,10 @@ static inline uint16_t lean_int16_shift_right(uint16_t a1, uint16_t a2) { } static inline uint16_t lean_int16_shift_left(uint16_t a1, uint16_t a2) { - int16_t lhs = (int16_t)a1; int16_t rhs = (((int16_t)a2 % 16) + 16) % 16; // this is smod 16 - return (uint16_t)(lhs << rhs); + // do not cast to `int16_t`, as there negative `a1` is undefined behavior + return a1 << (uint16_t)rhs; } static inline uint16_t lean_int16_complement(uint16_t a) { @@ -2267,11 +2258,8 @@ static inline uint16_t lean_int16_complement(uint16_t a) { } static inline uint16_t lean_int16_abs(uint16_t a) { - int16_t arg = (int16_t)a; - - // Recall that we are compiling with -fwrapv so this is guaranteed to - // map INT16_MIN to INT16_MIN - return (uint16_t)(arg < 0 ? -arg : arg); + // do not cast to `int16_t` to negate, as there underflow is undefined behavior + return (int16_t)a < 0 ? -a : a; } static inline uint8_t lean_int16_dec_eq(uint16_t a1, uint16_t a2) { @@ -2333,30 +2321,23 @@ static inline lean_obj_res lean_int32_to_int(uint32_t a) { } static inline uint32_t lean_int32_neg(uint32_t a) { - int32_t arg = (int32_t)a; - - return (uint32_t)(-arg); + // do not cast to `int32_t`, as there underflow is undefined behavior + return -a; } static inline uint32_t lean_int32_add(uint32_t a1, uint32_t a2) { - int32_t lhs = (int32_t)a1; - int32_t rhs = (int32_t)a2; - - return (uint32_t)(lhs + rhs); + // do not cast to `int32_t`, as there overflow is undefined behavior + return a1 + a2; } static inline uint32_t lean_int32_sub(uint32_t a1, uint32_t a2) { - int32_t lhs = (int32_t)a1; - int32_t rhs = (int32_t)a2; - - return (uint32_t)(lhs - rhs); + // do not cast to `int32_t`, as there overflow is undefined behavior + return a1 - a2; } static inline uint32_t lean_int32_mul(uint32_t a1, uint32_t a2) { - int32_t lhs = (int32_t)a1; - int32_t rhs = (int32_t)a2; - - return (uint32_t)(lhs * rhs); + // do not cast to `int32_t`, as there overflow is undefined behavior + return 1U * a1 * a2; } static inline uint32_t lean_int32_div(uint32_t a1, uint32_t a2) { @@ -2404,10 +2385,10 @@ static inline uint32_t lean_int32_shift_right(uint32_t a1, uint32_t a2) { } static inline uint32_t lean_int32_shift_left(uint32_t a1, uint32_t a2) { - int32_t lhs = (int32_t)a1; int32_t rhs = (((int32_t)a2 % 32) + 32) % 32; // this is smod 32 - return (uint32_t)(lhs << rhs); + // do not cast to `int32_t`, as there negative `a1` is undefined behavior + return a1 << (uint32_t)rhs; } static inline uint32_t lean_int32_complement(uint32_t a) { @@ -2417,11 +2398,8 @@ static inline uint32_t lean_int32_complement(uint32_t a) { } static inline uint32_t lean_int32_abs(uint32_t a) { - int32_t arg = (int32_t)a; - - // Recall that we are compiling with -fwrapv so this is guaranteed to - // map INT32_MIN to INT32_MIN - return (uint32_t)(arg < 0 ? -arg : arg); + // do not cast to `int32_t` to negate, as there underflow is undefined behavior + return (int32_t)a < 0 ? -a : a; } static inline uint8_t lean_int32_dec_eq(uint32_t a1, uint32_t a2) { @@ -2483,30 +2461,23 @@ static inline lean_obj_res lean_int64_to_int_sint(uint64_t a) { } static inline uint64_t lean_int64_neg(uint64_t a) { - int64_t arg = (int64_t)a; - - return (uint64_t)(-arg); + // do not cast to `int64_t`, as there underflow is undefined behavior + return -a; } static inline uint64_t lean_int64_add(uint64_t a1, uint64_t a2) { - int64_t lhs = (int64_t)a1; - int64_t rhs = (int64_t)a2; - - return (uint64_t)(lhs + rhs); + // do not cast to `int64_t`, as there overflow is undefined behavior + return a1 + a2; } static inline uint64_t lean_int64_sub(uint64_t a1, uint64_t a2) { - int64_t lhs = (int64_t)a1; - int64_t rhs = (int64_t)a2; - - return (uint64_t)(lhs - rhs); + // do not cast to `int64_t`, as there overflow is undefined behavior + return a1 - a2; } static inline uint64_t lean_int64_mul(uint64_t a1, uint64_t a2) { - int64_t lhs = (int64_t)a1; - int64_t rhs = (int64_t)a2; - - return (uint64_t)(lhs * rhs); + // do not cast to `int64_t`, as there overflow is undefined behavior + return 1U * a1 * a2; } static inline uint64_t lean_int64_div(uint64_t a1, uint64_t a2) { @@ -2556,10 +2527,10 @@ static inline uint64_t lean_int64_shift_right(uint64_t a1, uint64_t a2) { } static inline uint64_t lean_int64_shift_left(uint64_t a1, uint64_t a2) { - int64_t lhs = (int64_t)a1; int64_t rhs = (((int64_t)a2 % 64) + 64) % 64; // this is smod 64 - return (uint64_t)(lhs << rhs); + // do not cast to `int64_t`, as there negative `a1` is undefined behavior + return a1 << (uint64_t)rhs; } static inline uint64_t lean_int64_complement(uint64_t a) { @@ -2569,11 +2540,8 @@ static inline uint64_t lean_int64_complement(uint64_t a) { } static inline uint64_t lean_int64_abs(uint64_t a) { - int64_t arg = (int64_t)a; - - // Recall that we are compiling with -fwrapv so this is guaranteed to - // map INT64_MIN to INT64_MIN - return (uint64_t)(arg < 0 ? -arg : arg); + // do not cast to `int32_t` to negate, as there underflow is undefined behavior + return (int64_t)a < 0 ? -a : a; } static inline uint8_t lean_int64_dec_eq(uint64_t a1, uint64_t a2) { @@ -2635,30 +2603,23 @@ static inline lean_obj_res lean_isize_to_int(size_t a) { } static inline size_t lean_isize_neg(size_t a) { - ptrdiff_t arg = (ptrdiff_t)a; - - return (size_t)(-arg); + // do not cast to `ptrdiff_t`, as there underflow is undefined behavior + return -a; } static inline size_t lean_isize_add(size_t a1, size_t a2) { - ptrdiff_t lhs = (ptrdiff_t)a1; - ptrdiff_t rhs = (ptrdiff_t)a2; - - return (size_t)(lhs + rhs); + // do not cast to `ptrdiff_t`, as there overflow is undefined behavior + return a1 + a2; } static inline size_t lean_isize_sub(size_t a1, size_t a2) { - ptrdiff_t lhs = (ptrdiff_t)a1; - ptrdiff_t rhs = (ptrdiff_t)a2; - - return (size_t)(lhs - rhs); + // do not cast to `ptrdiff_t`, as there overflow is undefined behavior + return a1 - a2; } static inline size_t lean_isize_mul(size_t a1, size_t a2) { - ptrdiff_t lhs = (ptrdiff_t)a1; - ptrdiff_t rhs = (ptrdiff_t)a2; - - return (size_t)(lhs * rhs); + // do not cast to `ptrdiff_t`, as there overflow is undefined behavior + return 1U * a1 * a2; } static inline size_t lean_isize_div(size_t a1, size_t a2) { @@ -2709,11 +2670,11 @@ static inline size_t lean_isize_shift_right(size_t a1, size_t a2) { } static inline size_t lean_isize_shift_left(size_t a1, size_t a2) { - ptrdiff_t lhs = (ptrdiff_t)a1; ptrdiff_t size = sizeof(ptrdiff_t) * 8; ptrdiff_t rhs = (((ptrdiff_t)a2 % size) + size) % size; // this is smod - return (size_t)(lhs << rhs); + // do not cast to `int64_t`, as there negative `a1` is undefined behavior + return a1 << (size_t)rhs; } static inline size_t lean_isize_complement(size_t a) { @@ -2723,11 +2684,8 @@ static inline size_t lean_isize_complement(size_t a) { } static inline size_t lean_isize_abs(size_t a) { - ptrdiff_t arg = (ptrdiff_t)a; - - // Recall that we are compiling with -fwrapv so this is guaranteed to - // map ISIZE_MIN to ISIZE_MIN - return (size_t)(arg < 0 ? -arg : arg); + // do not cast to `ptrdiff_t` to negate, as there underflow is undefined behavior + return (ptrdiff_t)a < 0 ? -a : a; } static inline uint8_t lean_isize_dec_eq(size_t a1, size_t a2) {