iff AST Node

[bannsec]

I'm getting an error about iff AST nodes:

In [15]: print(rip_ast)
((_ extract 63 0) ((_ zero_extend 0) (ite (= (bvor (bvxor ((_ extract 0 0) ((_ extract 31 31) (bvsub ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ sign_extend 24) (_ bv4 8))))) ((_ extract 0 0) ((_ extract 31 31) (bvand (bvxor ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ sign_extend 24) (_ bv4 8))) (bvxor ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ extract 31 0) (bvsub ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ sign_extend 24) (_ bv4 8))))))))) ((_ extract 0 0) (ite (= ((_ extract 31 0) (bvsub ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ sign_extend 24) (_ bv4 8)))) (_ bv0 32)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1)) (_ bv20 64) (_ bv5 64))))

In [16]: state.ctx.simplify(rip_ast,True)
---------------------------------------------------------------------------
TypeError                                 Traceback (most recent call last)
<ipython-input-16-743ad7e3a694> in <module>()
----> 1 state.ctx.simplify(rip_ast,True)

TypeError: Z3ToTritonAst::visit(): 'iff' AST node not supported yet

I don't see any iff operations in there.

[JonathanSalwan]

Indeed, in your rip_ast expression, there is no iff node but using the simplify function, z3 simplifies it using such node. So, when Triton converts the z3's simplified expression into the Triton's representation, it raises an exception saying that it doesn't support such nodes.

(duplicate #409)

[bannsec]

Gotcha. Is there plans to support this? This actually came up immediately on simplifying rip after a conditional jump, so likely it is something that z3 would use a lot of.

[JonathanSalwan]

yep, the problem is that iff cannot be supported as a Python representation =/.

[JonathanSalwan]

ite can be represented as (0 if x else 1) but about the iff we are fucked :(

[JonathanSalwan]

Maybe a potential way could be to ask to z3 to do not use such node during its simplification process (but dunno if it's possible).

[bannsec]

So I thought the z3 wrapper just exposed it as an object. Why do we need to be able to express iff as a python statement instead of treating it as an opaque object that z3 understands?

[JonathanSalwan]

Why do we need to be able to express iff as a python statement instead of treating it as an opaque object that z3 understands?

Do you have an example?

[bannsec]

Just trying to understand the problem. Not sure why Triton has to be able to represent iff so long as z3 understands what it means.

[JonathanSalwan]

it's ok about z3 but how do we display our AST when setAstRepresentationMode(PYTHON) is enabled?

[bannsec]

my personal opinion on that is to simply make up some format for it. i would think the benefits of having it optimized would outweigh not having a legit way to print the representation out in python. Also, I wouldn't think anyone would need to directly evaluate the python representation itself. I see that more as a description of the ast (and obviously already leaves out size of the bitvector for example).

[thebabush]

What about using an instrinsic? It would break eval() but only if you don't import the instrinsic into the global scope.

My whole "I want a Z3 expression in python" issue was specifically because of this issue.

EDIT: In the other issue (#409) you mention that the operator must be ternary... Is that true? Maybe I'm missing something but it doesn't look like it. It's ==, isn't it?.
Also, iff does seem to occur during DSE... My getPathConstraintsAst + unrollAst gives me:

((0x1 == 0x1) and ((0x4004D0 if ((((((((SymVar_0 & 0xFF) - 0x30) & 0xFF) >> 7) & 0x1) ^ (((((SymVar_0 & 0xFF) ^ 0x30) & ((SymVar_0 & 0xFF) ^ (((SymVar_0 & 0xFF) - 0x30) & 0xFF))) >> 7) & 0x1)) | (0x1 if ((((SymVar_0 & 0xFF) - 0x30) & 0xFF) == 0x0) else 0x0)) == 0x0) else 0x4004B9) == 0x4004D0))

[JonathanSalwan]

Notes for myself:

The evaluation part regarding the symbolic emulation:

; $ z3 -smt2 iff.smt2
; sat
; true
; false
; false
; true

(check-sat)
(eval
    (iff
        (= (_ bv1 16) (_ bv1 16))
        (= (_ bv10 16) (_ bv10 16))
    )
)

(eval
    (iff
        (= (_ bv1 16) (_ bv1 16))
        (= (_ bv20 16) (_ bv10 16))
    )
)

(eval
    (iff
        (= (_ bv2 16) (_ bv1 16))
        (= (_ bv10 16) (_ bv10 16))
    )
)

(eval
    (iff
        (= (_ bv2 16) (_ bv1 16))
        (= (_ bv20 16) (_ bv10 16))
    )
)

The Python representation (solution 1):

In [1]: (10 == 10 if 1 == 1 else not (10 == 10))
Out[1]: True

In [2]: (20 == 10 if 1 == 1 else not (20 == 10))
Out[2]: False

In [3]: (10 == 10 if 2 == 1 else not (10 == 10))
Out[3]: False

In [4]: (20 == 10 if 2 == 1 else not (20 == 10))
Out[4]: True

The Python representation (solution 2):

In [1]: P = 1 == 1
In [2]: Q = 10 == 10
In [3]: (P and Q) or (not P and not Q)
Out[3]: True

In [4]: P = 1 == 1
In [5]: Q = 10 == 20
In [6]: (P and Q) or (not P and not Q)
Out[6]: False

In [7]: P = 1 == 2
In [8]: Q = 10 == 10
In [9]: (P and Q) or (not P and not Q)
Out[9]: False

In [10]: P = 1 == 2
In [11]: Q = 10 == 20
In [12]: (P and Q) or (not P and not Q)
Out[12]: True

Z3's API:

pub unsafe extern "C" fn Z3_mk_iff(
    c: Z3_context, 
    t1: Z3_ast, 
    t2: Z3_ast
) -> Z3_ast

[JonathanSalwan]

Merged into dev-v0.7.