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.

5 files changed, 1 insertions, 123 deletions

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
diff --git a/runtime/klee-libc/memcmp.c b/runtime/klee-libc/memcmp.c
deleted file mode 100644
index 7562f4f7..00000000
--- a/runtime/klee-libc/memcmp.c
+++ /dev/null
@@ -1,53 +0,0 @@
-/*-
- * Copyright (c) 1990, 1993
- *	The Regents of the University of California.  All rights reserved.
- *
- * This code is derived from software contributed to Berkeley by
- * Chris Torek.
- *
- * Redistribution and use in source and binary forms, with or without
- * modification, are permitted provided that the following conditions
- * are met:
- * 1. Redistributions of source code must retain the above copyright
- *    notice, this list of conditions and the following disclaimer.
- * 2. Redistributions in binary form must reproduce the above copyright
- *    notice, this list of conditions and the following disclaimer in the
- *    documentation and/or other materials provided with the distribution.
- * 3. All advertising materials mentioning features or use of this software
- *    must display the following acknowledgement:
- *	This product includes software developed by the University of
- *	California, Berkeley and its contributors.
- * 4. Neither the name of the University nor the names of its contributors
- *    may be used to endorse or promote products derived from this software
- *    without specific prior written permission.
- *
- * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND
- * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
- * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
- * ARE DISCLAIMED.  IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE
- * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
- * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
- * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
- * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
- * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
- * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
- * SUCH DAMAGE.
- */
-
-#include <string.h>
-
-/*
- * Compare memory regions.
- */
-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);
-      }
-    } while (--n != 0);
-  }
-  return (0);
-}
diff --git a/runtime/klee-libc/memcpy.c b/runtime/klee-libc/memcpy.c
deleted file mode 100644
index c7c6e6d3..00000000
--- a/runtime/klee-libc/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>
-
-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/klee-libc/memmove.c b/runtime/klee-libc/memmove.c
deleted file mode 100644
index 3e86de02..00000000
--- a/runtime/klee-libc/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>
-
-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/klee-libc/memset.c b/runtime/klee-libc/memset.c
deleted file mode 100644
index 81025d32..00000000
--- a/runtime/klee-libc/memset.c
+++ /dev/null
@@ -1,17 +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>
-
-void *memset(void * dst, int s, size_t count) {
-    char * a = dst;
-    while (count-- > 0)
-      *a++ = s;
-    return dst;
-}