Fix FindZ3.cmake to work with static Z3 libraries

[ArtemDinaburg]

Summary

The current FindZ3.cmake does not properly detect Z3 when it is built as a static library. This patch allows a Z3 static library to be used with LLVM.

The changes are:

• Build the Z3 version detection code as C++, since the static library brings in libstdc++ symbols
• Detect threading support and link against threading, in the (likely) case Z3 was built with threads

[ArtemDinaburg]

I've actually just run into another issue, triggered only in Docker-based builds, where the source generated from file(WRITE ...) that is used to emit the Z3 version is not visible to the try_run command.

I think that file_write is not the proper way to specify a static source file at configuration time in CMake. I am not sure of the best place to put such a file... llvm/cmake/extras perhaps?

[ArtemDinaburg]

Verified that having a pre-made testz3.cpp fixes my issue. Thinking about it more, there is no explicit dependency between file(WRITE ... and try_compile, so the two actions can happen in parallel. It just so happened that my particular build setup repeatedly hit this issue with try_compile failing before the write could occur.

Will try for an updated patch later tonight.

[ddcc]

I'm not too familiar with this part of CMake, but this mechanism is how CMake themselves implement C++ compilation and testing: https://github.com/Kitware/CMake/blob/master/Modules/CheckCXXSourceRuns.cmake . In fact, this code does include CheckCXXSourceRuns, but seems to reimplement most of the internals. Perhaps @esteffin would know more?

[ArtemDinaburg]

From a quick glance it looks like CheckCXXSourceRuns doesn't provide a documented way to store output of the command, and the output is what LLVM's build system is after. Interestingly CheckCXXSourceRuns also uses file(WRITE ... and then try_run, which makes me wonder if it has the same underlying issue, or if it is unaffected because it is in a macro.

[ArtemDinaburg]

Updated to use a pre-made file to fix a race between file(WRITE and try_compile

[ddcc]

I'm not entirely convinced that it's a race, but a separate file seems fine. Have you tested with e.g. LLVM_OPTIMIZED_TABLEGEN? It might be safer to use LLVM_MAIN_SRC_DIR instead of CMAKE_SOURCE_DIR.

Looks fine to me, but might be best to get someone else to take a look as well.

[ArtemDinaburg]

In D80227#2047567, @ddcc wrote:

I'm not entirely convinced that it's a race, but a separate file seems fine. Have you tested with e.g. LLVM_OPTIMIZED_TABLEGEN? It might be safer to use LLVM_MAIN_SRC_DIR instead of CMAKE_SOURCE_DIR.

Looks fine to me, but might be best to get someone else to take a look as well.

Hi Dominic,

I wasn't sure either; I asked on the CMake Developer forums and the answer was that a race was not possible. My issue was certainly real Maybe the write was failing for some unrelated reason.

[tomasz-kaminski-sonarsource]

In my case, the issue with file(WRITE race occurs only if the find_package(THREAD) is invoked afterwards. Rearanging the function as follows eliminates the issue for me:

function(check_z3_version z3_include z3_lib)
  # Get lib path
  get_filename_component(z3_lib_path ${z3_lib} PATH)
  set(z3_link_libs "-lz3")

  # Try to find a threading module in case Z3 was built with threading support.
  # Threads are required elsewhere in LLVM, but not marked as required here because
  # Z3 could have been compiled without threading support.
  find_package(Threads)
  if(CMAKE_THREAD_LIBS_INIT)
    list(APPEND z3_link_libs "${CMAKE_THREAD_LIBS_INIT}")
  endif()

  # The program that will be executed to print Z3's version.
  file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
       "#include <assert.h>
        #include <z3.h>
        int main() {
          unsigned int major, minor, build, rev;
          Z3_get_version(&major, &minor, &build, &rev);
          printf(\"%u.%u.%u\", major, minor, build);
          return 0;
       }")

  try_run(
    Z3_RETURNCODE
    Z3_COMPILED
    ${CMAKE_BINARY_DIR}
    ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
    COMPILE_DEFINITIONS -I"${z3_include}"
    LINK_LIBRARIES -L${z3_lib_path} ${z3_link_libs}
    COMPILE_OUTPUT_VARIABLE VAR_OUT
    RUN_OUTPUT_VARIABLE SRC_OUTPUT
  )

  message("Compiled ${VAR_OUT}")

  if(Z3_COMPILED)
    string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*)" "\\1"
           z3_version "${SRC_OUTPUT}")
    set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
  endif()
endfunction(check_z3_version)

[tomasz-kaminski-sonarsource]

Other (unrelated issue) in the file: The cross compilation version of section mode, refers to BUILD_VERSION instead of BUILD_NUMBER:

   file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
        z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*")
-       string(REGEX REPLACE "^.*Z3_BUILD_VERSION[\t ]+([0-9]).*$" "\\1"
+       string(REGEX REPLACE "^.*Z3_BUILD_NUMBER[\t ]+([0-9]).*$" "\\1"
         Z3_BUILD "${z3_version_str}")

llvm/cmake/extras/testz3.cpp

+#include <assert.h>
+#include <z3.h>
+int main() {
+  unsigned int major, minor, build, rev;
+  Z3_get_version(&major, &minor, &build, &rev);
+  printf("%u.%u.%u", major, minor, build);
+  return 0;
+}

llvm/cmake/modules/FindZ3.cmake

 INCLUDE(CheckCXXSourceRuns)
 
 # Function to check Z3's version
 function(check_z3_version z3_include z3_lib)
-  # The program that will be executed to print Z3's version.
-  file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
-       "#include <assert.h>
-        #include <z3.h>
-        int main() {
-          unsigned int major, minor, build, rev;
-          Z3_get_version(&major, &minor, &build, &rev);
-          printf(\"%u.%u.%u\", major, minor, build);
-          return 0;
-       }")
-
   # Get lib path
   get_filename_component(z3_lib_path ${z3_lib} PATH)
+  set(z3_link_libs "-lz3")
+
+  # Try to find a threading module in case Z3 was built with threading support.
+  # Threads are required elsewhere in LLVM, but not marked as required here because
+  # Z3 could have been compiled without threading support.
+  find_package(Threads)
+  if(CMAKE_THREAD_LIBS_INIT)
+    list(APPEND z3_link_libs "${CMAKE_THREAD_LIBS_INIT}")
+  endif()
 
   try_run(
     Z3_RETURNCODE
     Z3_COMPILED
     ${CMAKE_BINARY_DIR}
-    ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
+    ${CMAKE_SOURCE_DIR}/cmake/extras/testz3.cpp
     COMPILE_DEFINITIONS -I"${z3_include}"
-    LINK_LIBRARIES -L${z3_lib_path} -lz3
+    LINK_LIBRARIES -L${z3_lib_path} ${z3_link_libs}
     RUN_OUTPUT_VARIABLE SRC_OUTPUT
   )
 
   if(Z3_COMPILED)
     string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*)" "\\1"
            z3_version "${SRC_OUTPUT}")
     set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
   endif()