llvm/cmake/modules/FindZ3.cmake

   1 INCLUDE(CheckCXXSourceRuns)
   2
   3 # Function to check Z3's version
   4 function(check_z3_version z3_include z3_lib)
   5   # Get lib path
   6   set(z3_link_libs "${z3_lib}")
   7
   8   # Try to find a threading module in case Z3 was built with threading support.
   9   # Threads are required elsewhere in LLVM, but not marked as required here because
  10   # Z3 could have been compiled without threading support.
  11   find_package(Threads)
  12   # CMAKE_THREAD_LIBS_INIT may be empty if the thread functions are provided by the
  13   # system libraries and no special flags are needed.
  14   if(CMAKE_THREAD_LIBS_INIT)
  15     list(APPEND z3_link_libs "${CMAKE_THREAD_LIBS_INIT}")
  16   endif()
  17
  18   # The program that will be executed to print Z3's version.
  19   file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
  20        "#include <assert.h>
  21         #include <stdio.h>
  22         #include <z3.h>
  23         int main(void) {
  24           unsigned int major, minor, build, rev;
  25           Z3_get_version(&major, &minor, &build, &rev);
  26           printf(\"%u.%u.%u\", major, minor, build);
  27           return 0;
  28        }")
  29
  30   try_run(
  31     Z3_RETURNCODE
  32     Z3_COMPILED
  33     ${CMAKE_BINARY_DIR}
  34     ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
  35     COMPILE_DEFINITIONS -I"${z3_include}"
  36     LINK_LIBRARIES ${z3_link_libs}
  37     COMPILE_OUTPUT_VARIABLE COMPILE_OUTPUT
  38     RUN_OUTPUT_VARIABLE SRC_OUTPUT
  39   )
  40
  41   if(Z3_COMPILED)
  42     string(REGEX REPLACE "([0-9]+\\.[0-9]+\\.[0-9]+)" "\\1"
  43            z3_version "${SRC_OUTPUT}")
  44     set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
  45   else()
  46     message(NOTICE "${COMPILE_OUTPUT}")
  47     message(WARNING "Failed to compile Z3 program that is used to determine library version.")
  48   endif()
  49 endfunction(check_z3_version)
  50
  51 # Looking for Z3 in LLVM_Z3_INSTALL_DIR
  52 find_path(Z3_INCLUDE_DIR NAMES z3.h
  53   NO_DEFAULT_PATH
  54   PATHS ${LLVM_Z3_INSTALL_DIR}/include
  55   PATH_SUFFIXES libz3 z3
  56   )
  57
  58 find_library(Z3_LIBRARIES NAMES z3 libz3
  59   NO_DEFAULT_PATH
  60   PATHS ${LLVM_Z3_INSTALL_DIR}
  61   PATH_SUFFIXES lib bin
  62   )
  63
  64 # If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories
  65 find_path(Z3_INCLUDE_DIR NAMES z3.h
  66   PATH_SUFFIXES libz3 z3
  67   )
  68
  69 find_library(Z3_LIBRARIES NAMES z3 libz3
  70   PATH_SUFFIXES lib bin
  71   )
  72
  73 # Searching for the version of the Z3 library is a best-effort task
  74 unset(Z3_VERSION_STRING)
  75
  76 # First, try to check it dynamically, by compiling a small program that
  77 # prints Z3's version
  78 if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND NOT CMAKE_CROSSCOMPILING)
  79   # We do not have the Z3 binary to query for a version. Try to use
  80   # a small C++ program to detect it via the Z3_get_version() API call.
  81   check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES})
  82 endif()
  83
  84 # If the dynamic check fails, we might be cross compiling: if that's the case,
  85 # check the version in the headers, otherwise, fail with a message
  86 if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
  87                               Z3_INCLUDE_DIR AND
  88                               EXISTS "${Z3_INCLUDE_DIR}/z3_version.h"))
  89   # TODO: print message warning that we couldn't find a compatible lib?
  90
  91   # Z3 4.8.1+ has the version is in a public header.
  92   file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
  93        z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*")
  94   string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]+).*$" "\\1"
  95          Z3_MAJOR "${z3_version_str}")
  96
  97   file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
  98        z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*")
  99   string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]+).*$" "\\1"
 100          Z3_MINOR "${z3_version_str}")
 101
 102   file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
 103        z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*")
 104   string(REGEX REPLACE "^.*Z3_BUILD_NUMBER[\t ]+([0-9]+).*$" "\\1"
 105          Z3_BUILD "${z3_version_str}")
 106
 107   set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD})
 108   unset(z3_version_str)
 109 endif()
 110
 111 if(NOT Z3_VERSION_STRING)
 112   # Give up: we are unable to obtain a version of the Z3 library. Be
 113   # conservative and force the found version to 0.0.0 to make version
 114   # checks always fail.
 115   set(Z3_VERSION_STRING "0.0.0")
 116   message(WARNING "Failed to determine Z3 library version, defaulting to 0.0.0.")
 117 endif()
 118
 119 # handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
 120 # all listed variables are TRUE
 121 include(FindPackageHandleStandardArgs)
 122 FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
 123                                   REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
 124                                   VERSION_VAR Z3_VERSION_STRING)
 125
 126 mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)