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, 134 insertions, 0 deletions

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/FreeStanding/memcmp.c b/runtime/FreeStanding/memcmp.c
new file mode 100644
index 00000000..566daf48
--- /dev/null
+++ b/runtime/FreeStanding/memcmp.c
@@ -0,0 +1,53 @@
+/*-
+ * 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/FreeStanding/memcpy.c b/runtime/FreeStanding/memcpy.c
new file mode 100644
index 00000000..c7c6e6d3
--- /dev/null
+++ b/runtime/FreeStanding/memcpy.c
@@ -0,0 +1,19 @@
+/*===-- 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/FreeStanding/memmove.c b/runtime/FreeStanding/memmove.c
new file mode 100644
index 00000000..ee0e53ae
--- /dev/null
+++ b/runtime/FreeStanding/memmove.c
@@ -0,0 +1,30 @@
+/*===-- 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/FreeStanding/memset.c b/runtime/FreeStanding/memset.c
new file mode 100644
index 00000000..b439001e
--- /dev/null
+++ b/runtime/FreeStanding/memset.c
@@ -0,0 +1,17 @@
+/*===-- 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;
+}