angr-z3
angr-z3 copied to clipboard
angr
New z3 versions for pypi
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?
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
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:
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.
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.
