libTriton  version 0.9 build 1468
AstContext

[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. This class is used to build your own AST nodes.

Python API - Methods of the AstContext class


  • 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 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 var, ...], 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 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 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::expr 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::expr 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