diff options
Diffstat (limited to 'runtime')
57 files changed, 4273 insertions, 0 deletions
diff --git a/runtime/Intrinsic/Makefile b/runtime/Intrinsic/Makefile new file mode 100644 index 00000000..ce4a34ba --- /dev/null +++ b/runtime/Intrinsic/Makefile @@ -0,0 +1,20 @@ +#===-- runtime/Intrinsic/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=intrinsic +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/Intrinsic/klee_div_zero_check.c b/runtime/Intrinsic/klee_div_zero_check.c new file mode 100644 index 00000000..3fde1af5 --- /dev/null +++ b/runtime/Intrinsic/klee_div_zero_check.c @@ -0,0 +1,15 @@ +//===-- klee_div_zero_check.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> + +void klee_div_zero_check(long long z) { + if (z == 0) + klee_report_error(__FILE__, __LINE__, "divide by zero", "div.err"); +} diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c new file mode 100644 index 00000000..88ec5026 --- /dev/null +++ b/runtime/Intrinsic/klee_int.c @@ -0,0 +1,17 @@ +//===-- klee_int.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 <klee/klee.h> + +int klee_int(const char *name) { + int x; + klee_make_symbolic_name(&x, sizeof x, name); + return x; +} diff --git a/runtime/Intrinsic/klee_make_symbolic.c b/runtime/Intrinsic/klee_make_symbolic.c new file mode 100644 index 00000000..b9dec2a7 --- /dev/null +++ b/runtime/Intrinsic/klee_make_symbolic.c @@ -0,0 +1,14 @@ +//===-- klee_make_symbolic.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> + +void klee_make_symbolic(void *addr, unsigned nbytes) { + klee_make_symbolic_name(addr, nbytes, "unnamed"); +} diff --git a/runtime/Intrinsic/klee_range.c b/runtime/Intrinsic/klee_range.c new file mode 100644 index 00000000..59d1a05e --- /dev/null +++ b/runtime/Intrinsic/klee_range.c @@ -0,0 +1,33 @@ +//===-- klee_range.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 <klee/klee.h> + +int klee_range(int start, int end, const char* name) { + int x; + + assert(start < end); + + if (start+1==end) { + return start; + } else { + klee_make_symbolic_name(&x, sizeof x, name); + + /* Make nicer constraint when simple... */ + if (start==0) { + klee_assume((unsigned) x < (unsigned) end); + } else { + klee_assume(start <= x); + klee_assume(x < end); + } + + return x; + } +} diff --git a/runtime/Intrinsic/memcpy.c b/runtime/Intrinsic/memcpy.c new file mode 100644 index 00000000..14b98ce6 --- /dev/null +++ b/runtime/Intrinsic/memcpy.c @@ -0,0 +1,19 @@ +//===-- memcpy.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +void *memcpy(void *destaddr, void const *srcaddr, unsigned int len) { + char *dest = destaddr; + char const *src = srcaddr; + + while (len-- > 0) + *dest++ = *src++; + return destaddr; +} diff --git a/runtime/Intrinsic/memmove.c b/runtime/Intrinsic/memmove.c new file mode 100644 index 00000000..c6e1ada9 --- /dev/null +++ b/runtime/Intrinsic/memmove.c @@ -0,0 +1,28 @@ +//===-- memmove.c ---------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +void *memmove(void *dst, const void *src, size_t count) { + char *a = dst; + const char *b = src; + + if (src == dst) + return dst; + + if (src>dst) { + while (count--) *a++ = *b++; + } else { + a+=count-1; + b+=count-1; + while (count--) *a-- = *b--; + } + + return dst; +} diff --git a/runtime/Intrinsic/mempcpy.c b/runtime/Intrinsic/mempcpy.c new file mode 100644 index 00000000..6327e748 --- /dev/null +++ b/runtime/Intrinsic/mempcpy.c @@ -0,0 +1,19 @@ +//===-- mempcpy.c ---------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +void *mempcpy(void *destaddr, void const *srcaddr, unsigned int len) { + char *dest = destaddr; + char const *src = srcaddr; + + while (len-- > 0) + *dest++ = *src++; + return dest; +} diff --git a/runtime/Intrinsic/memset.c b/runtime/Intrinsic/memset.c new file mode 100644 index 00000000..ee9ecb87 --- /dev/null +++ b/runtime/Intrinsic/memset.c @@ -0,0 +1,17 @@ +//===-- memset.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +void *memset(void * dst, int s, size_t count) { + char * a = dst; + while (count-- > 0) + *a++ = s; + return dst; +} diff --git a/runtime/Makefile b/runtime/Makefile new file mode 100755 index 00000000..24824d08 --- /dev/null +++ b/runtime/Makefile @@ -0,0 +1,26 @@ +#===-- runtime/Makefile ------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +# +# Relative path to the top of the source tree. +# +LEVEL=.. + +# +# List all of the subdirectories that we will compile. +# +PARALLEL_DIRS=Intrinsic klee-libc Runtest + +include $(LEVEL)/Makefile.config + +ifeq ($(ENABLE_POSIX_RUNTIME),1) +PARALLEL_DIRS += POSIX +endif + +include $(LEVEL)/Makefile.common 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 diff --git a/runtime/Runtest/Makefile b/runtime/Runtest/Makefile new file mode 100644 index 00000000..dd21c4a9 --- /dev/null +++ b/runtime/Runtest/Makefile @@ -0,0 +1,19 @@ +#===-- runtime/Runtest/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=../.. + +USEDLIBS=kleeBasic.a +LIBRARYNAME=kleeRuntest +SHARED_LIBRARY=1 +LINK_LIBS_IN_SHARED = 1 +DONT_BUILD_RELINKED = 1 +NO_PEDANTIC=1 + +include $(LEVEL)/Makefile.common diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c new file mode 100644 index 00000000..1a2fd030 --- /dev/null +++ b/runtime/Runtest/intrinsics.c @@ -0,0 +1,154 @@ +//===-- intrinsics.c ------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +/* Straight C for linking simplicity */ + +#include <assert.h> +#include <stdlib.h> +#include <stdio.h> +#include <string.h> +#include <sys/mman.h> +#include <sys/time.h> +#include <time.h> + +#include "klee/klee.h" + +#include "klee/Internal/ADT/BOut.h" + +static BOut *testData = 0; +static unsigned testPosition = 0; + +static unsigned char rand_byte(void) { + unsigned x = rand(); + x ^= x>>16; + x ^= x>>8; + return x & 0xFF; +} + +void klee_make_symbolic_name(void *array, unsigned nbytes, const char *name) { + static int rand_init = -1; + + if (rand_init == -1) { + if (getenv("KLEE_RANDOM")) { + struct timeval tv; + gettimeofday(&tv, 0); + rand_init = 1; + srand(tv.tv_sec ^ tv.tv_usec); + } else { + rand_init = 0; + } + } + + if (rand_init) { + if (!strcmp(name,"syscall_a0")) { + unsigned long long *v = array; + assert(nbytes == 8); + *v = rand() % 69; + } else { + char *c = array; + unsigned i; + for (i=0; i<nbytes; i++) + c[i] = rand_byte(); + } + return; + } + + if (!testData) { + char tmp[256]; + char *name = getenv("KLEE_RUNTEST"); + + if (!name) { + fprintf(stdout, "KLEE-RUNTIME: KLEE_RUNTEST not set, please enter .bout path: "); + fflush(stdout); + name = tmp; + if (!fgets(tmp, sizeof tmp, stdin) || !strlen(tmp)) { + fprintf(stderr, "KLEE-RUNTIME: cannot replay, no KLEE_RUNTEST or user input\n"); + exit(1); + } + tmp[strlen(tmp)-1] = '\0'; /* kill newline */ + } + testData = bOut_fromFile(name); + if (!testData) { + fprintf(stderr, "KLEE-RUNTIME: unable to open .bout file\n"); + exit(1); + } + } + + if (testPosition >= testData->numObjects) { + fprintf(stderr, "ERROR: out of inputs, using zero\n"); + memset(array, 0, nbytes); + } else { + BOutObject *o = &testData->objects[testPosition++]; + memcpy(array, o->bytes, nbytes<o->numBytes ? nbytes : o->numBytes); + if (nbytes != o->numBytes) { + fprintf(stderr, "ERROR: object sizes differ\n"); + if (o->numBytes < nbytes) + memset((char*) array + o->numBytes, 0, nbytes - o->numBytes); + } + } +} + +void klee_make_symbolic(void *array, unsigned nbytes) { + klee_make_symbolic_name(array, nbytes, "unnamed"); +} + +void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment) { +#if 1 + return mmap((void*) 0x90000000, nelems*size, PROT_READ|PROT_WRITE, + MAP_PRIVATE +#ifdef MAP_ANONYMOUS + |MAP_ANONYMOUS +#endif + , 0, 0); +#else + char *buffer = malloc(nelems*size + alignment - 1); + buffer += (alignment - (long)buffer % alignment); + return buffer; +#endif +} + +void klee_silent_exit(int x) { + exit(x); +} + +unsigned klee_choose(unsigned n) { + unsigned x; + klee_make_symbolic(&x, sizeof x); + if(x >= n) + fprintf(stderr, "ERROR: max = %d, got = %d\n", n, x); + assert(x < n); + return x; +} + +void klee_assume(unsigned x) { + if (!x) { + fprintf(stderr, "ERROR: invalid klee_assume\n"); + } +} + +unsigned klee_get_value(unsigned x) { + return x; +} + +int klee_range_name(int begin, int end, const char* name) { + int x; + klee_make_symbolic_name(&x, sizeof x, name); + if (x<begin || x>=end) { + fprintf(stderr, + "KLEE: ERROR: invalid klee_range(%u,%u,%s) value, got: %u\n", + begin, end, name, x); + abort(); + } + return x; +} + +/* not sure we should even define. is for debugging. */ +void klee_print_expr(const char *msg, ...) { } + +void klee_set_forking(unsigned enable) { } diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile new file mode 100755 index 00000000..bcd61f73 --- /dev/null +++ b/runtime/klee-libc/Makefile @@ -0,0 +1,19 @@ +#===-- runtime/klee-libc/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=klee-libc +DONT_BUILD_RELINKED=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/klee-libc/__cxa_atexit.c b/runtime/klee-libc/__cxa_atexit.c new file mode 100644 index 00000000..e7982848 --- /dev/null +++ b/runtime/klee-libc/__cxa_atexit.c @@ -0,0 +1,49 @@ +//===-- __cxa_atexit.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 MAX_ATEXIT 128 + +static struct { + void (*fn)(void*); + void *arg; + void *dso_handle; +} AtExit[MAX_ATEXIT]; +static unsigned NumAtExit = 0; + +static void RunAtExit(void) __attribute__((destructor)); +static void RunAtExit(void) { + unsigned i; + + for (i=0; i<NumAtExit; ++i) + AtExit[i].fn(AtExit[i].arg); +} + +int __cxa_atexit(void (*fn)(void*), + void *arg, + void *dso_handle) { + klee_warning_once("FIXME: __cxa_atexit being ignored"); + + /* Better to just report an error here than return 1 (the defined + * semantics). + */ + if (NumAtExit == MAX_ATEXIT) + klee_report_error(__FILE__, + __LINE__, + "__cxa_atexit: no room in array!", + "exec"); + + AtExit[NumAtExit].fn = fn; + AtExit[NumAtExit].arg = arg; + ++NumAtExit; + + return 0; +} + diff --git a/runtime/klee-libc/abort.c b/runtime/klee-libc/abort.c new file mode 100644 index 00000000..0332d095 --- /dev/null +++ b/runtime/klee-libc/abort.c @@ -0,0 +1,16 @@ +//===-- abort.c -----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +#include "klee/klee.h" + +void abort(void) { + klee_abort(); +} diff --git a/runtime/klee-libc/atexit.c b/runtime/klee-libc/atexit.c new file mode 100644 index 00000000..c71b2cd6 --- /dev/null +++ b/runtime/klee-libc/atexit.c @@ -0,0 +1,16 @@ +//===-- atexit.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +int __cxa_atexit(void (*fn)(void*), + void *arg, + void *dso_handle); + +int atexit(void (*fn)(void)) { + return __cxa_atexit((void(*)(void*)) fn, 0, 0); +} diff --git a/runtime/klee-libc/atoi.c b/runtime/klee-libc/atoi.c new file mode 100644 index 00000000..ab97bfbb --- /dev/null +++ b/runtime/klee-libc/atoi.c @@ -0,0 +1,37 @@ +/* + * Copyright (c) 1988, 1993 + * The Regents of the University of California. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ +#include <stdlib.h> + +int atoi(const char *str) { + return (int)strtol(str, (char **)NULL, 10); +} diff --git a/runtime/klee-libc/calloc.c b/runtime/klee-libc/calloc.c new file mode 100644 index 00000000..30b88b30 --- /dev/null +++ b/runtime/klee-libc/calloc.c @@ -0,0 +1,46 @@ +//===-- calloc.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> +#include <string.h> + +// DWD - I prefer to be internal +#if 0 +void *calloc(size_t nmemb, size_t size) { + unsigned nbytes = nmemb * size; + void *addr = malloc(nbytes); + if(addr) + memset(addr, 0, nbytes); + return addr; +} +// Always reallocate. +void *realloc(void *ptr, size_t nbytes) { + if(!ptr) + return malloc(nbytes); + + if(!nbytes) { + free(ptr); + return 0; + } + + unsigned copy_nbytes = klee_get_obj_size(ptr); + //printf("REALLOC: current object = %d bytes!\n", copy_nbytes); + + void *addr = malloc(nbytes); + if(addr) { + // shrinking + if(copy_nbytes > nbytes) + copy_nbytes = nbytes; + //printf("REALLOC: copying = %d bytes!\n", copy_nbytes); + memcpy(addr, ptr, copy_nbytes); + free(ptr); + } + return addr; +} +#endif diff --git a/runtime/klee-libc/htonl.c b/runtime/klee-libc/htonl.c new file mode 100644 index 00000000..cec2d0f5 --- /dev/null +++ b/runtime/klee-libc/htonl.c @@ -0,0 +1,49 @@ +//===-- htonl.c -----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <sys/types.h> +#include <sys/param.h> +#include <stdint.h> + +#undef htons +#undef htonl +#undef ntohs +#undef ntohl + +// Make sure we can recognize the endianness. +#if (!defined(BYTE_ORDER) || !defined(BIG_ENDIAN) || !defined(LITTLE_ENDIAN)) +#error "Unknown platform endianness!" +#endif + +#if BYTE_ORDER == LITTLE_ENDIAN + +uint16_t htons(uint16_t v) { + return (v >> 8) | (v << 8); +} +uint32_t htonl(uint32_t v) { + return htons(v >> 16) | (htons((uint16_t) v) << 16); +} + +#else + +uint16_t htons(uint16_t v) { + return v; +} +uint32_t htonl(uint32_t v) { + return v; +} + +#endif + +uint16_t ntohs(uint32_t v) { + return htons(v); +} +uint32_t ntohl(uint32_t v) { + return htonl(v); +} diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c new file mode 100644 index 00000000..106b4f89 --- /dev/null +++ b/runtime/klee-libc/klee-choose.c @@ -0,0 +1,20 @@ +//===-- klee-choose.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" + +unsigned klee_choose(unsigned n) { + unsigned x; + klee_make_symbolic(&x, sizeof x); + + // NB: this will *not* work if they don't compare to n values. + if(x >= n) + klee_silent_exit(0); + return x; +} diff --git a/runtime/klee-libc/memchr.c b/runtime/klee-libc/memchr.c new file mode 100644 index 00000000..fe0670a7 --- /dev/null +++ b/runtime/klee-libc/memchr.c @@ -0,0 +1,54 @@ +/*- + * Copyright (c) 1990, 1993 + * The Regents of the University of California. All rights reserved. + * + * This code is derived from software contributed to Berkeley by + * Chris Torek. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include <string.h> + +void * +memchr(s, c, n) + const void *s; + int c; + size_t n; +{ + if (n != 0) { + const unsigned char *p = s; + + do { + if (*p++ == c) + return ((void *)(p - 1)); + } while (--n != 0); + } + return (NULL); +} diff --git a/runtime/klee-libc/memcmp.c b/runtime/klee-libc/memcmp.c new file mode 100644 index 00000000..7562f4f7 --- /dev/null +++ b/runtime/klee-libc/memcmp.c @@ -0,0 +1,53 @@ +/*- + * Copyright (c) 1990, 1993 + * The Regents of the University of California. All rights reserved. + * + * This code is derived from software contributed to Berkeley by + * Chris Torek. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include <string.h> + +/* + * Compare memory regions. + */ +int memcmp(const void *s1, const void *s2, size_t n) { + if (n != 0) { + const unsigned char *p1 = s1, *p2 = s2; + + do { + if (*p1++ != *p2++) { + return (*--p1 - *--p2); + } + } while (--n != 0); + } + return (0); +} diff --git a/runtime/klee-libc/memcpy.c b/runtime/klee-libc/memcpy.c new file mode 100644 index 00000000..14b98ce6 --- /dev/null +++ b/runtime/klee-libc/memcpy.c @@ -0,0 +1,19 @@ +//===-- memcpy.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +void *memcpy(void *destaddr, void const *srcaddr, unsigned int len) { + char *dest = destaddr; + char const *src = srcaddr; + + while (len-- > 0) + *dest++ = *src++; + return destaddr; +} diff --git a/runtime/klee-libc/memmove.c b/runtime/klee-libc/memmove.c new file mode 100644 index 00000000..c6e1ada9 --- /dev/null +++ b/runtime/klee-libc/memmove.c @@ -0,0 +1,28 @@ +//===-- memmove.c ---------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +void *memmove(void *dst, const void *src, size_t count) { + char *a = dst; + const char *b = src; + + if (src == dst) + return dst; + + if (src>dst) { + while (count--) *a++ = *b++; + } else { + a+=count-1; + b+=count-1; + while (count--) *a-- = *b--; + } + + return dst; +} diff --git a/runtime/klee-libc/mempcpy.c b/runtime/klee-libc/mempcpy.c new file mode 100644 index 00000000..6327e748 --- /dev/null +++ b/runtime/klee-libc/mempcpy.c @@ -0,0 +1,19 @@ +//===-- mempcpy.c ---------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +void *mempcpy(void *destaddr, void const *srcaddr, unsigned int len) { + char *dest = destaddr; + char const *src = srcaddr; + + while (len-- > 0) + *dest++ = *src++; + return dest; +} diff --git a/runtime/klee-libc/memset.c b/runtime/klee-libc/memset.c new file mode 100644 index 00000000..ee9ecb87 --- /dev/null +++ b/runtime/klee-libc/memset.c @@ -0,0 +1,17 @@ +//===-- memset.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <stdlib.h> + +void *memset(void * dst, int s, size_t count) { + char * a = dst; + while (count-- > 0) + *a++ = s; + return dst; +} diff --git a/runtime/klee-libc/putchar.c b/runtime/klee-libc/putchar.c new file mode 100644 index 00000000..f3fcf01d --- /dev/null +++ b/runtime/klee-libc/putchar.c @@ -0,0 +1,17 @@ +//===-- putchar.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 <unistd.h> + +int putchar(int c) { + char x = c; + write(1, &x, 1); + return 1; +} diff --git a/runtime/klee-libc/stpcpy.c b/runtime/klee-libc/stpcpy.c new file mode 100644 index 00000000..1f774f3d --- /dev/null +++ b/runtime/klee-libc/stpcpy.c @@ -0,0 +1,43 @@ +/* + * Copyright (c) 1999 + * David E. O'Brien + * Copyright (c) 1988, 1993 + * The Regents of the University of California. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include <string.h> + +/* Defeat object checking stuff. */ +#undef stpcpy + +char * +stpcpy(char * to, const char * from) +{ + + for (; (*to = *from); ++from, ++to); + return(to); +} diff --git a/runtime/klee-libc/strcat.c b/runtime/klee-libc/strcat.c new file mode 100644 index 00000000..195e9460 --- /dev/null +++ b/runtime/klee-libc/strcat.c @@ -0,0 +1,47 @@ +/* + * Copyright (c) 1988, 1993 + * The Regents of the University of California. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include <string.h> + +/* Defeat object checking stuff. */ +#undef strcat + +char * strcat(char * s, const char * append) { + char *save = s; + + for (; *s; ++s) + ; + while ((*s++ = *append++)) + ; + return(save); +} diff --git a/runtime/klee-libc/strchr.c b/runtime/klee-libc/strchr.c new file mode 100644 index 00000000..33f97bea --- /dev/null +++ b/runtime/klee-libc/strchr.c @@ -0,0 +1,23 @@ +//===-- strchr.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +char *strchr(const char *p, int ch) { + char c; + + c = ch; + for (;; ++p) { + if (*p == c) { + return ((char *)p); + } else if (*p == '\0') { + return 0; + } + } + /* NOTREACHED */ + return 0; +} diff --git a/runtime/klee-libc/strcmp.c b/runtime/klee-libc/strcmp.c new file mode 100644 index 00000000..6b8c4e85 --- /dev/null +++ b/runtime/klee-libc/strcmp.c @@ -0,0 +1,14 @@ +//===-- strcmp.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +int strcmp(const char *a, const char *b) { + while (*a && *a == *b) + ++a, ++b; + return *a - *b; +} diff --git a/runtime/klee-libc/strcoll.c b/runtime/klee-libc/strcoll.c new file mode 100644 index 00000000..73d59f89 --- /dev/null +++ b/runtime/klee-libc/strcoll.c @@ -0,0 +1,15 @@ +//===-- strcoll.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> + +// according to the manpage, this is equiv in the POSIX/C locale. +int strcoll(const char *s1, const char *s2) { + return strcmp(s1,s2); +} diff --git a/runtime/klee-libc/strcpy.c b/runtime/klee-libc/strcpy.c new file mode 100644 index 00000000..0fbaf9a7 --- /dev/null +++ b/runtime/klee-libc/strcpy.c @@ -0,0 +1,17 @@ +//===-- strcpy.c ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +char *strcpy(char *to, const char *from) { + char *start = to; + + while ((*to = *from)) + ++to, ++from; + + return start; +} diff --git a/runtime/klee-libc/strlen.c b/runtime/klee-libc/strlen.c new file mode 100644 index 00000000..e298410c --- /dev/null +++ b/runtime/klee-libc/strlen.c @@ -0,0 +1,17 @@ +//===-- strlen.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> + +size_t strlen(const char *str) { + const char *s = str; + while (*s) + ++s; + return s - str; +} diff --git a/runtime/klee-libc/strncmp.c b/runtime/klee-libc/strncmp.c new file mode 100644 index 00000000..a8dc3749 --- /dev/null +++ b/runtime/klee-libc/strncmp.c @@ -0,0 +1,49 @@ +/* + * Copyright (c) 1989, 1993 + * The Regents of the University of California. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include <stdlib.h> + +int strncmp(const char *s1, const char *s2, size_t n) +{ + + if (n == 0) + return (0); + do { + if (*s1 != *s2++) + return (*(unsigned char *)s1 - + *(unsigned char *)(s2 - 1)); + if (*s1++ == 0) + break; + } while (--n != 0); + return (0); +} diff --git a/runtime/klee-libc/strncpy.c b/runtime/klee-libc/strncpy.c new file mode 100644 index 00000000..62ab7993 --- /dev/null +++ b/runtime/klee-libc/strncpy.c @@ -0,0 +1,58 @@ +/*- + * Copyright (c) 1990, 1993 + * The Regents of the University of California. All rights reserved. + * + * This code is derived from software contributed to Berkeley by + * Chris Torek. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include <stdlib.h> +/* + * Copy src to dst, truncating or null-padding to always copy n bytes. + * Return dst. + */ +char * strncpy(char * dst, const char * src, size_t n) +{ + if (n != 0) { + char *d = dst; + const char *s = src; + + do { + if ((*d++ = *s++) == 0) { + /* NUL pad the remaining n-1 bytes */ + while (--n != 0) + *d++ = 0; + break; + } + } while (--n != 0); + } + return (dst); +} diff --git a/runtime/klee-libc/strrchr.c b/runtime/klee-libc/strrchr.c new file mode 100644 index 00000000..01128b48 --- /dev/null +++ b/runtime/klee-libc/strrchr.c @@ -0,0 +1,21 @@ +//===-- strrchr.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> + +char *strrchr(const char *t, int c) { + char ch; + const char *l=0; + + ch = c; + for (;;) { + if (*t == ch) l=t; if (!*t) return (char*)l; ++t; + } + return (char*)l; +} diff --git a/runtime/klee-libc/strtol.c b/runtime/klee-libc/strtol.c new file mode 100644 index 00000000..3be7fff3 --- /dev/null +++ b/runtime/klee-libc/strtol.c @@ -0,0 +1,135 @@ +/*- + * Copyright (c) 1990, 1993 + * The Regents of the University of California. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include <limits.h> +#include <ctype.h> +#include <errno.h> +#include <stdlib.h> + + +/* + * Convert a string to a long integer. + * + * Assumes that the upper and lower case + * alphabets and digits are each contiguous. + */ +long +strtol(const char * nptr, char ** endptr, int base) +{ + const char *s; + unsigned long acc; + char c; + unsigned long cutoff; + int neg, any, cutlim; + + /* + * Skip white space and pick up leading +/- sign if any. + * If base is 0, allow 0x for hex and 0 for octal, else + * assume decimal; if base is already 16, allow 0x. + */ + s = nptr; + do { + c = *s++; + } while (isspace((unsigned char)c)); + if (c == '-') { + neg = 1; + c = *s++; + } else { + neg = 0; + if (c == '+') + c = *s++; + } + if ((base == 0 || base == 16) && + c == '0' && (*s == 'x' || *s == 'X')) { + c = s[1]; + s += 2; + base = 16; + } + if (base == 0) + base = c == '0' ? 8 : 10; + acc = any = 0; + if (base < 2 || base > 36) + goto noconv; + + /* + * Compute the cutoff value between legal numbers and illegal + * numbers. That is the largest legal value, divided by the + * base. An input number that is greater than this value, if + * followed by a legal input character, is too big. One that + * is equal to this value may be valid or not; the limit + * between valid and invalid numbers is then based on the last + * digit. For instance, if the range for longs is + * [-2147483648..2147483647] and the input base is 10, + * cutoff will be set to 214748364 and cutlim to either + * 7 (neg==0) or 8 (neg==1), meaning that if we have accumulated + * a value > 214748364, or equal but the next digit is > 7 (or 8), + * the number is too big, and we will return a range error. + * + * Set 'any' if any `digits' consumed; make it negative to indicate + * overflow. + */ + cutoff = neg ? (unsigned long)-(LONG_MIN + LONG_MAX) + LONG_MAX + : LONG_MAX; + cutlim = cutoff % base; + cutoff /= base; + for ( ; ; c = *s++) { + if (c >= '0' && c <= '9') + c -= '0'; + else if (c >= 'A' && c <= 'Z') + c -= 'A' - 10; + else if (c >= 'a' && c <= 'z') + c -= 'a' - 10; + else + break; + if (c >= base) + break; + if (any < 0 || acc > cutoff || (acc == cutoff && c > cutlim)) + any = -1; + else { + any = 1; + acc *= base; + acc += c; + } + } + if (any < 0) { + acc = neg ? LONG_MIN : LONG_MAX; + errno = ERANGE; + } else if (!any) { +noconv: + errno = EINVAL; + } else if (neg) + acc = -acc; + if (endptr != NULL) + *endptr = (char *)(any ? s - 1 : nptr); + return (acc); +} diff --git a/runtime/klee-libc/strtoul.c b/runtime/klee-libc/strtoul.c new file mode 100644 index 00000000..f23d5b54 --- /dev/null +++ b/runtime/klee-libc/strtoul.c @@ -0,0 +1,113 @@ +/* + * Copyright (c) 1990, 1993 + * The Regents of the University of California. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include <limits.h> +#include <ctype.h> +#include <errno.h> +#include <stdlib.h> + +/* + * Convert a string to an unsigned long integer. + * + * Assumes that the upper and lower case + * alphabets and digits are each contiguous. + */ +unsigned long +strtoul(const char * nptr, char ** endptr, int base) +{ + const char *s; + unsigned long acc; + char c; + unsigned long cutoff; + int neg, any, cutlim; + + /* + * See strtol for comments as to the logic used. + */ + s = nptr; + do { + c = *s++; + } while (isspace((unsigned char)c)); + if (c == '-') { + neg = 1; + c = *s++; + } else { + neg = 0; + if (c == '+') + c = *s++; + } + if ((base == 0 || base == 16) && + c == '0' && (*s == 'x' || *s == 'X')) { + c = s[1]; + s += 2; + base = 16; + } + if (base == 0) + base = c == '0' ? 8 : 10; + acc = any = 0; + if (base < 2 || base > 36) + goto noconv; + + cutoff = ULONG_MAX / base; + cutlim = ULONG_MAX % base; + for ( ; ; c = *s++) { + if (c >= '0' && c <= '9') + c -= '0'; + else if (c >= 'A' && c <= 'Z') + c -= 'A' - 10; + else if (c >= 'a' && c <= 'z') + c -= 'a' - 10; + else + break; + if (c >= base) + break; + if (any < 0 || acc > cutoff || (acc == cutoff && c > cutlim)) + any = -1; + else { + any = 1; + acc *= base; + acc += c; + } + } + if (any < 0) { + acc = ULONG_MAX; + errno = ERANGE; + } else if (!any) { +noconv: + errno = EINVAL; + } else if (neg) + acc = -acc; + if (endptr != NULL) + *endptr = (char *)(any ? s - 1 : nptr); + return (acc); +} diff --git a/runtime/klee-libc/tolower.c b/runtime/klee-libc/tolower.c new file mode 100644 index 00000000..265f5deb --- /dev/null +++ b/runtime/klee-libc/tolower.c @@ -0,0 +1,14 @@ +//===-- tolower.c ---------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +int tolower(int ch) { + if ( (unsigned int)(ch - 'A') < 26u ) + ch -= 'A' - 'a'; + return ch; +} diff --git a/runtime/klee-libc/toupper.c b/runtime/klee-libc/toupper.c new file mode 100644 index 00000000..37e5f9d6 --- /dev/null +++ b/runtime/klee-libc/toupper.c @@ -0,0 +1,14 @@ +//===-- toupper.c ---------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +int toupper(int ch) { + if ( (unsigned int)(ch - 'a') < 26u ) + ch += 'A' - 'a'; + return ch; +} |