search

angr / angr-z3

The Z3 Theorem Prover - repository for staging python distributions
Other
56 stars 15 forks source link

New z3 versions for pypi #9

Open norhh opened 5 years ago

norhh commented 5 years ago

Hi, It's been a long time since a release of z3 in pypi, So wouldn't it be good to have a release now with all the latest updates of z3?

subwire commented 5 years ago

IIRC, we are very actively working on it. @Phat3 is taking the lead on major optimizations to Claripy (found here: https://github.com/angr/claripy/pull/119) and I remember him saying a z3 upgrade was in the mix as well, but I'll let him and the others speak to that specifically.

We can't just do it, unfortunately, a bunch of stuff broke in the new versions, see https://github.com/angr/claripy/issues/86, and so we have to find some solution to all that before a release can happen

Phat3 commented 5 years ago

As @subwire said we are currently testing angr with the z3 version 4.8.5 and we still have a couple of problems to fix mostly related to the FP theory part.

Stay tuned for updates :smiley:

NikolajBjorner commented 5 years ago

question: does z3-solver use features specific to the angr fork? There is a pending pull request to Z3's master branch based on a faster FFI wrapper. I haven't taken it yet because it seemed to introduce new dependencies whose support I wasn't sure about. Is this feature or other in your fork? For a pip package I would believe that assembling it from release bits that are hosted on GitHub would be more sustainable. Thus, an option to setup.py that is similar to bdist_egg, but doesn't build and instead pulls binaries+source.

ltfish commented 5 years ago

Obviously I wasn’t subscribing to this repo...

rhelmot commented 5 years ago

Hi! Yeah, uh, I guess github doesn't subscribe you to repositories you fork...

There is no angr fork of z3 at this point. All our patches have been upstreamed. This repository is just for issues and for submitting PRs.

cffi is a well-supported and well-maintained package. Adding a dependency on it for the python bindings would be very easy and ought not to pose any issue. I was extremely excited to see that PR, and would support replacing the ctypes bindings entirely with cffi. This is actually something we had been considering trying to do for a while.

I have some doubts about a build process that doesn't involve doing the builds in the manner I outlined in the other issue, but I would be willing to look into it. Please let me know if this is something you actively desire and I'll put time into it.

LordAro commented 5 years ago

How goes this issue? I notice pypi is still on 4.8.0...

rhelmot commented 5 years ago

Just pushed 4.8.5.