#!/usr/bin/env python2
## -*- coding: utf-8 -*-
##
## Output:
##
##  r14:64 bv[63..0] = (r14v ^ r15v)
##  cf:1 bv[0..0] = 0x0
##  of:1 bv[0..0] = 0x0
##  pf:1 bv[0..0] = ((((((((0x1 ^ ((((r14v ^ r15v) & 0xFF) >> 0x0) & 0x1)) ^ ((((r14v ^ r15v) & 0xFF) >> 0x1) & 0x1)) ^ ((((r14v ^ r15v) & 0xFF) >> 0x2) & 0x1)) ^ ((((r14v ^ r15v) & 0xFF) >> 0x3) & 0x1)) ^ ((((r14v ^ r15v) & 0xFF) >> 0x4) & 0x1)) ^ ((((r14v ^ r15v) & 0xFF) >> 0x5) & 0x1)) ^ ((((r14v ^ r15v) & 0xFF) >> 0x6) & 0x1)) ^ ((((r14v ^ r15v) & 0xFF) >> 0x7) & 0x1))
##  sf:1 bv[0..0] = (((r14v ^ r15v) >> 63) & 0x1)
##  zf:1 bv[0..0] = (0x1 if ((r14v ^ r15v) == 0x0) else 0x0)
##  rip:64 bv[63..0] = 0x3
##

from __future__ import print_function
from triton     import *


ctx = TritonContext()
ctx.setArchitecture(ARCH.X86_64)

ctx.setAstRepresentationMode(AST_REPRESENTATION.PYTHON)

r14v = ctx.convertRegisterToSymbolicVariable(ctx.registers.r14)
r14v.setAlias("r14v")

r15v = ctx.convertRegisterToSymbolicVariable(ctx.registers.r15)
r15v.setAlias("r15v")


inst = Instruction("\x4d\x31\xfe")
ctx.processing(inst)

ast = ctx.getAstContext()
for se in inst.getSymbolicExpressions():
    print("%s = %s" %(se.getOrigin(), ast.unrollAst(se.getAst())))