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

[Mikhail Ramalho Gadelha via llvm-commits]

Hi,

Em qui., 15 de out. de 2020 às 07:25, Ella Ma via Phabricator <
reviews at reviews.llvm.org> escreveu:

> 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?


Yes, it's being used in the FindZ3.cmaks script.


>
> 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 issue here is that the z3 zip file does not include the cmake scripts,
that's why you're unable to configure it by only setting the Z3 directory.


> ---
>
> 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
>
>

-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20201015/6b5117f8/attachment.html>