1 - Implicit concretization when setting a concrete value

Thread: #808.

Triton keeps at each program point a concrete and a symbolic state. When the user modifies a concrete value at a specific program point, it may imply a de-synchronization between those two states and, before v0.8, the user had to force the re-synchronization by concretizing registers or memory cells. For example, we could have a snippet like this:

ctx.setConcreteRegisterValue(ctx.registers.rax, 0x1234)
ctx.concretizeRegister(ctx.registers.rax) # concretize the register which points to an old symbolic expression

With v0.8 you should have something like this:

ctx.setConcreteRegisterValue(ctx.registers.rax, 0x1234) # implicit concretization

2 - Dealing with the path predicate

Thread: #350.

During the execution, Triton builds the path predicate when it encounters conditional instructions. We provided some new methods which allow the user to deal a bit better with the path predicate. It's now possible to:

• remove the last constraint added to the path predicate using popPathConstraint();
• add new constraints using pushPathConstraint();
• clear the current path predicate using clearPathConstraints().

We also provided a new method which returns the path predicate to target a basic block address if this one is reachable during the execution (do not forget that we are in a dynamic analysis context): getPredicatesToReachAddress().

For example, let's consider at one point we want to add a post condition on our path predicate, such as rax must be different from 0. The snippet of code should look like this:

if inst.getAddress() == [my target address]:
    rax = ctx.getRegisterAst(ctx.registers.rax)
    ctx.pushPathConstraint(rax != 0)

3 - The CONSTANT_FOLDING optimization

Thread: #835.

We added a new optimization which performs a constant folding at the build time of AST nodes. This optimization is pretty similar to ONLY_ON_SYMBOLIZED except that the concretization occurs at each level of the AST during its construction while ONLY_ON_SYMBOLIZED only checks if a root node of a symbolic expression contains symbolic variables (which does not concretize sub-trees if it is true).

4 - Converting a Z3 expression to a Triton expression

Thread: #850.

It's now possible to convert a Z3 expression into a Triton expression and vice versa using Python bindings. Before v0.8, the conversion from z3 to Triton was only possible with the C++ API.

>>> from triton import *
>>> ctx = TritonContext(ARCH.X86_64)
>>> ast = ctx.getAstContext()

>>> x = ast.variable(ctx.newSymbolicVariable(8))
>>> y = ast.variable(ctx.newSymbolicVariable(8))

>>> n = x + y * 2
>>> print(n)
(bvadd SymVar_0 (bvmul SymVar_1 (_ bv2 8)))

>>> z3n = ast.tritonToZ3(n)
>>> print(type(z3n))
<class 'z3.z3.ExprRef'>
>>> print(z3n)
SymVar_0 + SymVar_1*2

>>> ttn = ast.z3ToTriton(z3n)
>>> print(type(ttn))
<class 'AstNode'>
>>> print(ttn)
(bvadd SymVar_0 (bvmul SymVar_1 (_ bv2 8)))

6 - The quantifier operator: forall

Thread: #860.

After reading a nice blog post about constant synthesizing, we thought it could be interesting to add the quantifier operator: forall. For example, let's assume we want to synthesize the following expression ((x << 8) >> 16) << 8 into x & 0xffff00 where x is a 32-bit vector and the constant 0xffff00 is the unknown. The SMT query looks like this:

(declare-fun C () (_ BitVec 32))
(assert (forall
            ((x (_ BitVec 32)))
            (=
                (bvand x C)
                (bvshl (bvlshr (bvshl x (_ bv8 32)) (_ bv16 32)) (_ bv8 32))
            )
        )
)
(check-sat)
(get-model)

The illustrated SMT query can be read as: There exists a constant C such that for all x the expression x & C is equal to ((x << 8) >> 16) << 8. To handle such query in Python with v0.8, you could have a snippet of code like the following:

#!/usr/bin/env python
## -*- coding: utf-8 -*-
##
##   $ python ./example.py
##   {1: C:32 = 0xffff00}
##

from triton import *

ctx = TritonContext(ARCH.X86_64)
ast = ctx.getAstContext()

x = ast.variable(ctx.newSymbolicVariable(32))
c = ast.variable(ctx.newSymbolicVariable(32))

x.getSymbolicVariable().setAlias('x')
c.getSymbolicVariable().setAlias('C')

print(ctx.getModel(ast.forall([x], ((x << 8) >> 16) << 8 == x & c)))

7 - Changes to the user API

Threads: #812, #864, #865 and #866.

The following v0.7 functions are deprecated and must be replaced by their v0.8 equivalent.

8 - ARMv7 support

Thread: #831.

Last but not least, Triton v0.8 introduces yet another architecture: ARMv7. With this new inclusion, Triton now has support for the most popular architectures, namely: x86, x86-64, ARM32 and AArch64.

The ubiquity of ARM processors is one of the main reasons for adding support for ARMv7 in Triton. ARMv7 is a widely popular architecture, particularly in embedded devices and mobile phones. We wanted to bring the advantages of Triton to this architecture (most tools are prepared to work on Intel x86/x86_64 only). The other reason is to show the flexibility and extensibility of Triton. ARMv7 poses some challenges in terms of implementation given its many features and peculiarities (some of them quite different from the rest of the supported architectures). Therefore, ARMv7 makes a great architecture to add to the list of supported ones.

You can start by checking some of the available samples.