diff options
| -rw-r--r-- | CMakeLists.txt | 2 | ||||
| -rw-r--r-- | cmake/compile_bitcode_library.cmake | 60 | ||||
| -rw-r--r-- | runtime/CMakeLists.txt | 231 | ||||
| -rw-r--r-- | runtime/FreeStanding/CMakeLists.txt | 21 | ||||
| -rw-r--r-- | runtime/FreeStanding/Makefile.cmake.bitcode | 15 | ||||
| -rw-r--r-- | runtime/Intrinsic/CMakeLists.txt | 24 | ||||
| -rw-r--r-- | runtime/Intrinsic/Makefile.cmake.bitcode | 15 | ||||
| -rw-r--r-- | runtime/Makefile.cmake.bitcode | 24 | ||||
| -rw-r--r-- | runtime/Makefile.cmake.bitcode.config.in | 53 | ||||
| -rw-r--r-- | runtime/Makefile.cmake.bitcode.rules | 190 | ||||
| -rw-r--r-- | runtime/POSIX/CMakeLists.txt | 26 | ||||
| -rw-r--r-- | runtime/POSIX/Makefile.cmake.bitcode | 15 | ||||
| -rw-r--r-- | runtime/klee-eh-cxx/CMakeLists.txt | 24 | ||||
| -rw-r--r-- | runtime/klee-eh-cxx/Makefile.cmake.bitcode | 13 | ||||
| -rw-r--r-- | runtime/klee-libc/CMakeLists.txt | 49 | ||||
| -rw-r--r-- | runtime/klee-libc/Makefile.cmake.bitcode | 19 |
16 files changed, 300 insertions, 481 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 12ec29c2..55e3e979 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -489,7 +489,7 @@ 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") +set(KLEE_RUNTIME_DIRECTORY "${CMAKE_BINARY_DIR}/runtime/lib") file(MAKE_DIRECTORY ${KLEE_RUNTIME_DIRECTORY}) diff --git a/cmake/compile_bitcode_library.cmake b/cmake/compile_bitcode_library.cmake new file mode 100644 index 00000000..e1fb3ba2 --- /dev/null +++ b/cmake/compile_bitcode_library.cmake @@ -0,0 +1,60 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +function(compile_bitcode_library library_name source_files compile_cc_flags compile_cxx_flags opt_suffix) + # Compile every source file + set(BC_FILES) + foreach(source_file ${source_files}) + # Get filename without extension + get_filename_component(file_name_only "${source_file}" NAME_WE) + set(bc_file "${CMAKE_CURRENT_BINARY_DIR}/${file_name_only}${opt_suffix}.bc" ) + get_filename_component(source_file_type "${source_file}" EXT) + if("${source_file_type}" STREQUAL ".cpp") + add_custom_command( + OUTPUT ${bc_file} + COMMAND ${LLVMCXX} -c "-emit-llvm" ${compile_cxx_flags} "${source_file}" -o ${bc_file} + DEPENDS ${source_file} + ) + else() + add_custom_command( + OUTPUT ${bc_file} + COMMAND ${LLVMCC} -c "-emit-llvm" ${compile_cc_flags} "${source_file}" -o ${bc_file} + DEPENDS ${source_file} + ) + endif() + + list(APPEND BC_FILES ${bc_file}) + endforeach() + + # Add command to link them to an archive + add_custom_command( + OUTPUT ${library_name} + COMMAND ${LLVM_AR} rcs ${library_name} ${BC_FILES} + DEPENDS ${BC_FILES} + ) +endfunction(compile_bitcode_library) + +function(prefix_with_path files prefix output_var) + set(_result) + foreach(file ${files}) + list(APPEND _result "${prefix}${file}") + endforeach() + set(${output_var} "${_result}" PARENT_SCOPE) +endfunction(prefix_with_path) + +function(add_bitcode_library_targets lib_prefix prefixed_files cc_extra_args cxx_extra_args) + set(_lib_dependencies) + foreach(_suffix ${LIB_BC_SUFFIX}) + set(final_cc_flags ${LIB_BC_FLAGS_${_suffix}} ${cc_extra_args}) + set(final_cxx_flags ${LIB_BC_FLAGS_${_suffix}} ${cxx_extra_args}) + compile_bitcode_library("${KLEE_RUNTIME_DIRECTORY}/libklee${lib_prefix}${_suffix}.bca" "${prefixed_files}" "${final_cc_flags}" "${final_cxx_flags}" "${_suffix}") + list(APPEND _lib_dependencies "${KLEE_RUNTIME_DIRECTORY}/libklee${lib_prefix}${_suffix}.bca") + endforeach() + + add_custom_target(${lib_prefix} DEPENDS "${_lib_dependencies}") +endfunction(add_bitcode_library_targets) \ No newline at end of file diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt index 88a3faf8..327f5407 100644 --- a/runtime/CMakeLists.txt +++ b/runtime/CMakeLists.txt @@ -6,150 +6,109 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# +# Handle binaries add_subdirectory(Runtest) -if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Release") - set(RUNTIME_IS_RELEASE 1) -else() - set(RUNTIME_IS_RELEASE 0) -endif() +# Handle bitcode libraries +# Define the different configurations to be compiled and made available using a specific suffix + +set(bc_architectures 32 64) + +set(LIB_BC_SUFFIX "") + +foreach (bc_architecture ${bc_architectures}) + foreach (bc_optimization ${available_klee_runtime_build_types}) + # Add configuration to the set of available configurations + list(APPEND LIB_BC_SUFFIX "${bc_architecture}_${bc_optimization}") + + # Set specific flags for that configuration + set(local_flags "") + if (bc_architecture EQUAL "32") + list(APPEND local_flags -m32) + endif () + + + # Set specific compiler flags depending on the optimization + if (bc_optimization STREQUAL "Release") + list(APPEND local_flags -O2 -DNDebug) + elseif (bc_optimization STREQUAL "Release+Debug") + list(APPEND local_flags -O2 -g -DNDebug) + elseif (bc_optimization STREQUAL "Release+Asserts") + list(APPEND local_flags -O2 -g) + elseif (bc_optimization STREQUAL "Release+Debug+Asserts") + list(APPEND local_flags -O2 -g) + elseif (bc_optimization STREQUAL "Debug") + list(APPEND local_flags -g -DNDebug) + elseif (bc_optimization STREQUAL "Debug+Asserts") + list(APPEND local_flags -g) + else() + message(FATAL_ERROR + "Optimization (\"${bc_optimization}\") for runtime library unknown.") + endif () + + # Define suffix-specific optimizations + set("LIB_BC_FLAGS_${bc_architecture}_${bc_optimization}" ${local_flags}) + endforeach () +endforeach () + +message(STATUS "LIB_BC_SUFFIX: ${LIB_BC_SUFFIX}") +message(STATUS "KLEE_RUNTIME_DIRECTORY: ${KLEE_RUNTIME_DIRECTORY}") + +# Add additional setups if needed, e.g. +# `list(APPEND LIB_BC_SUFFIX MY_SPECIAL_CONFIG)` + +# Following define the specific flags: LIB_BC_FLAGS_*SUFFIX_FROM_ABOVE* +set(LIB_BC_FLAGS_64) +set(LIB_BC_FLAGS_32 + -m32 + ) + +# Common for all library configurations +# Setup all compilation flags +set(COMMON_CC_FLAGS + "-I${CMAKE_SOURCE_DIR}/include" + "-I${CMAKE_BINARY_DIR}/include" + -g + -D_DEBUG + -D_GNU_SOURCE + -D__STDC_LIMIT_MACROS + -D__STDC_CONSTANT_MACROS + -Wall + -Wwrite-strings + ) -if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Asserts") - set(RUNTIME_HAS_ASSERTIONS 1) -else() - set(RUNTIME_HAS_ASSERTIONS 0) -endif() +if (${LLVM_VERSION_MAJOR} GREATER 4) + list(APPEND COMMON_CC_FLAGS "-Xclang" "-disable-O0-optnone") +endif () -if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Debug") - set(RUNTIME_HAS_DEBUG_SYMBOLS 1) -else() - set(RUNTIME_HAS_DEBUG_SYMBOLS 0) -endif() +foreach (_suffix ${LIB_BC_SUFFIX}) + list(APPEND "LIB_BC_FLAGS_${_suffix}" ${COMMON_CC_FLAGS}) +endforeach () -if (ENABLE_POSIX_RUNTIME) - set(BUILD_POSIX_RUNTIME 1) -else() - set(BUILD_POSIX_RUNTIME 0) -endif() +add_subdirectory(FreeStanding) +add_subdirectory(Intrinsic) +add_subdirectory(klee-libc) + +set(RUNTIME_LIBRARIES + RuntimeFreeStanding + RuntimeIntrinsic + RuntimeKLEELibc + ) if (ENABLE_KLEE_EH_CXX) - set(BUILD_KLEE_EH_CXX 1) -else() - set(BUILD_KLEE_EH_CXX 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" "FreeStanding") -if (ENABLE_POSIX_RUNTIME) - list(APPEND BITCODE_LIBRARIES "POSIX") -endif() -if (ENABLE_KLEE_EH_CXX) - list(APPEND BITCODE_LIBRARIES "klee-eh-cxx") -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() - -option(KLEE_RUNTIME_ALWAYS_REBUILD "Always try to rebuild KLEE runtime" ON) -if (KLEE_RUNTIME_ALWAYS_REBUILD) - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG 1) -else() - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG 0) -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 - BUILD_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command - INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command -) - -set(O0OPT "-O0") -if (${LLVM_VERSION_MAJOR} GREATER 4) - set(O0OPT "${O0OPT} -Xclang -disable-O0-optnone") -endif() - - -# Use `ExternalProject_Add_Step` with `ALWAYS` argument instead of directly -# building in `ExternalProject_Add` with `BUILD_ALWAYS` argument due to lack of -# support for the `BUILD_ALWAYS` argument in CMake < 3.1. -ExternalProject_Add_Step(BuildKLEERuntimes RuntimeBuild - # `env` is used here to make sure `MAKEFLAGS` of KLEE's build - # is not propagated into the bitcode build system. - COMMAND ${ENV_BINARY} MAKEFLAGS="" O0OPT=${O0OPT} ${MAKE_BINARY} -f Makefile.cmake.bitcode all - ALWAYS ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} - WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" - ${EXTERNAL_PROJECT_ADD_STEP_USES_TERMINAL_ARG} -) - -# Target for cleaning the bitcode build system -# NOTE: Invoking `make clean` does not invoke this target. -# Instead the user needs to invoke the `clean_all` target. -# It's also weird that `ExternalProject` provides no way to do a clean. -add_custom_target(clean_runtime - COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode clean - WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} -) -add_dependencies(clean_all clean_runtime) - -############################################################################### -# Runtime install -############################################################################### -set(RUNTIME_FILES_TO_INSTALL) - -list(APPEND RUNTIME_FILES_TO_INSTALL - "${KLEE_RUNTIME_DIRECTORY}/libkleeRuntimeIntrinsic.bca" - "${KLEE_RUNTIME_DIRECTORY}/libklee-libc.bca" - "${KLEE_RUNTIME_DIRECTORY}/libkleeRuntimeFreeStanding.bca" - ) + list(APPEND RUNTIME_LIBRARIES eh-cxx) + add_subdirectory(klee-eh-cxx) +endif () if (ENABLE_POSIX_RUNTIME) - list(APPEND RUNTIME_FILES_TO_INSTALL - "${KLEE_RUNTIME_DIRECTORY}/libkleeRuntimePOSIX.bca") -endif() + list(APPEND RUNTIME_LIBRARIES RuntimePOSIX) + add_subdirectory(POSIX) +endif () -if (ENABLE_KLEE_EH_CXX) - list(APPEND RUNTIME_FILES_TO_INSTALL - "${KLEE_RUNTIME_DIRECTORY}/libklee-eh-cxx.bca") -endif() +add_custom_target(BuildKLEERuntimes + DEPENDS "${RUNTIME_LIBRARIES}" + ) -install(FILES - ${RUNTIME_FILES_TO_INSTALL} - DESTINATION "${KLEE_INSTALL_RUNTIME_DIR}") +install(DIRECTORY "${KLEE_RUNTIME_DIRECTORY}/" + DESTINATION "${KLEE_INSTALL_RUNTIME_DIR}" + ) \ No newline at end of file diff --git a/runtime/FreeStanding/CMakeLists.txt b/runtime/FreeStanding/CMakeLists.txt new file mode 100644 index 00000000..cf558a7d --- /dev/null +++ b/runtime/FreeStanding/CMakeLists.txt @@ -0,0 +1,21 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +set(LIB_PREFIX "RuntimeFreeStanding") +set(SRC_FILES + memcmp.c + memcpy.c + memmove.c + memset.c + ) + +# Build it +include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") +prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files) +add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "" "") \ No newline at end of file diff --git a/runtime/FreeStanding/Makefile.cmake.bitcode b/runtime/FreeStanding/Makefile.cmake.bitcode deleted file mode 100644 index 0ad434d6..00000000 --- a/runtime/FreeStanding/Makefile.cmake.bitcode +++ /dev/null @@ -1,15 +0,0 @@ -#===--------------------------------------------------------*- 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=kleeRuntimeFreeStanding - -include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/Intrinsic/CMakeLists.txt b/runtime/Intrinsic/CMakeLists.txt new file mode 100644 index 00000000..488e149b --- /dev/null +++ b/runtime/Intrinsic/CMakeLists.txt @@ -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. +# +#===------------------------------------------------------------------------===# +# Set up +set(LIB_PREFIX "RuntimeIntrinsic") +set(SRC_FILES + dso_handle.c + klee_choose.c + klee_div_zero_check.c + klee_int.c + klee_is_replay.c + klee_overshift_check.c + klee_range.c + ) + +# Build it +include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") +prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files) +add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "-std=gnu89" "") \ No newline at end of file diff --git a/runtime/Intrinsic/Makefile.cmake.bitcode b/runtime/Intrinsic/Makefile.cmake.bitcode deleted file mode 100644 index 77727fb4..00000000 --- a/runtime/Intrinsic/Makefile.cmake.bitcode +++ /dev/null @@ -1,15 +0,0 @@ -#===--------------------------------------------------------*- 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=kleeRuntimeIntrinsic - -include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/Makefile.cmake.bitcode b/runtime/Makefile.cmake.bitcode deleted file mode 100644 index dd32161d..00000000 --- a/runtime/Makefile.cmake.bitcode +++ /dev/null @@ -1,24 +0,0 @@ -#===--------------------------------------------------------*- 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 -DIRS += FreeStanding - -ifneq ($(ENABLE_POSIX_RUNTIME),0) - DIRS += POSIX -endif - -ifneq ($(ENABLE_KLEE_EH_CXX),0) - DIRS += klee-eh-cxx -endif - -include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/Makefile.cmake.bitcode.config.in b/runtime/Makefile.cmake.bitcode.config.in deleted file mode 100644 index b3464a14..00000000 --- a/runtime/Makefile.cmake.bitcode.config.in +++ /dev/null @@ -1,53 +0,0 @@ -#===--------------------------------------------------------*- 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@ -LLVMCXX := @LLVMCXX@ -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@ - -# 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@ -ENABLE_KLEE_EH_CXX := @BUILD_KLEE_EH_CXX@ -KLEE_LIBCXX_INCLUDE_DIR := @KLEE_LIBCXX_INCLUDE_DIR@ -KLEE_LIBCXXABI_SRC_DIR := @KLEE_LIBCXXABI_SRC_DIR@ -KLEE_INCLUDE_DIR := @CMAKE_SOURCE_DIR@/include - -# Commands -MKDIR := mkdir -RM := rm -CMP := cmp - -# Compiler flags -LLVMCC.Flags += $(LLVMCC.ExtraFlags) \ - -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 deleted file mode 100644 index db731ac5..00000000 --- a/runtime/Makefile.cmake.bitcode.rules +++ /dev/null @@ -1,190 +0,0 @@ -#===--------------------------------------------------------*- 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 force - -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.rules \ - $(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 += $(O0OPT) -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 -# Note: Use of $(realpath) is to resolve any symlinks -DIR_SUFFIX := $(subst $(realpath $(RUNTIME_CMAKE_BINARY_DIR)),,$(realpath $(CURRENT_DIR))) -SRC_DIR := $(abspath $(ROOT_SRC)/$(DIR_SUFFIX)) -# Sanity check -ifeq ($(realpath $(SRC_DIR)),) -$(error SRC_DIR "$(SRC_DIR)" does not exist) -endif - -# Compute the directory to put build files -LOCAL_BUILD_DIR := $(abspath $(ROOT_OBJ)/$(DIR_SUFFIX)) - -C_SRCS := $(sort $(shell echo $(SRC_DIR)/*.c)) - -# Sanity check: Make sure at least one source file was found -ifneq ($(strip $(filter %*.c,$(C_SRCS))),) -$(error Failed to find C source files in $(SRC_DIR)) -endif - -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)) - -# Path to file that stores the flags used for LLVMCC. -# If the build flags are changed this should trigger -# a change to the this file which will force a recompile -# of all sources -LLVMCC_FLAGS_FILE := $(LOCAL_BUILD_DIR)/LLVMCC_FLAGS - -# Path to file that stores list of bc files that constitute -# bitcode archive or bitcode module. If the list of bitcode -# files changes this should trigger a rebuild of the bitcode -# archive or module -BC_FILE_LIST_FILE := $(LOCAL_BUILD_DIR)/BC_FILE_LIST - -# All bitcode files have these additional dependencies -$(BC_FILES) : $(ADDITIONAL_BUILD_DEPS) $(LLVMCC_FLAGS_FILE) - -# 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 - -# $(LLVMCC_FLAGS_FILE) depends on `force` which will force the rule to -# rerun every build. However the rule will only update the file when the -# compile flags change which means we will trigger a rebuild when the compile -# flags change. -LLVMCC_FLAGS_FOR_FILE := $(LLVMCC) $(LLVMCC.Flags) $(LLVMCC.Warnings) -$(LLVMCC_FLAGS_FILE): force - $(Verb) $(MKDIR) -p "$(dir $(LLVMCC_FLAGS_FILE))" - $(Verb)echo "$(LLVMCC_FLAGS_FOR_FILE)" | $(CMP) -s - $@ || echo "$(LLVMCC_FLAGS_FOR_FILE)" > $@ - -# $(BC_FILE_LIST_FILE) depends on `force` which will force rule to -# rerun every build. However the rule will only update the file when -# the list of bc files changes which means we should only trigger a rebuild -# or the bitcode archive/module when the list of bc files changes -$(BC_FILE_LIST_FILE): force - $(Verb) $(MKDIR) -p "$(dir $(BC_FILE_LIST_FILE))" - $(Verb)echo "$(BC_FILES_NO_DIR)" | $(CMP) -s - $@ || echo "$(BC_FILES_NO_DIR)" > $@ - -clean:: - @echo "Removing bitcode files" - $(Verb) $(RM) -f $(BC_FILES) - @echo "Removing dependency files" - $(Verb) $(RM) -f $(BC_FILES:.bc=.dep) - -ifdef ARCHIVE_NAME -ARCHIVE_FILE := $(ARCHIVE_DEST)/lib$(ARCHIVE_NAME).bca - -build_at_level:: $(ARCHIVE_FILE) - -# Rule for building LLVM bitcode archive -# NOTE: Dependency on $(BC_FILE_LIST_FILE) is to force -# rebuild when list of BC_FILES changes. -$(ARCHIVE_FILE): $(BC_FILES) $(BC_FILE_LIST_FILE) - $(Verb) $(MKDIR) -p $(ARCHIVE_DEST) - @echo "Creating LLVM archive $@" - $(Verb) $(RM) -f $@ - $(Verb)$(LLVM_AR) rcs $@ $(BC_FILES) - -clean:: - @echo "Removing LLVM bitcode archive $(ARCHIVE_FILE)" - $(Verb) $(RM) -f $(ARCHIVE_FILE) -else -$(error ARCHIVE_NAME must be defined) -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 "BC_FILES_NO_DIR := $(BC_FILES_NO_DIR)" - @echo "BC_FILE_LIST_FILE := $(BC_FILE_LIST_FILE)" - @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_FLAGS_FILE := $(LLVMCC_FLAGS_FILE)" - @echo "LLVMCC.Flags := $(LLVMCC.Flags)" - @echo "LLVMCC.ExtraFlags := $(LLVMCC.ExtraFlags)" - @echo "LLVMCC.Warnings := $(LLVMCC.Warnings)" - @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/CMakeLists.txt b/runtime/POSIX/CMakeLists.txt new file mode 100644 index 00000000..02d06736 --- /dev/null +++ b/runtime/POSIX/CMakeLists.txt @@ -0,0 +1,26 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +# Set up +set(LIB_PREFIX "RuntimePOSIX") +set(SRC_FILES + fd.c + fd_32.c + fd_64.c + fd_init.c + illegal.c + klee_init_env.c + misc.c + selinux.c + stubs.c + ) + +# Build it +include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") +prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files) +add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "-std=gnu89" "") \ No newline at end of file diff --git a/runtime/POSIX/Makefile.cmake.bitcode b/runtime/POSIX/Makefile.cmake.bitcode deleted file mode 100644 index 66e250ff..00000000 --- a/runtime/POSIX/Makefile.cmake.bitcode +++ /dev/null @@ -1,15 +0,0 @@ -#===--------------------------------------------------------*- 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/klee-eh-cxx/CMakeLists.txt b/runtime/klee-eh-cxx/CMakeLists.txt new file mode 100644 index 00000000..e016757b --- /dev/null +++ b/runtime/klee-eh-cxx/CMakeLists.txt @@ -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. +# +#===------------------------------------------------------------------------===# + +set(LIB_PREFIX "eh-cxx") +set(SRC_FILES + klee_eh_cxx.cpp + ) + +set(ADDITIONAL_CXX_FLAGS + -nostdinc++ + -I "${KLEE_LIBCXXABI_SRC_DIR}/src" + -I "${KLEE_LIBCXXABI_SRC_DIR}/include" + -I "${KLEE_LIBCXX_INCLUDE_DIR}" + ) +# Build it +include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") +prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files) +add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "" "${ADDITIONAL_CXX_FLAGS}") \ No newline at end of file diff --git a/runtime/klee-eh-cxx/Makefile.cmake.bitcode b/runtime/klee-eh-cxx/Makefile.cmake.bitcode deleted file mode 100644 index aa314613..00000000 --- a/runtime/klee-eh-cxx/Makefile.cmake.bitcode +++ /dev/null @@ -1,13 +0,0 @@ -include ../Makefile.cmake.bitcode.config - -SRC_DIR=$(ROOT_SRC)/klee-eh-cxx - -ARCHIVE_FILE=$(ARCHIVE_DEST)/libklee-eh-cxx.bca - -all: $(ARCHIVE_FILE) - -klee_eh_cxx.bc: $(SRC_DIR)/klee_eh_cxx.cpp - $(LLVMCXX) -nostdinc++ -emit-llvm -c -I$(KLEE_INCLUDE_DIR) -I $(KLEE_LIBCXXABI_SRC_DIR)/src -I $(KLEE_LIBCXXABI_SRC_DIR)/include -I $(KLEE_LIBCXX_INCLUDE_DIR) $(SRC_DIR)/klee_eh_cxx.cpp -o $@ - -$(ARCHIVE_FILE): klee_eh_cxx.bc - $(LLVM_AR) rcs $@ $< diff --git a/runtime/klee-libc/CMakeLists.txt b/runtime/klee-libc/CMakeLists.txt new file mode 100644 index 00000000..653ebb5a --- /dev/null +++ b/runtime/klee-libc/CMakeLists.txt @@ -0,0 +1,49 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +set(LIB_PREFIX "RuntimeKLEELibc") +set(SRC_FILES + __cxa_atexit.c + abort.c + atexit.c + atoi.c + bcmp.c + calloc.c + htonl.c + memchr.c + mempcpy.c + putchar.c + stpcpy.c + strcat.c + strchr.c + strcmp.c + strcoll.c + strcpy.c + strlen.c + strncmp.c + strncpy.c + strrchr.c + strtol.c + strtoul.c + tolower.c + toupper.c + ) + +# Add __NO_INLINE__ to prevent glibc from using inline definitions of some +# builtins (i.e. putchar and atoi). +set(ADDITIONAL_CC_FLAGS + -D__NO_INLINE__ + -std=gnu89 + ) + +# Build it +include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") +prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files) + +add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "${ADDITIONAL_CC_FLAGS}" "") \ No newline at end of file diff --git a/runtime/klee-libc/Makefile.cmake.bitcode b/runtime/klee-libc/Makefile.cmake.bitcode deleted file mode 100644 index 9902e558..00000000 --- a/runtime/klee-libc/Makefile.cmake.bitcode +++ /dev/null @@ -1,19 +0,0 @@ -#===--------------------------------------------------------*- 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__ - -ARCHIVE_NAME=klee-libc - -include $(LEVEL)/Makefile.cmake.bitcode.rules |