Build Z3 from source instead of downloading precompiled binaries.

[fruffy]

Fixes #4693.

[jafingerhut]

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.

[fruffy]

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.

[jafingerhut]

@fruffy I tried building using this branch on an aarch64 Ubuntu 24.04 system (not sure if those details are relevant yet -- also trying x86_64 Ubuntu 24.04 but not done yet), and I got this error when trying to use these steps to build p4c:

# First installed p4lang/PI, p4lang/behavioral-model, Ubuntu package for grpc and protobuf, and a few other things, then...
git clone https://github.com/p4lang/p4c
cd p4c
git checkout fruffy/z3_source
git submodule update --init --recursive
mkdir build
cd build
cmake .. -DCMAKE_BUILD_TYPE=RELEASE -DENABLE_TEST_TOOLS=ON

Here are the errors I saw near the end of the output of the failed cmake command:

[100%] Completed 'z3-populate'
[100%] Built target z3-populate
-- Z3 version 4.13.1.0
-- Failed to find git directory.
-- CMake generator: Unix Makefiles
-- Build type: RELEASE
CMake Error at build/_deps/z3-src/CMakeLists.txt:144 (message):
  "RELEASE" is an invalid build type.

  Use one of the following build types
  Debug;Release;RelWithDebInfo;MinSizeRel


-- Configuring incomplete, errors occurred!

It appears that p4c requires CMAKE_BUILD_TYPE to be RELEASE or DEBUG, but Z3 requires it to be one of Debug;Release;RelWithDebInfo;MinSizeRel?

How did you get around that?

[fruffy]

We fixed it here: #4765

In your list of steps RELEASE is used. I actually am not sure whether the names are case-insensitive, Z3 only enforces the right naming. We could remove that check.

Edit: Turns out this can matter in some cases: https://cmake.org/cmake/help/latest/manual/cmake-buildsystem.7.html#case-sensitivity

[jafingerhut]

I will try "Release" instead of "RELEASE" and see if things go better.

[jafingerhut]

It isn't finished yet, but it is going much further when I use this command when building p4c:

cmake .. -DCMAKE_BUILD_TYPE=Release -DENABLE_TEST_TOOLS=ON

instead of this command:

cmake .. -DCMAKE_BUILD_TYPE=RELEASE -DENABLE_TEST_TOOLS=ON

so as far as I can tell it is not case-insensitive. Well, or at least Z3's name check is not case-insensitive.

[jafingerhut]

Is there a reason you prefer this PR builds Z3 from source code, vs. getting precompiled binaries from the Z3 releases page? At least for versions since about Z3 4.12.x or so, it seems they release precompiled binaries for Linux for both x86_64 and arm64 processors. Not a big deal to me either way -- mainly curious.

[fruffy]

Is there a reason you prefer this PR builds Z3 from source code, vs. getting precompiled binaries from the Z3 releases page? At least for versions since about Z3 4.12.x or so, it seems they release precompiled binaries for Linux for both x86_64 and arm64 processors. Not a big deal to me either way -- mainly curious.

Yes, starting with 4.12 P4C will crash when used with the garbage collector BDWGC. The reason is that the Z3 developers added malloc_usable_size(https://github.com/Z3Prover/z3/blob/b0fef6429fb29a33eb14adf9a61353b59f0f7fd0/src/util/memory_manager.cpp#L319). BDWGC doesn't seem to handle that well.

I can't figure out how to fix BDWGC and the only other way is to patch Z3. That is only possible when pulling and compiling from source.

[jafingerhut]

I have not read and thought about the code changes. However, I have checked out this branch on both an aarch64 and x86_64 Ubuntu 24.04 Linux VM, and built p4c from source using these changes, and they pass tests, and p4testgen basically works at generating test cases.

[vlstill]

I think the PR name is misleading. But the PR itself looks OK