[PATCH] D88198: Hints CMake where to find Z3 with LLVM_Z3_INSTALL_DIR.

Thu Oct 15 04:25:00 PDT 2020

OikawaKirie added a comment.

I have another try in a newly installed system without Z3 installed from the distribute software source, and the following tests are carried out in `/tmp/ella.z3-patch`.

The source code of Z3 is located in `/tmp/ella.z3-patch/z3` and Z3 is configured with CMake and built in `/tmp/ella.z3-patch/z3/build`. After Z3 is built, it is not installed to the system directories.

The LLVM project is located in `/tmp/ella.z3-patch/llvm-project` and the directory `/tmp/ella.z3-patch/llvm-project/build` is used as the LLVM build directory, which is the location where `cmake` is executed for LLVM.

The followings are the tests I did with the above configurations. And every time I do a new test, the previous `/tmp/ella.z3-patch/llvm-project/build/CMakeCache.txt` is removed to make CMake configure the project from the very beginning without the influences from the previous configurations.

- When I run `cmake ../llvm`, the project is correctly configured with no error messages.
- When I run `cmake ../llvm -DLLVM_ENABLE_Z3_SOLVER=1`, CMakeLists.txt:382 reports "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available."
- When I run `cmake ../llvm -DLLVM_ENABLE_Z3_SOLVER=1 -DLLVM_Z3_INSTALL_DIR=/tmp/ella.z3-patch/z3`, CMakeLists.txt:377 reports "Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: /tmp/ella.z3-patch/z3."
- When I run `cmake ../llvm -DLLVM_ENABLE_Z3_SOLVER=1 -DLLVM_Z3_INSTALL_DIR=/tmp/ella.z3-patch/z3/build`, the project is correctly configured with no error messages and Z3 is reported to be found (CMakeLists.txt:387).

Then I installed (make install) Z3 to `/tmp/ella.z3-patch/z3-install`, and execute some other tests with `LLVM_Z3_INSTALL_DIR` set as subdirectries under `/tmp/ella.z3-patch/z3-install`. Only when I set `LLVM_Z3_INSTALL_DIR` as `/tmp/ella.z3-patch/z3-install/usr/local/lib/cmake` or `/tmp/ella.z3-patch/z3-install/usr/local/lib/cmake/z3` can I do a correct configuration (Z3 found and no other errors).

Finally, I downloaded the official binary release zip package and unzipped it to `/tmp/ella.z3-patch/z3-4.8.9/z3-4.8.9-x64-ubuntu-16.04` directory, but none of the subdirectories can be used to find Z3.

To avoid wrongly patching a previously implemented functionality, I disabled my patch and tested the directories mentioned above, none of the directories mentioned above can correctly configure LLVM for finding Z3 with the specified version. It seems that without the patch, CMake can only detect the Z3 solver installed from the distribute software source. If Z3 is not installed together with its CMake configurations, or if you want to customize the Z3 version with another installation in another directory, you cannot get the correct configurations you desire under the original version. And if I correctly searched, the variable `LLVM_Z3_INSTALL_DIR` is only used to print an error message on line 378 if it is set and Z3 is not found. Is this variable used anywhere else in the original version?

In the patch, the variable `LLVM_Z3_INSTALL_DIR` is used as the searching directory for the CMake target files of the Z3 solver, rather than the library itself. To be precise, I suggest modifying the variable name as `LLVM_Z3_CMAKE_FILE_DIR` or `LLVM_Z3_BUILD_DIR`.

---

The directories mentioned above:

- LLVM source directory: `/tmp/ella.z3-patch/llvm-project`
- LLVM build directory / CMake directory: `/tmp/ella.z3-patch/llvm-project/build`
- Z3 source directory: `/tmp/ella.z3-patch/z3`
- Z3 build directory: `/tmp/ella.z3-patch/z3/build`
- Z3 make install directory: `/tmp/ella.z3-patch/z3-install`
- Z3 pre-build install directory: `/tmp/ella.z3-patch/z3-4.8.9/z3-4.8.9-x64-ubuntu-16.04`

The settings for variable `LLVM_Z3_INSTALL_DIR` that can correctly configure Z3 with the patch:

- Z3 build directory: `/tmp/ella.z3-patch/z3/build`
- Z3 make install CMake directory: `/tmp/ella.z3-patch/z3-install/usr/local/lib/cmake`
- Z3 make install CMake Z3 directory: `/tmp/ella.z3-patch/z3-install/usr/local/lib/cmake/z3`

Versions: Ubuntu 20.04, CMake 3.16.3, Z3 commit 2841796

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88198/new/

https://reviews.llvm.org/D88198