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

1 files changed, 1287 insertions, 0 deletions

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;
+}