[cmake] Use LLVM's CMake functionality only

LLVM became more complex, use LLVM's CMake functionality directly instead
of replicating this behaviour in KLEE's build system.

Use the correct build flags provided by LLVM itself.
This is influenced by the way LLVM is built in the first place.

Remove older CMake support (< 3.0).

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()