diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2013-09-25 07:36:44 -0700 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2013-09-25 07:36:44 -0700 |
commit | 43138101d048394690a90fd9f5a6fb0df916161c (patch) | |
tree | 70e9d4a75804cc2ef12bda03fd029c013462e123 /runtime/POSIX | |
parent | 1510c721187f1e838d30fca376af2ab5af90ee6c (diff) | |
parent | 90601a60fb6a0f22337c46680f150ec04ad3c6cb (diff) | |
download | klee-43138101d048394690a90fd9f5a6fb0df916161c.tar.gz |
Merge pull request #25 from paulmar/master
Added some of the common *at functions & others to the model. Obey --max-forks in switch statements.
Diffstat (limited to 'runtime/POSIX')
-rw-r--r-- | runtime/POSIX/fd.c | 161 | ||||
-rw-r--r-- | runtime/POSIX/fd.h | 1 | ||||
-rw-r--r-- | runtime/POSIX/fd_32.c | 20 | ||||
-rw-r--r-- | runtime/POSIX/fd_64.c | 14 | ||||
-rw-r--r-- | runtime/POSIX/stubs.c | 7 |
5 files changed, 196 insertions, 7 deletions
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)"); |