[cmake] Add support to generate arbitrary runtime library configurations

Every runtime library can be build with multiple configurations.

Replace the Makefile-based setup by cmake one.
Currently, we generate 32bit and 64bit libraries simultaneously and can link against them.

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