127 lines · plain
1INCLUDE(CheckCXXSourceRuns)2 3# Function to check Z3's version4function(check_z3_version z3_include z3_lib)5 # Get lib path6 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 because10 # 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.cpp20 "#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_RETURNCODE32 Z3_COMPILED33 ${CMAKE_BINARY_DIR}34 ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp35 COMPILE_DEFINITIONS -I"${z3_include}"36 LINK_LIBRARIES ${z3_link_libs}37 COMPILE_OUTPUT_VARIABLE COMPILE_OUTPUT38 RUN_OUTPUT_VARIABLE SRC_OUTPUT39 )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()49endfunction(check_z3_version)50 51# Looking for Z3 in LLVM_Z3_INSTALL_DIR52find_path(Z3_INCLUDE_DIR NAMES z3.h53 NO_DEFAULT_PATH54 PATHS ${LLVM_Z3_INSTALL_DIR}/include55 PATH_SUFFIXES libz3 z356 )57 58find_library(Z3_LIBRARIES NAMES z3 libz359 NO_DEFAULT_PATH60 PATHS ${LLVM_Z3_INSTALL_DIR}61 PATH_SUFFIXES lib bin62 )63 64# If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories65find_path(Z3_INCLUDE_DIR NAMES z3.h66 PATH_SUFFIXES libz3 z367 )68 69find_library(Z3_LIBRARIES NAMES z3 libz370 PATH_SUFFIXES lib bin71 )72 73# Searching for the version of the Z3 library is a best-effort task74unset(Z3_VERSION_STRING)75 76# First, try to check it dynamically, by compiling a small program that77# prints Z3's version78if(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 use80 # a small C++ program to detect it via the Z3_get_version() API call.81 check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES})82endif()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 message86if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND87 Z3_INCLUDE_DIR AND88 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)109endif()110 111if(NOT Z3_VERSION_STRING)112 # Give up: we are unable to obtain a version of the Z3 library. Be113 # conservative and force the found version to 0.0.0 to make version114 # 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.")117endif()118 119# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if120# all listed variables are TRUE121include(FindPackageHandleStandardArgs)122FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3123 REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR124 VERSION_VAR Z3_VERSION_STRING)125 126mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)127