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 | 57 | ||||
| -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 | 246 | ||||
| -rw-r--r-- | cmake/find_metasmt.cmake | 14 | ||||
| -rw-r--r-- | cmake/find_stp.cmake | 2 | ||||
| -rw-r--r-- | cmake/find_z3.cmake | 6 | ||||
| -rw-r--r-- | cmake/klee_add_component.cmake | 20 | ||||
| -rw-r--r-- | cmake/klee_component_add_cxx_flag.cmake | 31 | ||||
| -rw-r--r-- | cmake/string_to_list.cmake | 13 |
12 files changed, 19 insertions, 570 deletions
diff --git a/cmake/add_global_flag.cmake b/cmake/add_global_flag.cmake deleted file mode 100644 index 893e1200..00000000 --- a/cmake/add_global_flag.cmake +++ /dev/null @@ -1,55 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# 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 deleted file mode 100644 index 1064022c..00000000 --- a/cmake/c_flags_override.cmake +++ /dev/null @@ -1,24 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# 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 index 9e6e67ef..b8d00a6b 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -13,67 +13,18 @@ # 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 +add_compile_options( "-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() + "-Wno-unused-parameter" +) ############################################################################### # 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() + add_compile_options("-Werror") message(STATUS "Treating compiler warnings as errors") else() message(STATUS "Not treating compiler warnings as errors") diff --git a/cmake/cxx_flags_override.cmake b/cmake/cxx_flags_override.cmake deleted file mode 100644 index 0e3946fe..00000000 --- a/cmake/cxx_flags_override.cmake +++ /dev/null @@ -1,25 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# 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 deleted file mode 100644 index 615931f3..00000000 --- a/cmake/find_bitcode_compiler.cmake +++ /dev/null @@ -1,96 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# 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 deleted file mode 100644 index 0f80a28b..00000000 --- a/cmake/find_llvm.cmake +++ /dev/null @@ -1,246 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# 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 relies on the `LLVMConfig.cmake` file -# 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) - # Use find_package() to detect LLVM in the user's environment. - # The user can force a particular copy by passing - # `-DLLVM_DIR=/path/to/LLVMConfig.cmake` to CMake. - find_package(LLVM CONFIG REQUIRED) - - list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}") - include(AddLLVM) - - # Provide function to map LLVM components to libraries. - function(klee_get_llvm_libs output_var) - llvm_map_components_to_libnames(${output_var} ${ARGN}) - set(${output_var} ${${output_var}} PARENT_SCOPE) - endfunction() - - # HACK: This information is not exported so just pretend its OFF for now. - set(LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN OFF) - - # make LLVM_DEFINITIONS into proper list - set(_new_llvm_definitions "${LLVM_DEFINITIONS}") - string(REPLACE " " ";" LLVM_DEFINITIONS "${_new_llvm_definitions}") - unset(_new_llvm_definitions) -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]+)(svn|git|-rust-dev)?$") - 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]+)(svn|git)?$") - 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) - set(LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN OFF) - _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) - elseif ("${flag}" STREQUAL "-fvisibility-inlines-hidden") - set(LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN ON) - 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") - - _run_llvm_config(LLVM_BUILD_MAIN_SRC_DIR "--src-root") - if (NOT EXISTS "${LLVM_BUILD_MAIN_SRC_DIR}") - set(LLVM_BUILD_MAIN_SRC_DIR "") - endif() - - # 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. - _run_llvm_config(_system_libs "--system-libs") - string_to_list("${_system_libs}" _system_libs_list) - - # Create an imported target for each LLVM library - # if it doesn't already exist. We need to do this - # so we can tell CMake that these libraries depend - # on the necessary libraries so that CMake - # can get the link order right. - set(targets_to_return "") - set(created_targets "") - foreach (llvm_lib ${_llvm_libs_list}) - get_filename_component(llvm_lib_file_name "${llvm_lib}" NAME) - - string(REGEX REPLACE "^(lib)?(LLVM[-.a-zA-Z0-9]+)\\..+$" "\\2" target_name "${llvm_lib_file_name}") - list(APPEND targets_to_return "${target_name}") - if (NOT TARGET "${target_name}") - # DEBUG: message(STATUS "Creating imported target \"${target_name}\"" " for \"${llvm_lib}\"") - list(APPEND created_targets "${target_name}") - - set(import_library_type "STATIC") - if ("${llvm_lib_file_name}" MATCHES "(so|dylib|dll)$") - set(import_library_type "SHARED") - endif() - # Create an imported target for the library - add_library("${target_name}" "${import_library_type}" IMPORTED GLOBAL) - set_property(TARGET "${target_name}" PROPERTY - IMPORTED_LOCATION "${llvm_lib}" - ) - endif() - endforeach() - - # Now state the dependencies of the created imported targets which we - # assume to be for each imported target the libraries which appear after - # the library in `{_llvm_libs_list}` and then finally the system libs. - # It is **essential** that we do this otherwise CMake will get the - # link order of the imported targets wrong. - list(LENGTH targets_to_return length_targets_to_return) - if ("${length_targets_to_return}" GREATER 0) - math(EXPR targets_to_return_last_index "${length_targets_to_return} -1") - foreach (llvm_target_lib ${created_targets}) - # DEBUG: message(STATUS "Adding deps for target ${llvm_target_lib}") - # Find position in `targets_to_return` - list(FIND targets_to_return "${llvm_target_lib}" position) - if ("${position}" EQUAL "-1") - message(FATAL_ERROR "couldn't find \"${llvm_target_lib}\" in list of targets") - endif() - if ("${position}" LESS "${targets_to_return_last_index}") - math(EXPR position_plus_one "${position} + 1") - foreach (index RANGE ${position_plus_one} ${targets_to_return_last_index}) - # Get the target for this index - list(GET targets_to_return ${index} target_for_index) - # DEBUG: message(STATUS "${llvm_target_libs} depends on ${target_for_index}") - set_property(TARGET "${llvm_target_lib}" APPEND PROPERTY - INTERFACE_LINK_LIBRARIES "${target_for_index}" - ) - endforeach() - endif() - # Now finally add the system library dependencies. These must be last. - set_property(TARGET "${target_name}" APPEND PROPERTY - INTERFACE_LINK_LIBRARIES "${_system_libs_list}" - ) - endforeach() - endif() - - set(${OUTPUT_VAR} ${targets_to_return} PARENT_SCOPE) - endfunction() -endif() - -# Filter out `-DNEBUG` from LLVM_DEFINITIONS. The caller can use -# `LLVM_ENABLE_ASSERTIONS` to decide how to set their defines. -set(_new_llvm_definitions "") -foreach (llvm_define ${LLVM_DEFINITIONS}) - if ("${llvm_define}" STREQUAL "-DNDEBUG") - # Skip - else() - list(APPEND _new_llvm_definitions "${llvm_define}") - endif() -endforeach() -set(LLVM_DEFINITIONS "${_new_llvm_definitions}") -unset(_new_llvm_definitions) diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake index 3dc9fe50..d4a2c155 100644 --- a/cmake/find_metasmt.cmake +++ b/cmake/find_metasmt.cmake @@ -34,13 +34,12 @@ if (ENABLE_SOLVER_METASMT) " `/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}) + list(APPEND KLEE_SOLVER_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) + string(REPLACE " " ";" _metaSMT_CXXFLAGS_list "${metaSMT_CXXFLAGS}") set(_metasmt_flags "") set(_metasmt_defines "") foreach (flag ${_metaSMT_CXXFLAGS_list}) @@ -59,12 +58,12 @@ if (ENABLE_SOLVER_METASMT) 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) + list(APPEND KLEE_COMPONENT_CXX_FLAGS "${f}") endforeach() # Check if metaSMT provides an useable backend if (NOT metaSMT_AVAILABLE_QF_ABV_SOLVERS) - message(FATAL_ERROR "metaSMT does not provide an useable backend.") + message(FATAL_ERROR "metaSMT does not provide an usable backend.") endif() message(STATUS "metaSMT has the following backend(s): ${metaSMT_AVAILABLE_QF_ABV_SOLVERS}.") @@ -72,7 +71,7 @@ if (ENABLE_SOLVER_METASMT) set(METASMT_DEFAULT_BACKEND "STP" CACHE STRING - "Default metaSMT backend. Availabe options ${available_metasmt_backends}") + "Default metaSMT backend. Available options ${available_metasmt_backends}") # Provide drop down menu options in cmake-gui set_property(CACHE METASMT_DEFAULT_BACKEND PROPERTY STRINGS ${available_metasmt_backends}) @@ -91,6 +90,9 @@ if (ENABLE_SOLVER_METASMT) foreach(backend ${available_metasmt_backends}) list(APPEND KLEE_COMPONENT_CXX_DEFINES -DMETASMT_HAVE_${backend}) endforeach() + + # Support newer CVC4 versions + list(APPEND KLEE_COMPONENT_CXX_DEFINES CVC4_WITHOUT_KIND_IFF) else() message(STATUS "metaSMT solver support disabled") set(ENABLE_METASMT 0) # For config.h diff --git a/cmake/find_stp.cmake b/cmake/find_stp.cmake index 7b10f1fe..2206cc88 100644 --- a/cmake/find_stp.cmake +++ b/cmake/find_stp.cmake @@ -44,7 +44,7 @@ if (ENABLE_SOLVER_STP) 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}") + list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${STP_INCLUDE_DIRS}) message(STATUS "STP_DIR: ${STP_DIR}") set(ENABLE_STP 1) # For config.h else() diff --git a/cmake/find_z3.cmake b/cmake/find_z3.cmake index 823cc051..c4e96fd7 100644 --- a/cmake/find_z3.cmake +++ b/cmake/find_z3.cmake @@ -26,6 +26,8 @@ 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) + include(CheckCXXSourceCompiles) + message(STATUS "Found Z3") set(ENABLE_Z3 1) # For config.h list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${Z3_INCLUDE_DIRS}) @@ -51,6 +53,10 @@ if (ENABLE_SOLVER_Z3) else() message(STATUS "Z3_get_error_msg does not require context") endif() + + list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${Z3_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_LIBRARY_DIRS ${Z3_LIBRARIES}) + else() message(FATAL_ERROR "Z3 not found.") endif() diff --git a/cmake/klee_add_component.cmake b/cmake/klee_add_component.cmake deleted file mode 100644 index 4f9770ac..00000000 --- a/cmake/klee_add_component.cmake +++ /dev/null @@ -1,20 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# 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) - # Components are explicitly STATIC because we don't support building them - # as shared libraries. - add_library(${target_name} STATIC ${ARGN}) - # 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}>) - 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 deleted file mode 100644 index c866f6da..00000000 --- a/cmake/klee_component_add_cxx_flag.cmake +++ /dev/null @@ -1,31 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# 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/string_to_list.cmake b/cmake/string_to_list.cmake deleted file mode 100644 index 65c04413..00000000 --- a/cmake/string_to_list.cmake +++ /dev/null @@ -1,13 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# 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() |