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