JonathanSalwan / Triton

Triton is a dynamic binary analysis library. Build your own program analysis tools, automate your reverse engineering, perform software verification or just emulate code.
https://triton-library.github.io
Apache License 2.0
3.4k stars 524 forks source link

Fix isSymbolic computation for IteNode #1290

Closed cnheitman closed 9 months ago

cnheitman commented 9 months ago

This PR fixes how isSymbolic is computed for ITE nodes. The following code shows the issue:

from triton import *

ctx = TritonContext(ARCH.X86_64)

ast_ctx = ctx.getAstContext()

x = ctx.newSymbolicVariable(32)

ite_node = ast_ctx.ite(
                ast_ctx.equal(ast_ctx.bv(1, 1), ast_ctx.bv(1, 1)),
                ast_ctx.bv(0x12345678, 32),
                ast_ctx.variable(x))

print(f'[+] ITE node: {ite_node}')
print(f'[+] ITE node is symbolic? {ite_node.isSymbolized()}')

It will output that ite_node is symbolic when it is not:

[+] ITE node: (ite (= (_ bv1 1) (_ bv1 1)) (_ bv305419896 32) SymVar_0)
[+] ITE node is symbolic? True

Now we check that first whether the IfExpr of the ITE node is symbolic. If it is, it marks the whole node as symbolic otherwise checks each children.

Note that the problem above is not present if either MODE.AST_OPTIMIZATIONS or MODE.CONSTANT_FOLDING is set, since the optimization basically does the same as the proposed fix (here).

JonathanSalwan commented 9 months ago

Nice one.