Fix FindZ3.cmake to support static libraries and Windows

[tomasz-kaminski-sonarsource]

Summary

Use absolute path to link z3 to allow builds both on windows and linux since the library name is platform dependent for Z3 (libz3 on Windows and z3 on Linux) and MSVC does not recognized -L and -l options.
Fix CMAKE_CROSSCOMPILING that does not work correctly since it uses Z3_BUILD_VERSION instead of Z3_BUILD_NUMBER
Fix building with the static version of z3 library (supersedes D80227).

• 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

Exposed compilation error from building a program that is used to detect z3 version in the warning message, to simplify troubleshooting.

[tomasz-kaminski-sonarsource]

Removed uncessary debug message.

[tomasz-kaminski-sonarsource]

Any input on the change?

[vsavchenko]

It looks reasonable to me, but I can't say that I'm an expert here, and I'm definitely not a frequent z3 user.

[steakhal]

I'm also not really comfortable with CMake, thus I'm requesting review from others who might have more experience on CMake/Windows stuff.
Don't mind me if I missed someone :D
On my side, this patch works on Linux x86_64 though, it did not break anything.

llvm/cmake/modules/FindZ3.cmake

17

Do you need to change it to cpp?

43–44

Ah, nice to see such an addition.

101–102

Oh, so it never matched. What is the purpose of this in that case?
If we did not recognize this sooner, I mean...

[tomasz-kaminski-sonarsource]

llvm/cmake/modules/FindZ3.cmake

17

Yes, for static version of z3, it's need to be linked with C++ runtime. Changing extension is the easiest way to signal cmake that this is meant to be C++ code.

101–102

If major.minor is greater than required (e.g. 4.8) the test passes despite ending up with "#define Z3_BUILD_NUMBER 11" as patch number, so once Z3 got minor updated, this does not cause issues.

[JDevlieghere]

Not an expert on Z3 either, but the CMake logic looks sound to me. LGTM.

llvm/cmake/modules/FindZ3.cmake

12

I was curious why you're checking CMAKE_THREAD_LIBS_INIT instead of Threads_FOUND . Maybe include a comment saying that CMAKE_THREAD_LIBS_INIT may be empty if the thread functions are provided by the system libraries and no special flags are needed.

[tomasz-kaminski-sonarsource]

Included sugguested comment regarding CMAKE_THREAD_LIBS_INIT.

[tomasz-kaminski-sonarsource]

Could you be possible to merge it for me, as I do not have a commit rights?
For the author information use:
Tomasz Kamiński
[e-mail]

llvm/cmake/modules/FindZ3.cmake

 INCLUDE(CheckCXXSourceRuns)
 
 # Function to check Z3's version
 function(check_z3_version z3_include z3_lib)
+  # Get lib path
+  set(z3_link_libs "${z3_lib}")
+
+  # 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.c
+  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;
        }")
 
-  # Get lib path
-  get_filename_component(z3_lib_path ${z3_lib} PATH)
-
   try_run(
     Z3_RETURNCODE
     Z3_COMPILED
     ${CMAKE_BINARY_DIR}
-    ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
+    ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
     COMPILE_DEFINITIONS -I"${z3_include}"
-    LINK_LIBRARIES -L${z3_lib_path} -lz3
+    LINK_LIBRARIES ${z3_link_libs}
+    COMPILE_OUTPUT_VARIABLE COMPILE_OUTPUT
     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)
+  else()
+    message(NOTICE "${COMPILE_OUTPUT}")
+    message(WARNING "Failed to compile Z3 program that is used to determine library version.")
   endif()
 endfunction(check_z3_version)
 
 # Looking for Z3 in LLVM_Z3_INSTALL_DIR
 find_path(Z3_INCLUDE_DIR NAMES z3.h
   NO_DEFAULT_PATH
   PATHS ${LLVM_Z3_INSTALL_DIR}/include
   PATH_SUFFIXES libz3 z3
if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
 
   file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
        z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*")
   string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]).*$" "\\1"
          Z3_MINOR "${z3_version_str}")
 
   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}")
 
   set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD})
   unset(z3_version_str)
 endif()
 
 if(NOT Z3_VERSION_STRING)
   # Give up: we are unable to obtain a version of the Z3 library. Be
   # conservative and force the found version to 0.0.0 to make version
   # checks always fail.
   set(Z3_VERSION_STRING "0.0.0")
+  message(WARNING "Failed to determine Z3 library version, defaulting to 0.0.0.")
 endif()
 
 # handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
 # all listed variables are TRUE
 include(FindPackageHandleStandardArgs)
 FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
                                   REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
                                   VERSION_VAR Z3_VERSION_STRING)
 
 mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)