diff options
53 files changed, 2835 insertions, 91 deletions
diff --git a/.travis.yml b/.travis.yml index 5c7adeed..060f4d0f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -30,6 +30,11 @@ env: # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set matrix: + # Check KLEE CMake build + - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 + - LLVM_VERSION=2.9 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 + # Test experimental metaSMT support - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 @@ -63,7 +68,6 @@ env: # Check with TCMALLOC - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 - global: - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I= - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw= diff --git a/.travis/klee.sh b/.travis/klee.sh index 98dbbc0d..64bfcb67 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -34,10 +34,18 @@ if [ "${KLEE_UCLIBC}" != "0" ]; then cd klee-uclibc ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION} make - KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime" + if [ "X${USE_CMAKE}" == "X1" ]; then + KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE" + else + KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime" + fi cd ../ else - KLEE_UCLIBC_CONFIGURE_OPTION="" + if [ "X${USE_CMAKE}" == "X1" ]; then + KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE" + else + KLEE_UCLIBC_CONFIGURE_OPTION="" + fi fi COVERAGE_FLAGS="" @@ -54,52 +62,110 @@ KLEE_STP_CONFIGURE_OPTION="" KLEE_METASMT_CONFIGURE_OPTION="" SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') -for solver in ${SOLVER_LIST}; do - echo "Setting configuration option for ${solver}" - case ${solver} in - STP) - KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build" - ;; - Z3) - echo "Z3" - KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr" - ;; - metaSMT) - echo "metaSMT" - KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}" - ;; - *) - echo "Unknown solver ${solver}" - exit 1 - esac -done - +if [ "X${USE_CMAKE}" == "X1" ]; then + # Set CMake configure options + for solver in ${SOLVER_LIST}; do + echo "Setting CMake configuration option for ${solver}" + case ${solver} in + STP) + KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=TRUE -DSTP_DIR=${BUILD_DIR}/stp/build" + ;; + Z3) + echo "Z3" + KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE" + ;; + metaSMT) + echo "metaSMT" + if [ "X${METASMT_DEFAULT}" == "X" ]; then + METASMT_DEFAULT=STP + fi + KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR=${BUILD_DIR}/metaSMT/build -DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}" + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac + done + TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE") +else + for solver in ${SOLVER_LIST}; do + echo "Setting configuration option for ${solver}" + case ${solver} in + STP) + KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build" + ;; + Z3) + echo "Z3" + KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr" + ;; + metaSMT) + echo "metaSMT" + KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}" + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac + done + + TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc") +fi -TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc") ############################################################################### # KLEE ############################################################################### mkdir klee cd klee -# Build KLEE -# Note: ENABLE_SHARED=0 is required because llvm-2.9 is incorectly packaged -# and is missing the shared library that was supposed to be built that the build -# system will try to use by default. -${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ - --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \ - --with-llvmcc=${KLEE_CC} \ - --with-llvmcxx=${KLEE_CXX} \ - ${KLEE_STP_CONFIGURE_OPTION} \ - ${KLEE_Z3_CONFIGURE_OPTION} \ - ${KLEE_METASMT_CONFIGURE_OPTION} \ - ${KLEE_UCLIBC_CONFIGURE_OPTION} \ - ${TCMALLOC_OPTION} \ - CXXFLAGS="${COVERAGE_FLAGS}" \ - && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ - ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ - ENABLE_SHARED=0 - +if [ "X${USE_CMAKE}" == "X1" ]; then + GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/" + if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then + KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE" + else + KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE" + fi + + if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then + CMAKE_BUILD_TYPE="RelWithDebInfo" + else + CMAKE_BUILD_TYPE="Debug" + fi + # Compute CMake build type + CXXFLAGS="${COVERAGE_FLAGS}" \ + cmake \ + -DLLVM_CONFIG_BINARY="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" \ + -DLLVMCC="${KLEE_CC}" \ + -DLLVMCXX="${KLEE_CXX}" \ + ${KLEE_STP_CONFIGURE_OPTION} \ + ${KLEE_Z3_CONFIGURE_OPTION} \ + ${KLEE_METASMT_CONFIGURE_OPTION} \ + ${KLEE_UCLIBC_CONFIGURE_OPTION} \ + ${TCMALLOC_OPTION} \ + -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \ + -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \ + ${KLEE_ASSERTS_OPTION} \ + -DENABLE_TESTS=TRUE \ + -DLIT_ARGS="-v" \ + ${KLEE_SRC} && make +else + # Build KLEE + # Note: ENABLE_SHARED=0 is required because llvm-2.9 is incorectly packaged + # and is missing the shared library that was supposed to be built that the build + # system will try to use by default. + ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ + --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \ + --with-llvmcc=${KLEE_CC} \ + --with-llvmcxx=${KLEE_CXX} \ + ${KLEE_STP_CONFIGURE_OPTION} \ + ${KLEE_Z3_CONFIGURE_OPTION} \ + ${KLEE_METASMT_CONFIGURE_OPTION} \ + ${KLEE_UCLIBC_CONFIGURE_OPTION} \ + ${TCMALLOC_OPTION} \ + CXXFLAGS="${COVERAGE_FLAGS}" \ + && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ + ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ + ENABLE_SHARED=0 +fi ############################################################################### # Testing ############################################################################### @@ -108,32 +174,42 @@ set +e # We want to let all the tests run before we exit ############################################################################### # Unit tests ############################################################################### -# The unittests makefile doesn't seem to have been packaged so get it from SVN -sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ -svn export http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittests/Makefile.unittest \ - ../Makefile.unittest -sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ - -make unittests \ - DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ - ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ - ENABLE_SHARED=0 -RETURN="$?" +if [ "X${USE_CMAKE}" == "X1" ]; then + make unittests + RETURN="$?" +else + # The unittests makefile doesn't seem to have been packaged so get it from SVN + sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ + svn export http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittests/Makefile.unittest \ + ../Makefile.unittest + sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ + + make unittests \ + DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ + ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ + ENABLE_SHARED=0 + RETURN="$?" +fi ############################################################################### # lit tests ############################################################################### -# Note can't use ``make check`` because llvm-lit is not available -cd test -# The build system needs to generate this file before we can run lit -make lit.site.cfg \ - DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ - ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ - ENABLE_SHARED=0 - -set +e # We want to let all the tests run before we exit -lit -v . -RETURN="${RETURN}$?" +if [ "X${USE_CMAKE}" == "X1" ]; then + make integrationtests + RETURN="${RETURN}$?" +else + # Note can't use ``make check`` because llvm-lit is not available + cd test + # The build system needs to generate this file before we can run lit + make lit.site.cfg \ + DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ + ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ + ENABLE_SHARED=0 + + set +e # We want to let all the tests run before we exit + lit -v . + RETURN="${RETURN}$?" +fi #generate and upload coverage if COVERAGE is set if [ ${COVERAGE} -eq 1 ]; then diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh index b2f608db..3d52457f 100755 --- a/.travis/testing-utils.sh +++ b/.travis/testing-utils.sh @@ -2,6 +2,14 @@ # Make sure we exit if there is a failure set -e +if [ "X${USE_CMAKE}" == "X1" ]; then + # The New CMake build system just needs the GTest sources regardless + # of LLVM version. + wget https://github.com/google/googletest/archive/release-1.7.0.zip + unzip release-1.7.0.zip + exit 0 +fi + if [ "${LLVM_VERSION}" != "2.9" ]; then # Using LLVM3.4 all we need is vanilla GoogleTest :) wget https://github.com/google/googletest/archive/release-1.7.0.zip diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 00000000..bede4bc7 --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,688 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +############################################################################### +# Minimum CMake version and policies +############################################################################### +cmake_minimum_required(VERSION 2.8.12) +if (POLICY CMP0054) + # FIXME: This is horrible. With the old behaviour, + # quoted strings like "MSVC" in if() conditionals + # get implicitly dereferenced. The NEW behaviour + # doesn't do this but CMP0054 was only introduced + # in CMake 3.1 and we support lower versions as the + # minimum. We could set NEW here but it would be very + # confusing to use NEW for some builds and OLD for others + # which could lead to some subtle bugs. Instead when the + # minimum version is 3.1 change this policy to NEW and remove + # the hacks in place to work around it. + cmake_policy(SET CMP0054 OLD) +endif() + +if (POLICY CMP0042) + # Enable `MACOSX_RPATH` by default. + cmake_policy(SET CMP0042 NEW) +endif() + +# This overrides the default flags for the different CMAKE_BUILD_TYPEs +set(CMAKE_USER_MAKE_RULES_OVERRIDE_C + "${CMAKE_CURRENT_SOURCE_DIR}/cmake/c_flags_override.cmake") +set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX + "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_flags_override.cmake") +project(KLEE CXX C) + +############################################################################### +# Project version +############################################################################### +set(KLEE_VERSION_MAJOR 1) +set(KLEE_VERSION_MINOR 2) +set(KLEE_VERSION_PATCH 0) +set(KLEE_VERSION_TWEAK 0) +set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}.${KLEE_VERSION_PATCH}.${KLEE_VERSION_TWEAK}") +message(STATUS "KLEE version ${KLEE_VERSION}") +set(PACKAGE_STRING "\"KLEE ${KLEE_VERSION}\"") +set(PACKAGE_URL "\"https://klee.github.io\"") + +################################################################################ +# Set various useful variables depending on CMake version +################################################################################ +if (("${CMAKE_VERSION}" VERSION_EQUAL "3.2") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.2")) + # In CMake >= 3.2 add_custom_command() supports a ``USES_TERMINAL`` argument + set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL") +else() + set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "") +endif() + +################################################################################ +# Sanity check - Disallow building in source. +# Otherwise we would overwrite the Makefiles of the old build system. +################################################################################ +if ("${CMAKE_SOURCE_DIR}" STREQUAL "${CMAKE_BINARY_DIR}") + message(FATAL_ERROR "In source builds are not allowed. You should invoke " + "CMake from a different directory.") +endif() + +################################################################################ +# Build type +################################################################################ +message(STATUS "CMake generator: ${CMAKE_GENERATOR}") +if (DEFINED CMAKE_CONFIGURATION_TYPES) + # Multi-configuration build (e.g. Xcode). Here + # CMAKE_BUILD_TYPE doesn't matter + message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}") +else() + # Single configuration generator (e.g. Unix Makefiles, Ninja) + set(available_build_types Debug Release RelWithDebInfo MinSizeRel) + if(NOT CMAKE_BUILD_TYPE) + message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default") + message(STATUS "The available build types are: ${available_build_types}") + set(CMAKE_BUILD_TYPE RelWithDebInfo CACHE String + "Options are ${available_build_types}" + FORCE) + # Provide drop down menu options in cmake-gui + set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types}) + endif() + message(STATUS "Build type: ${CMAKE_BUILD_TYPE}") + + # Check the selected build type is valid + list(FIND available_build_types "${CMAKE_BUILD_TYPE}" _build_type_index) + if ("${_build_type_index}" EQUAL "-1") + message(FATAL_ERROR "\"${CMAKE_BUILD_TYPE}\" is an invalid build type.\n" + "Use one of the following build types ${available_build_types}") + endif() +endif() + + +################################################################################ +# Add our CMake module directory to the list of module search directories +################################################################################ +list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules") + +################################################################################ +# Assertions +################################################################################ +option(ENABLE_KLEE_ASSERTS "Enable KLEE assertions" ON) +if (ENABLE_KLEE_ASSERTS) + message(STATUS "KLEE assertions enabled") + # Assume that -DNDEBUG isn't set. +else() + message(STATUS "KLEE assertions disabled") + list(APPEND KLEE_COMPONENT_CXX_DEFINES "NDEBUG") +endif() + +################################################################################ +# KLEE timestamps +################################################################################ +option(KLEE_ENABLE_TIMESTAMP "Add timestamps to KLEE sources" OFF) + +################################################################################ +# Include useful CMake functions +################################################################################ +include(GNUInstallDirs) +include(CheckIncludeFile) +include(CheckIncludeFileCXX) +include(CheckFunctionExists) +include(CheckPrototypeDefinition) +include("${CMAKE_SOURCE_DIR}/cmake/string_to_list.cmake") +include("${CMAKE_SOURCE_DIR}/cmake/klee_component_add_cxx_flag.cmake") +include("${CMAKE_SOURCE_DIR}/cmake/add_global_flag.cmake") + +################################################################################ +# Compiler flags for KLEE components +# Subsequent commands will append to these. These are used instead of +# directly modifying CMAKE_CXX_FLAGS so that other code can be easily built with +# different flags. +################################################################################ +set(KLEE_COMPONENT_EXTRA_INCLUDE_DIRS "") +set(KLEE_COMPONENT_CXX_DEFINES "") +set(KLEE_COMPONENT_CXX_FLAGS "") +set(KLEE_SOLVER_LIBRARIES "") +set(KLEE_COMPONENT_EXTRA_LIBRARIES "") + +################################################################################ +# Find LLVM +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/find_llvm.cmake) +set(NEEDED_LLVM_VARS + LLVM_PACKAGE_VERSION + LLVM_VERSION_MAJOR + LLVM_VERSION_MINOR + LLVM_VERSION_PATCH + LLVM_DEFINITIONS + LLVM_ENABLE_ASSERTIONS + LLVM_ENABLE_EH + LLVM_ENABLE_RTTI + LLVM_INCLUDE_DIRS + LLVM_LIBRARY_DIRS + LLVM_TOOLS_BINARY_DIR + TARGET_TRIPLE +) + +foreach (vname ${NEEDED_LLVM_VARS}) + message(STATUS "${vname}: \"${${vname}}\"") + if (NOT (DEFINED "${vname}")) + message(FATAL_ERROR "${vname} was not defined") + endif() +endforeach() + +if (LLVM_ENABLE_ASSERTIONS) + # Certain LLVM debugging macros only work when LLVM was built with asserts + set(ENABLE_KLEE_DEBUG 1) # for config.h +else() + unset(ENABLE_KLEE_DEBUG) # for config.h +endif() + + +list(APPEND KLEE_COMPONENT_CXX_DEFINES ${LLVM_DEFINITIONS}) +list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${LLVM_INCLUDE_DIRS}) + +# Find llvm-link +set(LLVM_LINK "${LLVM_TOOLS_BINARY_DIR}/llvm-link") +if (NOT EXISTS "${LLVM_LINK}") + message(FATAL_ERROR "Failed to find llvm-link at \"${LLVM_LINK}\"") +endif() + +# Find llvm-ar +set(LLVM_AR "${LLVM_TOOLS_BINARY_DIR}/llvm-ar") +if (NOT EXISTS "${LLVM_AR}") + message(FATAL_ERROR "Failed to find llvm-ar at \"${LLVM_AR}\"") +endif() + +# Find llvm-as +set(LLVM_AS "${LLVM_TOOLS_BINARY_DIR}/llvm-as") +if (NOT EXISTS "${LLVM_AS}") + message(FATAL_ERROR "Failed to find llvm-as at \"${LLVM_AS}\"") +endif() + +################################################################################ +# Find bitcode compiler +################################################################################ +include("${CMAKE_SOURCE_DIR}/cmake/find_bitcode_compiler.cmake") +message(STATUS "LLVMCC: ${LLVMCC}") +if (NOT EXISTS "${LLVMCC}") + message(FATAL_ERROR "Cannot find C bitcode compiler \"${LLVMCC}\"") +endif() +message(STATUS "LLVMCXX: ${LLVMCXX}") +if (NOT EXISTS "${LLVMCXX}") + message(FATAL_ERROR "Cannot find C++ bitcode compiler \"${LLVMCXX}\"") +endif() + +################################################################################ +# C++ version +################################################################################ +option(USE_CXX11 "Use C++11" OFF) +if ("${LLVM_PACKAGE_VERSION}" VERSION_GREATER "3.5.0") + message(STATUS "Using LLVM >= 3.5.0. Forcing using C++11") + set(USE_CXX11 ON CACHE BOOL "Use C++11" FORCE) +endif() + +if (USE_CXX11) + message(STATUS "Enabling C++11") + # FIXME: Use CMake's own mechanism for managing C++ version. + # Set globally because it is unlikely we would want to compile + # using mixed C++ versions. + add_global_cxx_flag("-std=c++11" REQUIRED) +else() + # This is needed because with GCC 6 the default changed from gnu++98 to + # gnu++14. + add_global_cxx_flag("-std=gnu++98" REQUIRED) +endif() + +################################################################################ +# Warnings +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake) + +################################################################################ +# Solvers +################################################################################ + +# STP: Use CMake facility to detect. The user can pass `-DSTP_DIR=` to force +# a particular directory. +option(ENABLE_SOLVER_STP "Enable STP solver support" OFF) +if (ENABLE_SOLVER_STP) + message(STATUS "STP solver support enabled") + # Although find_package() will set `STP_DIR` for us add it here so that + # is displayed in `ccmake` and `cmake-gui`. + set(STP_DIR "" CACHE PATH "Path to directory containing STPConfig.cmake") + find_package(STP CONFIG) + if (STP_FOUND) + message(STATUS "Found STP version ${STP_VERSION}") + # Try the STP shared library first + if ("${STP_SHARED_LIBRARY}" STREQUAL "") + # Try the static library instead + if ("${STP_STATIC_LIBRARY}" STREQUAL "") + message(FATAL_ERROR "Couldn't find STP shared or static library") + endif() + message(STATUS "Using STP static library") + list(APPEND KLEE_SOLVER_LIBRARIES "${STP_STATIC_LIBRARY}") + else() + 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}") + message(STATUS "STP_DIR: ${STP_DIR}") + set(ENABLE_STP 1) # For config.h + else() + message(FATAL_ERROR "STP not found. Try setting `-DSTP_DIR=/path` where" + " `/path` is the directory containing `STPConfig.cmake`") + endif() +else() + message(STATUS "STP solver support disabled") + set(ENABLE_STP 0) # For config.h +endif() + +# Z3 +option(ENABLE_SOLVER_Z3 "Enable Z3 solver support" OFF) +if (ENABLE_SOLVER_Z3) + message(STATUS "Z3 solver support enabled") + find_package(Z3) + if (Z3_FOUND) + message(STATUS "Found Z3") + set(ENABLE_Z3 1) # For config.h + list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${Z3_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_LIBRARIES ${Z3_LIBRARIES}) + + # Check the signature of `Z3_get_error_msg()` + set (_old_CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES}") + set(CMAKE_REQUIRED_LIBRARIES ${CMAKE_REQUIRED_LIBRARIES} ${Z3_LIBRARIES}) + check_prototype_definition(Z3_get_error_msg + "Z3_string Z3_get_error_msg(Z3_context c, Z3_error_code err)" + "NULL" "${Z3_INCLUDE_DIRS}/z3.h" HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT) + set(CMAKE_REQUIRED_LIBRARIES ${_old_CMAKE_REQUIRED_LIBRARIES}) + if (HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT) + message(STATUS "Z3_get_error_msg requires context") + else() + message(STATUS "Z3_get_error_msg does not require context") + endif() + else() + message(FATAL_ERROR "Z3 not found.") + endif() +else() + message(STATUS "Z3 solver support disabled") + set(ENABLE_Z3 0) # For config.h +endif() + +# metaSMT +option(ENABLE_SOLVER_METASMT "Enable metaSMT solver support" OFF) +if (ENABLE_SOLVER_METASMT) + message(STATUS "metaSMT solver support enabled") + set(ENABLE_METASMT 1) + include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake) +else() + message(STATUS "metaSMT solver support disabled") + set(ENABLE_METASMT 0) # For config.h +endif() + +if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT})) + message(FATAL_ERROR "No solver was specified. At least one solver is required." + "You should enable a solver by passing one of more the following options" + " to cmake:\n" + "\"-DENABLE_SOLVER_STP=ON\"\n" + "\"-DENABLE_SOLVER_Z3=ON\"\n" + "\"-DENABLE_SOLVER_METASMT=ON\"") +endif() + +############################################################################### +# Exception handling +############################################################################### +if (NOT LLVM_ENABLE_EH) + if (ENABLE_SOLVER_METASMT) + message(WARNING "Not disabling exceptions because metaSMT uses them") + else() + klee_component_add_cxx_flag("-fno-exceptions" REQUIRED) + endif() +endif() + +############################################################################### +# RTTI +############################################################################### +if (NOT LLVM_ENABLE_RTTI) + if (ENABLE_SOLVER_METASMT) + message(WARNING "Not disabling RTTI because metaSMT uses them") + # FIXME: Should this be FATAL_ERROR rather than ERROR? + message(WARNING + "This build configuration is not supported and will likely not work." + "You should recompile LLVM with RTTI enabled.") + else() + klee_component_add_cxx_flag("-fno-rtti" REQUIRED) + endif() +endif() + +################################################################################ +# Support for compressed logs +################################################################################ +find_package(ZLIB) +if (${ZLIB_FOUND}) + set(HAVE_ZLIB_H 1) # For config.h + set(TARGET_LIBS ${TARGET_LIBS} z) + list(APPEND KLEE_COMPONENT_EXTRA_LIBRARIES ${ZLIB_LIBRARIES}) + list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${ZLIB_INCLUDE_DIRS}) +else() + unset(HAVE_ZLIB_H) # For config.h +endif() + +################################################################################ +# TCMalloc support +################################################################################ +OPTION(ENABLE_TCMALLOC "Enable TCMalloc support" OFF) +if (ENABLE_TCMALLOC) + message(STATUS "TCMalloc support enabled") + set(TCMALLOC_HEADER "gperftools/malloc_extension.h") + check_include_file_cxx("${TCMALLOC_HEADER}" HAVE_GPERFTOOLS_MALLOC_EXTENSION_H) + if (${HAVE_GPERFTOOLS_MALLOC_EXTENSION_H}) + find_library(TCMALLOC_LIBRARIES + NAMES tcmalloc tcmalloc_minimal + DOC "TCMalloc libraries" + ) + if (NOT TCMALLOC_LIBRARIES) + message(FATAL_ERROR + "Found \"${TCMALLOC_HEADER}\" but could not find library") + endif() + list(APPEND KLEE_COMPONENT_EXTRA_LIBRARIES ${TCMALLOC_LIBRARIES}) + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + # TCMalloc's documentation says its safest to pass these flags when + # building with gcc because gcc can optimize assuming its using its own + # malloc. + klee_component_add_cxx_flag(-fno-builtin-malloc REQUIRED) + klee_component_add_cxx_flag(-fno-builtin-calloc REQUIRED) + klee_component_add_cxx_flag(-fno-builtin-realloc REQUIRED) + klee_component_add_cxx_flag(-fno-builtin-free REQUIRED) + endif() + else() + message(FATAL_ERROR "Can't find \"${TCMALLOC_HEADER}\"") + endif() +else() + message(STATUS "TCMalloc support disabled") +endif() + +################################################################################ +# Detect libcap +################################################################################ +check_include_file("sys/capability.h" HAVE_SYS_CAPABILITY_H) +if (HAVE_SYS_CAPABILITY_H) + find_library(LIBCAP_LIBRARIES + NAMES cap + DOC "libcap library" + ) + if (NOT LIBCAP_LIBRARIES) + message(FATAL_ERROR "Found \"sys/capability.h\" but could not find libcap") + endif() +else() + set(LIBCAP_LIBRARIES "") +endif() + +################################################################################ +# Detect libutil +################################################################################ +check_include_file("pty.h" HAVE_PTY_H) +if (HAVE_PTY_H) + find_library(LIBUTIL_LIBRARIES + NAMES util + DOC "libutil library. Typically part of glibc") + if (NOT LIBUTIL_LIBRARIES) + message(FATAL_ERROR "Found \"pty.h\" but could not find libutil") + endif() +endif() + +################################################################################ +# Miscellaneous header file detection +################################################################################ +check_function_exists(mallinfo HAVE_MALLINFO) # FIXME: should test CXX compiler not C +check_function_exists(__ctype_b_loc HAVE_CTYPE_EXTERNALS) # FIXME: should test CXX compiler not C + +check_include_file_cxx(malloc/malloc.h HAVE_MALLOC_MALLOC_H) +check_function_exists(malloc_zone_statistics HAVE_MALLOC_ZONE_STATISTICS) + +# FIXME: This is needed by the runtime not KLEE itself so we are testing the wrong +# compiler. +check_include_file("selinux/selinux.h" HAVE_SELINUX_SELINUX_H) +check_include_file("sys/acl.h" HAVE_SYS_ACL_H) +if (HAVE_SELINUX_SELINUX_H) + message(STATUS "SELinux support enabled") + set(HAVE_SELINUX 1) + # Test what function signature we need to use for SELinux. The signatures + # have changed between 2.2 and 2.3. In particular, the type of the "security + # context" parameter was changed from char * to const char *, with this + # patch: [PATCH] Get rid of security_context_t and fix const declarations. + # [http://www.spinics.net/lists/selinux/msg14827.html] + check_prototype_definition(setcon + "int setcon(char* context)" + "0" + "selinux/selinux.h" + SELINUX_SECURITY_CTX_NO_CONST + ) + if (SELINUX_SECURITY_CTX_NO_CONST) + message(STATUS "security_context_t is char*") + set(KLEE_SELINUX_CTX_CONST " ") + else() + check_prototype_definition(setcon + "int setcon(const char* context)" + "0" + "selinux/selinux.h" + SELINUX_SECURITY_CTX_WITH_CONST + ) + if (SELINUX_SECURITY_CTX_WITH_CONST) + message(STATUS "security_context_t is const char*") + set(KLEE_SELINUX_CTX_CONST "const") + else() + message(FATAL_ERROR "Failed to determine function signature for \"setcon\"") + endif() + endif() +else() + message(STATUS "SELinux support disabled") + set(HAVE_SELINUX 0) +endif() + +################################################################################ +# KLEE runtime support +################################################################################ +# This is set here and not in `runtime` because `config.h` needs to be generated. + + +set(available_klee_runtime_build_types + "Release" + "Release+Debug" + "Release+Asserts" + "Release+Debug+Asserts" + "Debug" + "Debug+Asserts" +) +if (NOT KLEE_RUNTIME_BUILD_TYPE) + message(STATUS "KLEE_RUNTIME_BUILD_TYPE is not set. Setting default") + message(STATUS "The available runtime build types are: ${available_klee_runtime_build_types}") + set(KLEE_RUNTIME_BUILD_TYPE "Release+Debug+Asserts" CACHE String + "Options are ${available_klee_runtime_build_types}" + FORCE) +endif() +# Provide drop down menu options in cmake-gui +set_property(CACHE + KLEE_RUNTIME_BUILD_TYPE + PROPERTY STRINGS ${available_klee_runtime_build_types}) +message(STATUS "KLEE_RUNTIME_BUILD_TYPE: ${KLEE_RUNTIME_BUILD_TYPE}") + +set(KLEE_INSTALL_RUNTIME_DIR "${CMAKE_INSTALL_FULL_LIBDIR}/klee/runtime") + +# Location where KLEE will look for the built runtimes by default. +set(KLEE_RUNTIME_DIRECTORY "${CMAKE_BINARY_DIR}/${KLEE_RUNTIME_BUILD_TYPE}/lib") + +################################################################################ +# KLEE POSIX Runtime Support +################################################################################ +option(ENABLE_POSIX_RUNTIME "Enable KLEE's POSIX runtime" OFF) +if (ENABLE_POSIX_RUNTIME) + message(STATUS "POSIX runtime enabled") + if (NOT ENABLE_KLEE_UCLIBC) + message(WARNING "Enabling POSIX runtime without klee-uclibc support." + "The runtime might not work without it. Pass `-DENABLE_KLEE_UCLIBC=ON`" + " to enable klee-uclibc support.") + endif() +else() + message(STATUS "POSIX runtime disabled") +endif() + +################################################################################ +# KLEE uclibc support +################################################################################ +option(ENABLE_KLEE_UCLIBC "Enable support for klee-uclibc" OFF) +if (ENABLE_KLEE_UCLIBC) + message(STATUS "klee-uclibc support enabled") + set(SUPPORT_KLEE_UCLIBC 1) # For config.h + set(KLEE_UCLIBC_PATH "" CACHE PATH "Path to klee-uclibc root directory") + if (NOT IS_DIRECTORY "${KLEE_UCLIBC_PATH}") + message(FATAL_ERROR + "KLEE_UCLIBC_PATH (\"${KLEE_UCLIBC_PATH}\") is not a valid directory.\n" + "Try passing -DKLEE_UCLIBC_PATH=<path> to cmake where <path> is the path" + " to the root of the klee-uclibc directory.") + endif() + + # Find the C library bitcode archive + set(KLEE_UCLIBC_BCA_NAME "klee-uclibc.bca") + set(KLEE_UCLIBC_C_BCA "${KLEE_UCLIBC_PATH}/lib/libc.a") + if (NOT EXISTS "${KLEE_UCLIBC_PATH}") + message(FATAL_ERROR + "klee-uclibc library not found at \"${KLEE_UCLIBC_C_BCA}\"") + endif() + message(STATUS "Found klee-uclibc library: \"${KLEE_UCLIBC_C_BCA}\"") + + # Make a symlink to KLEE_UCLIBC_C_BCA so KLEE can find it where it + # is expected. + file(MAKE_DIRECTORY "${KLEE_RUNTIME_DIRECTORY}") + execute_process(COMMAND ${CMAKE_COMMAND} -E create_symlink + "${KLEE_UCLIBC_C_BCA}" + "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_NAME}" + ) +list(APPEND KLEE_COMPONENT_CXX_DEFINES + -DKLEE_UCLIBC_BCA_NAME=\"${KLEE_UCLIBC_BCA_NAME}\") + +# Add klee-uclibc to the install target. We install the original +# file rather than the symlink because CMake would just copy the symlink +# rather than the file. +install(FILES "${KLEE_UCLIBC_C_BCA}" + DESTINATION "${KLEE_INSTALL_RUNTIME_DIR}" + RENAME "${KLEE_UCLIBC_BCA_NAME}" + ) + +else() + message(STATUS "klee-uclibc support disabled") + set(SUPPORT_KLEE_UCLIBC 0) # For config.h +endif() + +################################################################################ +# Generate `config.h` +################################################################################ +configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/config.h.cmin + ${CMAKE_BINARY_DIR}/include/klee/Config/config.h) + +################################################################################ +# Generate `CompileTimeInfo.h` +################################################################################ +# FIXME: Get information from git and have configure depend on this so we +# only re-generate the file when necessary. +set(AUTO_GEN_MSG "AUTOMATICALLY GENERATED. DO NOT EDIT!") +configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin + ${CMAKE_BINARY_DIR}/include/klee/Config/CompileTimeInfo.h +) + +################################################################################ +# Global include directories +################################################################################ +include_directories("${CMAKE_SOURCE_DIR}/include") +include_directories("${CMAKE_BINARY_DIR}/include") + +################################################################################ +# Set default location for targets in the build directory +################################################################################ +set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) +set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) +set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) + +################################################################################ +# KLEE components +################################################################################ +include("${CMAKE_SOURCE_DIR}/cmake/klee_add_component.cmake") +add_subdirectory(lib) +add_subdirectory(runtime) + +################################################################################ +# KLEE tools +################################################################################ +add_subdirectory(tools) + +################################################################################ +# Testing +################################################################################ +option(ENABLE_TESTS "Enable tests" ON) + +if (ENABLE_TESTS) + # Find lit + set(LIT_TOOL_NAMES "llvm-lit" "lit") + find_program( + LIT_TOOL + NAMES ${LIT_TOOL_NAMES} + HINTS "${LLVM_TOOLS_BINARY_DIR}" + DOC "Path to lit tool" + ) + + set(LIT_ARGS + "-v;-s" + CACHE + STRING + "Lit arguments" + ) + +if ((NOT LIT_TOOL) OR (NOT EXISTS "${LIT_TOOL}")) + message(FATAL_ERROR "The lit tool is required for testing." + " CMake tried to find lit with the following names \"${LIT_TOOL_NAMES}\"" + " but it could not be found.\n" + "You should either disable testing by passing \"-DENABLE_TESTS=OFF\" to cmake" + " or you should install the lit tool from the Python Package Index by running" + " \"pip install lit\". Note \"pip\" requires root privileges to run. If you" + " don't have root privileges you can create a virtual python environment using" + " the \"virtualenv\" tool and run \"pip\" from there.") + else() + message(STATUS "Using lit: ${LIT_TOOL}") + endif() + + option(ENABLE_UNIT_TESTS "Enable unittests" ON) + if (ENABLE_UNIT_TESTS) + message(STATUS "Unit tests enabled") + add_subdirectory(unittests) + else() + message(STATUS "Unit tests disabled") + endif() + option(ENABLE_INTEGRATION_TESTS "Enable integration tests" ON) + if (ENABLE_INTEGRATION_TESTS) + message(STATUS "Integration tests enabled") + add_subdirectory(test) + else() + message(STATUS "Integration tests disabled") + endif() + + # Add global test target + add_custom_target(check + DEPENDS unittests integrationtests + COMMENT "Running tests" + ) +else() + message(STATUS "Testing disabled") +endif() + +################################################################################ +# Documentation +################################################################################ +option(ENABLE_DOCS "Enable building documentation" ON) +if (ENABLE_DOCS) + add_subdirectory(docs) +endif() + +################################################################################ +# Miscellaneous install +################################################################################ +install(FILES include/klee/klee.h DESTINATION include/klee) diff --git a/Dockerfile b/Dockerfile index 6ee9a9ac..f1cce2ee 100644 --- a/Dockerfile +++ b/Dockerfile @@ -13,7 +13,8 @@ ENV LLVM_VERSION=3.4 \ KLEE_UCLIBC=klee_uclibc_v1.0.0 \ KLEE_SRC=/home/klee/klee_src \ COVERAGE=0 \ - BUILD_DIR=/home/klee/klee_build + BUILD_DIR=/home/klee/klee_build \ + USE_CMAKE=1 RUN apt-get update && \ apt-get -y --no-install-recommends install \ @@ -57,25 +58,7 @@ WORKDIR /home/klee # Copy across source files needed for build RUN mkdir ${KLEE_SRC} -ADD configure \ - LICENSE.TXT \ - Makefile \ - Makefile.* \ - README.md \ - MetaSMT.mk \ - TODO.txt \ - ${KLEE_SRC}/ -ADD .travis ${KLEE_SRC}/.travis/ -ADD autoconf ${KLEE_SRC}/autoconf/ -ADD docs ${KLEE_SRC}/docs/ -ADD include ${KLEE_SRC}/include/ -ADD lib ${KLEE_SRC}/lib/ -ADD runtime ${KLEE_SRC}/runtime/ -ADD scripts ${KLEE_SRC}/scripts/ -ADD test ${KLEE_SRC}/test/ -ADD tools ${KLEE_SRC}/tools/ -ADD unittests ${KLEE_SRC}/unittests/ -ADD utils ${KLEE_SRC}/utils/ +ADD / ${KLEE_SRC} # Set klee user to be owner RUN sudo chown --recursive klee: ${KLEE_SRC} @@ -87,9 +70,12 @@ RUN mkdir -p ${BUILD_DIR} RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/solvers.sh # Install testing utils (use TravisCI script) -RUN cd ${BUILD_DIR} && mkdir testing-utils && cd testing-utils && \ +RUN cd ${BUILD_DIR} && mkdir test-utils && cd test-utils && \ ${KLEE_SRC}/.travis/testing-utils.sh +# FIXME: All these hacks need to be removed. Once we no longer +# need to support KLEE's old build system they can be removed. + # FIXME: This is a nasty hack so KLEE's configure and build finds # LLVM's headers file, libraries and tools RUN sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin && \ @@ -108,13 +94,13 @@ RUN sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin && \ # FIXME: This is **really gross**. The Official Ubuntu LLVM packages don't ship # with ``FileCheck`` or the ``not`` tools so we have to hack building these # into KLEE's build system in order for the tests to pass -RUN cd ${KLEE_SRC}/tools && \ +RUN [ "X${USE_CMAKE}" != "X1" ] && ( cd ${KLEE_SRC}/tools && \ for tool in FileCheck not; do \ svn export \ http://llvm.org/svn/llvm-project/llvm/branches/release_34/utils/${tool} ${tool} ; \ sed -i 's/^USEDLIBS.*$/LINK_COMPONENTS = support/' ${tool}/Makefile; \ done && \ - sed -i '0,/^PARALLEL_DIRS/a PARALLEL_DIRS += FileCheck not' Makefile + sed -i '0,/^PARALLEL_DIRS/a PARALLEL_DIRS += FileCheck not' Makefile ) || echo "Skipping hack" # FIXME: The current TravisCI script expects clang-${LLVM_VERSION} to exist RUN sudo ln -s /usr/bin/clang /usr/bin/clang-${LLVM_VERSION} && \ @@ -131,12 +117,16 @@ RUN mv /etc/sudoers.bak /etc/sudoers && \ USER klee # Add KLEE binary directory to PATH -RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/klee/.bashrc +RUN [ "X${USE_CMAKE}" != "X1" ] && \ + (echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/klee/.bashrc) || \ + (echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/bin' >> /home/klee/.bashrc) # Link klee to /usr/bin so that it can be used by docker run USER root -RUN for exec in ${BUILD_DIR}/klee/Release+Asserts/bin/* ; do ln -s ${exec} /usr/bin/`basename ${exec}`; done +RUN [ "X${USE_CMAKE}" != "X1" ] && \ + (for executable in ${BUILD_DIR}/klee/Release+Asserts/bin/* ; do ln -s ${executable} /usr/bin/`basename ${executable}`; done) || \ + (for executable in ${BUILD_DIR}/klee/bin/* ; do ln -s ${executable} /usr/bin/`basename ${executable}`; done) # Link klee to the libkleeRuntest library needed by docker run -RUN ln -s ${BUILD_DIR}/klee/Release+Asserts/lib/libkleeRuntest.so /usr/lib/libkleeRuntest.so.1.0 +RUN [ "X${USE_CMAKE}" != "X1" ] && (ln -s ${BUILD_DIR}/klee/Release+Asserts/lib/libkleeRuntest.so /usr/lib/libkleeRuntest.so.1.0) || echo "Skipping hack" USER klee diff --git a/README-CMake.md b/README-CMake.md new file mode 100644 index 00000000..0b9cfd61 --- /dev/null +++ b/README-CMake.md @@ -0,0 +1,83 @@ +# CMake build system + +KLEE now has a CMake build system which is intended to replace +its autoconf/Makefile based build system. + +## Useful top level targets + +* `check` - Build and run all tests. +* `clean` - Clean the build tree. Note this won't clean the runtime build. +* `docs` - Build documentation +* `edit_cache` - Show cmake/ccmake/cmake-gui interface for chaning configure options. +* `help` - Show list of top level targets +* `integrationtests` - Run integration tests +* `unittests` - Build and run unittests + +## Useful CMake variables + +These can be set by passing `-DVAR_NAME=VALUE` to the CMake invocation. + +e.g. + +``` +cmake -DCMAKE_BUILD_TYPE=Release /path/to/klee/src +``` +* `LLVMCC` (STRING) - Path to the LLVM C compiler (e.g. Clang). + +* `LLVMCXX` (STRING) - Path to the LLVM C++ compiler (e.g. Clang++). + +* `CMAKE_BUILD_TYPE` (STRING) - Build type for KLEE. Can be + `Debug`, `Release`, `RelWithDebInfo` or `MinSizeRel`. + +* `DOWNLOAD_LLVM_TESTING_TOOLS` (BOOLEAN) - Force downloading + of LLVM testing tool sources. + +* `ENABLE_DOCS` (BOOLEAN) - Enable building documentation. + +* `ENABLE_DOXYGEN` (BOOLEAN) - Enable building doxygen documentation. + +* `ENABLE_INTEGRATION_TESTS` (BOOLEAN) - Enable KLEE integration tests. + +* `ENABLE_KLEE_ASSERTS` (BOOLEAN) - Enable assertions when building KLEE. + +* `ENABLE_KLEE_UCLIBC` (BOOLEAN) - Enable support for klee-uclibc. + +* `ENABLE_POSIX_RUNTIME` (BOOLEAN) - Enable POSIX runtime. + +* `ENABLE_SOLVER_METASMT` (BOOLEAN) - Enable MetaSMT solver support. + +* `ENABLE_SOLVER_STP` (BOOLEAN) - Enable STP solver support. + +* `ENABLE_SOLVER_Z3` (BOOLEAN) - Enable Z3 solver support. + +* `ENABLE_TCMALLOC` (BOOLEAN) - Enable TCMalloc support. + +* `ENABLE_TESTS` (BOOLEAN) - Enable testing. + +* `ENABLE_UNIT_TESTS` (BOOLEAN) - Enable KLEE unit tests. + +* `GTEST_SRC_DIR` (STRING) - Path to GTest source tree. + +* `KLEE_ENABLE_TIMESTAMP` (BOOLEAN) - Enable timestamps in KLEE sources. + +* `KLEE_UCLIBC_PATH` (STRING) - Path to klee-uclibc root directory. + +* `KLEE_RUNTIME_BUILD_TYPE` (STRING) - Build type for KLEE's runtimes. + Can be `Release`, `Release+Asserts`, `Debug` or `Debug+Asserts`. + +* `LIT_TOOL` (STRING) - Path to lit testing tool. + +* `LIT_ARGS` (STRING) - Semi-colon separated list of lit options. + +* `LLVM_CONFIG_BINARY` (STRING) - Path to `llvm-config` binary. This is + only relevant if `USE_CMAKE_FIND_PACKAGE_LLVM` is `FALSE`. This is used + to detect the LLVM version and find libraries. + +* `MAKE_BINARY` (STRING) - Path to `make` binary used to build KLEE's runtime. + +* `USE_CMAKE_FIND_PACKAGE_LLVM` (BOOLEAN) - Use `find_package(LLVM CONFIG)` + to find LLVM. + +* `USE_CXX11` (BOOLEAN) - Use C++11. + +* `WARNINGS_AS_ERRORS` (BOOLEAN) - Treat warnings as errors when building KLEE. 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() diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt new file mode 100644 index 00000000..386298ce --- /dev/null +++ b/docs/CMakeLists.txt @@ -0,0 +1,38 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +# Top level target for building all documentation +add_custom_target(docs) + +option(ENABLE_DOXYGEN "Enable building doxygen documentation" ON) +if (ENABLE_DOXYGEN) + find_package(Doxygen) + if (DOXYGEN_FOUND) + message(STATUS "Doxygen found") + set(abs_top_srcdir "${CMAKE_SOURCE_DIR}") + set(abs_top_builddir "${CMAKE_BINARY_DIR}") + + # Configure the Doxyfile + configure_file(doxygen.cfg.in doxygen.cfg @ONLY) + + # Add rule to build doxygen documentation + add_custom_target(doc-doxygen + COMMAND "${DOXYGEN_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/doxygen.cfg" + COMMENT "Generating Doxygen documentation" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + ) + add_dependencies(docs doc-doxygen) + else() + message(WARNING "Doxygen not found. Can't build Doxygen documentation") + set(ENABLE_DOXYGEN OFF + CACHE + BOOL + "Enable building doxygen documentation" FORCE) + endif() +endif() diff --git a/include/klee/Config/CompileTimeInfo.h.cmin b/include/klee/Config/CompileTimeInfo.h.cmin new file mode 100644 index 00000000..e07de010 --- /dev/null +++ b/include/klee/Config/CompileTimeInfo.h.cmin @@ -0,0 +1,19 @@ +//===-- CompileTimeInfo.h ---------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +// @AUTO_GEN_MSG@ +#ifndef KLEE_COMPILE_TIME_INFO_H +#define KLEE_COMPILE_TIME_INFO_H + +#define KLEE_BUILD_MODE "@CMAKE_BUILD_TYPE@ (Asserts: @ENABLE_KLEE_ASSERTS@)" +// TODO: Implement support for these +// KLEE_BUILD_REVISION +// KLEE_BUILD_TAG + +#endif diff --git a/include/klee/Config/config.h.cmin b/include/klee/Config/config.h.cmin new file mode 100644 index 00000000..c2a30c16 --- /dev/null +++ b/include/klee/Config/config.h.cmin @@ -0,0 +1,95 @@ +#ifndef KLEE_CONFIG_CONFIG_H +#define KLEE_CONFIG_CONFIG_H + +/* Enable KLEE DEBUG checks */ +#cmakedefine ENABLE_KLEE_DEBUG @ENABLE_KLEE_DEBUG@ + +/* Enable metaSMT API */ +#cmakedefine ENABLE_METASMT @ENABLE_METASMT@ + +/* Using STP Solver backend */ +#cmakedefine ENABLE_STP @ENABLE_STP@ + +/* Using Z3 Solver backend */ +#cmakedefine ENABLE_Z3 @ENABLE_Z3@ + +/* Does the platform use __ctype_b_loc, etc. */ +#cmakedefine HAVE_CTYPE_EXTERNALS @HAVE_CTYPE_EXTERNALS@ + +/* Define to 1 if you have the <gperftools/malloc_extension.h> header file. */ +#cmakedefine HAVE_GPERFTOOLS_MALLOC_EXTENSION_H @HAVE_GPERFTOOLS_MALLOC_EXTENSION_H@ + +/* Define if mallinfo() is available on this platform. */ +#cmakedefine HAVE_MALLINFO @HAVE_MALLINFO@ + +/* Define to 1 if you have the <malloc/malloc.h> header file. */ +#cmakedefine HAVE_MALLOC_MALLOC_H @HAVE_MALLOC_MALLOC_H@ + +/* Define to 1 if you have the `malloc_zone_statistics' function. */ +#cmakedefine HAVE_MALLOC_ZONE_STATISTICS @HAVE_MALLOC_ZONE_STATISTICS@ + +/* Define to 1 if you have the <selinux/selinux.h> header file. */ +#cmakedefine HAVE_SELINUX_SELINUX_H @HAVE_SELINUX_SELINUX_H@ + +/* Define to 1 if you have the <sys/acl.h> header file. */ +#cmakedefine HAVE_SYS_ACL_H @HAVE_SYS_ACL_H@ + +/* Define to 1 if you have the <sys/capability.h> header file. */ +#cmakedefine HAVE_SYS_CAPABILITY_H @HAVE_SYS_CAPABILITY_H@ + +/* Z3 needs a Z3_context passed to Z3_get_error_msg() */ +#cmakedefine HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT @HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT@ + +/* Define to 1 if you have the <zlib.h> header file. */ +#cmakedefine HAVE_ZLIB_H @HAVE_ZLIB_H@ + +/* Enable time stamping the sources */ +#cmakedefine KLEE_ENABLE_TIMESTAMP @KLEE_ENABLE_TIMESTAMP@ + +/* Define to empty or 'const' depending on how SELinux qualifies its security + context parameters. */ +#cmakedefine KLEE_SELINUX_CTX_CONST @KLEE_SELINUX_CTX_CONST@ + +/* LLVM major version number */ +#cmakedefine LLVM_VERSION_MAJOR @LLVM_VERSION_MAJOR@ + +/* LLVM minor version number */ +#cmakedefine LLVM_VERSION_MINOR @LLVM_VERSION_MINOR@ + +/* Define to the address where bug reports for this package should be sent. */ +#cmakedefine PACKAGE_BUGREPORT @PACKAGE_BUGREPORT@ + +/* Define to the full name of this package. */ +#cmakedefine PACKAGE_NAME @PACKAGE_NAME@ + +/* Define to the full name and version of this package. */ +#cmakedefine PACKAGE_STRING @PACKAGE_STRING@ + +/* Define to the one symbol short name of this package. */ +#cmakedefine PACKAGE_TARNAME @PACKAGE_TARNAME@ + +/* Define to the home page for this package. */ +#cmakedefine PACKAGE_URL @PACKAGE_URL@ + +/* Define to the version of this package. */ +#cmakedefine PACKAGE_VERSION @PACKAGE_VERSION@ + +/* klee-uclibc is supported */ +#cmakedefine SUPPORT_KLEE_UCLIBC @SUPPORT_KLEE_UCLIBC@ + +/* Configuration type of KLEE's runtime libraries */ +#define RUNTIME_CONFIGURATION "@KLEE_RUNTIME_BUILD_TYPE@" + +/* FIXME: This is a stupid name. Also this is only used for figuring out where +the runtime directory is in the build tree. Instead we should just define a +macro for that. That would simplify the C++ code. */ +/* Root of the KLEE binary build directory */ +#define KLEE_DIR "@CMAKE_BINARY_DIR@" + +/* Install directory for KLEE binaries */ +#define KLEE_INSTALL_BIN_DIR "@CMAKE_INSTALL_FULL_BINDIR@" + +/* Install directory for KLEE runtime */ +#define KLEE_INSTALL_RUNTIME_DIR "@KLEE_INSTALL_RUNTIME_DIR@" + +#endif diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt new file mode 100644 index 00000000..13f76d42 --- /dev/null +++ b/lib/Basic/CMakeLists.txt @@ -0,0 +1,14 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +klee_add_component(kleeBasic + CmdLineOptions.cpp + ConstructSolverChain.cpp + KTest.cpp + Statistics.cpp +) diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt new file mode 100644 index 00000000..8a074932 --- /dev/null +++ b/lib/CMakeLists.txt @@ -0,0 +1,14 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +add_subdirectory(Basic) +add_subdirectory(Support) +add_subdirectory(Expr) +add_subdirectory(Solver) +add_subdirectory(Module) +add_subdirectory(Core) diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt new file mode 100644 index 00000000..05e2cffa --- /dev/null +++ b/lib/Core/CMakeLists.txt @@ -0,0 +1,29 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +klee_add_component(kleeCore + AddressSpace.cpp + CallPathManager.cpp + Context.cpp + CoreStats.cpp + ExecutionState.cpp + Executor.cpp + ExecutorTimers.cpp + ExecutorUtil.cpp + ExternalDispatcher.cpp + ImpliedValue.cpp + Memory.cpp + MemoryManager.cpp + PTree.cpp + Searcher.cpp + SeedInfo.cpp + SpecialFunctionHandler.cpp + StatsTracker.cpp + TimingSolver.cpp + UserSearcher.cpp +) diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt new file mode 100644 index 00000000..6ea77544 --- /dev/null +++ b/lib/Expr/CMakeLists.txt @@ -0,0 +1,23 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +klee_add_component(kleaverExpr + ArrayCache.cpp + Assigment.cpp + Constraints.cpp + ExprBuilder.cpp + Expr.cpp + ExprEvaluator.cpp + ExprPPrinter.cpp + ExprSMTLIBPrinter.cpp + ExprUtil.cpp + ExprVisitor.cpp + Lexer.cpp + Parser.cpp + Updates.cpp +) diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt new file mode 100644 index 00000000..a952ed17 --- /dev/null +++ b/lib/Module/CMakeLists.txt @@ -0,0 +1,20 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +klee_add_component(kleeModule + Checks.cpp + InstructionInfoTable.cpp + IntrinsicCleaner.cpp + KInstruction.cpp + KModule.cpp + LowerSwitch.cpp + ModuleUtil.cpp + Optimize.cpp + PhiCleaner.cpp + RaiseAsm.cpp +) diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt new file mode 100644 index 00000000..8add4ad6 --- /dev/null +++ b/lib/Solver/CMakeLists.txt @@ -0,0 +1,32 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +klee_add_component(kleaverSolver + CachingSolver.cpp + CexCachingSolver.cpp + ConstantDivision.cpp + CoreSolver.cpp + DummySolver.cpp + FastCexSolver.cpp + IncompleteSolver.cpp + IndependentSolver.cpp + MetaSMTSolver.cpp + PCLoggingSolver.cpp + QueryLoggingSolver.cpp + SMTLIBLoggingSolver.cpp + Solver.cpp + SolverImpl.cpp + SolverStats.cpp + STPBuilder.cpp + STPSolver.cpp + ValidatingSolver.cpp + Z3Builder.cpp + Z3Solver.cpp +) + +target_link_libraries(kleaverSolver PRIVATE ${KLEE_SOLVER_LIBRARIES}) diff --git a/lib/Support/CMakeLists.txt b/lib/Support/CMakeLists.txt new file mode 100644 index 00000000..4bf7ea7d --- /dev/null +++ b/lib/Support/CMakeLists.txt @@ -0,0 +1,20 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +klee_add_component(kleeSupport + CompressionStream.cpp + ErrorHandling.cpp + MemoryUsage.cpp + PrintVersion.cpp + RNG.cpp + Time.cpp + Timer.cpp + TreeStream.cpp +) + +target_link_libraries(kleeSupport PRIVATE ${ZLIB_LIBRARIES}) 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}") diff --git a/runtime/Intrinsic/Makefile.cmake.bitcode b/runtime/Intrinsic/Makefile.cmake.bitcode new file mode 100644 index 00000000..654ee020 --- /dev/null +++ b/runtime/Intrinsic/Makefile.cmake.bitcode @@ -0,0 +1,22 @@ +#===--------------------------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +LEVEL := ../ + +include $(LEVEL)/Makefile.cmake.bitcode.config + +LLVMCC.Flags += -fno-builtin + +# FIXME: This is a horrible hack +ifeq ($(USE_MODULE_INSTEAD_OF_BCA),1) + MODULE_NAME=kleeRuntimeIntrinsic +else + ARCHIVE_NAME=kleeRuntimeIntrinsic +endif + +include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/Makefile.cmake.bitcode b/runtime/Makefile.cmake.bitcode new file mode 100644 index 00000000..94f8a60d --- /dev/null +++ b/runtime/Makefile.cmake.bitcode @@ -0,0 +1,18 @@ +#===--------------------------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +LEVEL := ./ +include $(LEVEL)/Makefile.cmake.bitcode.config + +DIRS += Intrinsic +DIRS += klee-libc +ifneq ($(ENABLE_POSIX_RUNTIME),0) + DIRS += POSIX +endif + +include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/Makefile.cmake.bitcode.config.in b/runtime/Makefile.cmake.bitcode.config.in new file mode 100644 index 00000000..9d31e907 --- /dev/null +++ b/runtime/Makefile.cmake.bitcode.config.in @@ -0,0 +1,51 @@ +#===--------------------------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# +# @AUTO_GEN_MSG@ +# +#===------------------------------------------------------------------------===# +LLVMCC := @LLVMCC@ +LLVM_LINK := @LLVM_LINK@ +LLVM_AR := @LLVM_AR@ +LLVM_VERSION_MAJOR := @LLVM_VERSION_MAJOR@ +LLVM_VERSION_MINOR := @LLVM_VERSION_MINOR@ + +ROOT_SRC := @CMAKE_CURRENT_SOURCE_DIR@ +RUNTIME_CMAKE_BINARY_DIR := @CMAKE_CURRENT_BINARY_DIR@ +ROOT_OBJ := @CMAKE_CURRENT_BINARY_DIR@/runtime_build_@KLEE_RUNTIME_BUILD_TYPE@/ + +# FIXME: For legacy reasons this is where the libraries need to end up +ARCHIVE_DEST := @KLEE_RUNTIME_DIRECTORY@ +MODULE_DEST := $(ARCHIVE_DEST) + +# Build type +IS_RELEASE := @RUNTIME_IS_RELEASE@ +ASSERTIONS_ENABLED := @RUNTIME_HAS_ASSERTIONS@ +DEBUG_SYMBOLS_ENABLED := @RUNTIME_HAS_DEBUG_SYMBOLS@ +RUNTIME_CONFIG_STRING := @KLEE_RUNTIME_BUILD_TYPE@ + +# Optional features +ENABLE_POSIX_RUNTIME := @BUILD_POSIX_RUNTIME@ + +# FIXME: Get rid of this! +USE_MODULE_INSTEAD_OF_BCA := @USE_RUNTIME_BINARY_TYPE_HACK@ + +# Commands +MKDIR := mkdir +RM := rm + +# Compiler flags +LLVMCC.Flags += \ + -I@CMAKE_SOURCE_DIR@/include \ + -I@CMAKE_BINARY_DIR@/include \ + -emit-llvm \ + -std=gnu89 \ + -D_DEBUG -D_GNU_SOURCE -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS + +LLVMCC.Warnings += -Wall -Wwrite-strings diff --git a/runtime/Makefile.cmake.bitcode.rules b/runtime/Makefile.cmake.bitcode.rules new file mode 100644 index 00000000..85151e2f --- /dev/null +++ b/runtime/Makefile.cmake.bitcode.rules @@ -0,0 +1,163 @@ +#===--------------------------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# This files defines the rules used for the bitcode build system. They are +# inspired by LLVM's old Makefile build system. +#===------------------------------------------------------------------------===# +.PHONY: all build_at_level clean debug_vars + +CURRENT_DIR:= $(shell pwd) + +# Sanity checks +ifndef LEVEL + $(error LEVEL must be defined) +endif + +ifndef LLVMCC + $(error Makefile.cmake.bitconfig.config must be included) +endif + +# Any changes to the files listed here will trigger a rebuild of the sources +ADDITIONAL_BUILD_DEPS := $(CURRENT_DIR)/Makefile.cmake.bitcode \ + $(RUNTIME_CMAKE_BINARY_DIR)/Makefile.cmake.bitcode.config \ + $(RUNTIME_CMAKE_BINARY_DIR)/Makefile.cmake.bitcode + +# Handle VERBOSE +VERBOSE ?= 0 +ifneq ($(VERBOSE),0) + Verb := +else + Verb := @ +endif +# +# Handle build mode flags +ifeq ($(IS_RELEASE),1) +LLVMCC.Flags += -O2 +else +LLVMCC.Flags += -O0 +endif + +# Handle assertion flags +ifeq ($(ASSERTIONS_ENABLED),0) +LLVMCC.Flags += -DNDEBUG +endif + +# Handle debug symbol flags +ifneq ($(DEBUG_SYMBOLS_ENABLED),0) +LLVMCC.Flags += -g +endif + +ifdef DIRS +# all directory recursion target +all:: + $(Verb) for dir in $(DIRS); do \ + ($(MAKE) -C $$dir -f Makefile.cmake.bitcode) || exit 1; \ + done + +clean:: + $(Verb) for dir in $(DIRS); do \ + ($(MAKE) -C $$dir -f Makefile.cmake.bitcode $@) || exit 1; \ + done +else +# Build sources + +all:: build_at_level + +# Compute the directory to find sources +DIR_SUFFIX := $(subst $(RUNTIME_CMAKE_BINARY_DIR),,$(CURRENT_DIR)) +SRC_DIR := $(abspath $(ROOT_SRC)/$(DIR_SUFFIX)) +LOCAL_BUILD_DIR := $(abspath $(ROOT_OBJ)/$(DIR_SUFFIX)) + +C_SRCS := $(shell echo $(SRC_DIR)/*.c) +C_SRCS_NO_DIR := $(notdir $(C_SRCS)) +BC_FILES_NO_DIR := $(C_SRCS_NO_DIR:.c=.bc) +BC_FILES := $(addprefix $(LOCAL_BUILD_DIR)/,$(BC_FILES_NO_DIR)) + +# All bitcode files have these additional dependencies +$(BC_FILES) : $(ADDITIONAL_BUILD_DEPS) + +# Include dependency information generated by previous +# compiler invocations if they exist +-include $(BC_FILES:.bc=.dep) + +# Pattern rule to build bitcode files +$(LOCAL_BUILD_DIR)/%.bc : $(SRC_DIR)/%.c + @echo "LLVMCC ($(RUNTIME_CONFIG_STRING)) $<" + $(Verb) $(MKDIR) -p $(LOCAL_BUILD_DIR) + $(Verb) $(LLVMCC) $(LLVMCC.Flags) $(LLVMCC.Warnings) $< -c -o $@ -MP -MMD -MF $(LOCAL_BUILD_DIR)/$*.dep + +clean:: + @echo "Removing bitcode files" + $(Verb) $(RM) -f $(BC_FILES) + @echo "Removing dependency files" + $(Verb) $(RM) -f $(BC_FILES:.bc=.dep) + + +ifndef MODULE_NAME +ifndef ARCHIVE_NAME +$(error MODULE_NAME or ARCHIVE_NAME must be defined) +endif +endif + +ifdef MODULE_NAME +MODULE_FILE := $(MODULE_DEST)/$(MODULE_NAME).bc +build_at_level:: $(MODULE_FILE) + +# Rule for building LLVM bitcode module +$(MODULE_FILE): $(BC_FILES) + $(Verb) $(MKDIR) -p $(MODULE_DEST) + @echo "Creating LLVM module $@" + $(Verb)$(LLVM_LINK) -o $@ $^ + +clean:: + @echo "Removing LLVM module $(MODULE_FILE)" + $(Verb) $(RM) -f $(MODULE_FILE) +endif # MODULE_NAME + +ifdef ARCHIVE_NAME +ARCHIVE_FILE := $(ARCHIVE_DEST)/lib$(ARCHIVE_NAME).bca + +build_at_level:: $(ARCHIVE_FILE) + +# Rule for building LLVM bitcode archive +$(ARCHIVE_FILE): $(BC_FILES) + $(Verb) $(MKDIR) -p $(ARCHIVE_DEST) + @echo "Creating LLVM archive $@" + $(Verb) $(RM) -f $@ + $(Verb)$(LLVM_AR) rcs $@ $^ + +clean:: + @echo "Removing LLVM bitcode archive $(ARCHIVE_FILE)" + $(Verb) $(RM) -f $(ARCHIVE_FILE) + +endif # ARCHIVE_NAME + + +endif # end not ifdef DIRS + +debug_vars: + @echo "********************************************************************************" + @echo "Makefile variables for debugging" + @echo "********************************************************************************" + @echo "ARCHIVE_FILE := $(ARCHIVE_FILE)" + @echo "ASSERTIONS_ENABLED := $(ASSERTIONS_ENABLED)" + @echo "BC_FILES := $(BC_FILES)" + @echo "BUILD_ROOT := $(BUILD_ROOT)" + @echo "C_SRCS := $(C_SRCS)" + @echo "CURRENT_DIR := $(CURRENT_DIR)" + @echo "DEBUG_SYMBOLS_ENABLED := $(DEBUG_SYMBOLS_ENABLED)" + @echo "IS_RELEASE := $(IS_RELEASE)" + @echo "LOCAL_BUILD_DIR := $(LOCAL_BUILD_DIR)" + @echo "LLVMCC := $(LLVMCC)" + @echo "LLVMCC.Flag := $(LLVMCC.Flags)" + @echo "LLVMCC.Warnings := $(LLVMCC.Warnings)" + @echo "MODULE_FILE := $(MODULE_FILE)" + @echo "ROOT_OBJ := $(ROOT_OBJ)" + @echo "RUNTIME_CONFIG_STRING := $(RUNTIME_CONFIG_STRING)" + @echo "SRC_DIR := $(SRC_DIR)" + @echo "VERBOSE := $(VERBOSE)" diff --git a/runtime/POSIX/Makefile.cmake.bitcode b/runtime/POSIX/Makefile.cmake.bitcode new file mode 100644 index 00000000..66e250ff --- /dev/null +++ b/runtime/POSIX/Makefile.cmake.bitcode @@ -0,0 +1,15 @@ +#===--------------------------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +LEVEL := ../ + +include $(LEVEL)/Makefile.cmake.bitcode.config + +ARCHIVE_NAME=kleeRuntimePOSIX + +include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/Runtest/CMakeLists.txt b/runtime/Runtest/CMakeLists.txt new file mode 100644 index 00000000..dd455861 --- /dev/null +++ b/runtime/Runtest/CMakeLists.txt @@ -0,0 +1,22 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +add_library(kleeRuntest SHARED + intrinsics.c + # HACK: + ${CMAKE_SOURCE_DIR}/lib/Basic/KTest.cpp +) +# Increment version appropriately if ABI/API changes, more details: +# http://tldp.org/HOWTO/Program-Library-HOWTO/shared-libraries.html#AEN135 +set(KLEE_RUNTEST_VERSION 1.0) +set_target_properties(kleeRuntest + PROPERTIES + VERSION ${KLEE_RUNTEST_VERSION} + SOVERSION ${KLEE_RUNTEST_VERSION} +) diff --git a/runtime/klee-libc/Makefile.cmake.bitcode b/runtime/klee-libc/Makefile.cmake.bitcode new file mode 100644 index 00000000..6e85952c --- /dev/null +++ b/runtime/klee-libc/Makefile.cmake.bitcode @@ -0,0 +1,24 @@ +#===--------------------------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +LEVEL := ../ + +include $(LEVEL)/Makefile.cmake.bitcode.config + +# Prevent glibc from inlining some definitions +# of builtins +LLVMCC.Flags += -D__NO_INLINE__ + +# FIXME: This is a horrible hack +ifeq ($(USE_MODULE_INSTEAD_OF_BCA),1) + MODULE_NAME=klee-libc +else + ARCHIVE_NAME=klee-libc +endif + +include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt new file mode 100644 index 00000000..6d3ec926 --- /dev/null +++ b/test/CMakeLists.txt @@ -0,0 +1,139 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +set(KLEE_TOOLS_DIR "${CMAKE_BINARY_DIR}/bin") +set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}") +# FIXME: Do this to avoid changing the template file that +# is shared by both build systems. +set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include") +set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include") +set(TARGET_TRIPLE "${TARGET_TRIPLE}") +if (ENABLE_KLEE_UCLIBC) + set(ENABLE_UCLIBC 1) +else() + set(ENABLE_UCLIBC 0) +endif() + +# FIXME: Do this to avoid changing the template file that +# is shared by both build systems. +if (ENABLE_POSIX_RUNTIME) + if (ENABLE_KLEE_UCLIBC) + set(ENABLE_POSIX_RUNTIME 1) + else() + message(AUTHOR_WARNING + "Disabling POSIX runtime tests because they depend on klee-uclibc" + "\nFIXME!") + set(ENABLE_POSIX_RUNTIME 0) + endif() +else() + set(ENABLE_POSIX_RUNTIME 0) +endif() + +############################################################################### +# Find LLVM testing tools +############################################################################### +option(DOWNLOAD_LLVM_TESTING_TOOLS "Always download LLVM testing tools sources" OFF) +mark_as_advanced(DOWNLOAD_LLVM_TESTING_TOOLS) + +# Check `FileCheck` and the `not` tools are available. By default we'll try +# looking in the LLVM binary directory. If that fails download the sources. +# This might be necessary if using a shipped version of LLVM because LLVM +# unfortunately does not ship its testing tools. +set(DOWNLOAD_FILECHECK_SOURCE FALSE) +set(DOWNLOAD_NOT_SOURCE FALSE) + +if (DOWNLOAD_LLVM_TESTING_TOOLS) + set(DOWNLOAD_FILECHECK_SOURCE TRUE) + set(DOWNLOAD_NOT_SOURCE TRUE) +endif() + +if (NOT EXISTS "${LLVM_TOOLS_BINARY_DIR}/FileCheck") + message(WARNING "\"${LLVM_TOOLS_BINARY_DIR}/FileCheck\" does not exist. Downloading sources.") + set(DOWNLOAD_FILECHECK_SOURCE TRUE) +endif() + +if (NOT EXISTS "${LLVM_TOOLS_BINARY_DIR}/not") + message(WARNING "\"${LLVM_TOOLS_BINARY_DIR}/not\" does not exist. Downloading sources.") + set(DOWNLOAD_NOT_SOURCE TRUE) +endif() + +if (DOWNLOAD_FILECHECK_SOURCE) + set(FILECHECK_SRC_URL "https://raw.githubusercontent.com/llvm-mirror/llvm/release_${LLVM_VERSION_MAJOR}${LLVM_VERSION_MINOR}/utils/FileCheck/FileCheck.cpp") + set(FILECHECK_SRC_FILE "${CMAKE_CURRENT_BINARY_DIR}/FileCheck.cpp") + if (NOT EXISTS "${FILECHECK_SRC_URL}") + message(STATUS "Downloading LLVM FileCheck source") + file(DOWNLOAD "${FILECHECK_SRC_URL}" "${FILECHECK_SRC_FILE}" SHOW_PROGRESS) + endif() + add_executable(FileCheck + ${FILECHECK_SRC_FILE} + ) + klee_get_llvm_libs(FILECHECK_NEEDED_LIBS Support) + target_include_directories(FileCheck PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) + target_compile_options(FileCheck PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) + target_compile_definitions(FileCheck PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + target_link_libraries(FileCheck PRIVATE ${FILECHECK_NEEDED_LIBS}) +endif() + +if (DOWNLOAD_NOT_SOURCE) + set(NOT_SRC_URL "https://raw.githubusercontent.com/llvm-mirror/llvm/release_${LLVM_VERSION_MAJOR}${LLVM_VERSION_MINOR}/utils/not/not.cpp") + set(NOT_SRC_FILE "${CMAKE_CURRENT_BINARY_DIR}/not.cpp") + if (NOT EXISTS "${NOT_SRC_FILE}") + message(STATUS "Downloading LLVM not source") + file(DOWNLOAD "${NOT_SRC_URL}" "${NOT_SRC_FILE}" SHOW_PROGRESS) + endif() + add_executable("not" + ${NOT_SRC_FILE} + ) + klee_get_llvm_libs(NOT_NEEDED_LIBS Support) + target_include_directories("not" PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) + target_compile_options("not" PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) + target_compile_definitions("not" PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + target_link_libraries("not" PRIVATE ${FILECHECK_NEEDED_LIBS}) +endif() + +############################################################################### +# Concrete tests build system +############################################################################### +add_subdirectory(Concrete) + +############################################################################### +# Configure lit test suite +############################################################################### +configure_file(lit.site.cfg.in + ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg + @ONLY +) + +add_custom_target(integrationtests + COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}" + DEPENDS klee kleaver + COMMENT "Running integration tests" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) + +# Tell CMake to remove lit's output directories when +# running `make clean`. +file(GLOB_RECURSE + test_contents + LIST_DIRECTORIES true + RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}" + "*" +) +set(dirs_to_clean "") +foreach (f ${test_contents}) + if (IS_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/${f}") + list(APPEND dirs_to_clean "${CMAKE_CURRENT_BINARY_DIR}/${f}/Output") + endif() +endforeach() +set_property( + DIRECTORY + APPEND + PROPERTY ADDITIONAL_MAKE_CLEAN_FILES + ${dirs_to_clean} +) diff --git a/test/Concrete/CMakeLists.txt b/test/Concrete/CMakeLists.txt new file mode 100644 index 00000000..b3e4948f --- /dev/null +++ b/test/Concrete/CMakeLists.txt @@ -0,0 +1,9 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +configure_file(Makefile.cmake.test.in Makefile.cmake.test @ONLY) diff --git a/test/Concrete/ConcreteTest.py b/test/Concrete/ConcreteTest.py index 754c0fe6..66d18c83 100755 --- a/test/Concrete/ConcreteTest.py +++ b/test/Concrete/ConcreteTest.py @@ -8,11 +8,16 @@ import sys import shutil def testFile(name, klee_path, lli_path): + print("CWD: \"{}\"".format(os.getcwd())) baseName,ext = os.path.splitext(name) exeFile = 'Output/linked_%s.bc'%baseName print('-- building test bitcode --') - make_cmd = 'make %s 2>&1' % (exeFile,) + if os.path.exists("Makefile.cmake.test"): + # Prefer CMake generated make file + make_cmd = 'make -f Makefile.cmake.test %s 2>&1' % (exeFile,) + else: + make_cmd = 'make %s 2>&1' % (exeFile,) print("EXECUTING: %s" % (make_cmd,)) sys.stdout.flush() if os.system(make_cmd): diff --git a/test/Concrete/Makefile.cmake.test.in b/test/Concrete/Makefile.cmake.test.in new file mode 100644 index 00000000..feb879de --- /dev/null +++ b/test/Concrete/Makefile.cmake.test.in @@ -0,0 +1,48 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# +# @AUTO_GEN_MSG@ +# +#===------------------------------------------------------------------------===# +LLVMCC := @LLVMCC@ +LLVMAS := @LLVM_AS@ +LLVMLINK := @LLVM_LINK@ +LLVMCC.CFlags := -O0 -Wall + +# Make sure source files can match the pattern rules +VPATH := @CMAKE_CURRENT_SOURCE_DIR@ + +Output/.dir: + mkdir -p $@ + +clean:: + -rm -rf Output/ + +Output/%.bc: %.c Output/.dir + $(LLVMCC) -emit-llvm -c $(LLVMCC.CFlags) $< -o $@ + +Output/%.bc: %.ll $(LLVMAS) Output/.dir + $(LLVMAS) -f $< -o $@ + +# We build a separate testingUtils bitcode for each test, to make sure parallel +# tests don't interact with one another. +Output/%_testingUtils.bc: _testingUtils.c Output/.dir + $(LLVMCC) -emit-llvm -c $(LLVMCC.CFlags) $< -o $@ + +Output/linked_%.bc: Output/%.bc Output/%_testingUtils.bc + $(LLVMLINK) $< Output/$*_testingUtils.bc -o $@ + +.PRECIOUS: Output/.dir + +## Cancel built-in implicit rules that override above rules +%: %.s + +%: %.c + +%.o: %.c diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt new file mode 100644 index 00000000..9bf2acf8 --- /dev/null +++ b/tools/CMakeLists.txt @@ -0,0 +1,14 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +add_subdirectory(gen-random-bout) +add_subdirectory(kleaver) +add_subdirectory(klee) +add_subdirectory(klee-replay) +add_subdirectory(klee-stats) +add_subdirectory(ktest-tool) diff --git a/tools/gen-random-bout/CMakeLists.txt b/tools/gen-random-bout/CMakeLists.txt new file mode 100644 index 00000000..d1fa6b09 --- /dev/null +++ b/tools/gen-random-bout/CMakeLists.txt @@ -0,0 +1,17 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +add_executable(gen-random-bout + gen-random-bout.cpp +) + +set(KLEE_LIBS kleeBasic) + +target_link_libraries(gen-random-bout ${KLEE_LIBS}) + +install(TARGETS gen-random-bout RUNTIME DESTINATION bin) diff --git a/tools/kleaver/CMakeLists.txt b/tools/kleaver/CMakeLists.txt new file mode 100644 index 00000000..befbcc6e --- /dev/null +++ b/tools/kleaver/CMakeLists.txt @@ -0,0 +1,18 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +add_executable(kleaver + main.cpp +) + +klee_get_llvm_libs(LLVM_LIBS support) +set(KLEE_LIBS kleeBasic kleaverSolver kleaverExpr kleeSupport) + +target_link_libraries(kleaver ${KLEE_LIBS} ${LLVM_LIBS}) + +install(TARGETS kleaver RUNTIME DESTINATION bin) diff --git a/tools/klee-replay/CMakeLists.txt b/tools/klee-replay/CMakeLists.txt new file mode 100644 index 00000000..e0eb8d07 --- /dev/null +++ b/tools/klee-replay/CMakeLists.txt @@ -0,0 +1,30 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +if (HAVE_PTY_H) + add_executable(klee-replay + fd_init.c + file-creator.c + klee-replay.c + klee_init_env.c + ) + + target_link_libraries(klee-replay PRIVATE kleeBasic ${LIBCAP_LIBRARIES}) + # FIXME: This isn't quite right. This is actually an implementation detail + # of glibc not Linux. Really we need to test if we can use `openpty()` + # with/without an additional library. + if ("${CMAKE_SYSTEM_NAME}" MATCHES "Linux") + if (NOT LIBUTIL_LIBRARIES) + message(FATAL_ERROR "klee-replay needs libutil under Linux") + endif() + target_link_libraries(klee-replay PRIVATE ${LIBUTIL_LIBRARIES}) + endif() +install(TARGETS klee-replay RUNTIME DESTINATION bin) +else() + message(WARNING "Not building klee-replay due to missing \"pty.h\" header file") +endif() diff --git a/tools/klee-stats/CMakeLists.txt b/tools/klee-stats/CMakeLists.txt new file mode 100644 index 00000000..7203003d --- /dev/null +++ b/tools/klee-stats/CMakeLists.txt @@ -0,0 +1,9 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +install(PROGRAMS klee-stats DESTINATION bin) diff --git a/tools/klee/CMakeLists.txt b/tools/klee/CMakeLists.txt new file mode 100644 index 00000000..b6e907ab --- /dev/null +++ b/tools/klee/CMakeLists.txt @@ -0,0 +1,39 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +add_executable(klee + main.cpp +) + +# FIXME: This shouldn't be done here. Instead the KLEE libraries +# should declare their LLVM dependencies. +set(LLVM_COMPONENTS + bitreader + bitwriter + engine + ipo + jit + linker + support +) + +if ("${LLVM_PACKAGE_VERSION}" VERSION_EQUAL "3.3" OR + "${LLVM_PACKAGE_VERSION}" VERSION_GREATER "3.3") + list(APPEND LLVM_COMPONENTS irreader) +endif() + +klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS}) + +set(KLEE_LIBS kleeCore kleeBasic kleeModule kleaverSolver kleaverExpr kleeSupport) + +target_link_libraries(klee ${KLEE_LIBS} ${LLVM_LIBS}) + +install(TARGETS klee RUNTIME DESTINATION bin) + +# The KLEE binary depends on the runtimes +add_dependencies(klee BuildKLEERuntimes) diff --git a/tools/ktest-tool/CMakeLists.txt b/tools/ktest-tool/CMakeLists.txt new file mode 100644 index 00000000..76e31ac0 --- /dev/null +++ b/tools/ktest-tool/CMakeLists.txt @@ -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. +# +#===------------------------------------------------------------------------===# +install(PROGRAMS ktest-tool DESTINATION bin) + +# Copy into the build directory's binary directory +# so integration tests can find it +configure_file(ktest-tool "${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/ktest-tool" COPYONLY) diff --git a/unittests/Assignment/CMakeLists.txt b/unittests/Assignment/CMakeLists.txt new file mode 100644 index 00000000..e231ee39 --- /dev/null +++ b/unittests/Assignment/CMakeLists.txt @@ -0,0 +1,4 @@ +add_klee_unit_test(AssignmentTest + AssignmentTest.cpp) +klee_get_llvm_libs(LLVM_LIBS Support) +target_link_libraries(AssignmentTest PRIVATE kleaverExpr ${LLVM_LIBS}) diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt new file mode 100644 index 00000000..a85c0a74 --- /dev/null +++ b/unittests/CMakeLists.txt @@ -0,0 +1,100 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +# Build GTest. We don't use a pre-built version due to +# https://github.com/google/googletest/blob/master/googletest/docs/FAQ.md#why-is-it-not-recommended-to-install-a-pre-compiled-copy-of-google-test-for-example-into-usrlocal +set(GTEST_SRC_DIR + "/usr/src/gtest" + CACHE + PATH + "Path to GTest source directory" +) + +if (NOT EXISTS "${GTEST_SRC_DIR}") + message(FATAL_ERROR "GTest source directory \"${GTEST_SRC_DIR}\" cannot be found.\n" + "Try passing -DGTEST_SRC_DIR=<path_to_gtest_source> to cmake where " + "<path_to_gtest_source> is the path to the GoogleTest source tree.\n" + "Alternatively you can disable unit tests by passing " + "-DENABLE_UNIT_TESTS=OFF to cmake.") +endif() + +# It's important that GTest is built with KLEE's compile flags +# so set them here. +set(_OLD_CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS}") +foreach (f ${KLEE_COMPONENT_CXX_FLAGS}) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${f}") +endforeach() +foreach (f ${KLEE_COMPONENT_CXX_DEFINES}) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${f}") +endforeach() + +# Build GTest as part of our project +# FIXME: Prevent GTest from adding to our install target. +# This is a problem for GTest >= 1.8. I've filled a PR to fix the issue +# ( https://github.com/google/googletest/pull/921 ). If it gets accepted +# we can do `set(gtest_enable_install FALSE)` to fix this. +add_subdirectory(${GTEST_SRC_DIR} "${CMAKE_CURRENT_BINARY_DIR}/gtest_build") + +set(CMAKE_CXX_FLAGS "${_OLD_CMAKE_CXX_FLAGS}") # Restore the flags + +# This keeps track of all the unit test +# targets so we can ensure they are built +# before trying to run them. +define_property(GLOBAL + PROPERTY KLEE_UNIT_TEST_TARGETS + BRIEF_DOCS "KLEE unit tests" + FULL_DOCS "KLEE unit tests" +) + +set(GTEST_INCLUDE_DIR "${GTEST_SRC_DIR}/include") + +if (NOT IS_DIRECTORY "${GTEST_INCLUDE_DIR}") + message(FATAL_ERROR + "Cannot find GTest include directory \"${GTEST_INCLUDE_DIR}\"") +endif() + +function(add_klee_unit_test target_name) + add_executable(${target_name} ${ARGN}) + target_link_libraries(${target_name} PRIVATE gtest_main) + target_include_directories(${target_name} BEFORE PRIVATE "${GTEST_INCLUDE_DIR}") + set_target_properties(${target_name} + PROPERTIES + RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/unittests/" + ) + set_property(GLOBAL + APPEND + PROPERTY KLEE_UNIT_TEST_TARGETS + ${target_name} + ) +endfunction() + +# Unit Tests +add_subdirectory(Assignment) +add_subdirectory(Expr) +add_subdirectory(Ref) +add_subdirectory(Solver) + +# Set up lit configuration +set (UNIT_TEST_EXE_SUFFIX "Test") +configure_file(lit-unit-tests-common.site.cfg.in + ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg + @ONLY) + +# Add a target to run all the unit tests using lit +get_property(UNIT_TEST_DEPENDS + GLOBAL + PROPERTY KLEE_UNIT_TEST_TARGETS +) +add_custom_target(unittests + COMMAND + "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}" + DEPENDS ${UNIT_TEST_DEPENDS} + COMMENT "Running unittests" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) diff --git a/unittests/Expr/CMakeLists.txt b/unittests/Expr/CMakeLists.txt new file mode 100644 index 00000000..4e7bc997 --- /dev/null +++ b/unittests/Expr/CMakeLists.txt @@ -0,0 +1,6 @@ +add_klee_unit_test(ExprTest + ExprTest.cpp) +# FIXME: KLEE's libraries should just declare what libraries +# they depend on so we don't need to manually link. +klee_get_llvm_libs(LLVM_LIBS Support) +target_link_libraries(ExprTest PRIVATE kleaverExpr ${LLVM_LIBS}) diff --git a/unittests/Ref/CMakeLists.txt b/unittests/Ref/CMakeLists.txt new file mode 100644 index 00000000..d678930c --- /dev/null +++ b/unittests/Ref/CMakeLists.txt @@ -0,0 +1,6 @@ +add_klee_unit_test(RefTest + RefTest.cpp) +# FIXME: KLEE's libraries should just declare what libraries +# they depend on so we don't need to manually link. +klee_get_llvm_libs(LLVM_LIBS Support) +target_link_libraries(RefTest PRIVATE kleaverExpr ${LLVM_LIBS}) diff --git a/unittests/Solver/CMakeLists.txt b/unittests/Solver/CMakeLists.txt new file mode 100644 index 00000000..602a1196 --- /dev/null +++ b/unittests/Solver/CMakeLists.txt @@ -0,0 +1,12 @@ +add_klee_unit_test(SolverTest + SolverTest.cpp) +# FIXME: KLEE's libraries should just declare what libraries +# they depend on so we don't need to manually link. +klee_get_llvm_libs(LLVM_LIBS Support) +target_link_libraries(SolverTest + PRIVATE + kleaverSolver + kleaverExpr + kleeSupport + kleeBasic + ${LLVM_LIBS}) diff --git a/unittests/lit-unit-tests-common.cfg b/unittests/lit-unit-tests-common.cfg new file mode 100644 index 00000000..57663ff7 --- /dev/null +++ b/unittests/lit-unit-tests-common.cfg @@ -0,0 +1,11 @@ +# Configuration file for the 'lit' test runner. + +import os + +import lit.formats + +# suffixes: A list of file extensions to treat as test files. +config.suffixes = [] + +# testFormat: The test format to use to interpret tests. +config.test_format = lit.formats.GoogleTest('.', config.unit_test_exe_suffix) diff --git a/unittests/lit-unit-tests-common.site.cfg.in b/unittests/lit-unit-tests-common.site.cfg.in new file mode 100644 index 00000000..f106152f --- /dev/null +++ b/unittests/lit-unit-tests-common.site.cfg.in @@ -0,0 +1,9 @@ +import sys +import os + +## @AUTO_GEN_MSG@ +config.name = 'KLEE Unit tests' +config.unit_test_exe_suffix = "@UNIT_TEST_EXE_SUFFIX@" + +# Let the main config do the real work. +lit_config.load_config(config, "@CMAKE_SOURCE_DIR@/unittests/lit-unit-tests-common.cfg") |