<div dir="ltr"><div>Hi,</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Em qui., 15 de out. de 2020 às 07:25, Ella Ma via Phabricator <<a href="mailto:reviews@reviews.llvm.org">reviews@reviews.llvm.org</a>> escreveu:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">OikawaKirie added a comment.<br>
<br>
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`.<br>
<br>
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.<br>
<br>
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.<br>
<br>
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.<br>
<br>
- When I run `cmake ../llvm`, the project is correctly configured with no error messages.<br>
- 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."<br>
- 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."<br>
- 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).<br>
<br>
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).<br>
<br>
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.<br>
<br>
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? </blockquote><div><br></div><div>Yes, it's being used in the FindZ3.cmaks script.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
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`.<br>
<br></blockquote><div><br></div><div>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.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
---<br>
<br>
The directories mentioned above:<br>
<br>
- LLVM source directory: `/tmp/ella.z3-patch/llvm-project`<br>
- LLVM build directory / CMake directory: `/tmp/ella.z3-patch/llvm-project/build`<br>
- Z3 source directory: `/tmp/ella.z3-patch/z3`<br>
- Z3 build directory: `/tmp/ella.z3-patch/z3/build`<br>
- Z3 make install directory: `/tmp/ella.z3-patch/z3-install`<br>
- Z3 pre-build install directory: `/tmp/ella.z3-patch/z3-4.8.9/z3-4.8.9-x64-ubuntu-16.04`<br>
<br>
The settings for variable `LLVM_Z3_INSTALL_DIR` that can correctly configure Z3 with the patch:<br>
<br>
- Z3 build directory: `/tmp/ella.z3-patch/z3/build`<br>
- Z3 make install CMake directory: `/tmp/ella.z3-patch/z3-install/usr/local/lib/cmake`<br>
- Z3 make install CMake Z3 directory: `/tmp/ella.z3-patch/z3-install/usr/local/lib/cmake/z3`<br>
<br>
Versions: Ubuntu 20.04, CMake 3.16.3, Z3 commit 2841796<br>
<br>
<br>
Repository:<br>
  rG LLVM Github Monorepo<br>
<br>
CHANGES SINCE LAST ACTION<br>
  <a href="https://reviews.llvm.org/D88198/new/" rel="noreferrer" target="_blank">https://reviews.llvm.org/D88198/new/</a><br>
<br>
<a href="https://reviews.llvm.org/D88198" rel="noreferrer" target="_blank">https://reviews.llvm.org/D88198</a><br>
<br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div></div>