Use z3-solver pypi package for z3 installation

[bannsec]

Why not use python z3? The wrapper does basically the same things that z3 command line does, and anything that doesn't directly have a function in the library is exposed through other means.

This would be helpful because you could then pip install z3-solver as well, which would remove another package being installed directly to the system.

[offlinemark]

We're using command line z3 over a pipe for mostly historical reasons, but it does allow us a certain amount of flexibility for using other solvers. At the moment we can't justify the cost in dev time to port to pyz3 ourselves, but definitely acknowledge speed and installation ease benefits. This would definitely qualify for a bounty which would be above standard levels, due to the amount of work. (To anyone considering doing this, please reach out so we can chat on the best way to do this!)

[offlinemark]

I'm going to close this for now, but thanks for bringing it up!

[feliam]

ttbomk, pyz3 do not implement pickle protocol so it can not be serialized/pickled, saved to storage and reloaded. https://stackoverflow.com/questions/14596416/pickling-z3-python-objects

[feliam]

Also relying on generic smtlib instead on pyz3 you can do stuff like making several solver race for the solution.. etc. http://ceur-ws.org/Vol-832/paper_5.pdf There are similarly strong arguments against that and in favor of using the direct approach.

We actually can use pyz3 directly. Just crafting some visitor.py magic. Instead of building the smtlib string we can really easily build a pyz3 expression tree in memory. All that at least for solving.

[offlinemark]

Some pros of that would be

• Easier installation. We could do everything through pip, and not require z3 to be externally installed and available in $PATH
• Performance. I expect there would be a nearly negligible performance improvement, as we would be making direct library calls, without the overhead of a pipe. Considering all the various optimizations we can implement for manticore, this would certainly be a micro-optimization
• Possibly simpler code in some areas. For example, we have some code for parsing z3 cli output for stuff like the version in solver.py that might be able to be removed.

Of these, I do think easier installation is a significant benefit for the project — the fact that we’ve required external z3 installation has always been a wart imo

I think keeping the direct smtlib translation, but Pyz3 backend for solving would be a nice tradeoff between 1. fully gutting the generic smtlib -> replacing with Pyz3 and 2. full generic smtlib with no Pyz3.

To my understanding, the work to be done for this would be

• adding a new Visitor pass in visitor.py implementing Manticore Expression tree -> Pyz3 Expression tree translation
• refactoring various interfaces in manticore.core.smtlib module
• some logic to use Pyz3 by default, instead of generic smtlib + pipe

On Aug 29, 2017, at 3:38 PM, feliam notifications@github.com wrote:

Also relying on generic smtlib instead on pyz3 you can do stuff like making several solver race for the solution.. etc. http://ceur-ws.org/Vol-832/paper_5.pdf http://ceur-ws.org/Vol-832/paper_5.pdf There are similarly strong arguments against that and in favor of using the direct approach.

We actually can use pyz3 directly. Just crafting some visitor.py magic. Instead of building the smtlib string we can really easily build a pyz3 expression tree in memory. All that at least for solving.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/trailofbits/manticore/issues/219#issuecomment-325776394, or mute the thread https://github.com/notifications/unsubscribe-auth/ACWmGyXMW56T3jm0D3248OGcq_lz3T6pks5sdGirgaJpZM4NNPLk.

[offlinemark]

link to pip z3: https://pypi.python.org/pypi/z3-solver

[bannsec]

It should also be noted that z3-solver pypi package now also comes with z3 binary itself. Thus, my normal install for manticore is generally pip install manticore z3-solver. In this case, I'm just using the z3-solver package as an pip installer for z3 binary proper.

[offlinemark]

Whoa, I had no idea! That's awesome, thanks a lot for letting us know. At the very least now, we can simply add z3-solver to our setup.py and that will instantly solve the external installation wart. Specifically, all we need to do is add z3-solver to this list, and update any installation documentation mentioning z3 (like in the README). Help for this would be awesome!

https://github.com/trailofbits/manticore/blob/ca0d7b60d206a7f159694721317034ad49eae666/setup.py#L10-L15

We could go a step further and actually use the pyz3 library as the solver backend as @feliam mentioned (as opposed to generic smtlib -> solver binary backend), but I'm not sure that would yield useful results, so I don't think we should do this now.

@Owlz sorry for initially being dismissive of this issue; I jumped too quickly to thinking that we would need to completely redo our SMT plumbing, and didn't realize partial solutions exist :/

[bannsec]

No worries. I happen to know it's there because initially it wasn't being built in that package. I did the PR to add z3 executable building. lol