| //===-- 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 (((off64_t)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 < (off64_t) 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; |
| } |
| |
| { |
| #if __WORDSIZE == 64 |
| int r = syscall(__NR_stat, __concretize_string(path), buf); |
| #else |
| int r = syscall(__NR_stat64, __concretize_string(path), buf); |
| #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) { |
| memcpy(buf, dfile->stat, sizeof(*dfile->stat)); |
| return 0; |
| } |
| |
| { |
| #if __WORDSIZE == 64 |
| int r = syscall(__NR_lstat, __concretize_string(path), buf); |
| #else |
| int r = syscall(__NR_lstat64, __concretize_string(path), buf); |
| #endif |
| 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) { |
| #if __WORDSIZE == 64 |
| int r = syscall(__NR_fstat, f->fd, buf); |
| #else |
| int r = syscall(__NR_fstat64, f->fd, buf); |
| #endif |
| 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 { |
| #if __WORDSIZE == 64 |
| int r = syscall(__NR_ftruncate, f->fd, length); |
| #else |
| int r = syscall(__NR_ftruncate64, f->fd, length); |
| #endif |
| 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 long) f->off < 4096u) { |
| /* Return our dirents */ |
| unsigned i, pad, bytes=0; |
| |
| /* What happens for bad offsets? */ |
| i = f->off / sizeof(*dirp); |
| if (((off64_t) (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; |
| } |
| } |
| } |
| |
| #if __WORDSIZE == 64 |
| int ioctl(int fd, unsigned long int request, ...) { |
| #else |
| int ioctl(int fd, unsigned long request, ...) { |
| #endif |
| 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 < (off64_t) 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_valuel((long) p); |
| klee_assume(pc == p); |
| return pc; |
| } |
| |
| static size_t __concretize_size(size_t s) { |
| size_t sc = klee_get_valuel((long)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_valuel((long)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; |
| } |