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

29 files changed, 1039 insertions, 0 deletions

diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile
new file mode 100755
index 00000000..bcd61f73
--- /dev/null
+++ b/runtime/klee-libc/Makefile
@@ -0,0 +1,19 @@
+#===-- runtime/klee-libc/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=klee-libc
+DONT_BUILD_RELINKED=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/klee-libc/__cxa_atexit.c b/runtime/klee-libc/__cxa_atexit.c
new file mode 100644
index 00000000..e7982848
--- /dev/null
+++ b/runtime/klee-libc/__cxa_atexit.c
@@ -0,0 +1,49 @@
+//===-- __cxa_atexit.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"
+
+#define MAX_ATEXIT 128
+
+static struct {
+  void (*fn)(void*);
+  void *arg;
+  void *dso_handle;
+} AtExit[MAX_ATEXIT];
+static unsigned NumAtExit = 0;
+
+static void RunAtExit(void) __attribute__((destructor));
+static void RunAtExit(void) {
+  unsigned i;
+
+  for (i=0; i<NumAtExit; ++i)
+    AtExit[i].fn(AtExit[i].arg);
+}
+
+int __cxa_atexit(void (*fn)(void*),
+                 void *arg,
+                 void *dso_handle) {
+  klee_warning_once("FIXME: __cxa_atexit being ignored");
+  
+  /* Better to just report an error here than return 1 (the defined
+   * semantics).
+   */
+  if (NumAtExit == MAX_ATEXIT)
+    klee_report_error(__FILE__,
+                      __LINE__,
+                      "__cxa_atexit: no room in array!",
+                      "exec");
+  
+  AtExit[NumAtExit].fn = fn;
+  AtExit[NumAtExit].arg = arg;
+  ++NumAtExit;
+  
+  return 0;
+}
+
diff --git a/runtime/klee-libc/abort.c b/runtime/klee-libc/abort.c
new file mode 100644
index 00000000..0332d095
--- /dev/null
+++ b/runtime/klee-libc/abort.c
@@ -0,0 +1,16 @@
+//===-- abort.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>
+
+#include "klee/klee.h"
+
+void abort(void) {
+  klee_abort();
+}
diff --git a/runtime/klee-libc/atexit.c b/runtime/klee-libc/atexit.c
new file mode 100644
index 00000000..c71b2cd6
--- /dev/null
+++ b/runtime/klee-libc/atexit.c
@@ -0,0 +1,16 @@
+//===-- atexit.c ----------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+int __cxa_atexit(void (*fn)(void*),
+                 void *arg,
+                 void *dso_handle);
+
+int atexit(void (*fn)(void)) {
+  return __cxa_atexit((void(*)(void*)) fn, 0, 0);
+}
diff --git a/runtime/klee-libc/atoi.c b/runtime/klee-libc/atoi.c
new file mode 100644
index 00000000..ab97bfbb
--- /dev/null
+++ b/runtime/klee-libc/atoi.c
@@ -0,0 +1,37 @@
+/*
+ * Copyright (c) 1988, 1993
+ *	The Regents of the University of California.  All rights reserved.
+ *
+ * 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 <stdlib.h>
+
+int atoi(const char *str) {
+  return (int)strtol(str, (char **)NULL, 10);
+}
diff --git a/runtime/klee-libc/calloc.c b/runtime/klee-libc/calloc.c
new file mode 100644
index 00000000..30b88b30
--- /dev/null
+++ b/runtime/klee-libc/calloc.c
@@ -0,0 +1,46 @@
+//===-- calloc.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>
+#include <string.h>
+
+// DWD - I prefer to be internal
+#if 0
+void *calloc(size_t nmemb, size_t size) {
+	unsigned nbytes = nmemb * size;
+	void *addr = malloc(nbytes);
+	if(addr)
+		memset(addr, 0, nbytes);
+	return addr;
+}
+// Always reallocate.
+void *realloc(void *ptr, size_t nbytes) {
+	if(!ptr)
+		return malloc(nbytes);
+
+	if(!nbytes) {
+		free(ptr);
+		return 0;
+	}
+
+        unsigned copy_nbytes = klee_get_obj_size(ptr);
+	//printf("REALLOC: current object = %d bytes!\n", copy_nbytes);
+
+	void *addr = malloc(nbytes);
+	if(addr) {
+		// shrinking
+		if(copy_nbytes > nbytes)
+			copy_nbytes = nbytes;
+		//printf("REALLOC: copying = %d bytes!\n", copy_nbytes);
+		memcpy(addr, ptr, copy_nbytes);
+		free(ptr);
+	} 
+	return addr;
+}
+#endif
diff --git a/runtime/klee-libc/htonl.c b/runtime/klee-libc/htonl.c
new file mode 100644
index 00000000..cec2d0f5
--- /dev/null
+++ b/runtime/klee-libc/htonl.c
@@ -0,0 +1,49 @@
+//===-- htonl.c -----------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <sys/types.h>
+#include <sys/param.h>
+#include <stdint.h>
+
+#undef htons
+#undef htonl
+#undef ntohs
+#undef ntohl
+
+// Make sure we can recognize the endianness.
+#if (!defined(BYTE_ORDER) || !defined(BIG_ENDIAN) || !defined(LITTLE_ENDIAN))
+#error "Unknown platform endianness!"
+#endif
+
+#if BYTE_ORDER == LITTLE_ENDIAN
+
+uint16_t htons(uint16_t v) {
+  return (v >> 8) | (v << 8);
+}
+uint32_t htonl(uint32_t v) {
+  return htons(v >> 16) | (htons((uint16_t) v) << 16);
+}
+
+#else
+
+uint16_t htons(uint16_t v) {
+  return v;
+}
+uint32_t htonl(uint32_t v) {
+  return v;
+}
+
+#endif
+
+uint16_t ntohs(uint32_t v) {
+  return htons(v);
+}
+uint32_t ntohl(uint32_t v) {
+  return htonl(v);
+}
diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c
new file mode 100644
index 00000000..106b4f89
--- /dev/null
+++ b/runtime/klee-libc/klee-choose.c
@@ -0,0 +1,20 @@
+//===-- klee-choose.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"
+
+unsigned klee_choose(unsigned n) {
+  unsigned x;
+  klee_make_symbolic(&x, sizeof x);
+
+  // NB: this will *not* work if they don't compare to n values.
+  if(x >= n)
+    klee_silent_exit(0);
+  return x;
+}
diff --git a/runtime/klee-libc/memchr.c b/runtime/klee-libc/memchr.c
new file mode 100644
index 00000000..fe0670a7
--- /dev/null
+++ b/runtime/klee-libc/memchr.c
@@ -0,0 +1,54 @@
+/*-
+ * 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>
+
+void *
+memchr(s, c, n)
+	const void *s;
+	int c;
+	size_t n;
+{
+	if (n != 0) {
+		const unsigned char *p = s;
+
+		do {
+			if (*p++ == c)
+				return ((void *)(p - 1));
+		} while (--n != 0);
+	}
+	return (NULL);
+}
diff --git a/runtime/klee-libc/memcmp.c b/runtime/klee-libc/memcmp.c
new file mode 100644
index 00000000..7562f4f7
--- /dev/null
+++ b/runtime/klee-libc/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/klee-libc/memcpy.c b/runtime/klee-libc/memcpy.c
new file mode 100644
index 00000000..14b98ce6
--- /dev/null
+++ b/runtime/klee-libc/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/klee-libc/memmove.c b/runtime/klee-libc/memmove.c
new file mode 100644
index 00000000..c6e1ada9
--- /dev/null
+++ b/runtime/klee-libc/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/klee-libc/mempcpy.c b/runtime/klee-libc/mempcpy.c
new file mode 100644
index 00000000..6327e748
--- /dev/null
+++ b/runtime/klee-libc/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/klee-libc/memset.c b/runtime/klee-libc/memset.c
new file mode 100644
index 00000000..ee9ecb87
--- /dev/null
+++ b/runtime/klee-libc/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;
+}
diff --git a/runtime/klee-libc/putchar.c b/runtime/klee-libc/putchar.c
new file mode 100644
index 00000000..f3fcf01d
--- /dev/null
+++ b/runtime/klee-libc/putchar.c
@@ -0,0 +1,17 @@
+//===-- putchar.c ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <stdio.h>
+#include <unistd.h>
+
+int putchar(int c) {
+  char x = c;
+  write(1, &x, 1);
+  return 1;
+}
diff --git a/runtime/klee-libc/stpcpy.c b/runtime/klee-libc/stpcpy.c
new file mode 100644
index 00000000..1f774f3d
--- /dev/null
+++ b/runtime/klee-libc/stpcpy.c
@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 1999
+ *	David E. O'Brien
+ * Copyright (c) 1988, 1993
+ *	The Regents of the University of California.  All rights reserved.
+ *
+ * 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. 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>
+
+/* Defeat object checking stuff. */
+#undef stpcpy
+
+char *
+stpcpy(char * to, const char * from)
+{
+
+	for (; (*to = *from); ++from, ++to);
+	return(to);
+}
diff --git a/runtime/klee-libc/strcat.c b/runtime/klee-libc/strcat.c
new file mode 100644
index 00000000..195e9460
--- /dev/null
+++ b/runtime/klee-libc/strcat.c
@@ -0,0 +1,47 @@
+/*
+ * Copyright (c) 1988, 1993
+ *	The Regents of the University of California.  All rights reserved.
+ *
+ * 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>
+
+/* Defeat object checking stuff. */
+#undef strcat
+
+char * strcat(char * s, const char * append) {
+	char *save = s;
+
+	for (; *s; ++s)
+		;
+	while ((*s++ = *append++))
+		;
+	return(save);
+}
diff --git a/runtime/klee-libc/strchr.c b/runtime/klee-libc/strchr.c
new file mode 100644
index 00000000..33f97bea
--- /dev/null
+++ b/runtime/klee-libc/strchr.c
@@ -0,0 +1,23 @@
+//===-- strchr.c ----------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+char *strchr(const char *p, int ch) {
+  char c;
+
+  c = ch;
+  for (;; ++p) {
+    if (*p == c) {
+      return ((char *)p);
+    } else if (*p == '\0') {
+      return 0;
+    }
+  }
+  /* NOTREACHED */  
+  return 0;
+}
diff --git a/runtime/klee-libc/strcmp.c b/runtime/klee-libc/strcmp.c
new file mode 100644
index 00000000..6b8c4e85
--- /dev/null
+++ b/runtime/klee-libc/strcmp.c
@@ -0,0 +1,14 @@
+//===-- strcmp.c ----------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+int strcmp(const char *a, const char *b) {
+  while (*a && *a == *b)
+    ++a, ++b;
+  return *a - *b;
+}
diff --git a/runtime/klee-libc/strcoll.c b/runtime/klee-libc/strcoll.c
new file mode 100644
index 00000000..73d59f89
--- /dev/null
+++ b/runtime/klee-libc/strcoll.c
@@ -0,0 +1,15 @@
+//===-- strcoll.c ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <string.h>
+
+// according to the manpage, this is equiv in the POSIX/C locale.
+int strcoll(const char *s1, const char *s2) {
+  return strcmp(s1,s2);
+}
diff --git a/runtime/klee-libc/strcpy.c b/runtime/klee-libc/strcpy.c
new file mode 100644
index 00000000..0fbaf9a7
--- /dev/null
+++ b/runtime/klee-libc/strcpy.c
@@ -0,0 +1,17 @@
+//===-- strcpy.c ----------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+char *strcpy(char *to, const char *from) {
+  char *start = to;
+
+  while ((*to = *from))
+    ++to, ++from;
+
+  return start;
+}
diff --git a/runtime/klee-libc/strlen.c b/runtime/klee-libc/strlen.c
new file mode 100644
index 00000000..e298410c
--- /dev/null
+++ b/runtime/klee-libc/strlen.c
@@ -0,0 +1,17 @@
+//===-- strlen.c ----------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <string.h>
+
+size_t strlen(const char *str) {
+  const char *s = str;
+  while (*s)
+    ++s;
+  return s - str;
+}
diff --git a/runtime/klee-libc/strncmp.c b/runtime/klee-libc/strncmp.c
new file mode 100644
index 00000000..a8dc3749
--- /dev/null
+++ b/runtime/klee-libc/strncmp.c
@@ -0,0 +1,49 @@
+/*
+ * Copyright (c) 1989, 1993
+ *	The Regents of the University of California.  All rights reserved.
+ *
+ * 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 <stdlib.h>
+
+int strncmp(const char *s1, const char *s2, size_t n)
+{
+
+	if (n == 0)
+		return (0);
+	do {
+		if (*s1 != *s2++)
+			return (*(unsigned char *)s1 -
+				*(unsigned char *)(s2 - 1));
+		if (*s1++ == 0)
+			break;
+	} while (--n != 0);
+	return (0);
+}
diff --git a/runtime/klee-libc/strncpy.c b/runtime/klee-libc/strncpy.c
new file mode 100644
index 00000000..62ab7993
--- /dev/null
+++ b/runtime/klee-libc/strncpy.c
@@ -0,0 +1,58 @@
+/*-
+ * 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 <stdlib.h>
+/*
+ * Copy src to dst, truncating or null-padding to always copy n bytes.
+ * Return dst.
+ */
+char * strncpy(char * dst, const char * src, size_t n)
+{
+	if (n != 0) {
+		char *d = dst;
+		const char *s = src;
+
+		do {
+			if ((*d++ = *s++) == 0) {
+				/* NUL pad the remaining n-1 bytes */
+				while (--n != 0)
+					*d++ = 0;
+				break;
+			}
+		} while (--n != 0);
+	}
+	return (dst);
+}
diff --git a/runtime/klee-libc/strrchr.c b/runtime/klee-libc/strrchr.c
new file mode 100644
index 00000000..01128b48
--- /dev/null
+++ b/runtime/klee-libc/strrchr.c
@@ -0,0 +1,21 @@
+//===-- strrchr.c ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <string.h>
+
+char *strrchr(const char *t, int c) {
+  char ch;
+  const char *l=0;
+
+  ch = c;
+  for (;;) {
+    if (*t == ch) l=t; if (!*t) return (char*)l; ++t;
+  }
+  return (char*)l;
+}
diff --git a/runtime/klee-libc/strtol.c b/runtime/klee-libc/strtol.c
new file mode 100644
index 00000000..3be7fff3
--- /dev/null
+++ b/runtime/klee-libc/strtol.c
@@ -0,0 +1,135 @@
+/*-
+ * Copyright (c) 1990, 1993
+ *	The Regents of the University of California.  All rights reserved.
+ *
+ * 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 <limits.h>
+#include <ctype.h>
+#include <errno.h>
+#include <stdlib.h>
+
+
+/*
+ * Convert a string to a long integer.
+ *
+ * Assumes that the upper and lower case
+ * alphabets and digits are each contiguous.
+ */
+long
+strtol(const char * nptr, char ** endptr, int base)
+{
+	const char *s;
+	unsigned long acc;
+	char c;
+	unsigned long cutoff;
+	int neg, any, cutlim;
+
+	/*
+	 * Skip white space and pick up leading +/- sign if any.
+	 * If base is 0, allow 0x for hex and 0 for octal, else
+	 * assume decimal; if base is already 16, allow 0x.
+	 */
+	s = nptr;
+	do {
+		c = *s++;
+	} while (isspace((unsigned char)c));
+	if (c == '-') {
+		neg = 1;
+		c = *s++;
+	} else {
+		neg = 0;
+		if (c == '+')
+			c = *s++;
+	}
+	if ((base == 0 || base == 16) &&
+	    c == '0' && (*s == 'x' || *s == 'X')) {
+		c = s[1];
+		s += 2;
+		base = 16;
+	}
+	if (base == 0)
+		base = c == '0' ? 8 : 10;
+	acc = any = 0;
+	if (base < 2 || base > 36)
+		goto noconv;
+
+	/*
+	 * Compute the cutoff value between legal numbers and illegal
+	 * numbers.  That is the largest legal value, divided by the
+	 * base.  An input number that is greater than this value, if
+	 * followed by a legal input character, is too big.  One that
+	 * is equal to this value may be valid or not; the limit
+	 * between valid and invalid numbers is then based on the last
+	 * digit.  For instance, if the range for longs is
+	 * [-2147483648..2147483647] and the input base is 10,
+	 * cutoff will be set to 214748364 and cutlim to either
+	 * 7 (neg==0) or 8 (neg==1), meaning that if we have accumulated
+	 * a value > 214748364, or equal but the next digit is > 7 (or 8),
+	 * the number is too big, and we will return a range error.
+	 *
+	 * Set 'any' if any `digits' consumed; make it negative to indicate
+	 * overflow.
+	 */
+	cutoff = neg ? (unsigned long)-(LONG_MIN + LONG_MAX) + LONG_MAX
+	    : LONG_MAX;
+	cutlim = cutoff % base;
+	cutoff /= base;
+	for ( ; ; c = *s++) {
+		if (c >= '0' && c <= '9')
+			c -= '0';
+		else if (c >= 'A' && c <= 'Z')
+			c -= 'A' - 10;
+		else if (c >= 'a' && c <= 'z')
+			c -= 'a' - 10;
+		else
+			break;
+		if (c >= base)
+			break;
+		if (any < 0 || acc > cutoff || (acc == cutoff && c > cutlim))
+			any = -1;
+		else {
+			any = 1;
+			acc *= base;
+			acc += c;
+		}
+	}
+	if (any < 0) {
+		acc = neg ? LONG_MIN : LONG_MAX;
+		errno = ERANGE;
+	} else if (!any) {
+noconv:
+		errno = EINVAL;
+	} else if (neg)
+		acc = -acc;
+	if (endptr != NULL)
+		*endptr = (char *)(any ? s - 1 : nptr);
+	return (acc);
+}
diff --git a/runtime/klee-libc/strtoul.c b/runtime/klee-libc/strtoul.c
new file mode 100644
index 00000000..f23d5b54
--- /dev/null
+++ b/runtime/klee-libc/strtoul.c
@@ -0,0 +1,113 @@
+/*
+ * Copyright (c) 1990, 1993
+ *	The Regents of the University of California.  All rights reserved.
+ *
+ * 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 <limits.h>
+#include <ctype.h>
+#include <errno.h>
+#include <stdlib.h>
+
+/*
+ * Convert a string to an unsigned long integer.
+ *
+ * Assumes that the upper and lower case
+ * alphabets and digits are each contiguous.
+ */
+unsigned long
+strtoul(const char * nptr, char ** endptr, int base)
+{
+	const char *s;
+	unsigned long acc;
+	char c;
+	unsigned long cutoff;
+	int neg, any, cutlim;
+
+	/*
+	 * See strtol for comments as to the logic used.
+	 */
+	s = nptr;
+	do {
+		c = *s++;
+	} while (isspace((unsigned char)c));
+	if (c == '-') {
+		neg = 1;
+		c = *s++;
+	} else {
+		neg = 0;
+		if (c == '+')
+			c = *s++;
+	}
+	if ((base == 0 || base == 16) &&
+	    c == '0' && (*s == 'x' || *s == 'X')) {
+		c = s[1];
+		s += 2;
+		base = 16;
+	}
+	if (base == 0)
+		base = c == '0' ? 8 : 10;
+	acc = any = 0;
+	if (base < 2 || base > 36)
+		goto noconv;
+
+	cutoff = ULONG_MAX / base;
+	cutlim = ULONG_MAX % base;
+	for ( ; ; c = *s++) {
+		if (c >= '0' && c <= '9')
+			c -= '0';
+		else if (c >= 'A' && c <= 'Z')
+			c -= 'A' - 10;
+		else if (c >= 'a' && c <= 'z')
+			c -= 'a' - 10;
+		else
+			break;
+		if (c >= base)
+			break;
+		if (any < 0 || acc > cutoff || (acc == cutoff && c > cutlim))
+			any = -1;
+		else {
+			any = 1;
+			acc *= base;
+			acc += c;
+		}
+	}
+	if (any < 0) {
+		acc = ULONG_MAX;
+		errno = ERANGE;
+	} else if (!any) {
+noconv:
+		errno = EINVAL;
+	} else if (neg)
+		acc = -acc;
+	if (endptr != NULL)
+		*endptr = (char *)(any ? s - 1 : nptr);
+	return (acc);
+}
diff --git a/runtime/klee-libc/tolower.c b/runtime/klee-libc/tolower.c
new file mode 100644
index 00000000..265f5deb
--- /dev/null
+++ b/runtime/klee-libc/tolower.c
@@ -0,0 +1,14 @@
+//===-- tolower.c ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+int tolower(int ch) {
+  if ( (unsigned int)(ch - 'A') < 26u )
+    ch -= 'A' - 'a';
+  return ch;
+}
diff --git a/runtime/klee-libc/toupper.c b/runtime/klee-libc/toupper.c
new file mode 100644
index 00000000..37e5f9d6
--- /dev/null
+++ b/runtime/klee-libc/toupper.c
@@ -0,0 +1,14 @@
+//===-- toupper.c ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+int toupper(int ch) {
+  if ( (unsigned int)(ch - 'a') < 26u )
+    ch += 'A' - 'a';
+  return ch;
+}