Miasm ARM: T32 UDIV by zero leaves Rd unchanged in the symbolic engine (Arm ARM: result 0, no trap) #1573

Found by comparing the semantics described in the Arm A32/T32 ISA description with how Miasm implements them. An AI agent found this bug, reproduced it with Miasm 3671fc2 and drafted this report. A second agent tried to refute it and searched upstream for duplicates. The methodology is described here.

What went wrong: Wrong result. udiv in miasm/arch/arm/sem.py lifts a zero divisor to a block that only sets exception_flags = EXCEPT_DIV_BY_ZERO and never writes Rd.

Version: miasm 0.1.5 (v0.1.5, ef52b54d), and upstream 3671fc2 (2026-09-21).

Preconditions: Thumb-2 UDIV (the A32 encoding is not decoded by Miasm); divisor 0. Symbolic engine: no further condition. python/gcc jitters: stop with DIV_BY_ZERO at the instruction.

Input

Thumb bytes b0fb f1f2 531c = udiv r2, r0, r1 ; adds r3, r2, #1, with r0 = 0xffffffff, r1 = 0, r2 = 0x1234.

Command

./run.sh   # PYTHON=<python with miasm> ./run.sh

Output

UDIV       R2, R0, R1
ADDS       R3, R2, 0x1
r2=0x1234 r3=0x1235 (expected r2=0x0 r3=0x1)
BUG PRESENT

Expected

Arm A32/T32 ISA, 2026-03, UDIV, Operation: "if divisor == 0 then result = 0;" followed by "R(d) = result[31:0];", so r2 = 0 and r3 = 1 (qemu-arm 10.2.1 gives r2=0x0 r3=0x1 for the same bytes). The condition flags are not affected. The pseudocode has no trap; the symbolic engine instead keeps the old r2 and SymbolicExecutionEngine.run_at does not stop on exception_flags, so later instructions use the stale value. (The engine does set exception_flags = 0x2010000 in its state, so a caller that checks it after every instruction can see the modelled fault, but the CPU raises none.) With a symbolic divisor, run_at returns R1?(loc_div,loc_except), and the R1 == 0 path again keeps the old Rd. The jitters raise JitterException ... DIV_BY_ZERO (0x2010000) where the CPU continues. Non-zero divisors match.

Location: miasm/arch/arm/sem.py udiv (line 986). Related: open PR #1548 makes the same change for AArch64 only. Older profiles have an optional trap that is off at reset (ARMv7-M CCR.DIV_0_TRP, ARMv7-R SCTLR.DZ). Miasm models neither bit and traps unconditionally.

#!/usr/bin/env bash
# T32 UDIV r2, r0, r1 with r1 = 0, then ADDS r3, r2, #1, in Miasm's symbolic engine.
# Arm ARM pseudocode: divisor == 0 -> result = 0, so r2 = 0 and r3 = 1.
# PYTHON must be a Python with miasm installed. Exit 0 = conforms, 1 = differs, 2 = tool missing.
PYTHON=${PYTHON:-python3}
D="$(cd "$(dirname "$0")" && pwd)"
"$PYTHON" -I -c "import miasm" 2>/dev/null || { echo "miasm not importable with $PYTHON"; exit 2; }
"$PYTHON" -I "$D/udiv.py"

import sys
from miasm.analysis.machine import Machine
from miasm.core.locationdb import LocationDB
from miasm.core.bin_stream import bin_stream_str
from miasm.expression.expression import ExprInt
from miasm.ir.symbexec import SymbolicExecutionEngine
import miasm.arch.arm.regs as R

CODE = 0x1000
# udiv r2, r0, r1 ; adds r3, r2, #1  (Thumb-2)
code = bytes.fromhex("b0fbf1f2" + "531c")
mach = Machine("armtl")
ldb = LocationDB()
mdis = mach.dis_engine(bin_stream_str(code, base_address=CODE), loc_db=ldb)
end = CODE + len(code)
mdis.dont_dis = [end]
asmcfg = mdis.dis_multiblock(CODE)
for b in asmcfg.blocks:
    for l in b.lines:
        print(l)
lifter = mach.lifter_model_call(ldb)
ircfg = lifter.new_ircfg_from_asmcfg(asmcfg)
st = {R.regs32_expr[i]: ExprInt(0, 32) for i in range(13)}
st[R.regs32_expr[0]] = ExprInt(0xffffffff, 32)   # dividend
st[R.regs32_expr[1]] = ExprInt(0, 32)            # divisor
st[R.regs32_expr[2]] = ExprInt(0x1234, 32)       # old Rd
for e in (R.nf, R.zf, R.cf, R.of):
    st[e] = ExprInt(0, 1)
se = SymbolicExecutionEngine(lifter, st)
se.run_at(ircfg, CODE, lbl_stop=ldb.get_offset_location(end))
r2 = int(se.eval_expr(R.regs32_expr[2]))
r3 = int(se.eval_expr(R.regs32_expr[3]))
print("r2=%#x r3=%#x (expected r2=0x0 r3=0x1)" % (r2, r3))
if (r2, r3) != (0, 1):
    print("BUG PRESENT")
    sys.exit(1)
print("OK")

If this is intended behaviour or a duplicate, feel free to close it, and I'll use that as feedback to improve future reports. For questions, or to have this re-checked on a newer version of Miasm, mention @JeroenRobben or email jeroen@robben.io.