diff options
Diffstat (limited to 'cmake/find_metasmt.cmake')
| -rw-r--r-- | cmake/find_metasmt.cmake | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake new file mode 100644 index 00000000..a0a02cb9 --- /dev/null +++ b/cmake/find_metasmt.cmake @@ -0,0 +1,92 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +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`") +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}) + +# THIS IS HORRIBLE. The ${metaSMT_CXXFLAGS} variable +# is badly formed. It is a string but we can't just split +# on spaces because its contents looks like this +# " -DmetaSMT_BOOLECTOR_1_API -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS". +# So handle defines specially +string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_broken_list) +list(LENGTH _metaSMT_CXXFLAGS_broken_list _metaSMT_CXXFLAGS_broken_list_length) +math(EXPR _metaSMT_CXXFLAGS_broken_list_last_index "${_metaSMT_CXXFLAGS_broken_list_length} -1") +set(_metasmt_flags "") +set(_metasmt_defines "") +set(_index_to_skip "") +foreach (index RANGE 0 ${_metaSMT_CXXFLAGS_broken_list_last_index}) + list(FIND _index_to_skip "${index}" _should_skip) + if ("${_should_skip}" EQUAL "-1") + list(GET _metaSMT_CXXFLAGS_broken_list ${index} _current_flag) + if ("${_current_flag}" MATCHES "^-D") + # This is a define + if ("${_current_flag}" MATCHES "^-D$") + # This is a bad define. We have just `-D` and the next item + # is the actually definition. + if ("${index}" EQUAL "${_metaSMT_CXXFLAGS_broken_list_last_index}") + message(FATAL_ERROR "Stray -D flag!") + else() + # Get next value + math(EXPR _next_index "${index} + 1") + list(GET _metaSMT_CXXFLAGS_broken_list ${_next_index} _next_flag) + if ("${_next_flag}" STREQUAL "") + message(FATAL_ERROR "Next flag shouldn't be empty!") + endif() + list(APPEND _metasmt_defines "-D${_next_flag}") + list(APPEND _index_to_skip "${_next_index}") + endif() + else() + # This is well formed defined (e.g. `-DHELLO`) + list(APPEND _metasmt_defines "${_current_flag}") + endif() + else() + # Regular flag + list(APPEND _metasmt_flags "${_current_flag}") + endif() + 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() + +# Set appropriate define +list(APPEND KLEE_COMPONENT_CXX_DEFINES + -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND}) |