About Symbolic Expression

[pfsun]

Hi,

Just find your great work!!

I was wondering whether I can get the symbolic expression at any point while doing symbolic execution by Ponce?

Thanks, Pengfei

[0ca]

@pfsun Try this option: It adds comments below every instruction with all the symbolic expressions generated.

[pfsun]

@0ca Thanks for pointing out this option. I have got the symbolic expression for each instruction which are same results with Triton. For Triton, I have to use getFullAst to get the complete symbolic expression. I wonder whether we can simply the symbolic expression. If we send the symbolic expression to solver, how the symbolic expression will be after solver? Thanks.

[0ca]

@pfsun in Ponce we also get the complete expression with getFullAst before send it to the solver.

About simplify expressions, Triton supports some simplifications but you need to code them individually. https://github.com/JonathanSalwan/Triton/blob/a9e8f24dcdaf3c3eba040dc371c71c344107e526/src/examples/python/simplification.py

Triton has also some optimizations and we are using in Ponce almost all of them: http://triton.quarkslab.com/documentation/doxygen/py_OPTIMIZATION_page.html

But I am not very sure about how you can use the solver to simplify one expression. If you know how, tell us and we will try to implement it in Ponce ;)

[pfsun]

@0ca Thanks for these information. I will go further detail. Actually, I also don't know how :-). If I know, I do discuss with you.