SymbolicExpression

Table of Contents

• Description
• Python API - Methods of the SymbolicExpression class

[python api] All information about the SymbolicExpression Python object.

Description

---

This object is used to represent a symbolic expression.

>>> from __future__ import print_function
>>> from triton import TritonContext, ARCH, Instruction, REG
 
>>> ctxt = TritonContext()
>>> ctxt.setArchitecture(ARCH.X86_64)
 
>>> opcode = b"\x48\x31\xD0"
>>> inst = Instruction()
 
>>> inst.setOpcode(opcode)
>>> inst.setAddress(0x400000)
>>> ctxt.setConcreteRegisterValue(ctxt.registers.rax, 12345)
>>> ctxt.setConcreteRegisterValue(ctxt.registers.rdx, 67890)
 
>>> ctxt.processing(inst)
0
>>> print(inst)
0x400000: xor rax, rdx
 
>>> for expr in inst.getSymbolicExpressions():
...     print(expr)
...
(define-fun ref!0 () (_ BitVec 64) (bvxor (_ bv12345 64) (_ bv67890 64))) ; XOR operation
(define-fun ref!1 () (_ BitVec 1) (_ bv0 1)) ; Clears carry flag
(define-fun ref!2 () (_ BitVec 1) (_ bv0 1)) ; Clears overflow flag
(define-fun ref!3 () (_ BitVec 1) (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (_ bv1 1) ((_ extract 0 0) ref!0)) ((_ extract 1 1) ref!0)) ((_ extract 2 2) ref!0)) ((_ extract 3 3) ref!0)) ((_ extract 4 4) ref!0)) ((_ extract 5 5) ref!0)) ((_ extract 6 6) ref!0)) ((_ extract 7 7) ref!0))) ; Parity flag
(define-fun ref!4 () (_ BitVec 1) ((_ extract 63 63) ref!0)) ; Sign flag
(define-fun ref!5 () (_ BitVec 1) (ite (= ref!0 (_ bv0 64)) (_ bv1 1) (_ bv0 1))) ; Zero flag
(define-fun ref!6 () (_ BitVec 64) (_ bv4194307 64)) ; Program Counter
 
>>> expr_1 = inst.getSymbolicExpressions()[0]
>>> print(expr_1)
(define-fun ref!0 () (_ BitVec 64) (bvxor (_ bv12345 64) (_ bv67890 64))) ; XOR operation
 
>>> print(expr_1.getId())
0
 
>>> ast = expr_1.getAst()
>>> print(ast)
(bvxor (_ bv12345 64) (_ bv67890 64))
 
 
>>> expr_1.isMemory()
False
 
>>> expr_1.isRegister()
True
 
>>> print(expr_1.getOrigin())
rax:64 bv[63..0]
 
>>> print(expr_1.getDisassembly())
0x400000: xor rax, rdx

Python API - Methods of the SymbolicExpression class

---

• AstNode getAst(void)
  Returns the AST root node of the symbolic expression.
• string getComment(void)
  Returns the comment (if exists) of the symbolic expression.
• string getDisassembly(void)
  Returns the instruction disassembly where the symbolic expression comes from.
• integer getId(void)
  Returns the id of the symbolic expression. This id is always unique.
  e.g: 2387
• AstNode getNewAst(void)
  Returns a new AST root node of the symbolic expression. This new instance is a duplicate of the original node and may be changed without changing the original semantics.
• MemoryAccess / Register getOrigin(void)
  Returns the origin of the symbolic expression. For example, if the symbolic expression is assigned to a memory cell, this function returns a MemoryAccess, else if it is assigned to a register, this function returns a Register otherwise it returns None. Note that for a MemoryAccess all information about LEA are lost at this level.
• SYMBOLIC getType(void)
  Returns the type of the symbolic expression.
  e.g: SYMBOLIC.REGISTER_EXPRESSION
• bool isMemory(void)
  Returns true if the expression is assigned to memory.
• bool isRegister(void)
  Returns true if the expression is assigned to a register.
• bool isSymbolized(void)
  Returns true if the expression contains a symbolic variable.
• bool isTainted(void)
  Returns true if the expression is tainted.
• void setAst(AstNode node)
  Sets a root node.
• void setComment(string comment)
  Sets a comment to the symbolic expression.