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

16 files changed, 2853 insertions, 0 deletions

diff --git a/runtime/POSIX/Makefile b/runtime/POSIX/Makefile
new file mode 100644
index 00000000..9a42f5c0
--- /dev/null
+++ b/runtime/POSIX/Makefile
@@ -0,0 +1,20 @@
+#===-- runtime/POSIX/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=kleeRuntimePOSIX
+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/POSIX/fd.c b/runtime/POSIX/fd.c
new file mode 100644
index 00000000..367a8c4a
--- /dev/null
+++ b/runtime/POSIX/fd.c
@@ -0,0 +1,1287 @@
+//===-- fd.c --------------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#define _LARGEFILE64_SOURCE
+#include "fd.h"
+
+#include <string.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <errno.h>
+#include <sys/syscall.h>
+#include <sys/stat.h>
+#include <sys/types.h>
+#include <fcntl.h>
+#include <stdarg.h>
+#include <assert.h>
+#include <sys/vfs.h>
+#include <unistd.h>
+#include <dirent.h>
+#include <sys/ioctl.h>
+#include <sys/mtio.h>
+#include <termios.h>
+#include <sys/select.h>
+#include <klee/klee.h>
+
+/* #define DEBUG */
+
+void klee_warning(const char*);
+void klee_warning_once(const char*);
+int klee_get_errno(void);
+
+/* Returns pointer to the symbolic file structure is the pathname is symbolic */
+static exe_disk_file_t *__get_sym_file(const char *pathname) {
+  char c = pathname[0];
+  unsigned i;
+
+  if (c == 0 || pathname[1] != 0)
+    return NULL;
+
+  for (i=0; i<__exe_fs.n_sym_files; ++i) {
+    if (c == 'A' + (char) i) {
+      exe_disk_file_t *df = &__exe_fs.sym_files[i];
+      if (df->stat->st_ino == 0)
+        return NULL;
+      return df;
+    }
+  }
+  
+  return NULL;
+}
+
+static void *__concretize_ptr(const void *p);
+static size_t __concretize_size(size_t s);
+static const char *__concretize_string(const char *s);
+
+/* Returns pointer to the file entry for a valid fd */
+static exe_file_t *__get_file(int fd) {
+  if (fd>=0 && fd<MAX_FDS) {
+    exe_file_t *f = &__exe_env.fds[fd];
+    if (f->flags & eOpen)
+      return f;
+  }
+
+  return 0;
+}
+
+int access(const char *pathname, int mode) {
+  exe_disk_file_t *dfile = __get_sym_file(pathname);
+  
+  if (dfile) {
+    /* XXX we should check against stat values but we also need to
+       enforce in open and friends then. */
+    return 0;
+  } else {
+    int r = syscall(__NR_access, __concretize_string(pathname), mode);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  } 
+}
+
+mode_t umask(mode_t mask) {  
+  mode_t r = __exe_env.umask;
+  __exe_env.umask = mask & 0777;
+  return r;
+}
+
+
+/* Returns 1 if the process has the access rights specified by 'flags'
+   to the file with stat 's'.  Returns 0 otherwise*/
+static int has_permission(int flags, struct stat64 *s) {
+  int write_access, read_access;
+  mode_t mode = s->st_mode;
+  
+  if (flags & O_RDONLY || flags & O_RDWR)
+    read_access = 1;
+  else read_access = 0;
+
+  if (flags & O_WRONLY || flags & O_RDWR)
+    write_access = 1;
+  else write_access = 0;
+
+  /* XXX: We don't worry about process uid and gid for now. 
+     We allow access if any user has access to the file. */
+#if 0
+  uid_t uid = s->st_uid;
+  uid_t euid = geteuid();
+  gid_t gid = s->st_gid;
+  gid_t egid = getegid();
+#endif  
+
+  if (read_access && ((mode & S_IRUSR) | (mode & S_IRGRP) | (mode & S_IROTH)))
+    return 0;
+
+  if (write_access && !((mode & S_IWUSR) | (mode & S_IWGRP) | (mode & S_IWOTH)))
+    return 0;
+
+  return 1;
+}
+
+
+int __fd_open(const char *pathname, int flags, mode_t mode) {
+  exe_disk_file_t *df;
+  exe_file_t *f;
+  int fd;
+
+  for (fd = 0; fd < MAX_FDS; ++fd)
+    if (!(__exe_env.fds[fd].flags & eOpen))
+      break;
+  if (fd == MAX_FDS) {
+    errno = EMFILE;
+    return -1;
+  }
+  
+  f = &__exe_env.fds[fd];
+
+  /* Should be the case if file was available, but just in case. */
+  memset(f, 0, sizeof *f);
+
+  df = __get_sym_file(pathname); 
+  if (df) {    
+    /* XXX Should check access against mode / stat / possible
+       deletion. */
+    f->dfile = df;
+    
+    if ((flags & O_CREAT) && (flags & O_EXCL)) {
+      errno = EEXIST;
+      return -1;
+    }
+    
+    if ((flags & O_TRUNC) && (flags & O_RDONLY)) {
+      /* The result of using O_TRUNC with O_RDONLY is undefined, so we
+	 return error */
+      fprintf(stderr, "Undefined call to open(): O_TRUNC | O_RDONLY\n");
+      errno = EACCES;
+      return -1;
+    }
+
+    if ((flags & O_EXCL) && !(flags & O_CREAT)) {
+      /* The result of using O_EXCL without O_CREAT is undefined, so
+	 we return error */
+      fprintf(stderr, "Undefined call to open(): O_EXCL w/o O_RDONLY\n");
+      errno = EACCES;
+      return -1;
+    }
+
+    if (!has_permission(flags, df->stat)) {
+	errno = EACCES;
+	return -1;
+    }
+    else
+      f->dfile->stat->st_mode = ((f->dfile->stat->st_mode & ~0777) |
+				 (mode & ~__exe_env.umask));
+  } else {    
+    int os_fd = syscall(__NR_open, __concretize_string(pathname), flags, mode);
+    if (os_fd == -1) {
+      errno = klee_get_errno();
+      return -1;
+    }
+    f->fd = os_fd;
+  }
+  
+  f->flags = eOpen;
+  if ((flags & O_ACCMODE) == O_RDONLY) {
+    f->flags |= eReadable;
+  } else if ((flags & O_ACCMODE) == O_WRONLY) {
+    f->flags |= eWriteable;
+  } else { /* XXX What actually happens here if != O_RDWR. */
+    f->flags |= eReadable | eWriteable;
+  }
+  
+  return fd;
+}
+
+int close(int fd) {
+  static int n_calls = 0;
+  exe_file_t *f;
+  int r = 0;
+  
+  n_calls++;  
+
+  f = __get_file(fd);
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  } 
+
+  if (__exe_fs.max_failures && *__exe_fs.close_fail == n_calls) {
+    __exe_fs.max_failures--;
+    errno = EIO;
+    return -1;
+  }
+
+#if 0
+  if (!f->dfile) {
+    /* if a concrete fd */
+    r = syscall(__NR_close, f->fd);
+  }
+  else r = 0;
+#endif
+
+  memset(f, 0, sizeof *f);
+  
+  return r;
+}
+
+ssize_t read(int fd, void *buf, size_t count) {
+  static int n_calls = 0;
+  exe_file_t *f;
+
+  n_calls++;
+
+  if (count == 0) 
+    return 0;
+
+  if (buf == NULL) {
+    errno = EFAULT;
+    return -1;
+  }
+  
+  f = __get_file(fd);
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }  
+
+  if (__exe_fs.max_failures && *__exe_fs.read_fail == n_calls) {
+    __exe_fs.max_failures--;
+    errno = EIO;
+    return -1;
+  }
+  
+  if (!f->dfile) {
+    /* concrete file */
+    int r;
+    buf = __concretize_ptr(buf);
+    count = __concretize_size(count);
+    /* XXX In terms of looking for bugs we really should do this check
+       before concretization, at least once the routine has been fixed
+       to properly work with symbolics. */
+    klee_check_memory_access(buf, count);
+    if (f->fd == 0)
+      r = syscall(__NR_read, f->fd, buf, count);
+    else
+      r = syscall(__NR_pread64, f->fd, buf, count, (off64_t) f->off);
+
+    if (r == -1) {
+      errno = klee_get_errno();
+      return -1;
+    }
+    
+    if (f->fd != 0)
+      f->off += r;
+    return r;
+  }
+  else {
+    assert(f->off >= 0);
+    if (f->dfile->size < f->off)
+      return 0;
+
+    /* symbolic file */
+    if (f->off + count > f->dfile->size) {
+      count = f->dfile->size - f->off;
+    }
+    
+    memcpy(buf, f->dfile->contents + f->off, count);
+    f->off += count;
+    
+    return count;
+  }
+}
+
+
+ssize_t write(int fd, const void *buf, size_t count) {
+  static int n_calls = 0;
+  exe_file_t *f;
+
+  n_calls++;
+
+  f = __get_file(fd);
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+
+  if (__exe_fs.max_failures && *__exe_fs.write_fail == n_calls) {
+    __exe_fs.max_failures--;
+    errno = EIO;
+    return -1;
+  }
+
+  if (!f->dfile) {
+    int r;
+
+    buf = __concretize_ptr(buf);
+    count = __concretize_size(count);
+    /* XXX In terms of looking for bugs we really should do this check
+       before concretization, at least once the routine has been fixed
+       to properly work with symbolics. */
+    klee_check_memory_access(buf, count);
+    if (f->fd == 1 || f->fd == 2)
+      r = syscall(__NR_write, f->fd, buf, count);
+    else r = syscall(__NR_pwrite64, f->fd, buf, count, (off64_t) f->off);
+    
+    if (r == -1) {
+      errno = klee_get_errno();
+      return -1;
+    }
+    
+    assert(r >= 0);
+    if (f->fd != 1 && f->fd != 2)
+      f->off += r;
+
+    return r;
+  }
+  else {
+    /* symbolic file */    
+    size_t actual_count = 0;
+    if (f->off + count <= f->dfile->size)
+      actual_count = count;
+    else {
+      if (__exe_env.save_all_writes)
+	assert(0);
+      else {
+	if (f->off < f->dfile->size)
+	  actual_count = f->dfile->size - f->off;	
+      }
+    }
+    
+    if (actual_count)
+      memcpy(f->dfile->contents + f->off, buf, actual_count);
+    
+    if (count != actual_count)
+      fprintf(stderr, "WARNING: write() ignores bytes.\n");
+
+    if (f->dfile == __exe_fs.sym_stdout)
+      __exe_fs.stdout_writes += actual_count;
+
+    f->off += count;
+    return count;
+  }
+}
+
+
+off64_t __fd_lseek(int fd, off64_t offset, int whence) {
+  off64_t new_off;
+  exe_file_t *f = __get_file(fd);
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+
+  if (!f->dfile) {
+    /* We could always do SEEK_SET then whence, but this causes
+       troubles with directories since we play nasty tricks with the
+       offset, and the OS doesn't want us to randomly seek
+       directories. We could detect if it is a directory and correct
+       the offset, but really directories should only be SEEK_SET, so
+       this solves the problem. */
+    if (whence == SEEK_SET) {
+      new_off = syscall(__NR_lseek, f->fd, (int) offset, SEEK_SET);
+    } else {
+      new_off = syscall(__NR_lseek, f->fd, (int) f->off, SEEK_SET);
+
+      /* If we can't seek to start off, just return same error.
+         Probably ESPIPE. */
+      if (new_off != -1) {
+        assert(new_off == f->off);
+        new_off = syscall(__NR_lseek, f->fd, (int) offset, whence);
+      }
+    }
+
+    if (new_off == -1) {
+      errno = klee_get_errno();
+      return -1;
+    }
+
+    f->off = new_off;
+    return new_off;
+  }
+  
+  switch (whence) {
+  case SEEK_SET: new_off = offset; break;
+  case SEEK_CUR: new_off = f->off + offset; break;
+  case SEEK_END: new_off = f->dfile->size + offset; break;
+  default: {
+    errno = EINVAL;
+    return (off64_t) -1;
+  }
+  }
+
+  if (new_off < 0) {
+    errno = EINVAL;
+    return (off64_t) -1;
+  }
+    
+  f->off = new_off;
+  return f->off;
+}
+
+int __fd_stat(const char *path, struct stat64 *buf) {  
+  exe_disk_file_t *dfile = __get_sym_file(path);
+  if (dfile) {
+    memcpy(buf, dfile->stat, sizeof(*dfile->stat));
+    return 0;
+  } 
+
+  {
+    int r = syscall(__NR_stat64, __concretize_string(path), buf);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int __fd_lstat(const char *path, struct stat64 *buf) {
+  exe_disk_file_t *dfile = __get_sym_file(path);
+  if (dfile) {
+    memcpy(buf, dfile->stat, sizeof(*dfile->stat));
+    return 0;
+  } 
+
+  {    
+    int r = syscall(__NR_lstat64, __concretize_string(path), buf);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int chdir(const char *path) {
+  exe_disk_file_t *dfile = __get_sym_file(path);
+
+  if (dfile) {
+    /* XXX incorrect */
+    klee_warning("symbolic file, ignoring (ENOENT)");
+    errno = ENOENT;
+    return -1;
+  }
+
+  {
+    int r = syscall(__NR_chdir, __concretize_string(path));
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int fchdir(int fd) {
+  exe_file_t *f = __get_file(fd);
+  
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+
+  if (f->dfile) {
+    klee_warning("symbolic file, ignoring (ENOENT)");
+    errno = ENOENT;
+    return -1;
+  } else {
+    int r = syscall(__NR_fchdir, f->fd);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+/* Sets mode and or errno and return appropriate result. */
+static int __df_chmod(exe_disk_file_t *df, mode_t mode) {
+  if (geteuid() == df->stat->st_uid) {
+    if (getgid() != df->stat->st_gid)
+      mode &= ~ S_ISGID;
+    df->stat->st_mode = ((df->stat->st_mode & ~07777) | 
+                         (mode & 07777));
+    return 0;
+  } else {
+    errno = EPERM;
+    return -1;
+  }
+}
+
+int chmod(const char *path, mode_t mode) {
+  static int n_calls = 0;
+
+  exe_disk_file_t *dfile = __get_sym_file(path);
+
+  n_calls++;
+  if (__exe_fs.max_failures && *__exe_fs.chmod_fail == n_calls) {
+    __exe_fs.max_failures--;
+    errno = EIO;
+    return -1;
+  }
+
+  if (dfile) {
+    return __df_chmod(dfile, mode);
+  } else {
+    int r = syscall(__NR_chmod, __concretize_string(path), mode);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int fchmod(int fd, mode_t mode) {
+  static int n_calls = 0;
+
+  exe_file_t *f = __get_file(fd);
+  
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+
+  n_calls++;
+  if (__exe_fs.max_failures && *__exe_fs.fchmod_fail == n_calls) {
+    __exe_fs.max_failures--;
+    errno = EIO;
+    return -1;
+  }
+
+  if (f->dfile) {
+    return __df_chmod(f->dfile, mode);
+  } else {
+    int r = syscall(__NR_fchmod, f->fd, mode);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }  
+}
+
+static int __df_chown(exe_disk_file_t *df, uid_t owner, gid_t group) {
+  klee_warning("symbolic file, ignoring (EPERM)");
+  errno = EPERM;
+  return -1;  
+}
+
+int chown(const char *path, uid_t owner, gid_t group) {
+  exe_disk_file_t *df = __get_sym_file(path);
+
+  if (df) {
+    return __df_chown(df, owner, group);
+  } else {
+    int r = syscall(__NR_chown, __concretize_string(path), owner, group);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int fchown(int fd, uid_t owner, gid_t group) {
+  exe_file_t *f = __get_file(fd);
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+
+  if (f->dfile) {
+    return __df_chown(f->dfile, owner, group);
+  } else {
+    int r = syscall(__NR_fchown, fd, owner, group);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int lchown(const char *path, uid_t owner, gid_t group) {
+  /* XXX Ignores 'l' part */
+  exe_disk_file_t *df = __get_sym_file(path);
+
+  if (df) {
+    return __df_chown(df, owner, group);
+  } else {
+    int r = syscall(__NR_chown, __concretize_string(path), owner, group);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int __fd_fstat(int fd, struct stat64 *buf) {
+  exe_file_t *f = __get_file(fd);
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+  
+  if (!f->dfile) {
+    int r = syscall(__NR_fstat64, f->fd, buf);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+  
+  memcpy(buf, f->dfile->stat, sizeof(*f->dfile->stat));
+  return 0;
+}
+
+int __fd_ftruncate(int fd, off64_t length) {
+  static int n_calls = 0;
+  exe_file_t *f = __get_file(fd);
+
+  n_calls++;
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+
+  if (__exe_fs.max_failures && *__exe_fs.ftruncate_fail == n_calls) {
+    __exe_fs.max_failures--;
+    errno = EIO;
+    return -1;
+  }
+  
+  if (f->dfile) {
+    klee_warning("symbolic file, ignoring (EIO)");
+    errno = EIO;
+    return -1;
+  } else {
+    int r = syscall(__NR_ftruncate64, f->fd, length);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }  
+}
+
+int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) {
+  exe_file_t *f = __get_file(fd);
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+  
+  if (f->dfile) {
+    klee_warning("symbolic file, ignoring (EINVAL)");
+    errno = EINVAL;
+    return -1;
+  } else {
+    if ((unsigned) f->off < 4096u) {
+      /* Return our dirents */
+      unsigned i, pad, bytes=0;
+
+      /* What happens for bad offsets? */
+      i = f->off / sizeof(*dirp);
+      if ((i * sizeof(*dirp) != f->off) ||
+          i > __exe_fs.n_sym_files) {
+        errno = EINVAL;
+        return -1;
+      } 
+      for (; i<__exe_fs.n_sym_files; ++i) {
+        exe_disk_file_t *df = &__exe_fs.sym_files[i];
+        dirp->d_ino = df->stat->st_ino;
+        dirp->d_reclen = sizeof(*dirp);
+        dirp->d_type = IFTODT(df->stat->st_mode);
+        dirp->d_name[0] = 'A' + i;
+        dirp->d_name[1] = '\0';
+        dirp->d_off = (i+1) * sizeof(*dirp);
+        bytes += dirp->d_reclen;
+        ++dirp;
+      }
+      
+      /* Fake jump to OS records by a "deleted" file. */
+      pad = count>=4096 ? 4096 : count;
+      dirp->d_ino = 0;
+      dirp->d_reclen = pad - bytes;
+      dirp->d_type = DT_UNKNOWN;
+      dirp->d_name[0] = '\0';
+      dirp->d_off = 4096;
+      bytes += dirp->d_reclen;
+      f->off = pad;
+      return bytes;
+    } else {
+      unsigned os_pos = f->off - 4096;
+      int res, s;
+
+      /* For reasons which I really don't understand, if I don't
+         memset this then sometimes the kernel returns d_ino==0 for
+         some valid entries? Am I crazy? Can writeback possibly be
+         failing? 
+      
+         Even more bizarre, interchanging the memset and the seek also
+         case strange behavior. Really should be debugged properly. */
+      memset(dirp, 0, count);
+      s = syscall(__NR_lseek, f->fd, (int) os_pos, SEEK_SET);
+      assert(s != (off64_t) -1);
+      res = syscall(__NR_getdents64, f->fd, dirp, count);
+      if (res == -1) {
+        errno = klee_get_errno();
+      } else {
+        int pos = 0;
+
+        f->off = syscall(__NR_lseek, f->fd, 0, SEEK_CUR) + 4096;
+
+        /* Patch offsets */
+        
+        while (pos < res) {
+          struct dirent64 *dp = (struct dirent64*) ((char*) dirp + pos);
+          dp->d_off += 4096;
+          pos += dp->d_reclen;
+        }
+      }
+      return res;
+    }
+  }
+}
+
+int ioctl(int fd, unsigned long request, ...) {
+  exe_file_t *f = __get_file(fd);
+  va_list ap;
+  void *buf;
+
+#if 0
+  printf("In ioctl(%d, ...)\n", fd);
+#endif
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+  
+  va_start(ap, request);
+  buf = va_arg(ap, void*);
+  va_end(ap);
+  
+  if (f->dfile) {
+    struct stat *stat = (struct stat*) f->dfile->stat;
+
+    switch (request) {
+    case TCGETS: {      
+      struct termios *ts = buf;
+
+      klee_warning_once("(TCGETS) symbolic file, incomplete model");
+
+      /* XXX need more data, this is ok but still not good enough */
+      if (S_ISCHR(stat->st_mode)) {
+        /* Just copied from my system, munged to match what fields
+           uclibc thinks are there. */
+        ts->c_iflag = 27906;
+        ts->c_oflag = 5;
+        ts->c_cflag = 1215;
+        ts->c_lflag = 35287;
+        ts->c_line = 0;
+        ts->c_cc[0] = '\x03';
+        ts->c_cc[1] = '\x1c';
+        ts->c_cc[2] = '\x7f';
+        ts->c_cc[3] = '\x15';
+        ts->c_cc[4] = '\x04';
+        ts->c_cc[5] = '\x00';
+        ts->c_cc[6] = '\x01';
+        ts->c_cc[7] = '\xff';
+        ts->c_cc[8] = '\x11';
+        ts->c_cc[9] = '\x13';
+        ts->c_cc[10] = '\x1a';
+        ts->c_cc[11] = '\xff';
+        ts->c_cc[12] = '\x12';
+        ts->c_cc[13] = '\x0f';
+        ts->c_cc[14] = '\x17';
+        ts->c_cc[15] = '\x16';
+        ts->c_cc[16] = '\xff';
+        ts->c_cc[17] = '\x0';
+        ts->c_cc[18] = '\x0';
+        return 0;
+      } else {
+        errno = ENOTTY;
+        return -1;
+      }
+    }
+    case TCSETS: {
+      /* const struct termios *ts = buf; */
+      klee_warning_once("(TCSETS) symbolic file, silently ignoring");
+      if (S_ISCHR(stat->st_mode)) {
+        return 0;
+      } else {
+        errno = ENOTTY;
+        return -1;
+      }
+    }
+    case TCSETSW: {
+      /* const struct termios *ts = buf; */
+      klee_warning_once("(TCSETSW) symbolic file, silently ignoring");
+      if (fd==0) {
+        return 0;
+      } else {
+        errno = ENOTTY;
+        return -1;
+      }
+    }
+    case TCSETSF: {
+      /* const struct termios *ts = buf; */
+      klee_warning_once("(TCSETSF) symbolic file, silently ignoring");
+      if (S_ISCHR(stat->st_mode)) {        
+        return 0;
+      } else {
+        errno = ENOTTY;
+        return -1;
+      }
+    }
+    case TIOCGWINSZ: {
+      struct winsize *ws = buf;
+      ws->ws_row = 24;
+      ws->ws_col = 80;
+      klee_warning_once("(TIOCGWINSZ) symbolic file, incomplete model");
+      if (S_ISCHR(stat->st_mode)) {
+        return 0;
+      } else {
+        errno = ENOTTY;
+        return -1;
+      }
+    }
+    case TIOCSWINSZ: {
+      /* const struct winsize *ws = buf; */
+      klee_warning_once("(TIOCSWINSZ) symbolic file, ignoring (EINVAL)");
+      if (S_ISCHR(stat->st_mode)) {
+        errno = EINVAL;
+        return -1;
+      } else {
+        errno = ENOTTY;
+        return -1;
+      }
+    }
+    case FIONREAD: {
+      int *res = buf;
+      klee_warning_once("(FIONREAD) symbolic file, incomplete model");
+      if (S_ISCHR(stat->st_mode)) {
+        if (f->off < f->dfile->size) {
+          *res = f->dfile->size - f->off;
+        } else {
+          *res = 0;
+        }
+        return 0;
+      } else {
+        errno = ENOTTY;
+        return -1;
+      }
+    }
+    case MTIOCGET: {
+      klee_warning("(MTIOCGET) symbolic file, ignoring (EINVAL)");
+      errno = EINVAL;
+      return -1;
+    }
+    default:
+      klee_warning("symbolic file, ignoring (EINVAL)");
+      errno = EINVAL;
+      return -1;
+    }
+  } else {
+    int r = syscall(__NR_ioctl, f->fd, request, buf );
+    if (r == -1) 
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int fcntl(int fd, int cmd, ...) {
+  exe_file_t *f = __get_file(fd);
+  va_list ap;
+  unsigned arg; /* 32 bit assumption (int/ptr) */
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+  
+  if (cmd==F_GETFD || cmd==F_GETFL || cmd==F_GETOWN || cmd==F_GETSIG ||
+      cmd==F_GETLEASE || cmd==F_NOTIFY) {
+    arg = 0;
+  } else {
+    va_start(ap, cmd);
+    arg = va_arg(ap, int);
+    va_end(ap);
+  }
+
+  if (f->dfile) {
+    switch(cmd) {
+    case F_GETFD: {
+      int flags = 0;
+      if (f->flags & eCloseOnExec)
+        flags |= FD_CLOEXEC;
+      return flags;
+    } 
+    case F_SETFD: {
+      f->flags &= ~eCloseOnExec;
+      if (arg & FD_CLOEXEC)
+        f->flags |= eCloseOnExec;
+      return 0;
+    }
+    case F_GETFL: {
+      /* XXX (CrC): This should return the status flags: O_APPEND,
+	 O_ASYNC, O_DIRECT, O_NOATIME, O_NONBLOCK.  As of now, we
+	 discard these flags during open().  We should save them and
+	 return them here.  These same flags can be set by F_SETFL,
+	 which we could also handle properly. 
+      */
+      return 0;
+    }
+    default:
+      klee_warning("symbolic file, ignoring (EINVAL)");
+      errno = EINVAL;
+      return -1;
+    }
+  } else {
+    int r = syscall(__NR_fcntl, f->fd, cmd, arg );
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int __fd_statfs(const char *path, struct statfs *buf) {
+  exe_disk_file_t *dfile = __get_sym_file(path);
+  if (dfile) {
+    /* XXX incorrect */
+    klee_warning("symbolic file, ignoring (ENOENT)");
+    errno = ENOENT;
+    return -1;
+  }
+
+  {
+    int r = syscall(__NR_statfs, __concretize_string(path), buf);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int fstatfs(int fd, struct statfs *buf) {
+  exe_file_t *f = __get_file(fd);
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  }
+  
+  if (f->dfile) {
+    klee_warning("symbolic file, ignoring (EBADF)");
+    errno = EBADF;
+    return -1;
+  } else {
+    int r = syscall(__NR_fstatfs, f->fd, buf);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int fsync(int fd) {
+  exe_file_t *f = __get_file(fd);
+
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  } else if (f->dfile) {
+    return 0;
+  } else {
+    int r = syscall(__NR_fsync, f->fd);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+int dup2(int oldfd, int newfd) {
+  exe_file_t *f = __get_file(oldfd);
+
+  if (!f || !(newfd>=0 && newfd<MAX_FDS)) {
+    errno = EBADF;
+    return -1;
+  } else {
+    exe_file_t *f2 = &__exe_env.fds[newfd];
+    if (f2->flags & eOpen) close(newfd);
+
+    /* XXX Incorrect, really we need another data structure for open
+       files */
+    *f2 = *f;
+
+    f2->flags &= ~eCloseOnExec;
+      
+    /* I'm not sure it is wise, but we can get away with not dup'ng
+       the OS fd, since actually that will in many cases effect the
+       sharing of the open file (and the process should never have
+       access to it). */
+
+    return newfd;
+  }
+}
+
+int dup(int oldfd) {
+  exe_file_t *f = __get_file(oldfd);
+  if (!f) {
+    errno = EBADF;
+    return -1;
+  } else {
+    int fd;
+    for (fd = 0; fd < MAX_FDS; ++fd)
+      if (!(__exe_env.fds[fd].flags & eOpen))
+        break;
+    if (fd == MAX_FDS) {
+      errno = EMFILE;
+      return -1;
+    } else {
+      return dup2(oldfd, fd);
+    }
+  }
+}
+
+int rmdir(const char *pathname) {
+  exe_disk_file_t *dfile = __get_sym_file(pathname);
+  if (dfile) {
+    /* XXX check access */ 
+    if (S_ISDIR(dfile->stat->st_mode)) {
+      dfile->stat->st_ino = 0;
+      return 0;
+    } else {
+      errno = ENOTDIR;
+      return -1;
+    }
+  }
+
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int unlink(const char *pathname) {
+  exe_disk_file_t *dfile = __get_sym_file(pathname);
+  if (dfile) {
+    /* XXX check access */ 
+    if (S_ISREG(dfile->stat->st_mode)) {
+      dfile->stat->st_ino = 0;
+      return 0;
+    } else if (S_ISDIR(dfile->stat->st_mode)) {
+      errno = EISDIR;
+      return -1;
+    } else {
+      errno = EPERM;
+      return -1;
+    }
+  }
+
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+ssize_t readlink(const char *path, char *buf, size_t bufsize) {
+  exe_disk_file_t *dfile = __get_sym_file(path);
+  if (dfile) {
+    /* XXX We need to get the sym file name really, but since we don't
+       handle paths anyway... */
+    if (S_ISLNK(dfile->stat->st_mode)) {
+      buf[0] = path[0];
+      if (bufsize>1) buf[1] = '.';
+      if (bufsize>2) buf[2] = 'l';
+      if (bufsize>3) buf[3] = 'n';
+      if (bufsize>4) buf[4] = 'k';
+      return (bufsize>5) ? 5 : bufsize;
+    } else {
+      errno = EINVAL;
+      return -1;
+    }
+  } else {
+    int r = syscall(__NR_readlink, path, buf, bufsize);
+    if (r == -1)
+      errno = klee_get_errno();
+    return r;
+  }
+}
+
+#undef FD_SET
+#undef FD_CLR
+#undef FD_ISSET
+#undef FD_ZERO
+#define	FD_SET(n, p)	((p)->fds_bits[(n)/NFDBITS] |= (1 << ((n) % NFDBITS)))
+#define	FD_CLR(n, p)	((p)->fds_bits[(n)/NFDBITS] &= ~(1 << ((n) % NFDBITS)))
+#define	FD_ISSET(n, p)	((p)->fds_bits[(n)/NFDBITS] & (1 << ((n) % NFDBITS)))
+#define FD_ZERO(p)	memset((char *)(p), '\0', sizeof(*(p)))
+int select(int nfds, fd_set *read, fd_set *write,
+           fd_set *except, struct timeval *timeout) {
+  fd_set in_read, in_write, in_except, os_read, os_write, os_except;
+  int i, count = 0, os_nfds = 0;
+
+  if (read) {
+    in_read = *read;
+    FD_ZERO(read);
+  } else {
+    FD_ZERO(&in_read);
+  }
+
+  if (write) {
+    in_write = *write;
+    FD_ZERO(write);
+  } else {
+    FD_ZERO(&in_write);
+  }
+   
+  if (except) {
+    in_except = *except;
+    FD_ZERO(except);
+  } else {
+    FD_ZERO(&in_except);
+  }
+
+  FD_ZERO(&os_read);
+  FD_ZERO(&os_write);
+  FD_ZERO(&os_except);
+
+  /* Check for symbolic stuff */
+  for (i=0; i<nfds; i++) {    
+    if (FD_ISSET(i, &in_read) || FD_ISSET(i, &in_write) || FD_ISSET(i, &in_except)) {
+      exe_file_t *f = __get_file(i);
+      if (!f) {
+        errno = EBADF;
+        return -1;
+      } else if (f->dfile) {
+        /* Operations on this fd will never block... */
+        if (FD_ISSET(i, &in_read)) FD_SET(i, read);
+        if (FD_ISSET(i, &in_write)) FD_SET(i, write);
+        if (FD_ISSET(i, &in_except)) FD_SET(i, except);
+        ++count;
+      } else {
+        if (FD_ISSET(i, &in_read)) FD_SET(f->fd, &os_read);
+        if (FD_ISSET(i, &in_write)) FD_SET(f->fd, &os_write);
+        if (FD_ISSET(i, &in_except)) FD_SET(f->fd, &os_except);
+        if (f->fd >= os_nfds) os_nfds = f->fd + 1;
+      }
+    }
+  }
+
+  if (os_nfds > 0) {
+    /* Never allow blocking select. This is broken but what else can
+       we do. */
+    struct timeval tv = { 0, 0 };    
+    int r = syscall(__NR_select, os_nfds, 
+                    &os_read, &os_write, &os_except, &tv);
+    
+    if (r == -1) {
+      /* If no symbolic results, return error. Otherwise we will
+         silently ignore the OS error. */
+      if (!count) {
+        errno = klee_get_errno();
+        return -1;
+      }
+    } else {
+      count += r;
+
+      /* Translate resulting sets back */
+      for (i=0; i<nfds; i++) {
+        exe_file_t *f = __get_file(i);
+        if (f && !f->dfile) {
+          if (read && FD_ISSET(f->fd, &os_read)) FD_SET(i, read);
+          if (write && FD_ISSET(f->fd, &os_write)) FD_SET(i, write);
+          if (except && FD_ISSET(f->fd, &os_except)) FD_SET(i, except);
+        }
+      }
+    }
+  }
+
+  return count;
+}
+
+/*** Library functions ***/
+
+char *getcwd(char *buf, size_t size) {
+  static int n_calls = 0;
+  int r;
+
+  n_calls++;
+
+  if (__exe_fs.max_failures && *__exe_fs.getcwd_fail == n_calls) {
+    __exe_fs.max_failures--;
+    errno = ERANGE;
+    return NULL;
+  }
+
+  if (!buf) {
+    if (!size)
+      size = 1024;
+    buf = malloc(size);
+  }
+  
+  buf = __concretize_ptr(buf);
+  size = __concretize_size(size);
+  /* XXX In terms of looking for bugs we really should do this check
+     before concretization, at least once the routine has been fixed
+     to properly work with symbolics. */
+  klee_check_memory_access(buf, size);
+  r = syscall(__NR_getcwd, buf, size);
+  if (r == -1) {
+    errno = klee_get_errno();
+    return NULL;
+  }
+    
+  return buf;
+}
+
+/*** Helper functions ***/
+
+static void *__concretize_ptr(const void *p) {
+  /* XXX 32-bit assumption */
+  char *pc = (char*) klee_get_value((unsigned) (long) p);
+  klee_assume(pc == p);
+  return pc;
+}
+
+static size_t __concretize_size(size_t s) {
+  size_t sc = klee_get_value(s);
+  klee_assume(sc == s);
+  return sc;
+}
+
+static const char *__concretize_string(const char *s) {
+  char *sc = __concretize_ptr(s);
+  unsigned i;
+
+  for (i=0; ; ++i) {
+    char c = *sc;
+    if (!(i&(i-1))) {
+      if (!c) {
+        *sc++ = 0;
+        break;
+      } else if (c=='/') {
+        *sc++ = '/';
+      } 
+    } else {
+      char cc = (char) klee_get_value(c);
+      klee_assume(cc == c);
+      *sc++ = cc;
+      if (!cc) break;
+    }
+  }
+
+  return s;
+}
+
+
+
+/* Trivial model:
+   if path is "/" (basically no change) accept, otherwise reject
+*/
+int chroot(const char *path) {
+  if (path[0] == '\0') {
+    errno = ENOENT;
+    return -1;
+  }
+    
+  if (path[0] == '/' && path[1] == '\0') {
+    return 0;
+  }
+  
+  klee_warning("ignoring (ENOENT)");
+  errno = ENOENT;
+  return -1;
+}
diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h
new file mode 100644
index 00000000..f2780143
--- /dev/null
+++ b/runtime/POSIX/fd.h
@@ -0,0 +1,90 @@
+//===-- fd.h ---------------------------------------------------*- C++ -*--===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef __EXE_FD__
+#define __EXE_FD__
+
+#ifndef _LARGEFILE64_SOURCE
+#error "_LARGEFILE64_SOURCE should be defined"
+#endif
+#include <sys/types.h>
+#include <sys/statfs.h>
+#include <dirent.h>
+
+typedef struct {  
+  unsigned size;  /* in bytes */
+  char* contents;
+  struct stat64* stat;
+} exe_disk_file_t;
+
+typedef enum {
+  eOpen         = (1 << 0),
+  eCloseOnExec  = (1 << 1),
+  eReadable     = (1 << 2),
+  eWriteable    = (1 << 3)
+} exe_file_flag_t;
+
+typedef struct {      
+  int fd;                   /* actual fd if not symbolic */
+  unsigned flags;           /* set of exe_file_flag_t values. fields
+                               are only defined when flags at least
+                               has eOpen. */
+  off64_t off;              /* offset */
+  exe_disk_file_t* dfile;   /* ptr to file on disk, if symbolic */
+} exe_file_t;
+
+typedef struct {
+  unsigned n_sym_files; /* number of symbolic input files, excluding stdin */
+  exe_disk_file_t *sym_stdin, *sym_stdout;
+  unsigned stdout_writes; /* how many chars were written to stdout */
+  exe_disk_file_t *sym_files;
+  /* --- */
+  /* the maximum number of failures on one path; gets decremented after each failure */
+  unsigned max_failures; 
+
+  /* Which read, write etc. call should fail */
+  int *read_fail, *write_fail, *close_fail, *ftruncate_fail, *getcwd_fail;
+  int *chmod_fail, *fchmod_fail;
+} exe_file_system_t;
+
+#define MAX_FDS 32
+
+/* Note, if you change this structure be sure to update the
+   initialization code if necessary. New fields should almost
+   certainly be at the end. */
+typedef struct {
+  exe_file_t fds[MAX_FDS];
+  mode_t umask; /* process umask */
+  unsigned version;
+  /* If set, writes execute as expected.  Otherwise, writes extending
+     the file size only change the contents up to the initial
+     size. The file offset is always incremented correctly. */
+  int save_all_writes; 
+} exe_sym_env_t;
+
+extern exe_file_system_t __exe_fs;
+extern exe_sym_env_t __exe_env;
+
+void klee_init_fds(unsigned n_files, unsigned file_length, 
+		   int sym_stdout_flag, int do_all_writes_flag, 
+		   unsigned max_failures);
+void klee_init_env(int *argcPtr, char ***argvPtr);
+
+/* *** */
+
+int __fd_open(const char *pathname, int flags, mode_t mode);
+off64_t __fd_lseek(int fd, off64_t offset, int whence);
+int __fd_stat(const char *path, struct stat64 *buf);
+int __fd_lstat(const char *path, struct stat64 *buf);
+int __fd_fstat(int fd, struct stat64 *buf);
+int __fd_ftruncate(int fd, off64_t length);
+int __fd_statfs(const char *path, struct statfs *buf);
+int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count);
+
+#endif /* __EXE_FD__ */
diff --git a/runtime/POSIX/fd_32.c b/runtime/POSIX/fd_32.c
new file mode 100644
index 00000000..4eea1805
--- /dev/null
+++ b/runtime/POSIX/fd_32.c
@@ -0,0 +1,196 @@
+//===-- fd_32.c -----------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#define _LARGEFILE64_SOURCE
+#include "fd.h"
+
+#include <string.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <errno.h>
+#include <sys/syscall.h>
+#include <sys/stat.h>
+#include <sys/types.h>
+#include <sys/time.h>
+#include <sys/vfs.h>
+#include <fcntl.h>
+#include <stdarg.h>
+#include <assert.h>
+#include <unistd.h>
+#include <dirent.h>
+
+/***/
+
+static void __stat64_to_stat(struct stat64 *a, struct stat *b) {
+  b->st_dev = a->st_dev;
+  b->st_ino = a->st_ino;
+  b->st_mode = a->st_mode;
+  b->st_nlink = a->st_nlink;
+  b->st_uid = a->st_uid;
+  b->st_gid = a->st_gid;
+  b->st_rdev = a->st_rdev;
+  b->st_size = a->st_size;
+  b->st_atime = a->st_atime;
+  b->st_mtime = a->st_mtime;
+  b->st_ctime = a->st_ctime;
+  b->st_blksize = a->st_blksize;
+  b->st_blocks = a->st_blocks;
+}
+
+/***/
+
+int open(const char *pathname, int flags, ...) {
+  mode_t mode = 0;
+
+  if (flags & O_CREAT) {
+    /* get mode */
+    va_list ap;
+    va_start(ap, flags);
+    mode = va_arg(ap, mode_t);
+    va_end(ap);
+  }
+
+  return __fd_open(pathname, flags, mode);
+}
+
+off_t lseek(int fd, off_t off, int whence) {
+  return (off_t) __fd_lseek(fd, off, whence);
+}
+
+int __xstat(int vers, const char *path, struct stat *buf) {
+  struct stat64 tmp;
+  int res = __fd_stat(path, &tmp);
+  __stat64_to_stat(&tmp, buf);
+  return res;
+}
+
+int stat(const char *path, struct stat *buf) {
+  struct stat64 tmp;
+  int res = __fd_stat(path, &tmp);
+  __stat64_to_stat(&tmp, buf);
+  return res;
+}
+
+int __lxstat(int vers, const char *path, struct stat *buf) {
+  struct stat64 tmp;
+  int res = __fd_lstat(path, &tmp);
+  __stat64_to_stat(&tmp, buf);
+  return res;
+}
+
+int lstat(const char *path, struct stat *buf) {
+  struct stat64 tmp;
+  int res = __fd_lstat(path, &tmp);
+  __stat64_to_stat(&tmp, buf);
+  return res;
+}
+
+int __fxstat(int vers, int fd, struct stat *buf) {
+  struct stat64 tmp;
+  int res = __fd_fstat(fd, &tmp);
+  __stat64_to_stat(&tmp, buf);
+  return res;
+}
+
+int fstat(int fd, struct stat *buf) {
+  struct stat64 tmp;
+  int res = __fd_fstat(fd, &tmp);
+  __stat64_to_stat(&tmp, buf);
+  return res;
+}
+
+int ftruncate(int fd, off_t length) {
+  return __fd_ftruncate(fd, length);
+}
+
+int statfs(const char *path, struct statfs *buf32) {
+#if 0
+    struct statfs64 buf;
+
+    if (__fd_statfs(path, &buf) < 0)
+	return -1;
+
+    buf32->f_type = buf.f_type;
+    buf32->f_bsize = buf.f_bsize;
+    buf32->f_blocks = buf.f_blocks;
+    buf32->f_bfree = buf.f_bfree;
+    buf32->f_bavail = buf.f_bavail;
+    buf32->f_files = buf.f_files;
+    buf32->f_ffree = buf.f_ffree;
+    buf32->f_fsid = buf.f_fsid;
+    buf32->f_namelen = buf.f_namelen;
+
+    return 0;
+#else
+    return __fd_statfs(path, buf32);
+#endif
+}
+
+/* Based on uclibc version. We use getdents64 and then rewrite the
+   results over themselves, as dirent32s. */
+ssize_t getdents(int fd, struct dirent *dirp, size_t nbytes) {
+  struct dirent64 *dp64 = (struct dirent64*) dirp;
+  ssize_t res = __fd_getdents(fd, dp64, nbytes);
+
+  if (res>0) {
+    struct dirent64 *end = (struct dirent64*) ((char*) dp64 + res);
+    while (dp64 < end) {
+      struct dirent *dp = (struct dirent *) dp64;
+      unsigned name_len = (dp64->d_reclen - 
+                           (unsigned) &((struct dirent64*) 0)->d_name);
+      dp->d_ino = dp64->d_ino;
+      dp->d_off = dp64->d_off;
+      dp->d_reclen = dp64->d_reclen;
+      dp->d_type = dp64->d_type;
+      memmove(dp->d_name, dp64->d_name, name_len);
+      dp64 = (struct dirent64*) ((char*) dp64 + dp->d_reclen);
+    }
+  }
+
+  return res;
+}
+int __getdents(unsigned int fd, struct dirent *dirp, unsigned int count)
+     __attribute__((alias("getdents")));
+
+/* Forward to 64 versions (uclibc expects versions w/o asm specifier) */
+
+int open64(const char *pathname, int flags, ...) __attribute__((weak));
+int open64(const char *pathname, int flags, ...) {
+  mode_t mode = 0;
+
+  if (flags & O_CREAT) {
+    /* get mode */
+    va_list ap;
+    va_start(ap, flags);
+    mode = va_arg(ap, mode_t);
+    va_end(ap);
+  }
+
+  return __fd_open(pathname, flags, mode);
+}
+
+off64_t lseek64(int fd, off64_t off, int whence) __attribute__((weak));
+off64_t lseek64(int fd, off64_t off, int whence) {
+  return __fd_lseek(fd, off, whence);
+}
+
+int stat64(const char *path, struct stat64 *buf) __attribute__((weak));
+int stat64(const char *path, struct stat64 *buf) {
+  return __fd_stat(path, buf);
+}
+
+int lstat64(const char *path, struct stat64 *buf) __attribute__((weak));
+int lstat64(const char *path, struct stat64 *buf) {
+  return __fd_lstat(path, buf);
+}
+
+int fstat64(int fd, struct stat64 *buf) __attribute__((weak));
+int fstat64(int fd, struct stat64 *buf) {
+  return __fd_fstat(fd, buf);
+}
diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c
new file mode 100644
index 00000000..d0710caf
--- /dev/null
+++ b/runtime/POSIX/fd_64.c
@@ -0,0 +1,90 @@
+//===-- fd_64.c -----------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#define _LARGEFILE64_SOURCE
+#define _FILE_OFFSET_BITS 64
+#include "fd.h"
+
+#include <string.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <errno.h>
+#include <sys/syscall.h>
+#include <sys/stat.h>
+#include <sys/types.h>
+#include <fcntl.h>
+#include <stdarg.h>
+#include <assert.h>
+#include <sys/vfs.h>
+#include <unistd.h>
+#include <dirent.h>
+#include <sys/ioctl.h>
+#include <sys/mtio.h>
+#include <termios.h>
+#include <sys/select.h>
+#include <klee/klee.h>
+
+/*** Forward to actual implementations ***/
+
+int open(const char *pathname, int flags, ...) {
+  mode_t mode = 0;
+  
+  if (flags & O_CREAT) {
+    /* get mode */
+    va_list ap;
+    va_start(ap, flags);
+    mode = va_arg(ap, mode_t);
+    va_end(ap);
+  }
+
+  return __fd_open(pathname, flags, mode);
+}
+
+off64_t lseek(int fd, off64_t offset, int whence) {
+  return __fd_lseek(fd, offset, whence);
+}
+
+int __xstat(int vers, const char *path, struct stat *buf) {
+  return __fd_stat(path, (struct stat64*) buf);
+}
+
+int stat(const char *path, struct stat *buf) {
+  return __fd_stat(path, (struct stat64*) buf);
+}
+
+int __lxstat(int vers, const char *path, struct stat *buf) {
+  return __fd_lstat(path, (struct stat64*) buf);
+}
+
+int lstat(const char *path, struct stat *buf) {
+  return __fd_lstat(path, (struct stat64*) buf);
+}
+
+int __fxstat(int vers, int fd, struct stat *buf) {
+  return __fd_fstat(fd, (struct stat64*) buf);
+}
+
+int fstat(int fd, struct stat *buf) {
+  return __fd_fstat(fd, (struct stat64*) buf);
+}
+
+int ftruncate64(int fd, off64_t length) {
+  return __fd_ftruncate(fd, length);
+}
+
+int statfs(const char *path, struct statfs *buf) __attribute__((weak));
+int statfs(const char *path, struct statfs *buf) {
+  return __fd_statfs(path, buf);
+}
+
+int getdents64(unsigned int fd, struct dirent *dirp, unsigned int count) {
+  return __fd_getdents(fd, (struct dirent64*) dirp, count);
+}
+int __getdents64(unsigned int fd, struct dirent *dirp, unsigned int count)
+     __attribute__((alias("getdents64")));
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c
new file mode 100644
index 00000000..61e49893
--- /dev/null
+++ b/runtime/POSIX/fd_init.c
@@ -0,0 +1,161 @@
+//===-- fd_init.c ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#define _LARGEFILE64_SOURCE
+#define _FILE_OFFSET_BITS 64
+#include "fd.h"
+#include <klee/klee.h>
+
+#include <string.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+#include <sys/stat.h>
+#include <sys/syscall.h>
+#include <unistd.h>
+
+
+exe_file_system_t __exe_fs;
+
+/* NOTE: It is important that these are statically initialized
+   correctly, since things that run before main may hit them given the
+   current way things are linked. */
+
+/* XXX Technically these flags are initialized w.o.r. to the
+   environment we are actually running in. We could patch them in
+   klee_init_fds, but we still have the problem that uclibc calls
+   prior to main will get the wrong data. Not such a big deal since we
+   mostly care about sym case anyway. */
+
+
+exe_sym_env_t __exe_env = { 
+  {{ 0, eOpen | eReadable, 0, 0}, 
+   { 1, eOpen | eWriteable, 0, 0}, 
+   { 2, eOpen | eWriteable, 0, 0}},
+  022,
+  0,
+  0
+};
+
+static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, 
+                               const char *name, struct stat64 *defaults) {
+  struct stat64 *s = malloc(sizeof(*s));
+  const char *sp;
+  char sname[64];
+  for (sp=name; *sp; ++sp)
+    sname[sp-name] = *sp;
+  memcpy(&sname[sp-name], "-stat", 6);
+
+  assert(size);
+
+  dfile->size = size;
+  dfile->contents = malloc(dfile->size);
+  klee_make_symbolic_name(dfile->contents, dfile->size, name);
+  
+  klee_make_symbolic_name(s, sizeof(*s), sname);
+
+  /* For broken tests */
+  if (!klee_is_symbolic(s->st_ino) && 
+      (s->st_ino & 0x7FFFFFFF) == 0)
+    s->st_ino = defaults->st_ino;
+  
+  /* Important since we copy this out through getdents, and readdir
+     will otherwise skip this entry. For same reason need to make sure
+     it fits in low bits. */
+  klee_assume((s->st_ino & 0x7FFFFFFF) != 0);
+
+  /* uclibc opendir uses this as its buffer size, try to keep
+     reasonable. */
+  klee_assume((s->st_blksize & ~0xFFFF) == 0);
+
+  klee_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777)));
+  klee_prefer_cex(s, s->st_dev == defaults->st_dev);
+  klee_prefer_cex(s, s->st_rdev == defaults->st_rdev);
+  klee_prefer_cex(s, (s->st_mode&0700) == 0600);
+  klee_prefer_cex(s, (s->st_mode&0070) == 0020);
+  klee_prefer_cex(s, (s->st_mode&0007) == 0002);
+  klee_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG);
+  klee_prefer_cex(s, s->st_nlink == 1);
+  klee_prefer_cex(s, s->st_uid == defaults->st_uid);
+  klee_prefer_cex(s, s->st_gid == defaults->st_gid);
+  klee_prefer_cex(s, s->st_blksize == 4096);
+  klee_prefer_cex(s, s->st_atime == defaults->st_atime);
+  klee_prefer_cex(s, s->st_mtime == defaults->st_mtime);
+  klee_prefer_cex(s, s->st_ctime == defaults->st_ctime);
+
+  s->st_size = dfile->size;
+  s->st_blocks = 8;
+  dfile->stat = s;
+}
+
+static unsigned __sym_uint32(const char *name) {
+  unsigned x;
+  klee_make_symbolic_name(&x, sizeof x, name);
+  return x;
+}
+
+/* n_files: number of symbolic input files, excluding stdin
+   file_length: size in bytes of each symbolic file, including stdin
+   sym_stdout_flag: 1 if stdout should be symbolic, 0 otherwise
+   save_all_writes_flag: 1 if all writes are executed as expected, 0 if 
+                         writes past the initial file size are discarded 
+			 (file offset is always incremented)
+   max_failures: maximum number of system call failures */
+void klee_init_fds(unsigned n_files, unsigned file_length, 
+		   int sym_stdout_flag, int save_all_writes_flag,
+		   unsigned max_failures) {
+  unsigned k;
+  char name[7] = "?-data";
+  struct stat64 s;
+
+  stat64(".", &s);
+
+  __exe_fs.n_sym_files = n_files;
+  __exe_fs.sym_files = malloc(sizeof(*__exe_fs.sym_files) * n_files);
+  for (k=0; k < n_files; k++) {
+    name[0] = 'A' + k;
+    __create_new_dfile(&__exe_fs.sym_files[k], file_length, name, &s);
+  }
+  
+  /* setting symbolic stdin */
+  if (file_length) {
+    __exe_fs.sym_stdin = malloc(sizeof(*__exe_fs.sym_stdin));
+    __create_new_dfile(__exe_fs.sym_stdin, file_length, "stdin", &s);
+    __exe_env.fds[0].dfile = __exe_fs.sym_stdin;
+  }
+  else __exe_fs.sym_stdin = NULL;
+
+  __exe_fs.max_failures = max_failures;
+  if (__exe_fs.max_failures) {
+    __exe_fs.read_fail = malloc(sizeof(*__exe_fs.read_fail));
+    __exe_fs.write_fail = malloc(sizeof(*__exe_fs.write_fail));
+    __exe_fs.close_fail = malloc(sizeof(*__exe_fs.close_fail));
+    __exe_fs.ftruncate_fail = malloc(sizeof(*__exe_fs.ftruncate_fail));
+    __exe_fs.getcwd_fail = malloc(sizeof(*__exe_fs.getcwd_fail));
+
+    klee_make_symbolic_name(__exe_fs.read_fail, sizeof(*__exe_fs.read_fail), "read_fail");
+    klee_make_symbolic_name(__exe_fs.write_fail, sizeof(*__exe_fs.write_fail), "write_fail");
+    klee_make_symbolic_name(__exe_fs.close_fail, sizeof(*__exe_fs.close_fail), "close_fail");
+    klee_make_symbolic_name(__exe_fs.ftruncate_fail, sizeof(*__exe_fs.ftruncate_fail), "ftruncate_fail");
+    klee_make_symbolic_name(__exe_fs.getcwd_fail, sizeof(*__exe_fs.getcwd_fail), "getcwd_fail");
+  }
+
+  /* setting symbolic stdout */
+  if (sym_stdout_flag) {
+    __exe_fs.sym_stdout = malloc(sizeof(*__exe_fs.sym_stdout));
+    __create_new_dfile(__exe_fs.sym_stdout, 1024, "stdout", &s);
+    __exe_env.fds[1].dfile = __exe_fs.sym_stdout;
+    __exe_fs.stdout_writes = 0;
+  }
+  else __exe_fs.sym_stdout = NULL;
+  
+  __exe_env.save_all_writes = save_all_writes_flag;
+  __exe_env.version = __sym_uint32("model_version");
+  klee_assume(__exe_env.version == 1);
+}
diff --git a/runtime/POSIX/illegal.c b/runtime/POSIX/illegal.c
new file mode 100644
index 00000000..469ea623
--- /dev/null
+++ b/runtime/POSIX/illegal.c
@@ -0,0 +1,70 @@
+//===-- illegal.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 <errno.h>
+#include <unistd.h>
+#include <signal.h>
+#include <setjmp.h>
+#include <sys/types.h>
+
+#include <klee/klee.h>
+
+void klee_warning(const char*);
+void klee_warning_once(const char*);
+
+int kill(pid_t pid, int sig) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int _setjmp (struct __jmp_buf_tag __env[1]) __attribute__((weak));
+int _setjmp (struct __jmp_buf_tag __env[1]) {
+  klee_warning_once("ignoring");
+  return 0;
+}
+
+void longjmp(jmp_buf env, int val) {
+  klee_report_error(__FILE__, __LINE__, "longjmp unsupported", "xxx.err");
+}
+
+/* Macro so function name from klee_warning comes out correct. */
+#define __bad_exec() \
+  (klee_warning("ignoring (EACCES)"),\
+   errno = EACCES,\
+   -1)
+
+/* This need to be weak because uclibc wants to define them as well,
+   but we will want to make sure a definition is around in case we
+   don't link with it. */
+
+int execl(const char *path, const char *arg, ...) __attribute__((weak));
+int execlp(const char *file, const char *arg, ...) __attribute__((weak));
+int execle(const char *path, const char *arg, ...) __attribute__((weak));
+int execv(const char *path, char *const argv[]) __attribute__((weak));
+int execvp(const char *file, char *const argv[]) __attribute__((weak));
+int execve(const char *file, char *const argv[], char *const envp[]) __attribute__((weak));
+
+int execl(const char *path, const char *arg, ...) { return __bad_exec(); }
+int execlp(const char *file, const char *arg, ...) { return __bad_exec(); }
+int execle(const char *path, const char *arg, ...)  { return __bad_exec(); }
+int execv(const char *path, char *const argv[]) { return __bad_exec(); }
+int execvp(const char *file, char *const argv[]) { return __bad_exec(); }
+int execve(const char *file, char *const argv[], char *const envp[]) { return __bad_exec(); }
+
+pid_t fork(void) {
+  klee_warning("ignoring (ENOMEM)");
+  errno = ENOMEM;
+  return -1;
+}
+
+pid_t vfork(void) {
+  return fork();
+}
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
new file mode 100644
index 00000000..83e9fde6
--- /dev/null
+++ b/runtime/POSIX/klee_init_env.c
@@ -0,0 +1,181 @@
+//===-- klee_init_env.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 _LARGEFILE64_SOURCE
+#include "fd.h"
+
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <errno.h>
+#include <sys/syscall.h>
+#include <unistd.h>
+
+static void __emit_error(const char *msg) {
+  klee_report_error(__FILE__, __LINE__, msg, "user.err");
+}
+
+/* Helper function that converts a string to an integer, and
+   terminates the program with an error message is the string is not a
+   proper number */   
+static long int __str_to_int(char *s, const char *error_msg) {
+  long int res = 0;
+  char c;
+
+  if (!*s) __emit_error(error_msg);
+
+  while ((c = *s++)) {
+    if (c == '\0') {
+      break;
+    } else if (c>='0' && c<='9') {
+      res = res*10 + (c - '0');
+    } else {
+      __emit_error(error_msg);
+    }
+  }
+  return res;
+}
+
+static int __isprint(const char c) {
+  /* Assume ASCII */
+  return (32 <= c && c <= 126);
+}
+
+static int __streq(const char *a, const char *b) {
+  while (*a == *b) {
+    if (!*a)
+      return 1;
+    a++;
+    b++;
+  }
+  return 0;
+}
+
+static char *__get_sym_str(int numChars, char *name) {
+  int i;
+  char *s = malloc(numChars+1);
+  klee_mark_global(s);
+  klee_make_symbolic_name(s, numChars+1, name);
+
+  for (i=0; i<numChars; i++)
+    klee_prefer_cex(s, __isprint(s[i]));
+  
+  s[numChars] = '\0';
+  return s;
+}
+
+static void __add_arg(int *argc, char **argv, char *arg, int argcMax) {
+  if (*argc==argcMax) {
+    __emit_error("too many arguments for klee_init_env");
+  } else {
+    argv[*argc] = arg;
+    (*argc)++;
+  }
+}
+
+void klee_init_env(int* argcPtr, char*** argvPtr) {
+  int argc = *argcPtr;
+  char** argv = *argvPtr;
+
+  int new_argc = 0, n_args;
+  char* new_argv[1024];
+  unsigned max_len, min_argvs, max_argvs;
+  unsigned sym_files = 0, sym_file_len = 0;
+  int sym_stdout_flag = 0;
+  int save_all_writes_flag = 0;
+  int fd_fail = 0;
+  char** final_argv;
+  char sym_arg_name[5] = "arg";
+  unsigned sym_arg_num = 0;
+  int k=0, i;
+
+  sym_arg_name[4] = '\0';
+
+  while (k < argc) {
+    if (__streq(argv[k], "--sym-arg") || __streq(argv[k], "-sym-arg")) {
+      const char *msg = "--sym-arg expects an integer argument <max-len>";
+      if (++k == argc)        
+	__emit_error(msg);
+		
+      max_len = __str_to_int(argv[k++], msg);
+      sym_arg_name[3] = '0' + sym_arg_num++;
+      __add_arg(&new_argc, new_argv, 
+                __get_sym_str(max_len, sym_arg_name),
+                1024);
+    }
+    else if (__streq(argv[k], "--sym-args") || __streq(argv[k], "-sym-args")) {
+      const char *msg = 
+        "--sym-args expects three integer arguments <min-argvs> <max-argvs> <max-len>";
+
+      if (k+3 >= argc)
+	__emit_error(msg);
+      
+      k++;
+      min_argvs = __str_to_int(argv[k++], msg);
+      max_argvs = __str_to_int(argv[k++], msg);
+      max_len = __str_to_int(argv[k++], msg);
+
+      n_args = klee_range(min_argvs, max_argvs+1, "n_args");
+      for (i=0; i < n_args; i++) {
+        sym_arg_name[3] = '0' + sym_arg_num++;
+        __add_arg(&new_argc, new_argv, 
+                  __get_sym_str(max_len, sym_arg_name),
+                  1024);
+      }
+    }
+    else if (__streq(argv[k], "--sym-files") || __streq(argv[k], "-sym-files")) {
+      const char* msg = "--sym-files expects two integer arguments <no-sym-files> <sym-file-len>";      
+
+      if (k+2 >= argc)
+	__emit_error(msg);
+      
+      k++;
+      sym_files = __str_to_int(argv[k++], msg);
+      sym_file_len = __str_to_int(argv[k++], msg);
+
+    }
+    else if (__streq(argv[k], "--sym-stdout") || __streq(argv[k], "-sym-stdout")) {
+      sym_stdout_flag = 1;
+      k++;
+    }
+    else if (__streq(argv[k], "--save-all-writes") || __streq(argv[k], "-save-all-writes")) {
+      save_all_writes_flag = 1;
+      k++;
+    }
+    else if (__streq(argv[k], "--fd-fail") || __streq(argv[k], "-fd-fail")) {
+      fd_fail = 1;
+      k++;
+    }
+    else if (__streq(argv[k], "--max-fail") || __streq(argv[k], "-max-fail")) {
+      const char *msg = "--max-fail expects an integer argument <max-failures>";
+      if (++k == argc)
+	__emit_error(msg);
+		
+      fd_fail = __str_to_int(argv[k++], msg);
+    }
+    else {
+      /* simply copy arguments */
+      __add_arg(&new_argc, new_argv, argv[k++], 1024);
+    }
+  }
+
+  final_argv = (char**) malloc((new_argc+1) * sizeof(*final_argv));
+  klee_mark_global(final_argv);
+  memcpy(final_argv, new_argv, new_argc * sizeof(*final_argv));
+  final_argv[new_argc] = 0;
+
+  *argcPtr = new_argc;
+  *argvPtr = final_argv;
+
+  klee_init_fds(sym_files, sym_file_len, 
+		sym_stdout_flag, save_all_writes_flag, 
+		fd_fail);
+}
+
diff --git a/runtime/POSIX/misc.c b/runtime/POSIX/misc.c
new file mode 100644
index 00000000..12ff2f58
--- /dev/null
+++ b/runtime/POSIX/misc.c
@@ -0,0 +1,87 @@
+//===-- misc.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 <unistd.h>
+#include <sys/syscall.h>
+#include <errno.h>
+#include <stdlib.h>
+#include <klee/klee.h>
+#include <string.h>
+
+#if 0
+#define MAX_SYM_ENV_SIZE 32
+typedef struct {
+  char name[MAX_SYM_ENV_SIZE];
+  char *value;
+} sym_env_var;
+
+static sym_env_var *__klee_sym_env = 0;
+static unsigned __klee_sym_env_count = 0;
+static unsigned __klee_sym_env_nvars = 0;
+static unsigned __klee_sym_env_var_size = 0;
+void __klee_init_environ(unsigned nvars, 
+                         unsigned var_size) {
+  assert(var_size);
+  __klee_sym_env = malloc(sizeof(*__klee_sym_env) * nvars);
+  assert(__klee_sym_env);
+
+  __klee_sym_env_nvars = nvars;
+  __klee_sym_env_var_size = var_size;  
+}
+
+static unsigned __strlen(const char *s) {
+  const char *s2 = s;
+  while (*s2) ++s2;
+  return s2-s;
+}
+
+extern char *__getenv(const char *name);
+char *getenv(const char *name) {
+  char *res = __getenv(name);
+
+  if (!__klee_sym_env_nvars)
+    return res;
+
+  /* If it exists in the system environment fork and return the actual
+     result or 0. */
+  if (res) {
+    return klee_range(0, 2, name) ? res : 0;
+  } else {
+    unsigned i, len = __strlen(name);
+
+    if (len>=MAX_SYM_ENV_SIZE) {
+      /* Don't deal with strings to large to fit in our name. */
+      return 0;
+    } else {
+      /* Check for existing entry */
+      for (i=0; i<__klee_sym_env_count; ++i)
+        if (memcmp(__klee_sym_env[i].name, name, len+1)==0)
+          return __klee_sym_env[i].value;
+      
+      /* Otherwise create if room and we choose to */
+      if (__klee_sym_env_count < __klee_sym_env_nvars) {
+        if (klee_range(0, 2, name)) {
+          char *s = malloc(__klee_sym_env_var_size+1);
+          klee_make_symbolic(s, __klee_sym_env_var_size+1);
+          s[__klee_sym_env_var_size] = '\0';
+          
+          memcpy(__klee_sym_env[__klee_sym_env_count].name, name, len+1);
+          __klee_sym_env[__klee_sym_env_count].value = s;
+          ++__klee_sym_env_count;
+          
+          return s;
+        }
+      }
+      
+      return 0;
+    }
+  }
+}
+#endif
diff --git a/runtime/POSIX/selinux.c b/runtime/POSIX/selinux.c
new file mode 100644
index 00000000..38acba6c
--- /dev/null
+++ b/runtime/POSIX/selinux.c
@@ -0,0 +1,80 @@
+//===-- selinux.c ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+/* Very basic SELinux support */
+
+#include "klee/Config/config.h"
+
+#ifdef HAVE_SELINUX_SELINUX_H
+
+#include "klee/klee.h"
+
+#include <selinux/selinux.h>
+#include <stdlib.h>
+#include <errno.h>
+
+/* for now, assume we run on an SELinux machine */
+int exe_selinux = 1;
+
+/* NULL is the default policy behavior */
+security_context_t create_con = NULL;
+
+
+int is_selinux_enabled() {
+  return exe_selinux;
+}
+
+
+/***/
+
+int getfscreatecon(security_context_t *context) {
+  *context = create_con;
+  return 0;
+}
+
+
+int setfscreatecon(security_context_t context) {
+  if (context == NULL) {
+    create_con = context;
+    return 0;
+  }
+
+  /* on my machine, setfscreatecon seems to incorrectly accept one
+     char strings.. Also, make sure mcstrans > 0.2.8 for replay 
+     (important bug fixed) */
+  if (context[0] != '\0' && context[1] == '\0')
+    klee_silent_exit(1);
+
+  return -1;
+}
+
+/***/
+
+int setfilecon(const char *path, security_context_t con) {
+  if (con)
+    return 0;
+  
+  errno = ENOSPC;
+  return -1;  
+}
+
+int lsetfilecon(const char *path, security_context_t con) {
+  return setfilecon(path, con);
+}
+
+int fsetfilecon(int fd, security_context_t con) {
+  return setfilecon("", con);
+}
+
+/***/
+
+void freecon(security_context_t con) {}
+void freeconary(security_context_t *con) {}
+
+#endif
diff --git a/runtime/POSIX/stubs.c b/runtime/POSIX/stubs.c
new file mode 100644
index 00000000..cf64f26b
--- /dev/null
+++ b/runtime/POSIX/stubs.c
@@ -0,0 +1,560 @@
+//===-- stubs.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>
+#include <stdio.h>
+#include <errno.h>
+#include <signal.h>
+#include <time.h>
+#include <utime.h>
+#include <utmp.h>
+#include <unistd.h>
+#include <limits.h>
+#include <stdlib.h>
+#include <sys/mman.h>
+#include <sys/stat.h>
+#include <sys/times.h>
+#include <sys/types.h>
+#include <sys/wait.h>
+
+#include "klee/Config/config.h"
+
+void klee_warning(const char*);
+void klee_warning_once(const char*);
+
+/* Silent ignore */
+
+int __syscall_rt_sigaction(int signum, const struct sigaction *act, 
+                           struct sigaction *oldact, size_t _something)
+     __attribute__((weak));
+
+int __syscall_rt_sigaction(int signum, const struct sigaction *act, 
+                           struct sigaction *oldact, size_t _something) {
+  klee_warning_once("silently ignoring");
+  return 0;
+}
+
+int sigaction(int signum, const struct sigaction *act, 
+              struct sigaction *oldact) __attribute__((weak));
+
+int sigaction(int signum, const struct sigaction *act, 
+              struct sigaction *oldact) {
+  klee_warning_once("silently ignoring");
+  return 0;
+}
+
+int sigprocmask(int how, const sigset_t *set, sigset_t *oldset)
+     __attribute__((weak));
+int sigprocmask(int how, const sigset_t *set, sigset_t *oldset) {
+  klee_warning_once("silently ignoring");
+  return 0;
+}
+
+/* Not even worth warning about these */
+int fdatasync(int fd) __attribute__((weak));
+int fdatasync(int fd) {
+  return 0;
+}
+
+/* Not even worth warning about this */
+void sync(void) __attribute__((weak));
+void sync(void) {
+}
+
+/* Error ignore */
+
+extern int __fgetc_unlocked(FILE *f);
+extern int __fputc_unlocked(int c, FILE *f);
+
+int __socketcall(int type, int *args) __attribute__((weak));
+int __socketcall(int type, int *args) {
+  klee_warning("ignoring (EAFNOSUPPORT)");
+  errno = EAFNOSUPPORT;
+  return -1;
+}
+
+int _IO_getc(FILE *f) __attribute__((weak));
+int _IO_getc(FILE *f) {
+  return __fgetc_unlocked(f);
+}
+
+int _IO_putc(int c, FILE *f) __attribute__((weak));
+int _IO_putc(int c, FILE *f) {
+  return __fputc_unlocked(c, f);
+}
+
+int mkdir(const char *pathname, mode_t mode) __attribute__((weak));
+int mkdir(const char *pathname, mode_t mode) {
+  klee_warning("ignoring (EIO)");
+  errno = EIO;
+  return -1;
+}
+
+int mkfifo(const char *pathname, mode_t mode) __attribute__((weak));
+int mkfifo(const char *pathname, mode_t mode) {
+  klee_warning("ignoring (EIO)");
+  errno = EIO;
+  return -1;
+}
+
+int mknod(const char *pathname, mode_t mode, dev_t dev) __attribute__((weak));
+int mknod(const char *pathname, mode_t mode, dev_t dev) {
+  klee_warning("ignoring (EIO)");
+  errno = EIO;
+  return -1;
+}
+
+int pipe(int filedes[2]) __attribute__((weak));
+int pipe(int filedes[2]) {
+  klee_warning("ignoring (ENFILE)");
+  errno = ENFILE;
+  return -1;
+}
+
+int link(const char *oldpath, const char *newpath) __attribute__((weak));
+int link(const char *oldpath, const char *newpath) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;  
+}
+
+int symlink(const char *oldpath, const char *newpath) __attribute__((weak));
+int symlink(const char *oldpath, const char *newpath) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;  
+}
+
+int rename(const char *oldpath, const char *newpath) __attribute__((weak));
+int rename(const char *oldpath, const char *newpath) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;  
+}
+
+int nanosleep(const struct timespec *req, struct timespec *rem) __attribute__((weak));
+int nanosleep(const struct timespec *req, struct timespec *rem) {
+  return 0;
+}
+
+/* XXX why can't I call this internally? */
+int clock_gettime(clockid_t clk_id, struct timespec *res) __attribute__((weak));
+int clock_gettime(clockid_t clk_id, struct timespec *res) {
+  /* Fake */
+  struct timeval tv;
+  gettimeofday(&tv, NULL);
+  res->tv_sec = tv.tv_sec;
+  res->tv_nsec = tv.tv_usec * 1000;
+  return 0;
+}
+
+int clock_settime(clockid_t clk_id, const struct timespec *res) __attribute__((weak));
+int clock_settime(clockid_t clk_id, const struct timespec *res) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+time_t time(time_t *t) {
+  struct timeval tv;
+  gettimeofday(&tv, NULL);
+  if (t)
+    *t = tv.tv_sec;
+  return tv.tv_sec;
+}
+
+clock_t times(struct tms *buf) {
+  /* Fake */
+  buf->tms_utime = 0;
+  buf->tms_stime = 0;
+  buf->tms_cutime = 0;
+  buf->tms_cstime = 0;
+  return 0;
+}
+
+struct utmpx *getutxent(void) __attribute__((weak));
+struct utmpx *getutxent(void) {
+  return (struct utmpx*) getutent();
+}
+
+void setutxent(void) __attribute__((weak));
+void setutxent(void) {
+  setutent();
+}
+
+void endutxent(void) __attribute__((weak));
+void endutxent(void) {
+  endutent();
+}
+
+int utmpxname(const char *file) __attribute__((weak));
+int utmpxname(const char *file) {
+  utmpname(file);
+  return 0;
+}
+
+int euidaccess(const char *pathname, int mode) __attribute__((weak));
+int euidaccess(const char *pathname, int mode) {
+  return access(pathname, mode);
+}
+
+int eaccess(const char *pathname, int mode) __attribute__((weak));
+int eaccess(const char *pathname, int mode) {
+  return euidaccess(pathname, mode);
+}
+
+int group_member (gid_t __gid) __attribute__((weak));
+int group_member (gid_t __gid) {
+  return ((__gid == getgid ()) || (__gid == getegid ()));
+}
+
+int utime(const char *filename, const struct utimbuf *buf) __attribute__((weak));
+int utime(const char *filename, const struct utimbuf *buf) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int utimes(const char *filename, const struct timeval times[2]) __attribute__((weak));
+int utimes(const char *filename, const struct timeval times[2]) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int futimes(int fd, const struct timeval times[2]) __attribute__((weak));
+int futimes(int fd, const struct timeval times[2]) {
+  klee_warning("ignoring (EBADF)");
+  errno = EBADF;
+  return -1;
+}
+
+int strverscmp (__const char *__s1, __const char *__s2) {
+  return strcmp(__s1, __s2); /* XXX no doubt this is bad */
+}
+
+unsigned int gnu_dev_major(unsigned long long int __dev) __attribute__((weak));
+unsigned int gnu_dev_major(unsigned long long int __dev) {
+  return ((__dev >> 8) & 0xfff) | ((unsigned int) (__dev >> 32) & ~0xfff);
+}
+
+unsigned int gnu_dev_minor(unsigned long long int __dev) __attribute__((weak));
+unsigned int gnu_dev_minor(unsigned long long int __dev) {
+  return (__dev & 0xff) | ((unsigned int) (__dev >> 12) & ~0xff);
+}
+
+unsigned long long int gnu_dev_makedev(unsigned int __major, unsigned int __minor) __attribute__((weak));
+unsigned long long int gnu_dev_makedev(unsigned int __major, unsigned int __minor) {
+  return ((__minor & 0xff) | ((__major & 0xfff) << 8)
+	  | (((unsigned long long int) (__minor & ~0xff)) << 12)
+	  | (((unsigned long long int) (__major & ~0xfff)) << 32));
+}
+
+char *canonicalize_file_name (const char *name) __attribute__((weak));
+char *canonicalize_file_name (const char *name) {
+  char *res = malloc(PATH_MAX);
+  char *rp_res = realpath(name, res);
+  if (!rp_res)
+    free(res);
+  return rp_res;
+}
+
+int getloadavg(double loadavg[], int nelem) __attribute__((weak));
+int getloadavg(double loadavg[], int nelem) {
+  klee_warning("ignoring (-1 result)");
+  return -1;
+}
+
+pid_t wait(int *status) __attribute__((weak));
+pid_t wait(int *status) {
+  klee_warning("ignoring (ECHILD)");
+  errno = ECHILD;
+  return -1;
+}
+
+pid_t wait3(int *status, int options, struct rusage *rusage) __attribute__((weak));
+pid_t wait3(int *status, int options, struct rusage *rusage) {
+  klee_warning("ignoring (ECHILD)");
+  errno = ECHILD;
+  return -1;
+}
+
+pid_t wait4(pid_t pid, int *status, int options, struct rusage *rusage) __attribute__((weak));
+pid_t wait4(pid_t pid, int *status, int options, struct rusage *rusage) {
+  klee_warning("ignoring (ECHILD)");
+  errno = ECHILD;
+  return -1;
+}
+
+pid_t waitpid(pid_t pid, int *status, int options) __attribute__((weak));
+pid_t waitpid(pid_t pid, int *status, int options) {
+  klee_warning("ignoring (ECHILD)");
+  errno = ECHILD;
+  return -1;
+}
+
+pid_t waitid(idtype_t idtype, id_t id, siginfo_t *infop, int options) __attribute__((weak));
+pid_t waitid(idtype_t idtype, id_t id, siginfo_t *infop, int options) {
+  klee_warning("ignoring (ECHILD)");
+  errno = ECHILD;
+  return -1;
+}
+
+/* ACL */
+
+/* FIXME: We need autoconf magic for this. */
+
+#ifdef HAVE_SYS_ACL_H
+
+#include <sys/acl.h>
+
+int acl_delete_def_file(const char *path_p) __attribute__((weak));
+int acl_delete_def_file(const char *path_p) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int acl_extended_file(const char path_p) __attribute__((weak));
+int acl_extended_file(const char path_p) {
+  klee_warning("ignoring (ENOENT)");
+  errno = ENOENT;
+  return -1;
+}
+
+int acl_entries(acl_t acl) __attribute__((weak));
+int acl_entries(acl_t acl) {
+  klee_warning("ignoring (EINVAL)");
+  errno = EINVAL;
+  return -1;
+}
+
+acl_t acl_from_mode(mode_t mode) __attribute__((weak));
+acl_t acl_from_mode(mode_t mode) {
+  klee_warning("ignoring (ENOMEM)");
+  errno = ENOMEM;
+  return NULL;
+}
+
+acl_t acl_get_fd(int fd) __attribute__((weak));
+acl_t acl_get_fd(int fd) {
+  klee_warning("ignoring (ENOMEM)");
+  errno = ENOMEM;
+  return NULL;
+}
+
+acl_t acl_get_file(const char *pathname, acl_type_t type) __attribute__((weak));
+acl_t acl_get_file(const char *pathname, acl_type_t type) {
+  klee_warning("ignoring (ENONMEM)");
+  errno = ENOMEM;
+  return NULL;
+}
+
+int acl_set_fd(int fd, acl_t acl) __attribute__((weak));
+int acl_set_fd(int fd, acl_t acl) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int acl_set_file(const char *path_p, acl_type_t type, acl_t acl) __attribute__((weak));
+int acl_set_file(const char *path_p, acl_type_t type, acl_t acl) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int acl_free(void *obj_p) __attribute__((weak));
+int acl_free(void *obj_p) {
+  klee_warning("ignoring (EINVAL)");
+  errno = EINVAL;
+  return -1;
+}
+
+#endif
+
+int mount(const char *source, const char *target, const char *filesystemtype, unsigned long mountflags, const void *data) __attribute__((weak));
+int mount(const char *source, const char *target, const char *filesystemtype, unsigned long mountflags, const void *data) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int umount(const char *target) __attribute__((weak));
+int umount(const char *target) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int umount2(const char *target, int flags) __attribute__((weak));
+int umount2(const char *target, int flags) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int swapon(const char *path, int swapflags) __attribute__((weak));
+int swapon(const char *path, int swapflags) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int swapoff(const char *path) __attribute__((weak));
+int swapoff(const char *path) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setgid(gid_t gid) __attribute__((weak));
+int setgid(gid_t gid) {
+  klee_warning("silently ignoring (returning 0)");
+  return 0;
+}
+
+int setgroups(size_t size, const gid_t *list) __attribute__((weak));
+int setgroups(size_t size, const gid_t *list) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int sethostname(const char *name, size_t len) __attribute__((weak));
+int sethostname(const char *name, size_t len) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setpgid(pid_t pid, pid_t pgid) __attribute__((weak));
+int setpgid(pid_t pid, pid_t pgid) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setpgrp(void) __attribute__((weak));
+int setpgrp(void) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setpriority(__priority_which_t which, id_t who, int prio) __attribute__((weak));
+int setpriority(__priority_which_t which, id_t who, int prio) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setresgid(gid_t rgid, gid_t egid, gid_t sgid) __attribute__((weak));
+int setresgid(gid_t rgid, gid_t egid, gid_t sgid) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setresuid(uid_t ruid, uid_t euid, uid_t suid) __attribute__((weak));
+int setresuid(uid_t ruid, uid_t euid, uid_t suid) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setrlimit(__rlimit_resource_t resource, const struct rlimit *rlim) __attribute__((weak));
+int setrlimit(__rlimit_resource_t resource, const struct rlimit *rlim) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setrlimit64(__rlimit_resource_t resource, const struct rlimit64 *rlim) __attribute__((weak));
+int setrlimit64(__rlimit_resource_t resource, const struct rlimit64 *rlim) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+pid_t setsid(void) __attribute__((weak));
+pid_t setsid(void) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int settimeofday(const struct timeval *tv, const struct timezone *tz) __attribute__((weak));
+int settimeofday(const struct timeval *tv, const struct timezone *tz) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int setuid(uid_t uid) __attribute__((weak));
+int setuid(uid_t uid) {
+  klee_warning("silently ignoring (returning 0)");
+  return 0;
+}
+
+int reboot(int flag) __attribute__((weak));
+int reboot(int flag) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int mlock(const void *addr, size_t len) __attribute__((weak));
+int mlock(const void *addr, size_t len) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int munlock(const void *addr, size_t len) __attribute__((weak));
+int munlock(const void *addr, size_t len) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+int pause(void) __attribute__((weak));
+int pause(void) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+ssize_t readahead(int fd, off64_t *offset, size_t count) __attribute__((weak));
+ssize_t readahead(int fd, off64_t *offset, size_t count) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
+void *mmap(void *start, size_t length, int prot, int flags, int fd, off_t offset) __attribute__((weak));
+void *mmap(void *start, size_t length, int prot, int flags, int fd, off_t offset) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return (void*) -1;
+}
+
+void *mmap64(void *start, size_t length, int prot, int flags, int fd, off64_t offset) __attribute__((weak));
+void *mmap64(void *start, size_t length, int prot, int flags, int fd, off64_t offset) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return (void*) -1;
+}
+
+int munmap(void*start, size_t length) __attribute__((weak));
+int munmap(void*start, size_t length) {
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
diff --git a/runtime/POSIX/testing-dir/a b/runtime/POSIX/testing-dir/a
new file mode 120000
index 00000000..dc1dc0cd
--- /dev/null
+++ b/runtime/POSIX/testing-dir/a
@@ -0,0 +1 @@
+/dev/null
\ No newline at end of file
diff --git a/runtime/POSIX/testing-dir/b b/runtime/POSIX/testing-dir/b
new file mode 120000
index 00000000..b9251ec6
--- /dev/null
+++ b/runtime/POSIX/testing-dir/b
@@ -0,0 +1 @@
+/dev/random
\ No newline at end of file
diff --git a/runtime/POSIX/testing-dir/c b/runtime/POSIX/testing-dir/c
new file mode 100755
index 00000000..2b45f6a5
--- /dev/null
+++ b/runtime/POSIX/testing-dir/c
@@ -0,0 +1,2 @@
+#!/bin/sh
+echo "Hello world!"
diff --git a/runtime/POSIX/testing-dir/d b/runtime/POSIX/testing-dir/d
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/runtime/POSIX/testing-dir/d
diff --git a/runtime/POSIX/testing-env b/runtime/POSIX/testing-env
new file mode 100644
index 00000000..5a6e8eb8
--- /dev/null
+++ b/runtime/POSIX/testing-env
@@ -0,0 +1,27 @@
+# This file is sourced prior to running the testing environment, make
+# sure to quote things.
+
+export TERM="xterm"
+export SHELL="/bin/bash"
+export LS_COLORS="no=00:fi=00:di=01;34:ln=01;36:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:su=37;41:sg=30;43:tw=30;42:ow=34;42:st=37;44:ex=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.gz=01;31:*.bz2=01;31:*.deb=01;31:*.rpm=01;31:*.jar=01;31:*.jpg=01;35:*.jpeg=01;35:*.gif=01;35:*.bmp=01;35:*.pbm=01;35:*.pgm=01;35:*.ppm=01;35:*.tga=01;35:*.xbm=01;35:*.xpm=01;35:*.tif=01;35:*.tiff=01;35:*.png=01;35:*.mov=01;35:*.mpg=01;35:*.mpeg=01;35:*.avi=01;35:*.fli=01;35:*.gl=01;35:*.dl=01;35:*.xcf=01;35:*.xwd=01;35:*.flac=01;35:*.mp3=01;35:*.mpc=01;35:*.ogg=01;35:*.wav=01;35:"
+export PATH="/usr/local/bin:/usr/bin:/bin"
+export COLORTERM="gnome-terminal"
+export LC_ALL=C
+export TABSIZE=8
+export COLUMNS=80
+
+#       1 BLOCK_SIZE
+#       2 COLUMNS
+#       1 DF_BLOCK_SIZE
+#       1 DU_BLOCK_SIZE
+#       1 HOME
+#       1 LS_BLOCK_SIZE
+#       1 LS_COLORS
+#      11 POSIXLY_CORRECT
+#       1 QUOTING_STYLE
+#       3 SHELL
+#       4 SIMPLE_BACKUP_SUFFIX
+#       1 TABSIZE
+#       2 TERM
+#       2 TIME_STYLE
+#       4 TMPDIR