libTriton  version 0.8 build 1439
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 expr1, AstNode expr2)
    Creates a bvadd node.
    e.g: (bvadd expr1 epxr2).
  • AstNode bvand(AstNode expr1, AstNode expr2)
    Creates a bvand node.
    e.g: (bvand expr1 epxr2).
  • AstNode bvashr(AstNode expr1, AstNode expr2)
    Creates a bvashr node (arithmetic shift right).
    e.g: (bvashr expr1 epxr2).
  • AstNode bvfalse(void)
    This is an alias on the (_ bv0 1) ast expression.
  • AstNode bvlshr(AstNode expr1, AstNode expr2)
    Creates a bvlshr node (logical shift right).
    e.g: (lshr expr1 epxr2).
  • AstNode bvmul(AstNode expr1, AstNode expr2)
    Creates a bvmul node.
    e.g: (bvmul expr1 expr2).
  • AstNode bvnand(AstNode expr1, AstNode expr2)
    Creates a bvnand node.
    e.g: (bvnand expr1 expr2).
  • AstNode bvneg(AstNode expr1)
    Creates a bvneg node.
    e.g: (bvneg expr1).
  • AstNode bvnor(AstNode expr1, AstNode expr2)
    Creates a bvnor node.
    e.g: (bvnor expr1 expr2).
  • AstNode bvnot(AstNode expr1)
    Creates a bvnot node.
    e.g: (bvnot expr1).
  • AstNode bvor(AstNode expr1, AstNode expr2)
    Creates a bvor node.
    e.g: (bvor expr1 expr2).
  • AstNode bvror(AstNode expr, AstNode rot)
    Creates a bvror node (rotate right).
    e.g: ((_ rotate_right rot) expr).
  • AstNode bvrol(AstNode expr, AstNode rot)
    Creates a bvrol node (rotate left).
    e.g: ((_ rotate_left rot) expr).
  • AstNode bvsdiv(AstNode expr1, AstNode expr2)
    Creates a bvsdiv node.
    e.g: (bvsdiv expr1 epxr2).
  • AstNode bvsge(AstNode expr1, AstNode expr2)
    Creates a bvsge node.
    e.g: (bvsge expr1 epxr2).
  • AstNode bvsgt(AstNode expr1, AstNode expr2)
    Creates a bvsgt node.
    e.g: (bvsgt expr1 epxr2).
  • AstNode bvshl(AstNode expr1, AstNode expr2)
    Creates a Bvshl node (shift left).
    e.g: (bvshl expr1 expr2).
  • AstNode bvsle(AstNode expr1, AstNode expr2)
    Creates a bvsle node.
    e.g: (bvsle expr1 epxr2).
  • AstNode bvslt(AstNode expr1, AstNode expr2)
    Creates a bvslt node.
    e.g: (bvslt expr1 epxr2).
  • AstNode bvsmod(AstNode expr1, AstNode expr2)
    Creates a bvsmod node (2's complement signed remainder, sign follows divisor).
    e.g: (bvsmod expr1 expr2).
  • AstNode bvsrem(AstNode expr1, AstNode expr2)
    Creates a bvsrem node (2's complement signed remainder, sign follows dividend).
    e.g: (bvsrem expr1 expr2).
  • AstNode bvsub(AstNode expr1, AstNode expr2)
    Creates a bvsub node.
    e.g: (bvsub expr1 epxr2).
  • AstNode bvtrue(void)
    This is an alias on the (_ bv1 1) ast expression.
  • AstNode bvudiv(AstNode expr1, AstNode expr2)
    Creates a bvudiv node.
    e.g: (bvudiv expr1 epxr2).
  • AstNode bvuge(AstNode expr1, AstNode expr2)
    Creates a bvuge node.
    e.g: (bvuge expr1 epxr2).
  • AstNode bvugt(AstNode expr1, AstNode expr2)
    Creates a bvugt node.
    e.g: (bvugt expr1 epxr2).
  • AstNode bvule(AstNode expr1, AstNode expr2)
    Creates a bvule node.
    e.g: (bvule expr1 epxr2).
  • AstNode bvult(AstNode expr1, AstNode expr2)
    Creates a bvult node.
    e.g: (bvult expr1 epxr2).
  • AstNode bvurem(AstNode expr1, AstNode expr2)
    Creates a bvurem node (unsigned remainder).
    e.g: (bvurem expr1 expr2).
  • AstNode bvxnor(AstNode expr1, AstNode expr2)
    Creates a bvxnor node.
    e.g: (bvxnor expr1 expr2).
  • AstNode bvxor(AstNode expr1, AstNode expr2)
    Creates a bvxor node.
    e.g: (bvxor expr1 epxr2).
  • AstNode concat([AstNode, ...])
    Concatenates several nodes.
  • AstNode distinct(AstNode expr1, AstNode expr2)
    Creates a distinct node.
    e.g: (distinct expr1 expr2)
  • AstNode equal(AstNode expr1, AstNode expr2)
    Creates an equal node.
    e.g: (= expr1 epxr2).
  • AstNode extract(integer high, integer low, AstNode expr1)
    Creates an extract node. The high and low fields represent the bits position.
    e.g: ((_ extract high low) expr1).
  • AstNode iff(AstNode expr1, AstNode expr2)
    Creates an iff node (if and only if).
    e.g: (iff expr1 expr2).
  • 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 expr1 expr2 expr3 expr4).
  • AstNode let(string alias, AstNode expr2, AstNode expr3)
    Creates a let node.
    e.g: (let ((alias expr2)) expr3).
  • AstNode lnot(AstNode expr)
    Creates a lnot node (logical NOT).
    e.g: (not expr).
  • AstNode lor([AstNode, ...])
    Creates a logical OR on several nodes. e.g: (or expr1 expr2 expr3 expr4).
  • AstNode lxor([AstNode, ...])
    Creates a logical XOR on several nodes. e.g: (xor expr1 expr2 expr3 expr4).
  • 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 expr1)
    Creates a sx node (sign extend).
    e.g: ((_ sign_extend sizeExt) expr1).
  • AstNode variable(SymbolicVariable symVar)
    Creates a variable node.
  • AstNode zx(integer sizeExt, AstNode expr1)
    Creates a zx node (zero extend).
    e.g: ((_ zero_extend sizeExt) expr1).

Python API - Utility methods of the AstContext class


  • AstNode duplicate(AstNode expr)
    Duplicates the node and returns a new instance as AstNode.
  • [AstNode, ...] search(AstNode expr, AST_NODE match)
    Returns a list of collected matched nodes via a depth-first pre order traversal.
  • z3::expr tritonToZ3(AstNode expr)
    Convert a Triton AST to a Z3 AST.
  • AstNode unroll(AstNode node)
    Unrolls the SSA form of a given 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