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
Version: miasm 0.1.5 (tag v0.1.5, ef52b54d). Also reproduces at master 3671fc2 (2026-09-21).
Preconditions: none, default Machine("aarch64l") lifter; any CCMP (register or immediate, 32 or 64-bit) whose condition holds.
Input
repro.py runs five CCMP words whose condition holds, in SymbolicExecutionEngine and the python jitter, and compares NZCV with the Arm AddWithCarry pseudocode. It then runs cmp x0,#0; ccmp x1,x2,#0,eq; cset w0,lt, the clang -O2 code for a == 0 && b < c.
Command
PYTHON=python3 ./run.sh
Output
CCMP X1, X2, 0x0, EQ x1=0x0 op2=0x1 NZCV before=0100: spec 1000 symb 0000 python-jit 0000 WRONG
CCMP W1, W2, 0x0, EQ x1=0x7fffffff op2=0x80000000 NZCV before=0100: spec 1001 symb 0001 python-jit 0001 WRONG
CCMP X1, X2, 0x8, AL x1=0x2 op2=0x1 NZCV before=1000: spec 0010 symb 1010 python-jit 1010 WRONG
CCMP X1, 0x5, 0x0, EQ x1=0x3 op2=0x5 NZCV before=0100: spec 1000 symb 0000 python-jit 0000 WRONG
CCMP W1, W2, 0x0, GE x1=0x1 op2=0x2 NZCV before=0100: spec 1000 symb 0000 python-jit 0000 WRONG
cmp/ccmp/cset lt, a=0 b=1 c=2: spec w0=1 symb w0=0 WRONG
symbolic b, c (a=0): w0 = ((b ^ c) & (b ^ (b + -c)))[63:64]?(0x1,0x0)
RESULT: CCMP N flag differs from the Arm ARM (exit 1)
Only N differs; it keeps its value from before the instruction. qemu-aarch64 gives the spec values for all five words. The cset lt result becomes the overflow bit alone, so b < c without overflow is never reported.
Expected
Arm A64 ISA 2026-03, CCMP (register): "This instruction sets the value of the condition flags to the result of the comparison of two registers if the condition is TRUE, and an immediate value otherwise." Its Operation computes (-, flags) = AddWithCarry{datasize}(operand1, NOT(operand2), '1'); then PSTATE.[N,Z,C,V] = flags;, and AddWithCarry sets n : bit = result[N-1]. CCMP (immediate) uses the same Operation.
ccmp in miasm/arch/aarch64/sem.py:1171 assigns new_nf = nf; Z, C and V are computed from arg1 - arg2. update_flag_nf(res)[0].src there makes ./run.sh exit 0. This is separate from #1491 (the #nzcv immediate when the condition is false).
Reproducer files
repro.py
"""AArch64 CCMP with its condition TRUE: NZCV must be AddWithCarry(op1, NOT(op2), 1) flags (Arm ARM CCMP Operation).
Runs each instruction in miasm's SymbolicExecutionEngine and the python jitter; expected flags are computed from the
AddWithCarry pseudocode. Then runs `cmp x0,#0; ccmp x1,x2,#0,eq; cset w0,lt` (clang -O2 for `a == 0 && b < c`)."""
import sys
from miasm.analysis.machine import Machine
from miasm.core.locationdb import LocationDB
from miasm.expression.expression import ExprInt, ExprId
from miasm.ir.symbexec import SymbolicExecutionEngine
from miasm.jitter.csts import PAGE_READ, PAGE_WRITE, PAGE_EXEC
import miasm.arch.aarch64.regs as R
m = Machine("aarch64l")
FLAGS = (R.nf, R.zf, R.cf, R.of)
def add_with_carry(x, y, carry, n): # Arm shared pseudocode AddWithCarry, flags only
mask = (1 << n) - 1
sint = lambda v: v - (1 << n) if v >> (n - 1) else v
usum = x + y + carry; ssum = sint(x) + sint(y) + carry; res = usum & mask
return "%d%d%d%d" % (res >> (n - 1), res == 0, res != usum, sint(res) != ssum)
def symb(code, regs, nzcv):
ldb = LocationDB(); lifter = m.lifter(ldb)
st = {R.gpregs64_expr[i]: ExprInt(regs.get(i, 0), 64) for i in range(31)}
st.update({f: ExprInt(int(b), 1) for f, b in zip(FLAGS, nzcv)})
se = SymbolicExecutionEngine(lifter, st)
for i in range(0, len(code), 4):
ins = m.mn.dis(code[i:i + 4], "l"); ins.offset = 0x1000 + i
ircfg = lifter.new_ircfg(); lifter.add_instr_to_ircfg(ins, ircfg)
se.run_block_at(ircfg, ldb.get_offset_location(ins.offset))
return se
def jit_python(code, regs, nzcv):
j = m.jitter(LocationDB(), "python")
j.vm.add_memory_page(0x1000, PAGE_READ | PAGE_WRITE | PAGE_EXEC, code + bytes.fromhex("000020d4"))
j.cpu.X1, j.cpu.X2 = regs[1], regs[2]
j.cpu.nf, j.cpu.zf, j.cpu.cf, j.cpu.of = (int(b) for b in nzcv)
j.add_breakpoint(0x1000 + len(code), lambda jit: False); j.run(0x1000)
return "%d%d%d%d" % (j.cpu.nf, j.cpu.zf, j.cpu.cf, j.cpu.of)
# word, x1, x2 (or imm5), NZCV before, datasize; every condition below holds
CASES = [("200042fa", 0x0, 0x1, "0100", 64),
("2000427a", 0x7fffffff, 0x80000000, "0100", 32),
("28e042fa", 0x2, 0x1, "1000", 64),
("200845fa", 0x3, 0x5, "0100", 64),
("20a0427a", 0x1, 0x2, "0100", 32)]
bad = 0
for hx, x1, x2, nzcv, n in CASES:
code = bytes.fromhex(hx); ins = m.mn.dis(code, "l")
want = add_with_carry(x1, ~x2 & ((1 << n) - 1), 1, n)
se = symb(code, {1: x1, 2: x2}, nzcv)
got_s = "".join(str(int(se.eval_expr(f))) for f in FLAGS)
got_p = jit_python(code, {1: x1, 2: x2}, nzcv)
ok = got_s == want and got_p == want; bad |= not ok
print("%-26s x1=%#x op2=%#x NZCV before=%s: spec %s symb %s python-jit %s %s"
% (ins, x1, x2, nzcv, want, got_s, got_p, "OK" if ok else "WRONG"))
code = bytes.fromhex("1f0000f1" "200042fa" "e0a79f1a") # cmp x0,#0; ccmp x1,x2,#0,eq; cset w0,lt
w0 = int(symb(code, {0: 0, 1: 1, 2: 2}, "0000").eval_expr(R.gpregs64_expr[0]))
ok = w0 == 1; bad |= not ok
print("cmp/ccmp/cset lt, a=0 b=1 c=2: spec w0=1 symb w0=%d %s" % (w0, "OK" if ok else "WRONG"))
lifter = m.lifter(LocationDB())
st = {R.gpregs64_expr[0]: ExprInt(0, 64), R.gpregs64_expr[1]: ExprId("b", 64), R.gpregs64_expr[2]: ExprId("c", 64)}
st.update({f: ExprInt(0, 1) for f in FLAGS})
ldb = LocationDB(); lifter = m.lifter(ldb); se = SymbolicExecutionEngine(lifter, st)
for i in range(3):
ins = m.mn.dis(code[4 * i:4 * i + 4], "l"); ins.offset = 0x1000 + 4 * i
ircfg = lifter.new_ircfg(); lifter.add_instr_to_ircfg(ins, ircfg)
se.run_block_at(ircfg, ldb.get_offset_location(ins.offset))
print(" symbolic b, c (a=0): w0 =", se.eval_expr(R.gpregs64_expr[0]))
print("RESULT: %s" % ("CCMP N flag differs from the Arm ARM (exit 1)" if bad else "conforms (exit 0)"))
sys.exit(1 if bad else 0)run.sh
#!/usr/bin/env bash
# exit 1 = miasm's AArch64 CCMP flags differ from the Arm ARM, 0 = conforms, 2 = miasm not found
PYTHON=${PYTHON:-python3}
D="$(cd "$(dirname "$0")" && pwd)"
"$PYTHON" -c 'import miasm' 2>/dev/null || { echo "tool not found: miasm (set PYTHON to an interpreter with miasm installed)"; exit 2; }
"$PYTHON" -W ignore "$D/repro.py"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.
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.