[llvm] f1ab60e - Fix FindZ3.cmake to support static libraries and Windows
Balazs Benics via llvm-commits
llvm-commits at lists.llvm.org
Thu Jul 29 01:57:00 PDT 2021
Author: Tomasz KamiĆski
Date: 2021-07-29T10:55:44+02:00
New Revision: f1ab60e40d16970381a003e145be6d5932823597
URL: https://github.com/llvm/llvm-project/commit/f1ab60e40d16970381a003e145be6d5932823597
DIFF: https://github.com/llvm/llvm-project/commit/f1ab60e40d16970381a003e145be6d5932823597.diff
LOG: 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
Added:
Modified:
llvm/cmake/modules/FindZ3.cmake
Removed:
################################################################################
diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake
index 95dd37789a876..118b1eac3b322 100644
--- 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
More information about the llvm-commits
mailing list