Fix FindZ3.cmake to support static libraries and Windows

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.

Reviewed By: JDevlieghere

Differential Revision: https://reviews.llvm.org/D106131

diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake
index 95dd377..118b1ea 100644 (file)
--- a/llvm/cmake/modules/FindZ3.cmake
+++ b/llvm/cmake/modules/FindZ3.cmake
@@ -2,8 +2,21 @@ 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)
+  # CMAKE_THREAD_LIBS_INIT may be empty if the thread functions are provided by the 
+  # system libraries and no special flags are needed.
+  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() {
@@ -13,16 +26,14 @@ function(check_z3_version z3_include z3_lib)
           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
   )
 
@@ -30,6 +41,9 @@ function(check_z3_version z3_include z3_lib)
     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)
 
@@ -86,7 +100,7 @@ if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
 
   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})
@@ -98,6 +112,7 @@ if(NOT Z3_VERSION_STRING)
   # 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