Build Z3 from source for P4Tools. #4697
Conversation
fruffy
force-pushed
the
fruffy/z3_source
branch
8 times, most recently
from
5ba0346
to
156b925
Compare
|
I have no urgency for this issue, but if I understand correctly that with this change, then building p4c will by default fetch z3 source code of a particular desired version and build it from source code, then as long as that version also compiles and works for arm64 processors (e.g. Apple Silicon running arm64/aarch64 Linux in a VM), it would slightly simplify the work of those building P4 tools for that processor ach. |
Yes! It also allows us to finally upgrade Z3 in tools and fix some of the segmentation fault problems. But there is still some work to do. |
| set(P4TOOLS_Z3_INCLUDE_DIR ${Z3_INCLUDE_DIR}) | ||
| else() | ||
| # Pull in a specific version of Z3 and link against it. | ||
| set(P4TOOLS_Z3_VERSION "4.13.0") |
There was a problem hiding this comment.
It seems odd that Z#_MAX_VERSION_EXCL above is 4.12, but you are explicitly pulling in 4.13.0 here. Do you expect one of those two things to change before this PR is ready to merge?
There was a problem hiding this comment.
Z3 versions above 4.12 added malloc_usable_size which causes problems with P4C's garbage collector. I have not figured out a fix for BDWGC yet.
When we build from scratch we do not have this problem because we can patch the Z3 installation.
There was a problem hiding this comment.
That should be a comment clarifying that.
There was a problem hiding this comment.
There is some more work to be done first, need to figure out whether it is possible to patch bdwgc instead.
fruffy
force-pushed
the
fruffy/z3_source
branch
3 times, most recently
from
f0758ff
to
65a13ee
Compare
fruffy
force-pushed
the
fruffy/z3_source
branch
4 times, most recently
from
7c2aae3
to
3cd7652
Compare
* Remove a stray print in the smith code. (#4891) Signed-off-by: fruffy <[email protected]> * Make isSystemFile part of the parser options. Signed-off-by: fruffy <[email protected]> * Review comments. Signed-off-by: fruffy <[email protected]> --------- Signed-off-by: fruffy <[email protected]>
Signed-off-by: fruffy <[email protected]>
fruffy
force-pushed
the
fruffy/z3_source
branch
from
3cd7652
to
35548cb
Compare
Fixes #4693.