diff options
Diffstat (limited to 'runtime/CMakeLists.txt')
| -rw-r--r-- | runtime/CMakeLists.txt | 145 |
1 files changed, 145 insertions, 0 deletions
diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt new file mode 100644 index 00000000..68eb9016 --- /dev/null +++ b/runtime/CMakeLists.txt @@ -0,0 +1,145 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +add_subdirectory(Runtest) + +if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Release") + set(RUNTIME_IS_RELEASE 1) +else() + set(RUNTIME_IS_RELEASE 0) +endif() + +if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Asserts") + set(RUNTIME_HAS_ASSERTIONS 1) +else() + set(RUNTIME_HAS_ASSERTIONS 0) +endif() + +if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Debug") + set(RUNTIME_HAS_DEBUG_SYMBOLS 1) +else() + set(RUNTIME_HAS_DEBUG_SYMBOLS 0) +endif() + + +# FIXME: This is a horrible hack that needs to die. +# Things are very inconsistent. The runtime instrinsic +# is sometimes a LLVM module or a bitcode archive. +if ("${LLVM_PACKAGE_VERSION}" VERSION_EQUAL "3.3" OR + "${LLVM_PACKAGE_VERSION}" VERSION_GREATER "3.3") + set(USE_RUNTIME_BINARY_TYPE_HACK 1) +else() + set(USE_RUNTIME_BINARY_TYPE_HACK 0) +endif() + +if (ENABLE_POSIX_RUNTIME) + set(BUILD_POSIX_RUNTIME 1) +else() + set(BUILD_POSIX_RUNTIME 0) +endif() + +# Configure the bitcode build system +configure_file("Makefile.cmake.bitcode.config.in" + "Makefile.cmake.bitcode.config" + @ONLY +) + +# Copy over the makefiles to the build directory +configure_file("Makefile.cmake.bitcode" "Makefile.cmake.bitcode" COPYONLY) +configure_file("Makefile.cmake.bitcode.rules" "Makefile.cmake.bitcode.rules" COPYONLY) + +# Makefile for root runtime directory +# Copy over makefiles for libraries +set(BITCODE_LIBRARIES "Intrinsic" "klee-libc") +if (ENABLE_POSIX_RUNTIME) + list(APPEND BITCODE_LIBRARIES "POSIX") +endif() +foreach (bl ${BITCODE_LIBRARIES}) + configure_file("${bl}/Makefile.cmake.bitcode" + "${CMAKE_CURRENT_BINARY_DIR}/${bl}/Makefile.cmake.bitcode" + COPYONLY) +endforeach() + +# Find GNU make +find_program(MAKE_BINARY + NAMES make gmake +) + +if (NOT MAKE_BINARY) + message(STATUS "Failed to find make binary") +endif() + +# Find env +find_program(ENV_BINARY + NAMES env +) +if (NOT ENV_BINARY) + message(FATAL_ERROR "Failed to find env binary") +endif() + +# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject +# that shipped with CMake >= 3.1. Should we just avoid using this option? We don't really +# need it unless we are patching gsl itself and need to rebuild. +if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1")) + option(KLEE_RUNTIME_ALWAYS_REBUILD "Always try to rebuild KLEE runtime" ON) + if (KLEE_RUNTIME_ALWAYS_REBUILD) + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1) + else() + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 0) + endif() +else() + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") + message(WARNING "KLEE's runtime will not be automatically rebuilt.") +endif() + +# Build the runtime as an external project. +# We do this because CMake isn't really suitable +# for building the runtime because it can't handle +# the source file dependencies properly. +include(ExternalProject) +ExternalProject_Add(BuildKLEERuntimes + SOURCE_DIR "${CMAKE_CURRENT_BINARY_DIR}" + BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}" + CONFIGURE_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command + # `env` is used here to make sure `MAKEFLAGS` of KLEE's build + # is not propagated into the bitcode build system. + BUILD_COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode all + ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command +) + +# FIXME: Invoke `make clean` in the bitcode build system +# when the `clean` target is invoked. + +############################################################################### +# Runtime install +############################################################################### +set(RUNTIME_FILES_TO_INSTALL) + +# This is quite fragile and depends on knowledge in the bitcode +# build system. Hopefully it won't change very often though. + +# FIXME: This hack needs to die! +if (USE_RUNTIME_BINARY_TYPE_HACK) + list(APPEND RUNTIME_FILES_TO_INSTALL + "${KLEE_RUNTIME_DIRECTORY}/kleeRuntimeIntrinsic.bc" + "${KLEE_RUNTIME_DIRECTORY}/klee-libc.bc") +else() + list(APPEND RUNTIME_FILES_TO_INSTALL + "${KLEE_RUNTIME_DIRECTORY}/libkleeRuntimeIntrinsic.bca" + "${KLEE_RUNTIME_DIRECTORY}/libklee-libc.bca") +endif() + +if (ENABLE_POSIX_RUNTIME) + list(APPEND RUNTIME_FILES_TO_INSTALL + "${KLEE_RUNTIME_DIRECTORY}/libkleeRuntimePOSIX.bca") +endif() + +install(FILES + ${RUNTIME_FILES_TO_INSTALL} + DESTINATION "${KLEE_INSTALL_RUNTIME_DIR}") |