riscv64: do not trap on division by zero (RISC-V defines it) - #84
Open
DORA-B wants to merge 2 commits into
Open
Conversation
The RV64M remainder lifters were wrong for three of the four cases: * remu (OP, funct3=0b111) used Iop_DivModS64to64 -- the signed divmod, identical to rem -- so it returned the SIGNED remainder. Wrong whenever the signed and unsigned remainders differ (~60% of random operand pairs). VEX has no Iop_DivModU64to64, so this zero-extends rs1 to 128 bits and uses the unsigned 128/64 divmod (Iop_DivModU128to64); its high 64 bits are the unsigned remainder. * remw / remuw (OP-32, funct3=0b110 / 0b111) passed getIReg64(rs1), the full 64-bit register, as the dividend of a 64->32 divmod. These operate on rs1[31:0], so the dividend must be the sign/zero-extension of the low 32 bits, exactly as divw/divuw already do via getIReg32(rs1). Fixed to feed 32Sto64 / 32Uto64 of getIReg32(rs1). div/divu/divw/divuw and 64-bit rem were already correct. Verified by rebuilding pyvex against the patched VEX: all 8 div/rem ops match the RISC-V Unprivileged ISA (M extension) and the Sail formal model over 1500 random + edge inputs (0 mismatch); previously remu ~60% wrong and remw/remuw ~100% wrong.
RISC-V's M extension defines divide-by-zero and the signed overflow corner as NON-TRAPPING with fixed results: div/0=-1, divu/0=all-ones, rem/0=remu/0= dividend, div(INT_MIN,-1)=INT_MIN, rem(INT_MIN,-1)=0. pyvex's generic ZeroDivisionPostProcessor inserts an Ijk_SigFPE_IntDiv exit before every Div/Mod (correct for x86/ARM, wrong for RISC-V), and the defined values were never produced. Fix in the frontend: divide by a forced-nonzero divisor and select the RISC-V-defined value when the divisor is zero; the Div operand is then provably nonzero so the auto-inserted guard is always-false (dead) and no host divide-by- zero occurs. Overflow corner handled by the wrapping divmod. Verified by rebuilding pyvex: all 8 forms (div/divu/rem/remu + w) return the spec values for zero divisor and the INT_MIN/-1 corner, and remain correct over the nonzero domain (0/1000 mismatch each).
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.
Target: https://github.com/angr/vex —
priv/guest_riscv64_toIR.cKind: PR (patch + repro). Stacked on PR #83 (remainder fixes) — the two
touch the same eight div/rem cases; #83 should merge first, after which this
PR's diff reduces to the divide-by-zero delta.
Verified: angr/pyvex 9.2.221 / 9.3.0 and current
master.Summary
RISC-V's M extension defines integer divide-by-zero and the single signed
overflow case as non-trapping, with fixed results:
divdivuremremu(The spec: "We considered raising exceptions on integer divide by zero…
Instead… no exceptions are raised.")
But pyvex's generic
lifting/zerodivision.py(ZeroDivisionPostProcessor)inserts an
Ijk_SigFPE_IntDivexit before everyDiv/Modop — correctfor x86/ARM where ÷0 traps, wrong for RISC-V. Result: a RISC-V program doing
divu x, x, 0takes a spurious SIGFPE and never gets the defined all-onesvalue (under angr this surfaces as a
divide by zero!exception).Reproduction (before the fix)