AArch64 CASP stores the new pair when the compare fails and skips the store when it succeeds #1564

"""AArch64 CASP/CASPAL in miasm vs the Arm ARM (MemAtomic/CASCompare), little-endian.
Each case: memory pair at P = {m0, m1}, compare pair {Xs, Xs+1}, new pair {Xt, Xt+1} = {A, B}.
Arm ARM: equal -> memory = {A, B}; not equal -> memory unchanged. Either way {Xs, Xs+1} = old memory."""
import sys, struct, logging
from miasm.analysis.machine import Machine
from miasm.core.locationdb import LocationDB
from miasm.jitter.csts import PAGE_READ, PAGE_WRITE, PAGE_EXEC

CODE, DATA, P = 0x400000, 0x30000000, 0x30000800
M0, M1, A, B = 0x1111111111111111, 0x2222222222222222, 0xaaaaaaaaaaaaaaaa, 0xbbbbbbbbbbbbbbbb
CASES = [  # name, insn word, element size, s0, s1
    ("casp x equal",       0x48207c82, 64, M0, M1),   # casp x0, x1, x2, x3, [x4]
    ("casp x not-equal",   0x48207c82, 64, 5, M1),
    ("caspal x equal",     0x4860fc82, 64, M0, M1),   # caspal x0, x1, x2, x3, [x4]
    ("caspal x not-equal", 0x4860fc82, 64, M0, 6),
    ("casp w equal",       0x08207c82, 32, M0 & 0xffffffff, M1 & 0xffffffff),  # casp w0, w1, w2, w3, [x4]
    ("casp w not-equal",   0x08207c82, 32, M0 & 0xffffffff, 5),
]
RET = 0xd65f03c0  # ret

def run_symb(word, size, s0, s1, m0, m1, a, b):
    from miasm.ir.symbexec import SymbolicExecutionEngine
    from miasm.expression.expression import ExprInt, ExprMem
    logging.getLogger("asmblock").setLevel(logging.ERROR)  # only the CASP word is mapped
    mach, ldb = Machine("aarch64l"), LocationDB()
    block = mach.dis_engine(struct.pack("<I", word), loc_db=ldb).dis_block(0)
    lifter = mach.lifter_model_call(ldb); ircfg = lifter.new_ircfg(); lifter.add_asmblock_to_ircfg(block, ircfg)
    r, pair = mach.mn.regs, ExprMem(ExprInt(P, 64), 2 * size)
    sb = SymbolicExecutionEngine(lifter, {r.X0: ExprInt(s0, 64), r.X1: ExprInt(s1, 64), r.X2: ExprInt(a, 64),
                                          r.X3: ExprInt(b, 64), r.X4: ExprInt(P, 64),
                                          pair: ExprInt(m0 | (m1 << size), 2 * size)})
    pc = sb.run_at(ircfg, 0)
    while int(pc) != 4:
        pc = sb.run_at(ircfg, pc)
    mem = int(sb.eval_expr(pair))
    mask = (1 << size) - 1
    return (int(sb.eval_expr(r.X0)) & mask, int(sb.eval_expr(r.X1)) & mask, mem & mask, mem >> size)

def run(mode, word, size, s0, s1):
    mask = (1 << size) - 1
    m0, m1, a, b = M0 & mask, M1 & mask, A & mask, B & mask
    if mode == "symb":
        return run_symb(word, size, s0, s1, m0, m1, a, b)
    j = Machine("aarch64l").jitter(LocationDB(), mode)
    j.vm.add_memory_page(CODE, PAGE_READ | PAGE_WRITE | PAGE_EXEC, struct.pack("<II", word, RET) + b"\0" * 0xff8)
    j.vm.add_memory_page(DATA, PAGE_READ | PAGE_WRITE, b"\0" * 0x1000)
    fmt = "<QQ" if size == 64 else "<II"
    j.vm.set_mem(P, struct.pack(fmt, m0, m1))
    j.cpu.X0, j.cpu.X1, j.cpu.X2, j.cpu.X3, j.cpu.X4 = s0, s1, a, b, P
    j.cpu.SP = DATA + 0xf00; j.cpu.LR = CODE + 0x800
    j.add_breakpoint(CODE + 0x800, lambda jt: False)
    j.run(CODE)
    mem = struct.unpack(fmt, j.vm.get_mem(P, 2 * size // 8))
    return (j.cpu.X0 & mask, j.cpu.X1 & mask) + mem

modes = sys.argv[1:] or ["symb", "python"]
bad = 0
for name, word, size, s0, s1 in CASES:
    mask = (1 << size) - 1
    m0, m1 = M0 & mask, M1 & mask
    equal = (s0, s1) == (m0, m1)
    spec = (m0, m1) + (((A & mask, B & mask)) if equal else (m0, m1))
    line = "%-19s spec   : s0=%#x s1=%#x mem0=%#x mem1=%#x" % ((name,) + spec)
    print(line)
    for mode in modes:
        got = run(mode, word, size, s0, s1)
        ok = got == spec
        bad |= not ok
        print("%-19s %-7s: s0=%#x s1=%#x mem0=%#x mem1=%#x  %s" % ((name, mode) + got + ("OK" if ok else "WRONG",)))
print("RESULT: %s" % ("CASP differs from the Arm ARM (exit 1)" if bad else "conforms (exit 0)"))
sys.exit(1 if bad else 0)