libTriton  version 0.4 build 1351
SMT simplification passes

Table of Contents

[internal] All information about the SMT simplification passes.

Description


Triton allows you to optimize your AST (See: AST Representations) 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::API::addCallback() function. Your simplification callback must takes as unique parameter a pointer of triton::ast::AbstractNode and returns a pointer of triton::ast::AbstractNode. 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::API::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)
if (node->getKind() == triton::ast::BVXOR_NODE) {
if (*(node->getChilds()[0]) == *(node->getChilds()[1]))
return triton::ast::bv(0, node->getBitvectorSize());
}
return node;
}
int main(int ac, const char *av[]) {
...
// Record a simplification callback
api.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) \).

1 # Rule: if ((a & ~b) | (~a & b)) -> (a ^ b)
2 def xor_bitwise(node):
3 
4  def getNot(node):
5  a = node.getChilds()[0]
6  b = node.getChilds()[1]
7  if a.getKind() == AST_NODE.BVNOT and b.getKind() != AST_NODE.BVNOT:
8  return a
9  if b.getKind() == AST_NODE.BVNOT and a.getKind() != AST_NODE.BVNOT:
10  return b
11  return None
12 
13  def getNonNot(node):
14  a = node.getChilds()[0]
15  b = node.getChilds()[1]
16  if a.getKind() != AST_NODE.BVNOT and b.getKind() == AST_NODE.BVNOT:
17  return a
18  if b.getKind() != AST_NODE.BVNOT and a.getKind() == AST_NODE.BVNOT:
19  return b
20  return None
21 
22  if node.getKind() == AST_NODE.BVOR:
23  c1 = node.getChilds()[0]
24  c2 = node.getChilds()[1]
25  if c1.getKind() == AST_NODE.BVAND and c2.getKind() == AST_NODE.BVAND:
26  c1_not = getNot(c1)
27  c2_not = getNot(c2)
28  c1_nonNot = getNonNot(c1)
29  c2_nonNot = getNonNot(c2)
30  if c1_not == ~c2_nonNot and c2_not == ~c1_nonNot:
31  return c1_nonNot ^ c2_nonNot
32  return node
33 
34 
35 if __name__ == "__main__":
36 
37  # Set arch to init engines
38  setArchitecture(ARCH.X86_64)
39 
40  # Record simplifications
41  addCallback(xor_bitwise, SYMBOLIC_SIMPLIFICATION)
42 
43  a = bv(1, 8)
44  b = bv(2, 8)
45  c = (~b & a) | (~a & b)
46  print 'Expr: ', c
47  c = simplify(c)
48  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.

1 >>> var = newSymbolicVariable(8)
2 >>> a = variable(var)
3 >>> b = bv(0x38, 8)
4 >>> c = bv(0xde, 8)
5 >>> d = bv(0x4f, 8)
6 >>> e = a * ((b & c) | d)
7 
8 >>> print e
9 (bvmul SymVar_0 (bvor (bvand (_ bv56 8) (_ bv222 8)) (_ bv79 8)))
10 
11 >>> usingZ3 = True
12 >>> f = simplify(e, usingZ3)
13 >>> print f
14 (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.

1 >>> a = variable(var)
2 >>> b = bv(2, 8)
3 >>> c = (~b & a) | (~a & b) # a ^ b
4 
5 >>> print c
6 (bvor (bvand (bvnot (_ bv2 8)) SymVar_0) (bvand (bvnot SymVar_0) (_ bv2 8)))
7 
8 >>> d = simplify(c, True)
9 >>> print d
10 (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.