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

[Artem Dinaburg via Phabricator via llvm-commits]

ArtemDinaburg updated this revision to Diff 265143.
ArtemDinaburg added a comment.

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


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D80227/new/

https://reviews.llvm.org/D80227

Files:
  llvm/cmake/extras/testz3.cpp
  llvm/cmake/modules/FindZ3.cmake


Index: llvm/cmake/modules/FindZ3.cmake
===================================================================
--- llvm/cmake/modules/FindZ3.cmake
+++ llvm/cmake/modules/FindZ3.cmake
@@ -2,27 +2,25 @@
 
 # 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
   )
 
Index: llvm/cmake/extras/testz3.cpp
===================================================================
--- /dev/null
+++ llvm/cmake/extras/testz3.cpp
@@ -0,0 +1,8 @@
+#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;
+}


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D80227.265143.patch
Type: text/x-patch
Size: 1884 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200520/10f4f077/attachment.bin>