Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

9 files changed, 182 insertions, 0 deletions

diff --git a/runtime/Intrinsic/Makefile b/runtime/Intrinsic/Makefile
new file mode 100644
index 00000000..ce4a34ba
--- /dev/null
+++ b/runtime/Intrinsic/Makefile
@@ -0,0 +1,20 @@
+#===-- runtime/Intrinsic/Makefile --------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+LEVEL=../..
+
+LIBRARYNAME=intrinsic
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
+BYTECODE_LIBRARY=1
+# Don't strip debug info from the module.
+DEBUG_RUNTIME=1
+NO_PEDANTIC=1
+
+include $(LEVEL)/Makefile.common
diff --git a/runtime/Intrinsic/klee_div_zero_check.c b/runtime/Intrinsic/klee_div_zero_check.c
new file mode 100644
index 00000000..3fde1af5
--- /dev/null
+++ b/runtime/Intrinsic/klee_div_zero_check.c
@@ -0,0 +1,15 @@
+//===-- klee_div_zero_check.c ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <klee/klee.h>
+
+void klee_div_zero_check(long long z) {
+  if (z == 0)
+    klee_report_error(__FILE__, __LINE__, "divide by zero", "div.err");
+}
diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c
new file mode 100644
index 00000000..88ec5026
--- /dev/null
+++ b/runtime/Intrinsic/klee_int.c
@@ -0,0 +1,17 @@
+//===-- klee_int.c --------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <assert.h>
+#include <klee/klee.h>
+
+int klee_int(const char *name) {
+  int x;
+  klee_make_symbolic_name(&x, sizeof x, name);
+  return x;
+}
diff --git a/runtime/Intrinsic/klee_make_symbolic.c b/runtime/Intrinsic/klee_make_symbolic.c
new file mode 100644
index 00000000..b9dec2a7
--- /dev/null
+++ b/runtime/Intrinsic/klee_make_symbolic.c
@@ -0,0 +1,14 @@
+//===-- klee_make_symbolic.c ----------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <klee/klee.h>
+
+void klee_make_symbolic(void *addr, unsigned nbytes) {
+  klee_make_symbolic_name(addr, nbytes, "unnamed");
+}
diff --git a/runtime/Intrinsic/klee_range.c b/runtime/Intrinsic/klee_range.c
new file mode 100644
index 00000000..59d1a05e
--- /dev/null
+++ b/runtime/Intrinsic/klee_range.c
@@ -0,0 +1,33 @@
+//===-- klee_range.c ------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <assert.h>
+#include <klee/klee.h>
+
+int klee_range(int start, int end, const char* name) {
+  int x;
+
+  assert(start < end);
+
+  if (start+1==end) {
+    return start;
+  } else {
+    klee_make_symbolic_name(&x, sizeof x, name); 
+
+    /* Make nicer constraint when simple... */
+    if (start==0) {
+      klee_assume((unsigned) x < (unsigned) end);
+    } else {
+      klee_assume(start <= x);
+      klee_assume(x < end);
+    }
+
+    return x;
+  }
+}
diff --git a/runtime/Intrinsic/memcpy.c b/runtime/Intrinsic/memcpy.c
new file mode 100644
index 00000000..14b98ce6
--- /dev/null
+++ b/runtime/Intrinsic/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, unsigned int 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
new file mode 100644
index 00000000..c6e1ada9
--- /dev/null
+++ b/runtime/Intrinsic/memmove.c
@@ -0,0 +1,28 @@
+//===-- 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/Intrinsic/mempcpy.c b/runtime/Intrinsic/mempcpy.c
new file mode 100644
index 00000000..6327e748
--- /dev/null
+++ b/runtime/Intrinsic/mempcpy.c
@@ -0,0 +1,19 @@
+//===-- 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>
+
+void *mempcpy(void *destaddr, void const *srcaddr, unsigned int 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
new file mode 100644
index 00000000..ee9ecb87
--- /dev/null
+++ b/runtime/Intrinsic/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;
+}