Reorganise runtime libraries provided by KLEE

Strictly differentiate between the following type of libraries:

* FreeStanding: contains minimal amount of methods a compiler would expect
* klee-libc: contains a minimal libc implementation
* POSIX: contains a POSIX layer that can be used on top of a libc implementation
* Intrinsic: contains additional runtime functions which provide KLEE-specific functionalities, (e.g. checks)

Builds always archives instead of single modules.
This allows to reduce linked-in dependencies of tested applications.

14 files changed, 38 insertions, 134 deletions

diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt
index 2a056d9f..53a2f838 100644
--- a/runtime/CMakeLists.txt
+++ b/runtime/CMakeLists.txt
@@ -26,17 +26,6 @@ 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()
@@ -55,7 +44,7 @@ configure_file("Makefile.cmake.bitcode.rules" "Makefile.cmake.bitcode.rules" COP
 
 # Makefile for root runtime directory
 # Copy over makefiles for libraries
-set(BITCODE_LIBRARIES "Intrinsic" "klee-libc")
+set(BITCODE_LIBRARIES "Intrinsic" "klee-libc" "FreeStanding")
 if (ENABLE_POSIX_RUNTIME)
   list(APPEND BITCODE_LIBRARIES "POSIX")
 endif()
@@ -130,19 +119,11 @@ add_dependencies(clean_all clean_runtime)
 ###############################################################################
 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()
+list(APPEND RUNTIME_FILES_TO_INSTALL
+  "${KLEE_RUNTIME_DIRECTORY}/kleeRuntimeIntrinsic.bc"
+  "${KLEE_RUNTIME_DIRECTORY}/klee-libc.bc"
+  "${KLEE_RUNTIME_DIRECTORY}/kleeRuntimeFreeStanding.bc"
+  )
 
 if (ENABLE_POSIX_RUNTIME)
   list(APPEND RUNTIME_FILES_TO_INSTALL
diff --git a/runtime/FreeStanding/Makefile.cmake.bitcode b/runtime/FreeStanding/Makefile.cmake.bitcode
new file mode 100644
index 00000000..0ad434d6
--- /dev/null
+++ b/runtime/FreeStanding/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=kleeRuntimeFreeStanding
+
+include $(LEVEL)/Makefile.cmake.bitcode.rules
diff --git a/runtime/klee-libc/memcmp.c b/runtime/FreeStanding/memcmp.c
index 7562f4f7..566daf48 100644
--- a/runtime/klee-libc/memcmp.c
+++ b/runtime/FreeStanding/memcmp.c
@@ -42,7 +42,7 @@
 int memcmp(const void *s1, const void *s2, size_t n) {
   if (n != 0) {
     const unsigned char *p1 = s1, *p2 = s2;
-    
+
     do {
       if (*p1++ != *p2++) {
         return (*--p1 - *--p2);
diff --git a/runtime/klee-libc/memcpy.c b/runtime/FreeStanding/memcpy.c
index c7c6e6d3..c7c6e6d3 100644
--- a/runtime/klee-libc/memcpy.c
+++ b/runtime/FreeStanding/memcpy.c
diff --git a/runtime/klee-libc/memmove.c b/runtime/FreeStanding/memmove.c
index 3e86de02..ee0e53ae 100644
--- a/runtime/klee-libc/memmove.c
+++ b/runtime/FreeStanding/memmove.c
@@ -16,12 +16,14 @@ void *memmove(void *dst, const void *src, size_t count) {
   if (src == dst)
     return dst;
 
-  if (src>dst) {
-    while (count--) *a++ = *b++;
+  if (src > dst) {
+    while (count--)
+      *a++ = *b++;
   } else {
-    a+=count-1;
-    b+=count-1;
-    while (count--) *a-- = *b--;
+    a += count - 1;
+    b += count - 1;
+    while (count--)
+      *a-- = *b--;
   }
 
   return dst;
diff --git a/runtime/klee-libc/memset.c b/runtime/FreeStanding/memset.c
index 81025d32..b439001e 100644
--- a/runtime/klee-libc/memset.c
+++ b/runtime/FreeStanding/memset.c
@@ -9,9 +9,9 @@
 
 #include <stdlib.h>
 
-void *memset(void * dst, int s, size_t count) {
-    char * a = dst;
-    while (count-- > 0)
-      *a++ = s;
-    return dst;
+void *memset(void *dst, int s, size_t count) {
+  char *a = dst;
+  while (count-- > 0)
+    *a++ = s;
+  return dst;
 }
diff --git a/runtime/Intrinsic/Makefile.cmake.bitcode b/runtime/Intrinsic/Makefile.cmake.bitcode
index 654ee020..77727fb4 100644
--- a/runtime/Intrinsic/Makefile.cmake.bitcode
+++ b/runtime/Intrinsic/Makefile.cmake.bitcode
@@ -10,13 +10,6 @@ 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
+ARCHIVE_NAME=kleeRuntimeIntrinsic
 
 include $(LEVEL)/Makefile.cmake.bitcode.rules
diff --git a/runtime/Intrinsic/memcpy.c b/runtime/Intrinsic/memcpy.c
deleted file mode 100644
index bd9f3e38..00000000
--- a/runtime/Intrinsic/memcpy.c
+++ /dev/null
@@ -1,19 +0,0 @@
-//===-- memcpy.c ----------------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include <stdlib.h>
-
-__attribute__((weak)) void *memcpy(void *destaddr, void const *srcaddr, size_t len) {
-  char *dest = destaddr;
-  char const *src = srcaddr;
-
-  while (len-- > 0)
-    *dest++ = *src++;
-  return destaddr;
-}
diff --git a/runtime/Intrinsic/memmove.c b/runtime/Intrinsic/memmove.c
deleted file mode 100644
index e89abf7d..00000000
--- a/runtime/Intrinsic/memmove.c
+++ /dev/null
@@ -1,28 +0,0 @@
-//===-- memmove.c ---------------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include <stdlib.h>
-
-__attribute__((weak)) void *memmove(void *dst, const void *src, size_t count) {
-  char *a = dst;
-  const char *b = src;
-
-  if (src == dst)
-    return dst;
-
-  if (src>dst) {
-    while (count--) *a++ = *b++;
-  } else {
-    a+=count-1;
-    b+=count-1;
-    while (count--) *a-- = *b--;
-  }
-
-  return dst;
-}
diff --git a/runtime/Intrinsic/mempcpy.c b/runtime/Intrinsic/mempcpy.c
deleted file mode 100644
index e47a94b1..00000000
--- a/runtime/Intrinsic/mempcpy.c
+++ /dev/null
@@ -1,18 +0,0 @@
-//===-- mempcpy.c ---------------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include <stdlib.h>
-__attribute__((weak)) void *mempcpy(void *destaddr, void const *srcaddr, size_t len) {
-  char *dest = destaddr;
-  char const *src = srcaddr;
-
-  while (len-- > 0)
-    *dest++ = *src++;
-  return dest;
-}
diff --git a/runtime/Intrinsic/memset.c b/runtime/Intrinsic/memset.c
deleted file mode 100644
index c21f1fa9..00000000
--- a/runtime/Intrinsic/memset.c
+++ /dev/null
@@ -1,16 +0,0 @@
-//===-- memset.c ----------------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include <stdlib.h>
-__attribute__ ((weak)) void *memset(void * dst, int s, size_t count) {
-    volatile char * a = dst;
-    while (count-- > 0)
-      *a++ = s;
-    return dst;
-}
diff --git a/runtime/Makefile.cmake.bitcode b/runtime/Makefile.cmake.bitcode
index 94f8a60d..03da435e 100644
--- a/runtime/Makefile.cmake.bitcode
+++ b/runtime/Makefile.cmake.bitcode
@@ -11,6 +11,8 @@ include $(LEVEL)/Makefile.cmake.bitcode.config
 
 DIRS += Intrinsic
 DIRS += klee-libc
+DIRS += FreeStanding
+
 ifneq ($(ENABLE_POSIX_RUNTIME),0)
 	DIRS += POSIX
 endif
diff --git a/runtime/Makefile.cmake.bitcode.config.in b/runtime/Makefile.cmake.bitcode.config.in
index 5efa0154..5d1931b8 100644
--- a/runtime/Makefile.cmake.bitcode.config.in
+++ b/runtime/Makefile.cmake.bitcode.config.in
@@ -33,9 +33,6 @@ 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
diff --git a/runtime/klee-libc/Makefile.cmake.bitcode b/runtime/klee-libc/Makefile.cmake.bitcode
index 6e85952c..9902e558 100644
--- a/runtime/klee-libc/Makefile.cmake.bitcode
+++ b/runtime/klee-libc/Makefile.cmake.bitcode
@@ -14,11 +14,6 @@ include $(LEVEL)/Makefile.cmake.bitcode.config
 # 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
+ARCHIVE_NAME=klee-libc
 
 include $(LEVEL)/Makefile.cmake.bitcode.rules