PathConstraint

Table of Contents

• Description
• Python API - Methods of the PathConstraint class

[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.
• string getComment(void)
  Returns the comment (if exists) of the path constraint.
• integer getSourceAddress(void)
  Returns the source address of the branch.
• 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.
• void setComment(string comment)
  Sets comment of the path constraint.