diff options
| -rwxr-xr-x | .travis/klee.sh | 9 | ||||
| -rw-r--r-- | CMakeLists.txt | 101 | ||||
| -rw-r--r-- | README-CMake.md | 2 | ||||
| -rw-r--r-- | cmake/find_metasmt.cmake | 127 | ||||
| -rw-r--r-- | cmake/find_stp.cmake | 57 | ||||
| -rw-r--r-- | cmake/find_z3.cmake | 51 |
6 files changed, 213 insertions, 134 deletions
diff --git a/.travis/klee.sh b/.travis/klee.sh index 19b9e47f..119fbb47 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -51,13 +51,13 @@ fi ############################################################################### # Handle setting up solver configure flags for KLEE ############################################################################### -KLEE_Z3_CONFIGURE_OPTION="" -KLEE_STP_CONFIGURE_OPTION="" -KLEE_METASMT_CONFIGURE_OPTION="" SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') if [ "X${USE_CMAKE}" == "X1" ]; then # Set CMake configure options + KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=OFF" + KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=OFF" + KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=OFF" for solver in ${SOLVER_LIST}; do echo "Setting CMake configuration option for ${solver}" case ${solver} in @@ -82,6 +82,9 @@ if [ "X${USE_CMAKE}" == "X1" ]; then done TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE") else + KLEE_Z3_CONFIGURE_OPTION="" + KLEE_STP_CONFIGURE_OPTION="" + KLEE_METASMT_CONFIGURE_OPTION="" for solver in ${SOLVER_LIST}; do echo "Setting configuration option for ${solver}" case ${solver} in diff --git a/CMakeLists.txt b/CMakeLists.txt index e066b89e..2f162f21 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -307,83 +307,12 @@ include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake) ################################################################################ # Solvers ################################################################################ - -# STP: Use CMake facility to detect. The user can pass `-DSTP_DIR=` to force -# a particular directory. -option(ENABLE_SOLVER_STP "Enable STP solver support" OFF) -if (ENABLE_SOLVER_STP) - message(STATUS "STP solver support enabled") - # Although find_package() will set `STP_DIR` for us add it here so that - # is displayed in `ccmake` and `cmake-gui`. - set(STP_DIR "" CACHE PATH "Path to directory containing STPConfig.cmake") - find_package(STP CONFIG) - if (STP_FOUND) - message(STATUS "Found STP version ${STP_VERSION}") - # Try the STP shared library first - if ("${STP_SHARED_LIBRARY}" STREQUAL "") - # Try the static library instead - if ("${STP_STATIC_LIBRARY}" STREQUAL "") - message(FATAL_ERROR "Couldn't find STP shared or static library") - endif() - message(STATUS "Using STP static library") - list(APPEND KLEE_SOLVER_LIBRARIES "${STP_STATIC_LIBRARY}") - else() - message(STATUS "Using STP shared library") - list(APPEND KLEE_SOLVER_LIBRARIES "${STP_SHARED_LIBRARY}") - endif() - list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS "${STP_INCLUDE_DIRS}") - message(STATUS "STP_DIR: ${STP_DIR}") - set(ENABLE_STP 1) # For config.h - else() - message(FATAL_ERROR "STP not found. Try setting `-DSTP_DIR=/path` where" - " `/path` is the directory containing `STPConfig.cmake`") - endif() -else() - message(STATUS "STP solver support disabled") - set(ENABLE_STP 0) # For config.h -endif() - +# STP +include(${CMAKE_SOURCE_DIR}/cmake/find_stp.cmake) # Z3 -option(ENABLE_SOLVER_Z3 "Enable Z3 solver support" OFF) -if (ENABLE_SOLVER_Z3) - message(STATUS "Z3 solver support enabled") - find_package(Z3) - if (Z3_FOUND) - message(STATUS "Found Z3") - set(ENABLE_Z3 1) # For config.h - list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${Z3_INCLUDE_DIRS}) - list(APPEND KLEE_SOLVER_LIBRARIES ${Z3_LIBRARIES}) - - # Check the signature of `Z3_get_error_msg()` - set (_old_CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES}") - set(CMAKE_REQUIRED_LIBRARIES ${CMAKE_REQUIRED_LIBRARIES} ${Z3_LIBRARIES}) - check_prototype_definition(Z3_get_error_msg - "Z3_string Z3_get_error_msg(Z3_context c, Z3_error_code err)" - "NULL" "${Z3_INCLUDE_DIRS}/z3.h" HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT) - set(CMAKE_REQUIRED_LIBRARIES ${_old_CMAKE_REQUIRED_LIBRARIES}) - if (HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT) - message(STATUS "Z3_get_error_msg requires context") - else() - message(STATUS "Z3_get_error_msg does not require context") - endif() - else() - message(FATAL_ERROR "Z3 not found.") - endif() -else() - message(STATUS "Z3 solver support disabled") - set(ENABLE_Z3 0) # For config.h -endif() - +include(${CMAKE_SOURCE_DIR}/cmake/find_z3.cmake) # metaSMT -option(ENABLE_SOLVER_METASMT "Enable metaSMT solver support" OFF) -if (ENABLE_SOLVER_METASMT) - message(STATUS "metaSMT solver support enabled") - set(ENABLE_METASMT 1) - include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake) -else() - message(STATUS "metaSMT solver support disabled") - set(ENABLE_METASMT 0) # For config.h -endif() +include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake) if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT})) message(FATAL_ERROR "No solver was specified. At least one solver is required." @@ -423,12 +352,24 @@ endif() # Support for compressed logs ################################################################################ find_package(ZLIB) -if (${ZLIB_FOUND}) - set(HAVE_ZLIB_H 1) # For config.h - set(TARGET_LIBS ${TARGET_LIBS} z) - list(APPEND KLEE_COMPONENT_EXTRA_LIBRARIES ${ZLIB_LIBRARIES}) - list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${ZLIB_INCLUDE_DIRS}) +if (ZLIB_FOUND) + set(ENABLE_ZLIB_DEFAULT ON) +else() + set(ENABLE_ZLIB_DEFAULT OFF) +endif() +option(ENABLE_ZLIB "Enable use of zlib" ${ENABLE_ZLIB_DEFAULT}) +if (ENABLE_ZLIB) + message(STATUS "Zlib support enabled") + if (ZLIB_FOUND) + set(HAVE_ZLIB_H 1) # For config.h + set(TARGET_LIBS ${TARGET_LIBS} z) + list(APPEND KLEE_COMPONENT_EXTRA_LIBRARIES ${ZLIB_LIBRARIES}) + list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${ZLIB_INCLUDE_DIRS}) + else() + message(FATAL_ERROR "ENABLE_ZLIB is true but zlib could not be found") + endif() else() + message(STATUS "Zlib support disabled") unset(HAVE_ZLIB_H) # For config.h endif() diff --git a/README-CMake.md b/README-CMake.md index 2d438546..daa1e90c 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -55,6 +55,8 @@ cmake -DCMAKE_BUILD_TYPE=Release /path/to/klee/src * `ENABLE_UNIT_TESTS` (BOOLEAN) - Enable KLEE unit tests. +* `ENABLE_ZLIB` (BOOLEAN) - Enable zlib support. + * `GTEST_SRC_DIR` (STRING) - Path to GTest source tree. * `KLEE_ENABLE_TIMESTAMP` (BOOLEAN) - Enable timestamps in KLEE sources. diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake index 6751b31d..39079e2b 100644 --- a/cmake/find_metasmt.cmake +++ b/cmake/find_metasmt.cmake @@ -6,58 +6,83 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# +find_package(metaSMT QUIET CONFIG) -find_package(metaSMT CONFIG) -if (NOT metaSMT_FOUND) - message(FATAL_ERROR "metaSMT not found. Try setting `-DmetaSMT_DIR=/path` where" - " `/path` is the directory containing `metaSMTConfig.cmake`") +# Set the default so that if the following is true: +# * METASMT was found +# * ENABLE_SOLVER_METASMT is not already set as a cache variable +# +# then the default is set to `ON`. Otherwise set the default to `OFF`. +# A consequence of this is if we fail to detect METASMT the first time +# subsequent calls to CMake will not change the default. +if (metaSMT_FOUND) + set(ENABLE_SOLVER_METASMT_DEFAULT ON) +else() + set(ENABLE_SOLVER_METASMT_DEFAULT OFF) endif() -message(STATUS "metaSMT_DIR: ${metaSMT_DIR}") -list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS - "${metaSMT_INCLUDE_DIR}" ${metaSMT_INCLUDE_DIRS}) -# FIXME: We should test linking -list(APPEND KLEE_SOLVER_LIBRARIES ${metaSMT_LIBRARIES}) - -# Separate flags and defines from ${metaSMT_CXXFLAGS} -string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_list) -set(_metasmt_flags "") -set(_metasmt_defines "") -foreach (flag ${_metaSMT_CXXFLAGS_list}) - if ("${flag}" MATCHES "^-D") - # This is a define - list(APPEND _metasmt_defines "${flag}") - else() - # Regular flag - list(APPEND _metasmt_flags "${flag}") +option(ENABLE_SOLVER_METASMT + "Enable metaSMT solver support" + ${ENABLE_SOLVER_METASMT_DEFAULT} +) + +if (ENABLE_SOLVER_METASMT) + message(STATUS "metaSMT solver support enabled") + set(ENABLE_METASMT 1) # For config.h + + if (NOT metaSMT_FOUND) + message(FATAL_ERROR "metaSMT not found. Try setting `-DmetaSMT_DIR=/path` where" + " `/path` is the directory containing `metaSMTConfig.cmake`") endif() -endforeach() - -message(STATUS "metaSMT defines: ${_metasmt_defines}") -list(APPEND KLEE_COMPONENT_CXX_DEFINES ${_metasmt_defines}) - -message(STATUS "metaSMT flags: ${_metasmt_flags}") -foreach (f ${_metasmt_flags}) - # Test the flag and fail if it can't be used - klee_component_add_cxx_flag(${f} REQUIRED) -endforeach() - -set(available_metasmt_backends "BTOR" "STP" "Z3") -set(METASMT_DEFAULT_BACKEND "STP" - CACHE - STRING - "Default metaSMT backend. Availabe options ${available_metasmt_backends}") -# Provide drop down menu options in cmake-gui -set_property(CACHE METASMT_DEFAULT_BACKEND - PROPERTY STRINGS ${available_metasmt_backends}) - -# Check METASMT_DEFAULT_BACKEND has a valid value. -list(FIND available_metasmt_backends "${METASMT_DEFAULT_BACKEND}" _meta_smt_backend_index) -if ("${_meta_smt_backend_index}" EQUAL "-1") - message(FATAL_ERROR - "Invalid metaSMT default backend (\"${METASMT_DEFAULT_BACKEND}\").\n" - "Valid values are ${available_metasmt_backends}") -endif() + message(STATUS "metaSMT_DIR: ${metaSMT_DIR}") + list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS + "${metaSMT_INCLUDE_DIR}" ${metaSMT_INCLUDE_DIRS}) + # FIXME: We should test linking + list(APPEND KLEE_SOLVER_LIBRARIES ${metaSMT_LIBRARIES}) + + # Separate flags and defines from ${metaSMT_CXXFLAGS} + string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_list) + set(_metasmt_flags "") + set(_metasmt_defines "") + foreach (flag ${_metaSMT_CXXFLAGS_list}) + if ("${flag}" MATCHES "^-D") + # This is a define + list(APPEND _metasmt_defines "${flag}") + else() + # Regular flag + list(APPEND _metasmt_flags "${flag}") + endif() + endforeach() + + message(STATUS "metaSMT defines: ${_metasmt_defines}") + list(APPEND KLEE_COMPONENT_CXX_DEFINES ${_metasmt_defines}) -# Set appropriate define -list(APPEND KLEE_COMPONENT_CXX_DEFINES - -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND}) + message(STATUS "metaSMT flags: ${_metasmt_flags}") + foreach (f ${_metasmt_flags}) + # Test the flag and fail if it can't be used + klee_component_add_cxx_flag(${f} REQUIRED) + endforeach() + + set(available_metasmt_backends "BTOR" "STP" "Z3") + set(METASMT_DEFAULT_BACKEND "STP" + CACHE + STRING + "Default metaSMT backend. Availabe options ${available_metasmt_backends}") + # Provide drop down menu options in cmake-gui + set_property(CACHE METASMT_DEFAULT_BACKEND + PROPERTY STRINGS ${available_metasmt_backends}) + + # Check METASMT_DEFAULT_BACKEND has a valid value. + list(FIND available_metasmt_backends "${METASMT_DEFAULT_BACKEND}" _meta_smt_backend_index) + if ("${_meta_smt_backend_index}" EQUAL "-1") + message(FATAL_ERROR + "Invalid metaSMT default backend (\"${METASMT_DEFAULT_BACKEND}\").\n" + "Valid values are ${available_metasmt_backends}") + endif() + + # Set appropriate define + list(APPEND KLEE_COMPONENT_CXX_DEFINES + -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND}) +else() + message(STATUS "metaSMT solver support disabled") + set(ENABLE_METASMT 0) # For config.h +endif() diff --git a/cmake/find_stp.cmake b/cmake/find_stp.cmake new file mode 100644 index 00000000..7b10f1fe --- /dev/null +++ b/cmake/find_stp.cmake @@ -0,0 +1,57 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# STP: Use CMake facility to detect. The user can pass `-DSTP_DIR=` to force +# a particular directory. + +# Although find_package() will set `STP_DIR` for us add it here so that +# is displayed in `ccmake` and `cmake-gui`. +set(STP_DIR "" CACHE PATH "Path to directory containing STPConfig.cmake") +find_package(STP CONFIG) + +# Set the default so that if the following is true: +# * STP was found +# * ENABLE_SOLVER_STP is not already set as a cache variable +# +# then the default is set to `ON`. Otherwise set the default to `OFF`. +# A consequence of this is if we fail to detect STP the first time +# subsequent calls to CMake will not change the default. +if (STP_FOUND) + set(ENABLE_SOLVER_STP_DEFAULT ON) +else() + set(ENABLE_SOLVER_STP_DEFAULT OFF) +endif() +option(ENABLE_SOLVER_STP "Enable STP solver support" ${ENABLE_SOLVER_STP_DEFAULT}) + +if (ENABLE_SOLVER_STP) + message(STATUS "STP solver support enabled") + if (STP_FOUND) + message(STATUS "Found STP version ${STP_VERSION}") + # Try the STP shared library first + if ("${STP_SHARED_LIBRARY}" STREQUAL "") + # Try the static library instead + if ("${STP_STATIC_LIBRARY}" STREQUAL "") + message(FATAL_ERROR "Couldn't find STP shared or static library") + endif() + message(STATUS "Using STP static library") + list(APPEND KLEE_SOLVER_LIBRARIES "${STP_STATIC_LIBRARY}") + else() + message(STATUS "Using STP shared library") + list(APPEND KLEE_SOLVER_LIBRARIES "${STP_SHARED_LIBRARY}") + endif() + list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS "${STP_INCLUDE_DIRS}") + message(STATUS "STP_DIR: ${STP_DIR}") + set(ENABLE_STP 1) # For config.h + else() + message(FATAL_ERROR "STP not found. Try setting `-DSTP_DIR=/path` where" + " `/path` is the directory containing `STPConfig.cmake`") + endif() +else() + message(STATUS "STP solver support disabled") + set(ENABLE_STP 0) # For config.h +endif() diff --git a/cmake/find_z3.cmake b/cmake/find_z3.cmake new file mode 100644 index 00000000..60e27c26 --- /dev/null +++ b/cmake/find_z3.cmake @@ -0,0 +1,51 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +find_package(Z3) +# Set the default so that if the following is true: +# * Z3 was found +# * ENABLE_SOLVER_Z3 is not already set as a cache variable +# +# then the default is set to `ON`. Otherwise set the default to `OFF`. +# A consequence of this is if we fail to detect Z3 the first time +# subsequent calls to CMake will not change the default. +if (Z3_FOUND) + set(ENABLE_SOLVER_Z3_DEFAULT ON) +else() + set(ENABLE_SOLVER_Z3_DEFAULT OFF) +endif() +option(ENABLE_SOLVER_Z3 "Enable Z3 solver support" ${ENABLE_SOLVER_Z3_DEFAULT}) + +if (ENABLE_SOLVER_Z3) + message(STATUS "Z3 solver support enabled") + if (Z3_FOUND) + message(STATUS "Found Z3") + set(ENABLE_Z3 1) # For config.h + list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${Z3_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_LIBRARIES ${Z3_LIBRARIES}) + + # Check the signature of `Z3_get_error_msg()` + set (_old_CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES}") + set(CMAKE_REQUIRED_LIBRARIES ${CMAKE_REQUIRED_LIBRARIES} ${Z3_LIBRARIES}) + check_prototype_definition(Z3_get_error_msg + "Z3_string Z3_get_error_msg(Z3_context c, Z3_error_code err)" + "NULL" "${Z3_INCLUDE_DIRS}/z3.h" HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT) + set(CMAKE_REQUIRED_LIBRARIES ${_old_CMAKE_REQUIRED_LIBRARIES}) + if (HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT) + message(STATUS "Z3_get_error_msg requires context") + else() + message(STATUS "Z3_get_error_msg does not require context") + endif() + else() + message(FATAL_ERROR "Z3 not found.") + endif() +else() + message(STATUS "Z3 solver support disabled") + set(ENABLE_Z3 0) # For config.h +endif() |