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

[Tomasz Kamiński via Phabricator via llvm-commits]

tomasz-kaminski-sonarsource added a comment.

In my case, the issue with `file(WRITE` race occurs only if the `find_package(THREAD)` is invoked afterwards. Rearanging the function as follows eliminates the issue for me:

  function(check_z3_version z3_include z3_lib)
    # 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()
  
    # The program that will be executed to print Z3's version.
    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;
         }")
  
    try_run(
      Z3_RETURNCODE
      Z3_COMPILED
      ${CMAKE_BINARY_DIR}
      ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
      COMPILE_DEFINITIONS -I"${z3_include}"
      LINK_LIBRARIES -L${z3_lib_path} ${z3_link_libs}
      COMPILE_OUTPUT_VARIABLE VAR_OUT
      RUN_OUTPUT_VARIABLE SRC_OUTPUT
    )
  
    message("Compiled ${VAR_OUT}")
  
    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)
    endif()
  endfunction(check_z3_version)


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

https://reviews.llvm.org/D80227