diff options
Diffstat (limited to 'cmake')
| -rw-r--r-- | cmake/find_metasmt.cmake | 127 | ||||
| -rw-r--r-- | cmake/find_stp.cmake | 57 | ||||
| -rw-r--r-- | cmake/find_z3.cmake | 51 |
3 files changed, 184 insertions, 51 deletions
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() |