libTriton  version 0.9 build 1502
PathConstraint

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

Description


This object is used to represent a path constraint.

>>> pcl = ctxt.getPathConstraints()
>>> for pc in pcl:
... if pc.isMultipleBranches():
... b1 = pc.getBranchConstraints()[0]['constraint']
... b2 = pc.getBranchConstraints()[1]['constraint']
...
... print('Constraint branch 1: %s' % (b1))
... print('Constraint branch 2: %s' % (b2))
...
... seed = list()
...
... # Branch 1, we assume that the path constraint contains a symbolic variable
... models = ctxt.getModel(b)
... for k, v in models.items():
... seed.append(v)
...
... # Branch 2, we assume that the path constraint contains a symbolic variable.
... models = ctxt.getModel(b2)
... for k, v in models.items():
... seed.append(v)
...
... if seed:
... print('B1: %s (%c) | B2: %s (%c)' % (seed[0], chr(seed[0].getValue()), seed[1], chr(seed[1].getValue())))
...

A possible output is :

Constraint branch 1: (not (= (ite (= ((_ extract 0 0) ref!179) (_ bv1 1)) (_ bv4195769 64) (_ bv4195762 64)) (_ bv4195762 64)))
Constraint branch 2: (= (ite (= ((_ extract 0 0) ref!179) (_ bv1 1)) (_ bv4195769 64) (_ bv4195762 64)) (_ bv4195762 64))
B1: SymVar_0 = 65 (e) | B2: SymVar_0 = 0 ()
[...]

Python API - Methods of the PathConstraint class


  • dict getBranchConstraints(void)
    Returns the branch constraints as list of dictionary {isTaken, srcAddr, dstAddr, constraint}. The source address is the location of the branch instruction and the destination address is the destination of the jump. E.g: "0x11223344: jne 0x55667788", 0x11223344 is the source address and 0x55667788 is the destination if and only if the branch is taken, otherwise the destination is the next instruction address.
  • integer getTakenAddress(void)
    Returns the address of the taken branch.
  • AstNode getTakenPredicate(void)
    Returns the predicate of the taken branch.
  • integer getThreadId(void)
    Returns the thread id of the constraint. Returns -1 if thread id is undefined.
  • bool isMultipleBranches(void)
    Returns true if it is not a direct jump.