libTriton  version 0.6 build 1389
SymbolicExpression

Table of Contents

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

Description


This object is used to represent a symbolic expression.

>>> from triton import TritonContext, ARCH, Instruction, REG
>>> ctxt = TritonContext()
>>> ctxt.setArchitecture(ARCH.X86_64)
>>> opcode = "\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)
True
>>> 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) (bvlshr ((_ extract 7 0) ref!0) (_ bv0 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!0) (_ bv1 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!0) (_ bv2 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!0) (_ bv3 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!0) (_ bv4 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!0) (_ bv5 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!0) (_ bv6 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!0) (_ bv7 8))))) ; 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]
>>> expr_1 # doctest: +ELLIPSIS
<SymbolicExpression object at 0x...>
>>> 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()
>>> ast # doctest: +ELLIPSIS
<AstNode object at 0x...>
>>> print ast
(bvxor (_ bv12345 64) (_ bv67890 64))
>>> expr_1.isMemory()
False
>>> expr_1.isRegister()
True
>>> print expr_1.getOrigin()
rax:64 bv[63..0]

Python API - Methods of the SymbolicExpression class