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. CSEL/CSINC/CSINV/CSNEG/CCMP ..., NV take the "condition false" side in the symbolic engine and in the python and gcc jitters.
Version: miasm 0.1.5 (ef52b54d). Also reproduces at upstream head 3671fc2 (2026-09-21).
Preconditions: none beyond an instruction encoded with cond=1111 (hand-written or obfuscated code; compilers do not emit it).
Arm A64 shared pseudocode (2026-03), ConditionHolds:
when '111' => result = TRUE; // AL
// Condition flag values in the set '111x' indicate always true
// Otherwise, invert condition if necessary.
if cond[0] == '1' && cond != '1111' then
So NV behaves as AL. In miasm/arch/aarch64/sem.py cond2expr has 'AL': ExprInt(1, 1) but 'NV': ExprInt(0, 1) (line 908).
Input
repro/cases.txt: csel x0,x1,x2,nv (20f0829a), csinc, csinv, csneg, ccmp x1,x2,#15,nv, and an AL control, with x1=0x1111, x2=0x2222 (the ccmp case uses x1=x2=7).
Command
PYTHON=<python with miasm> bash ./run.sh (needs aarch64-linux-gnu-as/ld and qemu-aarch64 as the reference)
Output
== csel_x0_x1_x2_nv
qemu-aarch64 : x0=0x1111 sp=0x30001000 nzcv=0000
miasm symb : x0=0x2222 sp=0x30001000 nzcv=0000 [CSEL X0, X1, X2, NV]
miasm python : x0=0x2222 sp=0x30001000 nzcv=0000 [CSEL X0, X1, X2, NV]
miasm gcc : x0=0x2222 sp=0x30001000 nzcv=0000 [CSEL X0, X1, X2, NV]
== csinc_w0_w1_w2_nv
qemu-aarch64 : x0=0x1111 sp=0x30001000 nzcv=0000
miasm symb : x0=0x2223 sp=0x30001000 nzcv=0000 [CSINC W0, W1, W2, NV]
miasm python : x0=0x2223 sp=0x30001000 nzcv=0000 [CSINC W0, W1, W2, NV]
miasm gcc : x0=0x2223 sp=0x30001000 nzcv=0000 [CSINC W0, W1, W2, NV]
== csinv_x0_x1_x2_nv
qemu-aarch64 : x0=0x1111 sp=0x30001000 nzcv=0000
miasm symb : x0=0xffffffffffffdddd sp=0x30001000 nzcv=0000 [CSINV X0, X1, X2, NV]
miasm python : x0=0xffffffffffffdddd sp=0x30001000 nzcv=0000 [CSINV X0, X1, X2, NV]
miasm gcc : x0=0xffffffffffffdddd sp=0x30001000 nzcv=0000 [CSINV X0, X1, X2, NV]
== csneg_x0_x1_x2_nv
qemu-aarch64 : x0=0x1111 sp=0x30001000 nzcv=0000
miasm symb : x0=0xffffffffffffddde sp=0x30001000 nzcv=0000 [CSNEG X0, X1, X2, NV]
miasm python : x0=0xffffffffffffddde sp=0x30001000 nzcv=0000 [CSNEG X0, X1, X2, NV]
miasm gcc : x0=0xffffffffffffddde sp=0x30001000 nzcv=0000 [CSNEG X0, X1, X2, NV]
== ccmp_x1_x2_15_nv__7_7
qemu-aarch64 : x0=0x0 sp=0x30001000 nzcv=0110
miasm symb : x0=0x0 sp=0x30001000 nzcv=1111 [CCMP X1, X2, 0xF, NV]
miasm python : x0=0x0 sp=0x30001000 nzcv=1111 [CCMP X1, X2, 0xF, NV]
miasm gcc : x0=0x0 sp=0x30001000 nzcv=1111 [CCMP X1, X2, 0xF, NV]
== control_csel_al
qemu-aarch64 : x0=0x1111 sp=0x30001000 nzcv=0000
miasm symb : x0=0x1111 sp=0x30001000 nzcv=0000 [CSEL X0, X1, X2, AL]
miasm python : x0=0x1111 sp=0x30001000 nzcv=0000 [CSEL X0, X1, X2, AL]
miasm gcc : x0=0x1111 sp=0x30001000 nzcv=0000 [CSEL X0, X1, X2, AL]
RESULT: BUG PRESENT (exit 1)
(Expected: x0=0x1111 for the four selects, nzcv=0110 for the ccmp, as AL does.)
Impact: wrong value/flags for NV-conditioned instructions in emulation and symbolic analysis; no compiler-emitted code is affected.
Fix: 'NV': ExprInt(1, 1).
Reproducer files
a64_miasm.py
"""a64_miasm.py <symb|python|gcc> <cases.txt>: run each one-instruction case in Miasm (aarch64l).
Case line: name hex x1 x2 nzcv(4 bits) ; prints: name asm x0 sp nzcv"""
import sys
from miasm.analysis.machine import Machine
from miasm.core.locationdb import LocationDB
from miasm.expression.expression import ExprInt
import miasm.arch.aarch64.regs as R
mode, path = sys.argv[1], sys.argv[2]
mach = Machine("aarch64l"); SP0 = 0x30001000; CODE = 0x10000000
def symb(code, x1, x2, f):
from miasm.ir.symbexec import SymbolicExecutionEngine
ldb = LocationDB(); ins = mach.mn.dis(code, "l"); ins.offset = CODE
lifter = mach.lifter(ldb); ircfg = lifter.new_ircfg(); lifter.add_instr_to_ircfg(ins, ircfg)
st = {R.gpregs64_expr[i]: ExprInt(0, 64) for i in range(31)}
st[R.gpregs64_expr[1]] = ExprInt(x1, 64); st[R.gpregs64_expr[2]] = ExprInt(x2, 64)
st[R.SP] = ExprInt(SP0, 64); st[R.XZR] = ExprInt(0, 64); st[R.WZR] = ExprInt(0, 32)
for b, e in zip(f, (R.nf, R.zf, R.cf, R.of)): st[e] = ExprInt(int(b), 1)
se = SymbolicExecutionEngine(lifter, st)
se.run_block_at(ircfg, ldb.get_offset_location(CODE))
g = lambda e: (lambda v: ("%#x" % int(v)) if v.is_int() else str(v))(se.eval_expr(e))
return str(ins), g(R.gpregs64_expr[0]), g(R.SP), "".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))
def jit(code, x1, x2, f):
from miasm.jitter.csts import PAGE_READ, PAGE_WRITE, PAGE_EXEC
j = mach.jitter(LocationDB(), mode)
j.vm.add_memory_page(CODE, PAGE_READ | PAGE_WRITE | PAGE_EXEC, code + bytes.fromhex("000020d4"))
j.vm.add_memory_page(SP0 - 0x1000, PAGE_READ | PAGE_WRITE, b"\x00" * 0x2000)
j.cpu.SP = SP0; j.cpu.X1 = x1; j.cpu.X2 = x2
j.cpu.nf, j.cpu.zf, j.cpu.cf, j.cpu.of = (int(b) for b in f)
j.add_breakpoint(CODE + 4, lambda jit: False); j.run(CODE)
return mach.mn.dis(code, "l"), "%#x" % j.cpu.X0, "%#x" % j.cpu.SP, "%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
name, hx, x1, x2, f = line.split()
try: r = (symb if mode == "symb" else jit)(bytes.fromhex(hx), int(x1, 0), int(x2, 0), f)
except Exception as e: r = ("-", "EXC %s: %s" % (type(e).__name__, str(e)[:120]), "-", "-")
print("%s %s | x0=%s sp=%s nzcv=%s" % (name, r[0], r[1], r[2], r[3]))a64_qemu.py
"""a64_qemu.py <cases.txt> <workdir>: oracle. Builds a static AArch64 program per case (x1, x2, NZCV set with msr,
then the instruction word), runs it under qemu-aarch64, prints x0, sp, nzcv after the instruction."""
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
name, hx, x1, x2, f = line.split()
word = int.from_bytes(bytes.fromhex(hx), "little")
src = """.global _start
.text
_start:
ldr x9, =0x30001000
mov x13, sp
mov sp, x9
mov x0, #0
ldr x1, =%s
ldr x2, =%s
ldr x9, =%#x
msr nzcv, x9
.inst %#010x
mrs x9, nzcv
mov x10, sp
mov sp, x13
adr x11, buf
stp x0, x9, [x11]
str x10, [x11, #16]
mov x0, #1
mov x1, x11
mov x2, #24
mov x8, #64
svc 0
mov x0, #0
mov x8, #93
svc 0
.ltorg
.data
.balign 8
buf: .skip 32
""" % (x1, x2, int(f, 2) << 28, word)
b = os.path.join(wd, name)
open(b + ".s", "w").write(src)
subprocess.run(["aarch64-linux-gnu-as", "-o", b + ".o", b + ".s"], check=True)
subprocess.run(["aarch64-linux-gnu-ld", "-static", "-o", b, b + ".o"], check=True)
out = subprocess.run(["timeout", "10", "qemu-aarch64", b], capture_output=True).stdout
x0, n, sp = struct.unpack("<QQQ", out)
print("%s | x0=%#x sp=%#x nzcv=%d%d%d%d" % (name, x0, sp, (n >> 31) & 1, (n >> 30) & 1, (n >> 29) & 1, (n >> 28) & 1))cases.txt
# name hex x1 x2 nzcv (cond = 1111 "NV": ConditionHolds() returns TRUE)
csel_x0_x1_x2_nv 20f0829a 0x1111 0x2222 0000
csinc_w0_w1_w2_nv 20f4821a 0x1111 0x2222 0000
csinv_x0_x1_x2_nv 20f082da 0x1111 0x2222 0000
csneg_x0_x1_x2_nv 20f482da 0x1111 0x2222 0000
ccmp_x1_x2_15_nv__7_7 2ff042fa 0x7 0x7 0000
control_csel_al 20e0829a 0x1111 0x2222 0000
run.sh
#!/usr/bin/env bash
# AArch64 condition code 1111 (NV) behaves as AL: ConditionHolds() returns TRUE for cond 111x (Arm ARM shared
# pseudocode). Miasm cond2expr maps NV to constant 0. Compares Miasm (symbolic + python/gcc jitters) with qemu-aarch64.
D="$(cd "$(dirname "$0")" && pwd)"
PY="${PYTHON:-python3}" # interpreter with miasm installed
for t in "$PY" aarch64-linux-gnu-as aarch64-linux-gnu-ld qemu-aarch64; do command -v "$t" >/dev/null || { echo "missing $t"; exit 2; }; done
"$PY" -I -c "import importlib.metadata as m, sys; print('miasm', m.version('miasm'), sys.prefix)" || exit 2
T=$(mktemp -d); trap 'rm -rf "$T"' EXIT
python3 -I "$D/a64_qemu.py" "$D/cases.txt" "$T" > "$T/q" || exit 2
bug=0
for mode in symb python gcc; do
"$PY" -I -W ignore "$D/a64_miasm.py" $mode "$D/cases.txt" > "$T/m.$mode" || exit 2
done
while read -r name rest; do
q=$(grep "^$name |" "$T/q" | sed 's/.*| //')
echo "== $name"; echo " qemu-aarch64 : $q"
for mode in symb python gcc; do
m=$(grep "^$name " "$T/m.$mode"); echo " miasm $(printf %-6s $mode) : ${m#* | } [${m#* }]" | sed 's/ | .*\]/]/'
[ "${m#* | }" = "$q" ] || bug=1
done
done < <(grep -v '^#' "$D/cases.txt")
echo "RESULT: $([ $bug = 1 ] && echo 'BUG PRESENT (exit 1)' || echo 'conforms (exit 0)')"
exit $bugIf 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.