diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index f21d36c60d..69ca8df7d4 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -2664,15 +2664,19 @@ static inline size_t lean_isize_mul(size_t a1, size_t a2) { static inline size_t lean_isize_div(size_t a1, size_t a2) { ptrdiff_t lhs = (ptrdiff_t)a1; ptrdiff_t rhs = (ptrdiff_t)a2; - - return (size_t)(rhs == 0 ? 0 : lhs / rhs); + if (rhs == 0) return 0; + // Check for overflow: PTRDIFF_MIN / -1 would trap on x86 idiv + if (lhs == PTRDIFF_MIN && rhs == -1) return (size_t)PTRDIFF_MIN; + return (size_t)(lhs / rhs); } static inline size_t lean_isize_mod(size_t a1, size_t a2) { ptrdiff_t lhs = (ptrdiff_t)a1; ptrdiff_t rhs = (ptrdiff_t)a2; - - return (size_t)(rhs == 0 ? lhs : lhs % rhs); + if (rhs == 0) return (size_t)lhs; + // Check for overflow: PTRDIFF_MIN / -1 would trap on x86 idiv + if (lhs == PTRDIFF_MIN && rhs == -1) return 0; + return (size_t)(lhs % rhs); } static inline size_t lean_isize_land(size_t a1, size_t a2) { diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..ed90dfb687 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,7 @@ #include "util/options.h" +// I would like this to be regenerated please. + namespace lean { options get_default_options() { options opts; diff --git a/tests/lean/run/sint_div_overflow.lean b/tests/lean/run/sint_div_overflow.lean index 8cc521b19f..ce2e084e7b 100644 --- a/tests/lean/run/sint_div_overflow.lean +++ b/tests/lean/run/sint_div_overflow.lean @@ -15,6 +15,7 @@ and 0 for mod. #guard (Int16.minValue / -1 : Int16) == Int16.minValue #guard (Int32.minValue / -1 : Int32) == Int32.minValue #guard (Int64.minValue / -1 : Int64) == Int64.minValue +#guard (ISize.minValue / -1 : ISize) == ISize.minValue -- Test that signed mod handles overflow correctly -- INT_MIN % -1 should return 0 @@ -23,14 +24,17 @@ and 0 for mod. #guard (Int16.minValue % -1 : Int16) == 0 #guard (Int32.minValue % -1 : Int32) == 0 #guard (Int64.minValue % -1 : Int64) == 0 +#guard (ISize.minValue % -1 : ISize) == 0 -- Also test via #eval to exercise the C runtime #eval (Int8.minValue / -1 : Int8) #eval (Int16.minValue / -1 : Int16) #eval (Int32.minValue / -1 : Int32) #eval (Int64.minValue / -1 : Int64) +#eval (ISize.minValue / -1 : ISize) #eval (Int8.minValue % -1 : Int8) #eval (Int16.minValue % -1 : Int16) #eval (Int32.minValue % -1 : Int32) #eval (Int64.minValue % -1 : Int64) +#eval (ISize.minValue % -1 : ISize)