Repository navigation
Description
Found by comparing the semantics described in the Arm Architecture Reference Manual 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 in the symbolic engine. it eq; subseq.w r0, r0, r1 (also addseq.w, movseq.w, andseq.w) leaves N/Z/C/V unchanged, so a following beq takes the wrong side and a following adc.w adds the wrong carry.
Version: miasm 0.1.5 (ef52b54d). Also reproduces at upstream head 3671fc2 (2026-09-21).
Preconditions: default Machine("armtl"), IR built with new_ircfg_from_asmcfg, a 32-bit (T32) S-suffixed instruction inside an IT block. The python and gcc jitters cannot run IT blocks at all (PR #1034), so only the symbolic engine is compared.
do_it_block in miasm/arch/arm/sem.py removes every write to zf, nf, of, cf from each instruction of an IT block unless its name is CMP/CMN/TST:
# Remove flags assignment if instr != [CMP, CMN, TST]
if instr.name not in ["CMP", "CMN", "TST"]:
That is the rule for the 16-bit encodings (Arm ARM AArch32 ISA XML 2026-03, ADD (register) T1): let setflags : boolean = !InITBlock();. The 32-bit encoding (T3) is let setflags : boolean = (S == '1');, independent of IT state, and the operation is if setflags then PSTATE.[N,Z,C,V] = nzcv;. Miasm prints both forms as ADDS, so the name does not tell them apart (instr.l does).
Input
cases.txt: it eq; addseq.w / subseq.w / movseq.w / andseq.w with the condition true, a cmp r2,#0; it eq; subseq.w r0,r0,r1; beq case (r0=2, r1=1), a multi-word add it eq; addseq.w r0,r0,r1; adc.w r2,r2,#0 (r0=0xffffffff, r1=1: the carry must reach r2), and two controls (16-bit addeq, cmpne).
Command
PYTHON=<python with miasm> bash ./run.sh (needs arm-none-eabi-binutils and qemu-arm as reference)
Output
DIFF it_addseq_w [it eq ; addseq.w r0, r0, r1 ; mov.w r2, #0] miasm: [IT EQ ; ADDS R0, R0, R1 ; MOV R2, 0x0]
qemu-arm : r0=0x0 r1=0xffffffff r2=0x0 r3=0x0 nzcv=0110
miasm symb : r0=0x0 r1=0xffffffff r2=0x0 r3=0x0 nzcv=0100
DIFF it_subseq_w [it eq ; subseq.w r0, r0, r1 ; mov.w r2, #0] miasm: [IT EQ ; SUBS R0, R0, R1 ; MOV R2, 0x0]
qemu-arm : r0=0x0 r1=0x1 r2=0x0 r3=0x0 nzcv=0110
miasm symb : r0=0x0 r1=0x1 r2=0x0 r3=0x0 nzcv=0100
DIFF it_movseq_w [it eq ; movseq.w r0, r1 ; mov.w r2, #0] miasm: [IT EQ ; MOVS R0, R1 ; MOV R2, 0x0]
qemu-arm : r0=0x80000000 r1=0x80000000 r2=0x0 r3=0x0 nzcv=1000
miasm symb : r0=0x80000000 r1=0x80000000 r2=0x0 r3=0x0 nzcv=0100
DIFF it_subseq_w_then_beq [cmp r2, #0 ; it eq ; subseq.w r0, r0, r1 ; beq 1f ; movs r3, #1 ; b 2f ; 1: movs r3, #2 ; 2:] miasm: [CMP R2, 0x0 ; IT EQ ; SUBS R0, R0, R1 ; BEQ loc_key_1 ; MOVS R3, 0x1 ; B loc_key_3 ; MOVS R3, 0x2]
qemu-arm : r0=0x1 r1=0x1 r2=0x0 r3=0x1 nzcv=0010
miasm symb : r0=0x1 r1=0x1 r2=0x0 r3=0x2 nzcv=0010
DIFF it_andseq_w [it eq ; andseq.w r0, r0, r1 ; mov.w r2, #0] miasm: [IT EQ ; ANDS R0, R0, R1 ; MOV R2, 0x0]
qemu-arm : r0=0x80000000 r1=0x80000000 r2=0x0 r3=0x0 nzcv=1000
miasm symb : r0=0x80000000 r1=0x80000000 r2=0x0 r3=0x0 nzcv=0100
DIFF it_addseq_w_then_adc [it eq ; addseq.w r0, r0, r1 ; adc.w r2, r2, #0] miasm: [IT EQ ; ADDS R0, R0, R1 ; ADC R2, R2, 0x0]
qemu-arm : r0=0x0 r1=0x1 r2=0x1 r3=0x0 nzcv=0110
miasm symb : r0=0x0 r1=0x1 r2=0x0 r3=0x0 nzcv=0100
MATCH it_add16_control [it eq ; addeq r0, r0, r1 ; mov.w r2, #0] miasm: [IT EQ ; ADDS R0, R0, R1 ; MOV R2, 0x0]
qemu-arm : r0=0x0 r1=0xffffffff r2=0x0 r3=0x0 nzcv=0100
miasm symb : r0=0x0 r1=0xffffffff r2=0x0 r3=0x0 nzcv=0100
MATCH it_cmp_control [it ne ; cmpne r0, r1 ; mov.w r2, #0] miasm: [IT NE ; CMP R0, R1 ; MOV R2, 0x0]
qemu-arm : r0=0x1 r1=0x1 r2=0x0 r3=0x0 nzcv=0110
miasm symb : r0=0x1 r1=0x1 r2=0x0 r3=0x0 nzcv=0110
RESULT: BUG PRESENT (exit 1)
In it_addseq_w_then_adc the lost carry also makes a register wrong: r2 = 0 instead of 1.
Suggested fix: strip the flag writes only for 16-bit instructions (instr.l == 2); the 16-bit forms outside CMP/CMN/TST either set flags only outside an IT block (!InITBlock()) or never set them, so stripping their flag writes is safe. With the condition changed to if instr.l == 2 and instr.name not in ["CMP", "CMN", "TST"]: all eight cases above match qemu-arm.
Related: PR #946 (#946) added this filter for the 16-bit forms.
Reproducer files
a32_build.py
"""a32_build.py <cases.txt> <workdir>: for each case build a static ARM/Thumb program (r0-r3 and NZCV preset, then the
snippet), run it under qemu-arm, print r0-r3 and NZCV after the snippet; also write <workdir>/<name>.bin (snippet bytes).
Case line: name arm|thumb r0 r1 r2 r3 nzcv(4 bits) | insn ; insn ; ..."""
import subprocess, sys, struct, os
path, wd = sys.argv[1], sys.argv[2]
for line in open(path):
if not line.strip() or line.startswith("#"): continue
head, body = line.split("|", 1)
name, mode, r0, r1, r2, r3, f = head.split()
insns = "\n".join(" " + i.strip() for i in body.split(";") if i.strip())
src = """.syntax unified
.arch armv7-a
.arch_extension idiv
.%s
.global _start
.text
%s
_start:
ldr r4, =%#x
msr APSR_nzcvq, r4
ldr r0, =%s
ldr r1, =%s
ldr r2, =%s
ldr r3, =%s
snip_s:
%s
snip_e:
mrs r4, apsr
ldr r5, =buf
str r0, [r5]
str r1, [r5, #4]
str r2, [r5, #8]
str r3, [r5, #12]
str r4, [r5, #16]
movs r0, #1
mov r1, r5
movs r2, #20
movs r7, #4
svc 0
movs r0, #0
movs r7, #1
svc 0
.ltorg
.data
.balign 4
buf: .skip 32
""" % (mode, ".thumb_func" if mode == "thumb" else "", int(f, 2) << 28, r0, r1, r2, r3, insns)
b = os.path.join(wd, name)
open(b + ".s", "w").write(src)
if subprocess.run(["arm-none-eabi-as", "-o", b + ".o", b + ".s"]).returncode:
print("%s | asm-error" % name); open(b + ".bin", "wb").write(b""); continue
subprocess.run(["arm-none-eabi-ld", "-Ttext=0x400000", "-o", b, b + ".o"], check=True)
syms = {}
for l in subprocess.run(["arm-none-eabi-nm", b], capture_output=True, text=True).stdout.split("\n"):
p = l.split()
if len(p) == 3: syms[p[2]] = int(p[0], 16)
subprocess.run(["arm-none-eabi-objcopy", "-O", "binary", "-j", ".text", b, b + ".text"], check=True)
t = open(b + ".text", "rb").read()
s, e = syms["snip_s"] - 0x400000, syms["snip_e"] - 0x400000
open(b + ".bin", "wb").write(t[s:e]); open(b + ".addr", "w").write("%#x" % syms["snip_s"])
out = subprocess.run(["timeout", "10", "qemu-arm", b], capture_output=True).stdout
if len(out) != 20:
print("%s | qemu-error %r" % (name, out)); continue
v = struct.unpack("<5I", out); n = v[4]
print("%s | r0=%#x r1=%#x r2=%#x r3=%#x nzcv=%d%d%d%d" % ((name,) + v[:4] + ((n >> 31) & 1, (n >> 30) & 1, (n >> 29) & 1, (n >> 28) & 1)))a32_miasm.py
"""a32_miasm.py <symb|python|gcc> <cases.txt> <workdir>: run each snippet (<workdir>/<name>.bin) in Miasm
(arml / armtl) from the case's r0-r3 and NZCV; print the disassembly, r0-r3 and NZCV at the snippet end."""
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
mode, path, wd = sys.argv[1], sys.argv[2], sys.argv[3]
def symb(mach, code, regs, f, CODE):
from miasm.ir.symbexec import SymbolicExecutionEngine
import miasm.arch.arm.regs as R
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)
asm = " ; ".join(str(l) for b in sorted([b for b in asmcfg.blocks if b.lines], key=lambda b: b.lines[0].offset) for l in b.lines)
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)}
for i, v in enumerate(regs): st[R.regs32_expr[i]] = ExprInt(v, 32)
st[R.SP] = ExprInt(0x30001000, 32); st[R.LR] = ExprInt(0, 32)
for b, e in zip(f, (R.nf, R.zf, R.cf, R.of)): st[e] = ExprInt(int(b), 1)
for e in R.ge_regs: st[e] = ExprInt(0, 1)
se = SymbolicExecutionEngine(lifter, st)
addr = se.run_at(ircfg, CODE, lbl_stop=ldb.get_offset_location(end))
if not (addr.is_int() and int(addr) == end) and not (addr.is_loc() and ldb.get_location_offset(addr.loc_key) == end):
raise RuntimeError("stopped at %s" % addr)
def g(e):
v = se.eval_expr(e)
return ("%#x" % int(v)) if v.is_int() else "?(%s)" % v
fl = "".join(g(e)[-1] if g(e) in ("0x0", "0x1") else "?(%s)" % g(e) for e in (R.nf, R.zf, R.cf, R.of))
return asm, [g(R.regs32_expr[i]) for i in range(4)], fl
def jit(mach, code, regs, f, CODE):
from miasm.jitter.csts import PAGE_READ, PAGE_WRITE, PAGE_EXEC
j = mach.jitter(LocationDB(), mode)
j.vm.add_memory_page(CODE & ~0xfff, PAGE_READ | PAGE_WRITE | PAGE_EXEC, b"\x00" * (CODE & 0xfff) + code + b"\x00" * 16)
j.vm.add_memory_page(0x30000000, PAGE_READ | PAGE_WRITE, b"\x00" * 0x2000)
j.cpu.SP = 0x30001000
for i, v in enumerate(regs): setattr(j.cpu, "R%d" % i, v)
j.cpu.nf, j.cpu.zf, j.cpu.cf, j.cpu.of = (int(b) for b in f)
j.add_breakpoint(CODE + len(code), lambda jit: False)
if mach.name == "armtl": j.cpu.PC = CODE # thumb state
j.run(CODE)
return "-", ["%#x" % getattr(j.cpu, "R%d" % i) for i in range(4)], "%d%d%d%d" % (j.cpu.nf, j.cpu.zf, j.cpu.cf, j.cpu.of)
for line in open(path):
if not line.strip() or line.startswith("#"): continue
head = line.split("|", 1)[0].split()
name, m = head[0], head[1]
regs = [int(x, 0) for x in head[2:6]]
mach = Machine("armtl" if m == "thumb" else "arml")
code = open("%s/%s.bin" % (wd, name), "rb").read(); addr = int(open("%s/%s.addr" % (wd, name)).read(), 0)
try: asm, r, fl = (symb if mode == "symb" else jit)(mach, code, regs, head[6], addr)
except Exception as e: asm, r, fl = "-", ["EXC %s: %s" % (type(e).__name__, str(e)[:150])] + ["-"] * 3, "-"
print("%s | r0=%s r1=%s r2=%s r3=%s nzcv=%s [%s]" % (name, r[0], r[1], r[2], r[3], fl, asm))cases.txt
# name mode r0 r1 r2 r3 nzcv | snippet (assembled with arm-none-eabi-as, .syntax unified, armv7-a)
# 32-bit S-form inside an IT block: S == '1', so setflags is TRUE (the 16-bit forms are the ones that do not set flags)
it_addseq_w thumb 1 0xffffffff 0 0 0100 | it eq ; addseq.w r0, r0, r1 ; mov.w r2, #0
it_subseq_w thumb 1 1 0 0 0100 | it eq ; subseq.w r0, r0, r1 ; mov.w r2, #0
it_movseq_w thumb 0 0x80000000 0 0 0100 | it eq ; movseq.w r0, r1 ; mov.w r2, #0
# then a branch on the flags the S-form produced: 2 - 1 != 0 clears Z, so the CPU falls through beq (r3 = 1)
it_subseq_w_then_beq thumb 2 1 0 0 0100 | cmp r2, #0 ; it eq ; subseq.w r0, r0, r1 ; beq 1f ; movs r3, #1 ; b 2f ; 1: movs r3, #2 ; 2:
# 32-bit ANDS under IT (logical S-form); then a multi-word add: the carry of addseq.w feeds adc.w, so the lost C makes r2 wrong
it_andseq_w thumb 0x80000000 0x80000000 0 0 0100 | it eq ; andseq.w r0, r0, r1 ; mov.w r2, #0
it_addseq_w_then_adc thumb 0xffffffff 1 0 0 0100 | it eq ; addseq.w r0, r0, r1 ; adc.w r2, r2, #0
# controls: 16-bit ADD inside IT does not set flags; CMP inside IT sets them
it_add16_control thumb 1 0xffffffff 0 0 0100 | it eq ; addeq r0, r0, r1 ; mov.w r2, #0
it_cmp_control thumb 1 1 0 0 0000 | it ne ; cmpne r0, r1 ; mov.w r2, #0
cmp.sh
#!/usr/bin/env bash
# cmp.sh <cases.txt> <venv>: qemu-arm vs Miasm symb/python/gcc per case (fresh TMPDIR: no stale gcc-jitter cache)
D="$(cd "$(dirname "$0")" && pwd)"; C="$1"; PY="$2"
T=$(mktemp -d); trap 'rm -rf "$T"' EXIT; export TMPDIR=$T
python3 -I "$D/a32_build.py" "$C" "$T" > "$T/q" || exit 2
for m in ${MODES:-symb python gcc}; do "$PY" -I -W ignore "$D/a32_miasm.py" $m "$C" "$T" > "$T/m.$m" 2>"$T/err.$m" || { cat "$T/err.$m"; exit 2; }; done
while read -r name _; do
q=$(grep "^$name |" "$T/q" | sed 's/^[^|]*| //')
case "$q" in r0=*) ;; *) echo "ERR $name oracle: $q"; continue;; esac
s=$(grep "^$name |" "$T/m.symb"); asm=$(echo "$s" | sed 's/.* \[//; s/\]$//')
mark=""; for m in ${MODES:-symb python gcc}; do v=$(grep "^$name |" "$T/m.$m" | sed 's/^[^|]*| //; s/ \[.*//'); [ "$v" = "$q" ] || mark="$mark $m"; done
echo "$([ -n "$mark" ] && echo DIFF || echo MATCH) $name [$(grep "^$name " "$C" | sed 's/^[^|]*| //')] miasm: [$asm]"
echo " qemu-arm : $q"
for m in ${MODES:-symb python gcc}; do echo " miasm $(printf %-6s $m): $(grep "^$name |" "$T/m.$m" | sed 's/^[^|]*| //; s/ \[.*//')"; done
done < <(grep -v '^#' "$C" | grep .)run.sh
#!/usr/bin/env bash
# Compares qemu-arm (reference) with Miasm's symbolic engine per case in cases.txt.
# PYTHON = a python with miasm installed (default python3). Exit 1 = some case differs, 0 = all match, 2 = tool/harness error.
D="$(cd "$(dirname "$0")" && pwd)"
PYTHON=${PYTHON:-python3}
for t in "$PYTHON" arm-none-eabi-as arm-none-eabi-ld arm-none-eabi-nm arm-none-eabi-objcopy qemu-arm; do command -v "$t" >/dev/null || { echo "missing $t"; exit 2; }; done
"$PYTHON" -I -c "import miasm" || { echo "miasm not importable"; exit 2; }
# the python/gcc jitters raise AttributeError get_instr_label on any IT block (PR #1034): symbolic engine only
export MODES=symb
out=$(bash "$D/cmp.sh" "$D/cases.txt" "$PYTHON"); rc=$?
echo "$out"
[ $rc = 0 ] || { echo "RESULT: harness error"; exit 2; }
echo "$out" | grep -q '^ERR' && { echo "RESULT: harness error"; exit 2; }
if echo "$out" | grep -q '^DIFF'; then echo "RESULT: BUG PRESENT (exit 1)"; exit 1; fi
echo "RESULT: conforms (exit 0)"; exit 0If 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.
Activity
Redhpm commentedon Oct 28, 2026
Superseded by the semantic tracking issue.
See #1584
Closed as duplicate as a consequence, because we need to fix semantic issues more systematically.