[PATCH] D80227: Fix FindZ3.cmake to work with static Z3 libraries

[Artem Dinaburg via Phabricator via llvm-commits]

ArtemDinaburg created this revision.
ArtemDinaburg added reviewers: george.karpenkov, ddcc.
ArtemDinaburg added a project: clang.
Herald added subscribers: llvm-commits, mikhail.ramalho, mgorny.
Herald added a project: LLVM.

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


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D80227

Files:
  llvm/cmake/modules/FindZ3.cmake


Index: llvm/cmake/modules/FindZ3.cmake
===================================================================
--- llvm/cmake/modules/FindZ3.cmake
+++ llvm/cmake/modules/FindZ3.cmake
@@ -3,7 +3,7 @@
 # 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
+  file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
        "#include <assert.h>
         #include <z3.h>
         int main() {
@@ -16,13 +16,19 @@
   # Get lib path
   get_filename_component(z3_lib_path ${z3_lib} PATH)
 
+  # 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)
+  set(z3_link_libs "-lz3" "${CMAKE_THREAD_LIBS_INIT}")
+
   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 -L${z3_lib_path} ${z3_link_libs}
     RUN_OUTPUT_VARIABLE SRC_OUTPUT
   )
 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D80227.264982.patch
Type: text/x-patch
Size: 1360 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200519/6087a373/attachment.bin>