About Float Point Instructions

[pfsun]

I just try one float-point computing code. Some float-point instruction are missing.

@0ca @illera88 Will you try to add more float point instructions support or other solutions? I also saw some words about float point instructions in Triton website (5.1 - Few words about floating-point instructions) .

[0ca]

It looks it is a Triton issue, as you can see Triton is not generating symbolic expressions for those instructions.

So we can't check if they are symbolic or not :(

We hope in the future the Triton support for floating instructions will be better.

[pfsun]

Yes. It is a Triton issue. It looks they will not support recently :( Thanks.

[0ca]

We should show some warnings when Ponce finds unsupported instructions so the user can know without use the "Add comments with symbolic expression" if an instruction is supported.

[JonathanSalwan]

It looks it is a Triton issue, as you can see Triton is not generating symbolic expressions for those instructions.

Right. Here is our list of supported instructions. The problem with floating point is that SMT solvers cannot deal with expressions which contain both theories bit-vector and floating-point. This behavior is a real problem for us due to the SSA-form. Example:

mov [mem], rax    ; rax comes from bitvector theory
movq xmm1, [mem]  ; generic
addps xmm2, xmm1  ; computation based on floating point theory (where xmm1 comes from bv)

@0ca, regarding #400, I will return a boolean value to let you catch unsupported instructions.

Cheers,

[0ca]

Done, thank you for the help!
eff1ed4