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