Merge pull request #25 from paulmar/master

Added some of the common *at functions & others to the model.  Obey --max-forks in switch statements.

8 files changed, 286 insertions, 23 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index bef34059..caf0de36 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -572,20 +572,31 @@ void Executor::branch(ExecutionState &state,
   unsigned N = conditions.size();
   assert(N);
 
-  stats::forks += N-1;
-
-  // XXX do proper balance or keep random?
-  result.push_back(&state);
-  for (unsigned i=1; i<N; ++i) {
-    ExecutionState *es = result[theRNG.getInt32() % i];
-    ExecutionState *ns = es->branch();
-    addedStates.insert(ns);
-    result.push_back(ns);
-    es->ptreeNode->data = 0;
-    std::pair<PTree::Node*,PTree::Node*> res = 
-      processTree->split(es->ptreeNode, ns, es);
-    ns->ptreeNode = res.first;
-    es->ptreeNode = res.second;
+  if (MaxForks!=~0u && stats::forks >= MaxForks) {
+    unsigned next = theRNG.getInt32() % N;
+    for (unsigned i=0; i<N; ++i) {
+      if (i == next) {
+        result.push_back(&state);
+      } else {
+        result.push_back(NULL);
+      }
+    }
+  } else {
+    stats::forks += N-1;
+
+    // XXX do proper balance or keep random?
+    result.push_back(&state);
+    for (unsigned i=1; i<N; ++i) {
+      ExecutionState *es = result[theRNG.getInt32() % i];
+      ExecutionState *ns = es->branch();
+      addedStates.insert(ns);
+      result.push_back(ns);
+      es->ptreeNode->data = 0;
+      std::pair<PTree::Node*,PTree::Node*> res = 
+        processTree->split(es->ptreeNode, ns, es);
+      ns->ptreeNode = res.first;
+      es->ptreeNode = res.second;
+    }
   }
 
   // If necessary redistribute seeds to match conditions, killing
@@ -620,12 +631,14 @@ void Executor::branch(ExecutionState &state,
       if (i==N)
         i = theRNG.getInt32() % N;
 
-      seedMap[result[i]].push_back(*siit);
+      // Extra check in case we're replaying seeds with a max-fork
+      if (result[i])
+        seedMap[result[i]].push_back(*siit);
     }
 
     if (OnlyReplaySeeds) {
       for (unsigned i=0; i<N; ++i) {
-        if (!seedMap.count(result[i])) {
+        if (result[i] && !seedMap.count(result[i])) {
           terminateState(*result[i]);
           result[i] = NULL;
         }
diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index b9a848d0..09dd7be5 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -198,6 +198,108 @@ int __fd_open(const char *pathname, int flags, mode_t mode) {
   return fd;
 }
 
+int __fd_openat(int basefd, const char *pathname, int flags, mode_t mode) {
+  exe_file_t *f;
+  int fd;
+  if (basefd != AT_FDCWD) {
+    exe_file_t *bf = __get_file(basefd);
+
+    if (!bf) {
+      errno = EBADF;
+      return -1;
+    } else if (bf->dfile) {
+      klee_warning("symbolic file descriptor, ignoring (ENOENT)");
+      errno = ENOENT;
+      return -1;
+    }
+    basefd = bf->fd;
+  }
+
+  if (__get_sym_file(pathname)) {
+    /* for a symbolic file, it doesn't matter if/where it exists on disk */
+    return __fd_open(pathname, flags, mode);
+  }
+
+  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);
+
+  int os_fd = syscall(__NR_openat, (long)basefd, __concretize_string(pathname), (long)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 utimes(const char *path, const struct timeval times[2]) {
+  exe_disk_file_t *dfile = __get_sym_file(path);
+
+  if (dfile) {
+    /* don't bother with usecs */
+    dfile->stat->st_atime = times[0].tv_sec;
+    dfile->stat->st_mtime = times[1].tv_sec;
+#ifdef _BSD_SOURCE
+    dfile->stat->st_atim.tv_nsec = 1000000000ll * times[0].tv_sec;
+    dfile->stat->st_mtim.tv_nsec = 1000000000ll * times[1].tv_sec;
+#endif
+    return 0;
+  }
+  int r = syscall(__NR_utimes, __concretize_string(path), times);
+  if (r == -1)
+    errno = klee_get_errno();
+
+  return r;
+}
+
+
+int futimesat(int fd, const char* path, const struct timeval times[2]) {
+  if (fd != AT_FDCWD) {
+    exe_file_t *f = __get_file(fd);
+
+    if (!f) {
+      errno = EBADF;
+      return -1;
+    } else if (f->dfile) {
+      klee_warning("symbolic file descriptor, ignoring (ENOENT)");
+      errno = ENOENT;
+      return -1;
+    }
+    fd = f->fd;
+  }
+  if (__get_sym_file(path)) {
+    return utimes(path, times);
+  }
+
+  int r = syscall(__NR_futimesat, (long)fd,
+                 (path ? __concretize_string(path) : NULL),
+                 times);
+  if (r == -1)
+    errno = klee_get_errno();
+  return r;
+}
+ 
 int close(int fd) {
   static int n_calls = 0;
   exe_file_t *f;
@@ -446,6 +548,42 @@ int __fd_stat(const char *path, struct stat64 *buf) {
   }
 }
 
+int fstatat(int fd, const char *path, struct stat *buf, int flags) {  
+  if (fd != AT_FDCWD) {
+    exe_file_t *f = __get_file(fd);
+
+    if (!f) {
+      errno = EBADF;
+      return -1;
+    } else if (f->dfile) {
+      klee_warning("symbolic file descriptor, ignoring (ENOENT)");
+      errno = ENOENT;
+      return -1;
+    }
+    fd = f->fd;
+  }
+  exe_disk_file_t *dfile = __get_sym_file(path);
+  if (dfile) {
+    memcpy(buf, dfile->stat, sizeof(*dfile->stat));
+    return 0;
+  } 
+
+#if (defined __NR_newfstatat) && (__NR_newfstatat != 0)
+  int r = syscall(__NR_newfstatat, (long)fd,
+               (path ? __concretize_string(path) : NULL),
+               buf, (long)flags);
+#else
+  int r = syscall(__NR_fstatat64, (long)fd,
+               (path ? __concretize_string(path) : NULL),
+               buf, (long)flags);
+#endif
+
+  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) {
@@ -1096,6 +1234,29 @@ int unlink(const char *pathname) {
   return -1;
 }
 
+int unlinkat(int dirfd, const char *pathname, int flags) {
+  /* similar to unlink. keep them separated though to avoid
+     problems if unlink changes to actually delete files */
+  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) {
diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h
index f2780143..cb86295c 100644
--- a/runtime/POSIX/fd.h
+++ b/runtime/POSIX/fd.h
@@ -79,6 +79,7 @@ void klee_init_env(int *argcPtr, char ***argvPtr);
 /* *** */
 
 int __fd_open(const char *pathname, int flags, mode_t mode);
+int __fd_openat(int basefd, 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);
diff --git a/runtime/POSIX/fd_32.c b/runtime/POSIX/fd_32.c
index 1e96de37..13195fbf 100644
--- a/runtime/POSIX/fd_32.c
+++ b/runtime/POSIX/fd_32.c
@@ -53,6 +53,12 @@ static void __stat64_to_stat(struct stat64 *a, struct stat *b) {
   b->st_ctime = a->st_ctime;
   b->st_blksize = a->st_blksize;
   b->st_blocks = a->st_blocks;
+#ifdef _BSD_SOURCE
+  b->st_atim.tv_nsec = a->st_atim.tv_nsec;
+  b->st_mtim.tv_nsec = a->st_mtim.tv_nsec;
+  b->st_ctim.tv_nsec = a->st_ctim.tv_nsec;
+#endif
+
 }
 
 /***/
@@ -71,6 +77,20 @@ int open(const char *pathname, int flags, ...) {
   return __fd_open(pathname, flags, mode);
 }
 
+int openat(int fd, 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_openat(fd, pathname, flags, mode);
+}
+
 off_t lseek(int fd, off_t off, int whence) {
   return (off_t) __fd_lseek(fd, off, whence);
 }
diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c
index 268579c0..2178ad14 100644
--- a/runtime/POSIX/fd_64.c
+++ b/runtime/POSIX/fd_64.c
@@ -57,6 +57,20 @@ int open(const char *pathname, int flags, ...) {
   return __fd_open(pathname, flags, mode);
 }
 
+int openat(int fd, 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_openat(fd, pathname, flags, mode);
+}
+
 off64_t lseek(int fd, off64_t offset, int whence) {
   return __fd_lseek(fd, offset, whence);
 }
diff --git a/runtime/POSIX/stubs.c b/runtime/POSIX/stubs.c
index 3a9d380c..7a424d05 100644
--- a/runtime/POSIX/stubs.c
+++ b/runtime/POSIX/stubs.c
@@ -222,13 +222,6 @@ int utime(const char *filename, const struct utimbuf *buf) {
   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)");
diff --git a/test/Runtime/POSIX/Futimesat.c b/test/Runtime/POSIX/Futimesat.c
new file mode 100644
index 00000000..fd9ea0de
--- /dev/null
+++ b/test/Runtime/POSIX/Futimesat.c
@@ -0,0 +1,43 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t2.bc
+// RUN: touch /tmp/futimesat-dummy
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: rm /tmp/futimesat-dummy
+
+#include <assert.h>
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <time.h>
+
+int main(int argc, char **argv) {
+  int r;
+  struct stat buf;
+  struct timeval times[2];
+
+  times[0].tv_sec = time(NULL)-3600;
+  times[0].tv_usec = 0;
+  times[1].tv_sec = time(NULL)-3600;
+  times[1].tv_usec = 0;
+
+  r = futimesat(AT_FDCWD, "A", times);
+  assert(r != -1);
+
+  r = fstatat(AT_FDCWD, "A", &buf, 0);
+  assert(r != -1);
+  assert(buf.st_atime == times[0].tv_sec &&
+         buf.st_mtime == times[1].tv_sec);
+
+  /* assumes /tmp exists and is writeable */
+  int fd = open("/tmp", O_RDONLY);
+  assert(fd > 0);
+  r = futimesat(fd, "futimesat-dummy", times);
+  assert(r != -1);
+
+  r = fstatat(fd, "futimesat-dummy", &buf, 0);
+  assert(r != -1);
+  assert(buf.st_atime == times[0].tv_sec &&
+         buf.st_mtime == times[1].tv_sec);
+
+  close(fd);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c
new file mode 100644
index 00000000..d417ee47
--- /dev/null
+++ b/test/Runtime/POSIX/Openat.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: test -f klee-last/test000001.ktest
+
+#include <assert.h>
+#include <fcntl.h>
+
+int main(int argc, char **argv) {
+  int fd = openat(AT_FDCWD, "A", O_RDWR|O_TRUNC);
+  if (fd != -1) {
+    char buf[10];
+    assert(read(fd, buf, 10) == 10);
+    assert(klee_is_symbolic(buf[0]));
+  } else {
+    klee_silent_exit(0);
+  }
+  return 0;
+}