AArch64 implementation of instruction 'ccmp' may be incorrect

[Bri1987]

I wrote this unit test:

#!/usr/bin/env python4

from __future__          import print_function

from triton              import *
from unicorn             import *
from unicorn.arm64_const import *
from struct              import pack

import sys
import pprint

ADDR  = 0x100000
STACK = 0x200000
SIZE  = 5 * 1024 * 1024

CODE  = [
    (b"\xbf\x80\x01\x71", 'cmp w5, #0x60'),
    (b"\xc4\xc8\x40\x7a", 'ccmp w6, #0x0, #0x4, gt'),
]

def emu_with_unicorn(opcode, istate):
    # Initialize emulator in aarch64 mode
    mu = Uc(UC_ARCH_ARM64, UC_MODE_ARM)

    # map memory for this emulation
    mu.mem_map(ADDR, SIZE)

    # write machine code to be emulated to memory
    index = 0
    for op, _ in CODE:
        mu.mem_write(ADDR+index, op)
        index += len(op)

    mu.reg_write(UC_ARM64_REG_X5,   istate['x5'])
    mu.reg_write(UC_ARM64_REG_X6,   istate['x6'])
    mu.reg_write(UC_ARM64_REG_PC,   istate['pc'])
    mu.reg_write(UC_ARM64_REG_NZCV, istate['n'] << 31 | istate['z'] << 30 | istate['c'] << 29 | istate['v'] << 28)

    # emulate code in infinite time & unlimited instructions
    mu.emu_start(istate['pc'], istate['pc'] + len(opcode))

    ostate = {
        "x5":    mu.reg_read(UC_ARM64_REG_X5),
        "x6":    mu.reg_read(UC_ARM64_REG_X6),
        "pc":    mu.reg_read(UC_ARM64_REG_PC),
        "n":   ((mu.reg_read(UC_ARM64_REG_NZCV) >> 31) & 1),
        "z":   ((mu.reg_read(UC_ARM64_REG_NZCV) >> 30) & 1),
        "c":   ((mu.reg_read(UC_ARM64_REG_NZCV) >> 29) & 1),
        "v":   ((mu.reg_read(UC_ARM64_REG_NZCV) >> 28) & 1),
    }
    return ostate

def emu_with_triton(opcode, istate):
    ctx = TritonContext()
    ctx.setArchitecture(ARCH.AARCH64)

    inst = Instruction(opcode)
    inst.setAddress(istate['pc'])

    ctx.setConcreteRegisterValue(ctx.registers.x5,  istate['x5'])
    ctx.setConcreteRegisterValue(ctx.registers.x6,  istate['x6'])
    ctx.setConcreteRegisterValue(ctx.registers.pc,  istate['pc'])
    ctx.setConcreteRegisterValue(ctx.registers.n,   istate['n'])
    ctx.setConcreteRegisterValue(ctx.registers.z,   istate['z'])
    ctx.setConcreteRegisterValue(ctx.registers.c,   istate['c'])
    ctx.setConcreteRegisterValue(ctx.registers.v,   istate['v'])

    ctx.processing(inst)

    #print
    #print inst
    #for x in inst.getSymbolicExpressions():
    #    print x
    #print

    ostate = {
        "x5":    ctx.getSymbolicRegisterValue(ctx.registers.x5),
        "x6":    ctx.getSymbolicRegisterValue(ctx.registers.x6),
        "pc":    ctx.getSymbolicRegisterValue(ctx.registers.pc),
        "n":     ctx.getSymbolicRegisterValue(ctx.registers.n),
        "z":     ctx.getSymbolicRegisterValue(ctx.registers.z),
        "c":     ctx.getSymbolicRegisterValue(ctx.registers.c),
        "v":     ctx.getSymbolicRegisterValue(ctx.registers.v),
    }
    return ostate


def diff_state(state1, state2):
    for k, v in list(state1.items()):
        if (k == 'heap' or k == 'stack') and v != state2[k]:
            print('\t%s: (UC) != (TT)' %(k))
        elif not (k == 'heap' or k == 'stack') and v != state2[k]:
            print('\t%s: %#x (UC) != %#x (TT)' %(k, v, state2[k]))
    return


if __name__ == '__main__':
    # initial state
    state = {
        "x5":    0x41,
        "x6":    1,
        "pc":    ADDR,
        "n":     0,
        "z":     0,
        "c":     0,
        "v":     0,
    }

    for opcode, disassembly in CODE:
        try:
            uc_state = emu_with_unicorn(opcode, state)
            tt_state = emu_with_triton(opcode, state)
        except Exception as e:
            print('[EKO] %s' %(disassembly))
            print('\t%s' %(e))
            sys.exit(-1)

        if uc_state != tt_state:
            print('[KO] %s' %(disassembly))
            diff_state(uc_state, tt_state)
            sys.exit(-1)

        print('[OK] %s' %(disassembly))
        state = tt_state

    sys.exit(0)

and get output result:

[OK] cmp w5, #0x60
[KO] ccmp w6, #0x0, #0x4, gt
        z: 0x1 (UC) != 0x0 (TT)

It seems when the condition is false, Triton fails to update the flags from the provided nzcv operand (which is 4 in this case), and instead performs a comparison or do some other wrong things.

[zejunwang]

I think you are right, here is my change
file: /src/libtriton/arch/arm/aarch64/aarch64Semantics.cpp

      void AArch64Semantics::ccmp_s(triton::arch::Instruction &inst)
    {
      auto &src1 = inst.operands[0];
      auto &src2 = inst.operands[1];
      auto &src3 = inst.operands[2];
      auto ast = this->astCtxt;
      /* Operand ASTs */
      auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
      auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
      auto imm = this->symbolicEngine->getOperandAst(inst, src3);

      auto bits = src1.getBitSize();
      auto high = bits - 1;

      /* CMP result */
      auto result = ast->bvsub(op1, op2);

      /* ---------- CMP FLAGS ---------- */

      /* N flag (bitvector) */
      auto cmpN = ast->extract(high, high, result);

      /* Z flag -> convert logical -> bv1 */
      auto cmpZ = ast->ite(
          ast->equal(result, ast->bv(0, bits)),
          ast->bv(1, 1),
          ast->bv(0, 1));

      /* C flag -> convert logical -> bv1 */
      auto cmpC = ast->ite(
          ast->bvuge(op1, op2),
          ast->bv(1, 1),
          ast->bv(0, 1));

      /* V flag (signed overflow) */

      auto s1 = ast->extract(high, high, op1);
      auto s2 = ast->extract(high, high, op2);
      auto sr = ast->extract(high, high, result);

      auto overflow = ast->land(
          ast->distinct(s1, s2),
          ast->distinct(s1, sr));

      auto cmpV = ast->ite(
          overflow,
          ast->bv(1, 1),
          ast->bv(0, 1));

      /* ---------- IMM FLAGS ---------- */

      auto immN = ast->extract(3, 3, imm);
      auto immZ = ast->extract(2, 2, imm);
      auto immC = ast->extract(1, 1, imm);
      auto immV = ast->extract(0, 0, imm);

      /* ---------- APPLY CONDITION ---------- */

      auto N = this->getCodeConditionAst(inst, cmpN, immN);
      auto Z = this->getCodeConditionAst(inst, cmpZ, immZ);
      auto C = this->getCodeConditionAst(inst, cmpC, immC);
      auto V = this->getCodeConditionAst(inst, cmpV, immV);

      /* ---------- WRITE FLAGS ---------- */

      auto regN = this->architecture->getRegister(ID_REG_AARCH64_N);
      auto regZ = this->architecture->getRegister(ID_REG_AARCH64_Z);
      auto regC = this->architecture->getRegister(ID_REG_AARCH64_C);
      auto regV = this->architecture->getRegister(ID_REG_AARCH64_V);

      this->symbolicEngine->createSymbolicExpression(inst, N, regN, "CCMP N flag");
      this->symbolicEngine->createSymbolicExpression(inst, Z, regZ, "CCMP Z flag");
      this->symbolicEngine->createSymbolicExpression(inst, C, regC, "CCMP C flag");
      this->symbolicEngine->createSymbolicExpression(inst, V, regV, "CCMP V flag");

      /* Update control flow */
      this->controlFlow_s(inst);
    }