libTriton  version 0.7 build 1407
AstContext

Table of Contents

[python api] All information about the AstContext python object.

Description


Triton converts the x86, x86-64 and AArch64 instruction set architecture into an AST representation. The class is used to build your own AST nodes.

Python API - Methods of the AstContext class


Python API - Utility methods of the AstContext class


Python API - Operators


As we can not overload all AST's operators only these following operators are overloaded:

Python's Operator e.g: SMT2-Lib format
a + b (bvadd a b)
a - b (bvsub a b)
a * b (bvmul a b)
a / b (bvudiv a b)
a | b (bvor a b)
a & b (bvand a b)
a ^ b (bvxor a b)
a % b (bvurem a b)
a << b (bvshl a b)
a >> b (bvlshr a b)
~a (bvnot a)
-a (bvneg a)
a == b (= a b)
a != b (not (= a b))
a <= b (bvule a b)
a >= b (bvuge a b)
a < b (bvult a b)
a > b (bvugt a b)

The SMT or Python Syntax


By default, Triton represents semantics into SMT-LIB which is an international initiative aimed at facilitating research and development in Satisfiability Modulo Theories (SMT). However, Triton allows you to display your AST via a Python syntax.

>>> ctxt = TritonContext()
>>> ctxt.setArchitecture(ARCH.X86_64)
>>> ctxt.setAstRepresentationMode(AST_REPRESENTATION.PYTHON)
>>> inst = Instruction()
>>> inst.setOpcode("\x48\x01\xd8") # add rax, rbx
>>> inst.setAddress(0x400000)
>>> ctxt.setConcreteRegisterValue(ctxt.registers.rax, 0x1122334455667788)
>>> ctxt.setConcreteRegisterValue(ctxt.registers.rbx, 0x8877665544332211)
>>> ctxt.processing(inst)
True
>>> print inst
0x400000: add rax, rbx
>>> for expr in inst.getSymbolicExpressions():
... print expr
...
ref_0 = ((0x1122334455667788 + 0x8877665544332211) & 0xFFFFFFFFFFFFFFFF) # ADD operation
ref_1 = (0x1 if (0x10 == (0x10 & (ref_0 ^ (0x1122334455667788 ^ 0x8877665544332211)))) else 0x0) # Adjust flag
ref_2 = ((((0x1122334455667788 & 0x8877665544332211) ^ (((0x1122334455667788 ^ 0x8877665544332211) ^ ref_0) & (0x1122334455667788 ^ 0x8877665544332211))) >> 63) & 0x1) # Carry flag
ref_3 = ((((0x1122334455667788 ^ (~(0x8877665544332211) & 0xFFFFFFFFFFFFFFFF)) & (0x1122334455667788 ^ ref_0)) >> 63) & 0x1) # Overflow flag
ref_4 = ((((((((0x1 ^ (((ref_0 & 0xFF) >> 0x0) & 0x1)) ^ (((ref_0 & 0xFF) >> 0x1) & 0x1)) ^ (((ref_0 & 0xFF) >> 0x2) & 0x1)) ^ (((ref_0 & 0xFF) >> 0x3) & 0x1)) ^ (((ref_0 & 0xFF) >> 0x4) & 0x1)) ^ (((ref_0 & 0xFF) >> 0x5) & 0x1)) ^ (((ref_0 & 0xFF) >> 0x6) & 0x1)) ^ (((ref_0 & 0xFF) >> 0x7) & 0x1)) # Parity flag
ref_5 = ((ref_0 >> 63) & 0x1) # Sign flag
ref_6 = (0x1 if (ref_0 == 0x0) else 0x0) # Zero flag
ref_7 = 0x400003 # Program Counter