Description

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

Python API - Methods of the AstContext class

AstNode array(integer addrSize)
Creates an array node.
e.g: (Array (_ BitVec addrSize) (_ BitVec 8)).
AstNode assert_(AstNode node)
Creates a assert node. e.g: (assert node).
AstNode bswap(AstNode node)
Creates a bswap node. e.g: (bswap node).
AstNode bv(integer value, integer size)
Creates a bv node (bitvector). The size must be in bits.
e.g: (_ bv<balue> size).
AstNode bvadd(AstNode node1, AstNode node2)
Creates a bvadd node.
e.g: (bvadd node1 epxr2).
AstNode bvand(AstNode node1, AstNode node2)
Creates a bvand node.
e.g: (bvand node1 epxr2).
AstNode bvashr(AstNode node1, AstNode node2)
Creates a bvashr node (arithmetic shift right).
e.g: (bvashr node1 epxr2).
AstNode bvfalse(void)
This is an alias on the (_ bv0 1) ast expression.
AstNode bvlshr(AstNode node1, AstNode node2)
Creates a bvlshr node (logical shift right).
e.g: (lshr node1 epxr2).
AstNode bvmul(AstNode node1, AstNode node2)
Creates a bvmul node.
e.g: (bvmul node1 node2).
AstNode bvnand(AstNode node1, AstNode node2)
Creates a bvnand node.
e.g: (bvnand node1 node2).
AstNode bvneg(AstNode node1)
Creates a bvneg node.
e.g: (bvneg node1).
AstNode bvnor(AstNode node1, AstNode node2)
Creates a bvnor node.
e.g: (bvnor node1 node2).
AstNode bvnot(AstNode node1)
Creates a bvnot node.
e.g: (bvnot node1).
AstNode bvor(AstNode node1, AstNode node2)
Creates a bvor node.
e.g: (bvor node1 node2).
AstNode bvror(AstNode node, AstNode rot)
Creates a bvror node (rotate right).
e.g: ((_ rotate_right rot) node).
AstNode bvrol(AstNode node, AstNode rot)
Creates a bvrol node (rotate left).
e.g: ((_ rotate_left rot) node).
AstNode bvsdiv(AstNode node1, AstNode node2)
Creates a bvsdiv node.
e.g: (bvsdiv node1 epxr2).
AstNode bvsge(AstNode node1, AstNode node2)
Creates a bvsge node.
e.g: (bvsge node1 epxr2).
AstNode bvsgt(AstNode node1, AstNode node2)
Creates a bvsgt node.
e.g: (bvsgt node1 epxr2).
AstNode bvshl(AstNode node1, AstNode node2)
Creates a Bvshl node (shift left).
e.g: (bvshl node1 node2).
AstNode bvsle(AstNode node1, AstNode node2)
Creates a bvsle node.
e.g: (bvsle node1 epxr2).
AstNode bvslt(AstNode node1, AstNode node2)
Creates a bvslt node.
e.g: (bvslt node1 epxr2).
AstNode bvsmod(AstNode node1, AstNode node2)
Creates a bvsmod node (2's complement signed remainder, sign follows divisor).
e.g: (bvsmod node1 node2).
AstNode bvsrem(AstNode node1, AstNode node2)
Creates a bvsrem node (2's complement signed remainder, sign follows dividend).
e.g: (bvsrem node1 node2).
AstNode bvsub(AstNode node1, AstNode node2)
Creates a bvsub node.
e.g: (bvsub node1 epxr2).
AstNode bvtrue(void)
This is an alias on the (_ bv1 1) ast expression.
AstNode bvudiv(AstNode node1, AstNode node2)
Creates a bvudiv node.
e.g: (bvudiv node1 epxr2).
AstNode bvuge(AstNode node1, AstNode node2)
Creates a bvuge node.
e.g: (bvuge node1 epxr2).
AstNode bvugt(AstNode node1, AstNode node2)
Creates a bvugt node.
e.g: (bvugt node1 epxr2).
AstNode bvule(AstNode node1, AstNode node2)
Creates a bvule node.
e.g: (bvule node1 epxr2).
AstNode bvult(AstNode node1, AstNode node2)
Creates a bvult node.
e.g: (bvult node1 epxr2).
AstNode bvurem(AstNode node1, AstNode node2)
Creates a bvurem node (unsigned remainder).
e.g: (bvurem node1 node2).
AstNode bvxnor(AstNode node1, AstNode node2)
Creates a bvxnor node.
e.g: (bvxnor node1 node2).
AstNode bvxor(AstNode node1, AstNode node2)
Creates a bvxor node.
e.g: (bvxor node1 epxr2).
AstNode concat([AstNode, ...])
Concatenates several nodes.
AstNode declare(AstNode sort)
Declare a function without argument. Mainly used to delcare a variable or an array.
e.g: (declare-fun SymVar_0 () (_ BitVec 64))
AstNode distinct(AstNode node1, AstNode node2)
Creates a distinct node.
e.g: (distinct node1 node2)
AstNode equal(AstNode node1, AstNode node2)
Creates an equal node.
e.g: (= node1 epxr2).
AstNode extract(integer high, integer low, AstNode node1)
Creates an extract node. The high and low fields represent the bits position.
e.g: ((_ extract high low) node1).
AstNode forall([AstNode, ...], AstNode body)
Creates an forall node.
e.g: (forall ((x (_ BitVec <size>)), ...) body).
AstNode iff(AstNode node1, AstNode node2)
Creates an iff node (if and only if).
e.g: (iff node1 node2).
AstNode ite(AstNode ifExpr, AstNode thenExpr, AstNode elseExpr)
Creates an ite node (if-then-else node).
e.g: (ite ifExpr thenExpr elseExpr).
AstNode land([AstNode, ...])
Creates a logical AND on several nodes. e.g: (and node1 node2 node3 node4).
AstNode let(string alias, AstNode node2, AstNode node3)
Creates a let node.
e.g: (let ((alias node2)) node3).
AstNode lnot(AstNode node)
Creates a lnot node (logical NOT).
e.g: (not node).
AstNode lor([AstNode, ...])
Creates a logical OR on several nodes. e.g: (or node1 node2 node3 node4).
AstNode lxor([AstNode, ...])
Creates a logical XOR on several nodes. e.g: (xor node1 node2 node3 node4).
AstNode reference(SymbolicExpression expr)
Creates a reference node (SSA-based).
e.g: ref!123.
AstNode select(AstNode array, AstNode index)
Creates a select node.
e.g: (select array index).
AstNode store(AstNode array, AstNode index, AstNode expr)
Creates a store node.
e.g: (store array index expr).
AstNode string(string s)
Creates a string node.
AstNode sx(integer sizeExt, AstNode node1)
Creates a sx node (sign extend).
e.g: ((_ sign_extend sizeExt) node1).
AstNode variable(SymbolicVariable symVar)
Creates a variable node.
AstNode zx(integer sizeExt, AstNode node1)
Creates a zx node (zero extend).
e.g: ((_ zero_extend sizeExt) node1).

Python API - Utility methods of the AstContext class

AstNode dereference(AstNode node)
Returns the first non referene node encountered.
AstNode duplicate(AstNode node)
Duplicates the node and returns a new instance as AstNode.
[AstNode, ...] search(AstNode node, AST_NODE match)
Returns a list of collected matched nodes via a depth-first pre order traversal.
z3.ExprRef tritonToZ3(AstNode node)
Convert a Triton AST to a Z3 AST.
AstNode unroll(AstNode node)
Unrolls the SSA form of a given AST.
AstNode z3ToTriton(z3.ExprRef expr)
Convert a Z3 AST to a Triton AST.

Python API - Operators

As we can not overload all AST operators only the 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 in SMT-LIB which is an international initiative aimed at facilitating research and development in Satisfiability Modulo Theories (SMT). However, Triton also allows you to display your AST using a Python syntax.

>>> ctxt = TritonContext()
>>> ctxt.setArchitecture(ARCH.X86_64)
>>> ctxt.setAstRepresentationMode(AST_REPRESENTATION.PYTHON)
>>> inst = Instruction()
>>> inst.setOpcode(b"\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

Table of Contents

Description

Python API - Methods of the AstContext class

Python API - Utility methods of the AstContext class

Python API - Operators

The SMT or Python Syntax