Hints CMake where to find Z3 with LLVM_Z3_INSTALL_DIR.

[OikawaKirie]

Summary

It seems that the variable LLVM_Z3_INSTALL_DIR was only used to print the error messages when Z3 is not found. In this patch, this variable is now actually used to hint CMake where to find Z3Config.cake.

[OikawaKirie]

@mikhail.ramalho ping

[mikhail.ramalho]

Hi, sorry for the delay.

I'm having trouble getting it to work on my system, I keep getting:

$ cmake ../llvm/ -GNinja
-- Could NOT find Z3 (missing: Z3_DIR)
CMake Error at CMakeLists.txt:377 (message):
  Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: /home/mgadelha/z3.


-- Configuring incomplete, errors occurred!
See also "/home/mgadelha/llvm-project/build/CMakeFiles/CMakeOutput.log".
See also "/home/mgadelha/llvm-project/build/CMakeFiles/CMakeError.log".

Could you please double-check the patch? I'm using Ubuntu 20.04, CMake 3.16.3, Z3 4.8.9.

I can compile clang+Z3 just fine without your patch.

[OikawaKirie]

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

[mikhail.ramalho]

Hi,

Em qui., 15 de out. de 2020 às 07:25, Ella Ma via Phabricator <
[e-mail]> 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

[OikawaKirie]

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

I think I probably have been misled by the configuration method I previously used. In addition, the output notice of "Found Z3: /path/to/libz3.so (xxx)" makes me think I need to set the variable LLVM_Z3_INSTALL_DIR to the path of libz3.so rather than the path of both libraries and the headers. Especially when I set the variable to the path of libz3.so of a higher version but CMake reports that the lower version of Z3 found from the system directory cannot be used, I will become confused about whether the variable is correctly set and used to find Z3.

Maybe it could be better if the variable is documented in llvm/docs/CMake.rst after the variable LLVM_ENABLE_Z3_SOLVER. Do think the documentation is needed?

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.

You are correct. In the file llvm/cmake/modules/FindZ3.cmake, only file z3.h and libz3.{so|a} are used, but the directories I tested without the patch has none of these files included. Besides, when I set LLVM_Z3_INSTALL_DIR to /tmp/ella.z3-patch/z3-4.8.9/z3-4.8.9-x64-ubuntu-16.04 directly, which is the directory where the Z3 zip file is unzipped to, the project can also be correctly configured without the patch. There is no problem with the official pre-build Z3 solver binaries and the original LLVM code. It is the problem of the patch. I misled myself.

Thank you for the comments. I will abandon this revision. And if you think the document for the variable LLVM_Z3_INSTALL_DIR is required, I will add create another review for the document.

llvm/CMakeLists.txt

 set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.")
 
 option(LLVM_ENABLE_Z3_SOLVER
   "Enable Support for the Z3 constraint solver in LLVM."
   ${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
 )
 
 if (LLVM_ENABLE_Z3_SOLVER)
-  find_package(Z3 4.7.1)
-  
   if (LLVM_Z3_INSTALL_DIR)
+    find_package(Z3 4.7.1 HINTS ${LLVM_Z3_INSTALL_DIR})
     if (NOT Z3_FOUND)
       message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
     endif()
-  endif()
-  
+  else()
+    find_package(Z3 4.7.1)
     if (NOT Z3_FOUND)
       message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
     endif()
+  endif()
 
   set(LLVM_WITH_Z3 1)
+  message(STATUS "Found Z3 ${Z3_VERSION_STRING} in ${Z3_DIR}")
 endif()
 
 set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
 
 
 if( LLVM_TARGETS_TO_BUILD STREQUAL "all" )
   set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} )
 endif()