-
Notifications
You must be signed in to change notification settings - Fork 439
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Build Z3 from source for P4Tools. #4697
base: main
Are you sure you want to change the base?
Conversation
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That should be a comment clarifying that.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is some more work to be done first, need to figure out whether it is possible to patch bdwgc instead.
f0758ff
to
65a13ee
Compare
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]>
3cd7652
to
35548cb
Compare
Fixes #4693.