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