Skip to content

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Dec 11, 2025

This PR fixes a SIGFPE crash on x86_64 when evaluating INT_MIN / -1 or INT_MIN % -1 for signed integer types.

On x86_64, the idiv instruction traps when the quotient overflows the destination register. For signed integers, INT_MIN / -1 produces a result that overflows (e.g., -2147483648 / -1 = 2147483648 which doesn't fit in Int32). ARM64's sdiv instruction wraps instead of trapping.

The fix:

  • For Int8/Int16/Int32: widen to the next larger type before dividing/modding, then truncate back
  • For Int64: explicitly check for the overflow case and return the wrapped result

Fixes #11612

🤖 Prepared with Claude Code

@kim-em kim-em added the changelog-language Language features and metaprograms label Dec 12, 2025
@kim-em kim-em force-pushed the fix-sint-div-overflow branch from e4b1cc2 to 5792407 Compare December 12, 2025 00:53
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 12, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3bd1dd633f29de1dd0ea0e23833da7710bdb1c25 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-12 00:54:52)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3bd1dd633f29de1dd0ea0e23833da7710bdb1c25 --onto eee58f4506d28a14c9a171165f999445a0663d93. You can force reference manual CI using the force-manual-ci label. (2025-12-12 00:54:53)

On x86_64, INT_MIN / -1 and INT_MIN % -1 cause a SIGFPE because the x86
idiv instruction traps when the quotient overflows the destination
register. ARM64's sdiv wraps instead.

For Int8/Int16/Int32: widen to the next larger type, divide/mod, truncate back.
For Int64: explicitly check for the overflow case.

Fixes #11612
@kim-em kim-em force-pushed the fix-sint-div-overflow branch from a0cee2d to 219e5d6 Compare December 13, 2025 02:13
@kim-em kim-em added this pull request to the merge queue Dec 13, 2025
Merged via the queue into master with commit 67ba4da Dec 13, 2025
15 checks passed
@sgraf812
Copy link
Contributor

(LGTM!)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

SIGFPE crash on x86_64 when evaluating Int32.minValue / -1

5 participants