diff options
Diffstat (limited to 'cmake')
| -rw-r--r-- | cmake/add_global_flag.cmake | 55 | ||||
| -rw-r--r-- | cmake/c_flags_override.cmake | 24 | ||||
| -rw-r--r-- | cmake/compiler_warnings.cmake | 80 | ||||
| -rw-r--r-- | cmake/cxx_flags_override.cmake | 25 | ||||
| -rw-r--r-- | cmake/find_bitcode_compiler.cmake | 96 | ||||
| -rw-r--r-- | cmake/find_llvm.cmake | 166 | ||||
| -rw-r--r-- | cmake/find_metasmt.cmake | 92 | ||||
| -rw-r--r-- | cmake/klee_add_component.cmake | 25 | ||||
| -rw-r--r-- | cmake/klee_component_add_cxx_flag.cmake | 31 | ||||
| -rw-r--r-- | cmake/modules/FindZ3.cmake | 35 | ||||
| -rw-r--r-- | cmake/string_to_list.cmake | 13 |
11 files changed, 642 insertions, 0 deletions
diff --git a/cmake/add_global_flag.cmake b/cmake/add_global_flag.cmake new file mode 100644 index 00000000..893e1200 --- /dev/null +++ b/cmake/add_global_flag.cmake @@ -0,0 +1,55 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +include(CheckCXXCompilerFlag) +include(CheckCCompilerFlag) +include(CMakeParseArguments) + +function(add_global_cxx_flag flag) + CMAKE_PARSE_ARGUMENTS(add_global_cxx_flag "REQUIRED" "" "" ${ARGN}) + string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") + string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + unset(HAS_${SANITIZED_FLAG_NAME}) + CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}_CXX) + if (add_global_cxx_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}_CXX) + message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it") + endif() + if (HAS_${SANITIZED_FLAG_NAME}_CXX) + message(STATUS "C++ compiler supports ${flag}") + # NOTE: Have to be careful here as CMAKE_CXX_FLAGS is a string + # and not a list. + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}" PARENT_SCOPE) + else() + message(STATUS "C++ compiler does not support ${flag}") + endif() +endfunction() + +function(add_global_c_flag flag) + CMAKE_PARSE_ARGUMENTS(add_global_c_flag "REQUIRED" "" "" ${ARGN}) + string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") + string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + unset(HAS_${SANITIZED_FLAG_NAME}) + CHECK_C_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}_C) + if (add_global_c_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}_C) + message(FATAL_ERROR "The flag \"${flag}\" is required but your C compiler doesn't support it") + endif() + if (HAS_${SANITIZED_FLAG_NAME}_C) + message(STATUS "C compiler supports ${flag}") + # NOTE: Have to be careful here as CMAKE_C_FLAGS is a string + # and not a list. + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}" PARENT_SCOPE) + else() + message(STATUS "C compiler does not support ${flag}") + endif() +endfunction() diff --git a/cmake/c_flags_override.cmake b/cmake/c_flags_override.cmake new file mode 100644 index 00000000..1064022c --- /dev/null +++ b/cmake/c_flags_override.cmake @@ -0,0 +1,24 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# +# This file overrides the default compiler flags for CMake's built-in +# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set +# here. The main purpose is to make sure ``-DNDEBUG`` is never set by default. +# +#===------------------------------------------------------------------------===# +if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU")) + # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed + set(CMAKE_C_FLAGS_INIT "") + set(CMAKE_C_FLAGS_DEBUG_INIT "-O0 -g") + set(CMAKE_C_FLAGS_MINSIZEREL_INIT "-Os") + set(CMAKE_C_FLAGS_RELEASE_INIT "-O3") + set(CMAKE_C_FLAGS_RELWITHDEBINFO_INIT "-O2 -g") +else() + message(FATAL_ERROR "Overrides not set for compiler ${CMAKE_C_COMPILER_ID}") +endif() diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake new file mode 100644 index 00000000..9e6e67ef --- /dev/null +++ b/cmake/compiler_warnings.cmake @@ -0,0 +1,80 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +############################################################################### +# Compiler warnings +# +# NOTE: All these variables should be lists of flags and NOT a single string. +############################################################################### +# FIXME: -Wunused-parameter fires a lot so for now suppress it. +set(GCC_AND_CLANG_WARNINGS_CXX + "-Wall" + "-Wextra" + "-Wno-unused-parameter") +set(GCC_AND_CLANG_WARNINGS_C + "-Wall" + "-Wextra" + "-Wno-unused-parameter") +set(GCC_ONLY_WARNINGS_C "") +set(GCC_ONLY_WARNINGS_CXX "") +set(CLANG_ONLY_WARNINGS_C "") +set(CLANG_ONLY_WARNINGS_CXX "") + +############################################################################### +# Check which warning flags are supported and use them globally +############################################################################### +set(CXX_WARNING_FLAGS_TO_CHECK "") +set(C_WARNING_FLAGS_TO_CHECK "") + +if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") + list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_CXX}) + list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS_CXX}) +elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") + list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_CXX}) + list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS_CXX}) +else() + message(AUTHOR_WARNING "Unknown compiler") +endif() + +if ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU") + list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_C}) + list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS_C}) +elseif ("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") + list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_C}) + list(APPEND C_WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS_C}) +else() + message(AUTHOR_WARNING "Unknown compiler") +endif() + +# Loop through flags and use the ones which the compiler supports +foreach (flag ${CXX_WARNING_FLAGS_TO_CHECK}) + # Note `add_global_cxx_flag()` is used rather than + # `klee_component_add_cxx_flag()` because warning + # flags are typically useful for building everything. + add_global_cxx_flag("${flag}") +endforeach() +foreach (flag ${C_WARNING_FLAGS_TO_CHECK}) + add_global_c_flag("${flag}") +endforeach() + +############################################################################### +# Warnings as errors +############################################################################### +option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF) +if (WARNINGS_AS_ERRORS) + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + add_global_cxx_flag("-Werror" REQUIRED) + add_global_c_flag("-Werror" REQUIRED) + else() + message(AUTHOR_WARNING "Unknown compiler") + endif() + message(STATUS "Treating compiler warnings as errors") +else() + message(STATUS "Not treating compiler warnings as errors") +endif() diff --git a/cmake/cxx_flags_override.cmake b/cmake/cxx_flags_override.cmake new file mode 100644 index 00000000..0e3946fe --- /dev/null +++ b/cmake/cxx_flags_override.cmake @@ -0,0 +1,25 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# +# This file overrides the default compiler flags for CMake's built-in +# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set +# here. The main purpose is to make sure ``-DNDEBUG`` is never set by default. +# +#===------------------------------------------------------------------------===# + +if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed + set(CMAKE_CXX_FLAGS_INIT "") + set(CMAKE_CXX_FLAGS_DEBUG_INIT "-O0 -g") + set(CMAKE_CXX_FLAGS_MINSIZEREL_INIT "-Os") + set(CMAKE_CXX_FLAGS_RELEASE_INIT "-O3") + set(CMAKE_CXX_FLAGS_RELWITHDEBINFO_INIT "-O2 -g") +else() + message(FATAL_ERROR "Overrides not set for compiler ${CMAKE_CXX_COMPILER_ID}") +endif() diff --git a/cmake/find_bitcode_compiler.cmake b/cmake/find_bitcode_compiler.cmake new file mode 100644 index 00000000..615931f3 --- /dev/null +++ b/cmake/find_bitcode_compiler.cmake @@ -0,0 +1,96 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# +# This file tries to find compilers to build LLVM bitcode. +# It is implicitly dependent on `find_llvm.cmake` already being run in the +# same scope. +# +#===------------------------------------------------------------------------===# + +message(STATUS "Looking for bitcode compilers") + +find_program( + LLVMCC + NAMES "clang-${LLVM_VERSION_MAJOR}.${LLVM_VERSION_MINOR}" "clang" "llvm-gcc" + # Give the LLVM tools directory higher priority than the system directory. + HINTS "${LLVM_TOOLS_BINARY_DIR}" +) +if (LLVMCC) + message(STATUS "Found ${LLVMCC}") +else() + message(FATAL_ERROR "Failed to find C bitcode compiler") +endif() + +find_program( + LLVMCXX + NAMES "clang++-${LLVM_VERSION_MAJOR}.${LLVM_VERSION_MINOR}" "clang++" "llvm-g++" + # Give the LLVM tools directory higher priority than the system directory. + HINTS "${LLVM_TOOLS_BINARY_DIR}" +) +if (LLVMCXX) + message(STATUS "Found ${LLVMCXX}") +else() + message(FATAL_ERROR "Failed to find C++ bitcode compiler") +endif() + +# Check `llvm-dis` is available +set(LLVM_DIS_TOOL "${LLVM_TOOLS_BINARY_DIR}/llvm-dis") +if (NOT EXISTS "${LLVM_DIS_TOOL}") + message(FATAL_ERROR + "The llvm-dis tool cannot be found at \"${LLVM_DIS_TOOL}\"") +endif() + +# Test compiler +function(test_bitcode_compiler COMPILER SRC_EXT) + message(STATUS "Testing bitcode compiler ${COMPILER}") + set(SRC_FILE "${CMAKE_BINARY_DIR}/test_bitcode_compiler.${SRC_EXT}") + file(WRITE "${SRC_FILE}" "int main(int argc, char** argv) { return 0;}") + set(BC_FILE "${SRC_FILE}.bc") + execute_process( + COMMAND + "${COMPILER}" + "-c" + "-emit-llvm" + "-o" "${BC_FILE}" + "${SRC_FILE}" + RESULT_VARIABLE COMPILE_INVOKE_EXIT_CODE + ) + if ("${COMPILE_INVOKE_EXIT_CODE}" EQUAL 0) + message(STATUS "Compile success") + else() + message(FATAL_ERROR "Compilation failed") + endif() + + message(STATUS "Checking compatibility with LLVM ${LLVM_PACKAGE_VERSION}") + # Check if the LLVM version we are using is compatible + # with this compiler by invoking the `llvm-dis` tool + # on the generated bitcode. + set(LL_FILE "${SRC_FILE}.ll") + execute_process( + COMMAND + "${LLVM_DIS_TOOL}" + "-o" "${LL_FILE}" + "${BC_FILE}" + RESULT_VARIABLE LLVM_DIS_INVOKE_EXIT_CODE + ) + if ("${LLVM_DIS_INVOKE_EXIT_CODE}" EQUAL 0) + message(STATUS "\"${COMPILER}\" is compatible") + else() + message(FATAL_ERROR "\"${COMPILER}\" is not compatible with LLVM ${LLVM_PACKAGE_VERSION}") + endif() + + # Remove temporary files. It's okay to not remove these on failure + # as they will be useful for developer debugging. + file(REMOVE "${SRC_FILE}") + file(REMOVE "${BC_FILE}") + file(REMOVE "${LL_FILE}") +endfunction() + +test_bitcode_compiler("${LLVMCC}" "c") +test_bitcode_compiler("${LLVMCXX}" "cxx") diff --git a/cmake/find_llvm.cmake b/cmake/find_llvm.cmake new file mode 100644 index 00000000..60d7b3e4 --- /dev/null +++ b/cmake/find_llvm.cmake @@ -0,0 +1,166 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# +# This file provides multiple methods to detect LLVM. +# +# * llvm-config executable. This method is portable across LLVM build systems +# (i.e. works if LLVM was built with autoconf/Makefile or with CMake). +# +# * find_package(LLVM CONFIG). This method only works if LLVM was built with +# CMake or with LLVM >= 3.5 when built with the autoconf/Makefile build system +# This method relies on the `LLVMConfig.cmake` file generated to be generated +# by LLVM's build system. +# +#===------------------------------------------------------------------------===# + +option(USE_CMAKE_FIND_PACKAGE_LLVM "Use find_package(LLVM CONFIG) to find LLVM" OFF) + +if (USE_CMAKE_FIND_PACKAGE_LLVM) + find_package(LLVM CONFIG REQUIRED) + + # Provide function to map LLVM components to libraries. + function(klee_get_llvm_libs output_var) + if (${LLVM_PACKAGE_VERSION} VERSION_LESS "3.5") + llvm_map_components_to_libraries(${output_var} ${ARGN}) + else() + llvm_map_components_to_libnames(${output_var} ${ARGN}) + endif() + set(${output_var} ${${output_var}} PARENT_SCOPE) + endfunction() +else() + # Use the llvm-config binary to get the information needed. + # Try to detect it in the user's environment. The user can + # force a particular binary by passing `-DLLVM_CONFIG_BINARY=/path/to/llvm-config` + # to CMake. + find_program(LLVM_CONFIG_BINARY + NAMES llvm-config) + message(STATUS "LLVM_CONFIG_BINARY: ${LLVM_CONFIG_BINARY}") + + if (NOT LLVM_CONFIG_BINARY) + message(FATAL_ERROR + "Failed to find llvm-config.\n" + "Try passing -DLLVM_CONFIG_BINARY=/path/to/llvm-config to cmake") + endif() + + function(_run_llvm_config output_var) + set(_command "${LLVM_CONFIG_BINARY}" ${ARGN}) + execute_process(COMMAND ${_command} + RESULT_VARIABLE _exit_code + OUTPUT_VARIABLE ${output_var} + OUTPUT_STRIP_TRAILING_WHITESPACE + ERROR_STRIP_TRAILING_WHITESPACE + ) + if (NOT ("${_exit_code}" EQUAL "0")) + message(FATAL_ERROR "Failed running ${_command}") + endif() + set(${output_var} ${${output_var}} PARENT_SCOPE) + endfunction() + + # Get LLVM version + _run_llvm_config(LLVM_PACKAGE_VERSION "--version") + # Try x.y.z patern + set(_llvm_version_regex "^([0-9]+)\\.([0-9]+)\\.([0-9]+)$") + if ("${LLVM_PACKAGE_VERSION}" MATCHES "${_llvm_version_regex}") + string(REGEX REPLACE + "${_llvm_version_regex}" + "\\1" + LLVM_VERSION_MAJOR + "${LLVM_PACKAGE_VERSION}") + string(REGEX REPLACE + "${_llvm_version_regex}" + "\\2" + LLVM_VERSION_MINOR + "${LLVM_PACKAGE_VERSION}") + string(REGEX REPLACE + "${_llvm_version_regex}" + "\\3" + LLVM_VERSION_PATCH + "${LLVM_PACKAGE_VERSION}") + else() + # try x.y pattern + set(_llvm_version_regex "^([0-9]+)\\.([0-9]+)$") + if ("${LLVM_PACKAGE_VERSION}" MATCHES "${_llvm_version_regex}") + string(REGEX REPLACE + "${_llvm_version_regex}" + "\\1" + LLVM_VERSION_MAJOR + "${LLVM_PACKAGE_VERSION}") + string(REGEX REPLACE + "${_llvm_version_regex}" + "\\2" + LLVM_VERSION_MINOR + "${LLVM_PACKAGE_VERSION}") + set(LLVM_VERSION_PATCH 0) + else() + message(FATAL_ERROR + "Failed to parse LLVM version from \"${LLVM_PACKAGE_VERSION}\"") + endif() + endif() + + set(LLVM_DEFINITIONS "") + _run_llvm_config(_llvm_cpp_flags "--cppflags") + string_to_list("${_llvm_cpp_flags}" _llvm_cpp_flags_list) + foreach (flag ${_llvm_cpp_flags_list}) + # Filter out -I flags by only looking for -D flags. + if ("${flag}" MATCHES "^-D" AND NOT ("${flag}" STREQUAL "-D_DEBUG")) + list(APPEND LLVM_DEFINITIONS "${flag}") + endif() + endforeach() + + set(LLVM_ENABLE_ASSERTIONS ON) + set(LLVM_ENABLE_EH ON) + set(LLVM_ENABLE_RTTI ON) + _run_llvm_config(_llvm_cxx_flags "--cxxflags") + string_to_list("${_llvm_cxx_flags}" _llvm_cxx_flags_list) + foreach (flag ${_llvm_cxx_flags_list}) + if ("${flag}" STREQUAL "-DNDEBUG") + # Note we don't rely on `llvm-config --build-mode` because + # that seems broken when LLVM is built with CMake. + set(LLVM_ENABLE_ASSERTIONS OFF) + elseif ("${flag}" STREQUAL "-fno-exceptions") + set(LLVM_ENABLE_EH OFF) + elseif ("${flag}" STREQUAL "-fno-rtti") + set(LLVM_ENABLE_RTTI OFF) + endif() + endforeach() + + set(LLVM_INCLUDE_DIRS "") + foreach (flag ${_llvm_cpp_flags_list}) + # Filter out -D flags by only looking for -I flags. + if ("${flag}" MATCHES "^-I") + string(REGEX REPLACE "^-I(.+)$" "\\1" _include_dir "${flag}") + list(APPEND LLVM_INCLUDE_DIRS "${_include_dir}") + endif() + endforeach() + + _run_llvm_config(LLVM_LIBRARY_DIRS "--libdir") + _run_llvm_config(LLVM_TOOLS_BINARY_DIR "--bindir") + _run_llvm_config(TARGET_TRIPLE "--host-target") + + # Provide function to map LLVM components to libraries. + function(klee_get_llvm_libs OUTPUT_VAR) + _run_llvm_config(_llvm_libs "--libfiles" ${ARGN}) + string_to_list("${_llvm_libs}" _llvm_libs_list) + + # Now find the system libs that are needed. + # FIXME: This is a hack. We should really create imported + # targets for the LLVM libraries and have them depend + # on the necessary system libraries. + _run_llvm_config(_system_libs "--ldflags") + string_to_list("${_system_libs}" _system_libs_list) + set(_filtered_system_libs_list "") + foreach (l ${_system_libs_list}) + # Filter out `-L<path>`. + if ("${l}" MATCHES "^-l") + list(APPEND _filtered_system_libs_list "${l}") + endif() + endforeach() + set(${OUTPUT_VAR} ${_llvm_libs_list} ${_system_libs} PARENT_SCOPE) + endfunction() +endif() 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}) diff --git a/cmake/klee_add_component.cmake b/cmake/klee_add_component.cmake new file mode 100644 index 00000000..28e271c5 --- /dev/null +++ b/cmake/klee_add_component.cmake @@ -0,0 +1,25 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +function(klee_add_component target_name) + add_library(${target_name} ${ARGN}) + # Use of `PUBLIC` means these will propagate to targets that use this component. + if (("${CMAKE_VERSION}" VERSION_EQUAL "3.3") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.3")) + # In newer CMakes we can make sure that the flags are only used when compiling C++ + target_compile_options(${target_name} PUBLIC + $<$<COMPILE_LANGUAGE:CXX>:${KLEE_COMPONENT_CXX_FLAGS}>) + else() + # For older CMakes just live with the warnings we get for passing C++ only flags + # to the C compiler. + target_compile_options(${target_name} PUBLIC ${KLEE_COMPONENT_CXX_FLAGS}) + endif() + target_include_directories(${target_name} PUBLIC ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) + target_compile_definitions(${target_name} PUBLIC ${KLEE_COMPONENT_CXX_DEFINES}) + target_link_libraries(${target_name} PUBLIC ${KLEE_COMPONENT_EXTRA_LIBRARIES}) +endfunction() diff --git a/cmake/klee_component_add_cxx_flag.cmake b/cmake/klee_component_add_cxx_flag.cmake new file mode 100644 index 00000000..c866f6da --- /dev/null +++ b/cmake/klee_component_add_cxx_flag.cmake @@ -0,0 +1,31 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +include(CheckCXXCompilerFlag) +include(CMakeParseArguments) + +function(klee_component_add_cxx_flag flag) + CMAKE_PARSE_ARGUMENTS(klee_component_add_cxx_flag "REQUIRED" "" "" ${ARGN}) + string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") + string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + unset(HAS_${SANITIZED_FLAG_NAME}) + CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}) + if (klee_component_add_cxx_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}) + message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it") + endif() + if (HAS_${SANITIZED_FLAG_NAME}) + message(STATUS "C++ compiler supports ${flag}") + list(APPEND KLEE_COMPONENT_CXX_FLAGS "${flag}") + set(KLEE_COMPONENT_CXX_FLAGS ${KLEE_COMPONENT_CXX_FLAGS} PARENT_SCOPE) + else() + message(STATUS "C++ compiler does not support ${flag}") + endif() +endfunction() diff --git a/cmake/modules/FindZ3.cmake b/cmake/modules/FindZ3.cmake new file mode 100644 index 00000000..b5f90974 --- /dev/null +++ b/cmake/modules/FindZ3.cmake @@ -0,0 +1,35 @@ +# Tries to find an install of the Z3 library and header files +# +# Once done this will define +# Z3_FOUND - BOOL: System has the Z3 library installed +# Z3_INCLUDE_DIRS - LIST:The GMP include directories +# Z3_LIBRARIES - LIST:The libraries needed to use Z3 +include(FindPackageHandleStandardArgs) + +# Try to find libraries +find_library(Z3_LIBRARIES + NAMES z3 + DOC "Z3 libraries" +) +if (Z3_LIBRARIES) + message(STATUS "Found Z3 libraries: \"${Z3_LIBRARIES}\"") +else() + message(STATUS "Could not find Z3 libraries") +endif() + +# Try to find headers +find_path(Z3_INCLUDE_DIRS + NAMES z3.h + DOC "Z3 C header" +) +if (Z3_INCLUDE_DIRS) + message(STATUS "Found Z3 include path: \"${Z3_INCLUDE_DIRS}\"") +else() + message(STATUS "Could not find Z3 include path") +endif() + +# TODO: We should check we can link some simple code against libz3 + +# Handle QUIET and REQUIRED and check the necessary variables were set and if so +# set ``Z3_FOUND`` +find_package_handle_standard_args(Z3 DEFAULT_MSG Z3_INCLUDE_DIRS Z3_LIBRARIES) diff --git a/cmake/string_to_list.cmake b/cmake/string_to_list.cmake new file mode 100644 index 00000000..65c04413 --- /dev/null +++ b/cmake/string_to_list.cmake @@ -0,0 +1,13 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +function(string_to_list s output_var) + string(REPLACE " " ";" _output "${s}") + set(${output_var} ${_output} PARENT_SCOPE) +endfunction() |