SMT simplification passes

Table of Contents

• Description
  • Simplification via Triton's rules
  • Simplification via Z3

[internal] All information about the SMT simplification passes.

Description

---

Triton allows you to optimize your AST (See: AstContext) just before the assignment to a register, a memory or a volatile symbolic expression. The record of a simplification pass is really straightforward. You have to record your simplification callback using the triton::Context::addCallback() function. Your simplification callback must takes as parameters a triton::Context and a triton::ast::SharedAbstractNode. The callback must return a triton::ast::SharedAbstractNode. Then, your callback will be called before every symbolic assignment. Note that you can record several simplification callbacks or remove a specific callback using the triton::Context::removeCallback() function.

Simplification via Triton's rules

---

Below, a little example which replaces all \( A \oplus A \rightarrow A = 0\).

// Rule: if (bvxor x x) -> (_ bv0 x_size)
triton::ast::SharedAbstractNode xor_simplification(triton::Context& ctx, const triton::ast::SharedAbstractNode& node) {
 
  if (node->getType() == triton::ast::BVXOR_NODE) {
    if (node->getChildren()[0]->equalTo(node->getChildren()[1]))
      return ctx.getAstContext().bv(0, node->getBitvectorSize());
  }
 
  return node;
}
 
int main(int ac, const char *av[]) {
  ...
  // Record a simplification callback
  ctx.addCallback(xor_simplification);
  ...
}

Another example (this time in Python) which replaces a node with this rule \( ((A \land \lnot{B}) \lor (\lnot{A} \land B)) \rightarrow (A \oplus B) \).

# Rule: if ((a & ~b) | (~a & b)) -> (a ^ b)
def xor_bitwise(ctx, node):
 
    def getNot(node):
        a = node.getChildren()[0]
        b = node.getChildren()[1]
        if a.getType() == AST_NODE.BVNOT and b.getType() != AST_NODE.BVNOT:
            return a
        if b.getType() == AST_NODE.BVNOT and a.getType() != AST_NODE.BVNOT:
            return b
        return None
 
    def getNonNot(node):
        a = node.getChildren()[0]
        b = node.getChildren()[1]
        if a.getType() != AST_NODE.BVNOT and b.getType() == AST_NODE.BVNOT:
            return a
        if b.getType() != AST_NODE.BVNOT and a.getType() == AST_NODE.BVNOT:
            return b
        return None
 
    if node.getType() == AST_NODE.BVOR:
        c1 = node.getChildren()[0]
        c2 = node.getChildren()[1]
        if c1.getType() == AST_NODE.BVAND and c2.getType() == AST_NODE.BVAND:
            c1_not    = getNot(c1)
            c2_not    = getNot(c2)
            c1_nonNot = getNonNot(c1)
            c2_nonNot = getNonNot(c2)
            if c1_not.equalTo(~c2_nonNot) and c2_not.equalTo(~c1_nonNot):
                return c1_nonNot ^ c2_nonNot
    return node
 
 
if __name__ == "__main__":
    ctx = TritonContext()
 
    # Set arch to init engines
    ctx.setArchitecture(ARCH.X86_64)
 
    # Record simplifications
    ctx.addCallback(SYMBOLIC_SIMPLIFICATION, xor_bitwise)
 
    a = bv(1, 8)
    b = bv(2, 8)
    c = (~b & a) | (~a & b)
    print 'Expr: ', c
    c = ctx.simplify(c)
    print 'Simp: ', c

Simplification via Z3

---

As Triton is able to convert a Triton's AST to a Z3's AST and vice versa, you can benefit to the power of Z3 to simplify your expression, then, come back to a Triton's AST and apply your own rules.

>>> var = ctx.newSymbolicVariable(8)
>>> a = ctx.getAstContext().variable(var)
>>> b = bv(0x38, 8)
>>> c = bv(0xde, 8)
>>> d = bv(0x4f, 8)
>>> e = a * ((b & c) | d)
 
>>> print e
(bvmul SymVar_0 (bvor (bvand (_ bv56 8) (_ bv222 8)) (_ bv79 8)))
 
>>> usingZ3 = True
>>> f = ctx.simplify(e, usingZ3)
>>> print f
(bvmul (_ bv95 8) SymVar_0)

Note that applying a SMT simplification doesn't means that your expression will be more readable by an humain. For example, if we perform a simplification of a bitwise operation (as described in the previous section), the new expression is not really useful for an humain.

>>> a = ctx.getAstContext().variable(var)
>>> b = bv(2, 8)
>>> c = (~b & a) | (~a & b) # a ^ b
 
>>> print c
(bvor (bvand (bvnot (_ bv2 8)) SymVar_0) (bvand (bvnot SymVar_0) (_ bv2 8)))
 
>>> d = ctx.simplify(c, True)
>>> print d
(concat ((_ extract 7 2) SymVar_0) (bvnot ((_ extract 1 1) SymVar_0)) ((_ extract 0 0) SymVar_0))

As you can see, Z3 tries to apply a bit-to-bit simplification. That's why, Triton allows you to deal with both, Z3's simplification passes and your own rules.