Skip to content

riscv64: do not trap on division by zero (RISC-V defines it) - #84

Open
DORA-B wants to merge 2 commits into
angr:masterfrom
DORA-B:fix/riscv64-divzero
Open

riscv64: do not trap on division by zero (RISC-V defines it)#84
DORA-B wants to merge 2 commits into
angr:masterfrom
DORA-B:fix/riscv64-divzero

Conversation

@DORA-B

@DORA-B DORA-B commented Jul 26, 2026

Copy link
Copy Markdown

Target: https://github.com/angr/vexpriv/guest_riscv64_toIR.c
Kind: 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:

op divisor 0 INT_MIN ÷ −1
div −1 (all ones) INT_MIN
divu 2^XLEN−1 (all ones)
rem dividend 0
remu dividend

(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_IntDiv exit before every Div/Mod op — correct
for x86/ARM where ÷0 traps, wrong for RISC-V. Result: a RISC-V program doing
divu x, x, 0 takes a spurious SIGFPE and never gets the defined all-ones
value (under angr this surfaces as a divide by zero! exception).

Reproduction (before the fix)

import angr, claripy, archinfo, logging
[logging.getLogger(n).setLevel(logging.CRITICAL) for n in ('angr','pyvex','cle')]
A = archinfo.ArchRISCV64()
def run(word, a, b):
    st = angr.load_shellcode(word.to_bytes(4,'little'), arch=A).factory.blank_state(addr=0)
    st.regs.x6 = claripy.BVV(a,64); st.regs.x7 = claripy.BVV(b,64)
    try:    return hex(st.solver.eval(st.step(num_inst=1).successors[0].regs.x5))
    except Exception as e: return 'EXC: ' + str(e)
print(run(0x027352b3, 5, 0))   # divu x5,x6,x7 ; b=0 -> 'EXC: divide by zero!'  (spec: all ones)
print(run(0x027362b3, 5, 0))   # rem  x5,x6,x7 ; b=0 -> 'EXC: divide by zero!'  (spec: 5)

DORA-B added 2 commits July 25, 2026 23:15
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).
@DORA-B DORA-B changed the title Fix/riscv64 divzero riscv64: do not trap on division by zero (RISC-V defines it) Jul 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant