search

illera88 / Ponce

IDA 2016 plugin contest winner! Symbolic Execution just one-click away!
https://docs.idaponce.com
Other
1.5k stars 74 forks source link

About Float Point Instructions #59

Closed pfsun closed 8 years ago

pfsun commented 8 years ago

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

@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 commented 8 years ago

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 commented 8 years ago

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

0ca commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

Done, thank you for the help! https://github.com/illera88/Ponce/commit/eff1ed4158207cdd0349dce77c50639a5613b51c