Repository navigation
fix: x86 JIT remw returns stale RDX for i32::MIN % -1 - #3010
Merged
Merged
Conversation
The overflow special case in the x86 backend's `remw` was copied from `divw` and leaves its result in RAX, while `remw` stores `rd` from RDX. The `overflow:` block that zeroes RDX sits behind an unconditional jump and is unreachable, so `rd` received whatever RDX held. RISC-V defines `remw(-2^31, -1)` as 0, which the portable executor, the tracing VM and the AIR already compute, so the native executor diverged from them on this operand pair. Write the zero remainder to RDX directly, drop the dead block, and add regression tests for the `remw` and `divw` overflow pair in both immediate and register forms.
rkm0959
approved these changes
Oct 19, 2026
rkm0959
left a comment
rkm0959
left a comment
Contributor
There was a problem hiding this comment.
Thanks for the PR! LGTM.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Motivation
The x86-64 JIT backend special-cases
i32::MIN % -1inremwbecauseidivwould raise#DEfor that operand pair. The special-case branch was copied fromdivw: it writesi32::MINtoRAX, butremwstores its result fromRDX, sordreceives whateverRDXhappened to hold. Theoverflow:block that zeroesRDXsits after an unconditionaljmpand is unreachable.RISC-V defines
remwof-2^31by-1as0, and that is what the portable executor, the tracing VM and the AIR compute. On x86-64 Linux hosts (sp1_use_native_executor) the native executor therefore returns a wrong register value for this one operand pair:execute()reports wrong public values, and when the wrong value reaches memory the trace no longer matches the executor's memory oracle and proving fails. Safe Rust cannot reach it (%on this pair panics even with overflow checks off, and the wrapping/checked variants guard it before the instruction), but C or inline assembly can, and the 64-bitremas well asdiv/divwalready handle the same pair correctly.Found by differential fuzzing of the native executor against the portable executor, the tracing-VM replay and an independent RV64IM model; this was the only divergence across the RV64IM instruction set.
Solution
Write the zero remainder to
RDXon the overflow path and drop the unreachable block. No other code path changes.Tests added in the x86 backend test suite for the
i32::MIN/-1pair onremw(immediate and register forms) anddivw. Theremwtest first leaves a non-zero remainder inRDXso a stale-register result fails deterministically rather than by chance. On x86-64 Linux the newremwtest fails onmainand passes with the fix; the rest of thesp1-jitsuite is unaffected.PR Checklist