diff options
| -rw-r--r-- | tools/klee-replay/Makefile | 19 | ||||
| -rw-r--r-- | tools/klee-replay/fd_init.c | 1 | ||||
| -rw-r--r-- | tools/klee-replay/file-creator.c | 532 | ||||
| -rw-r--r-- | tools/klee-replay/klee-replay.c | 362 | ||||
| -rw-r--r-- | tools/klee-replay/klee-replay.h | 28 | ||||
| -rw-r--r-- | tools/klee-replay/klee_init_env.c | 1 |
6 files changed, 943 insertions, 0 deletions
diff --git a/tools/klee-replay/Makefile b/tools/klee-replay/Makefile new file mode 100644 index 00000000..fcce0483 --- /dev/null +++ b/tools/klee-replay/Makefile @@ -0,0 +1,19 @@ +#===-- tools/klee-replay/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=../.. +TOOLNAME = klee-replay + +USEDLIBS = kleeBasic.a +LINK_COMPONENTS = +NO_PEDANTIC=1 + +include $(LEVEL)/Makefile.common + +LIBS += -lutil diff --git a/tools/klee-replay/fd_init.c b/tools/klee-replay/fd_init.c new file mode 100644 index 00000000..e1dda970 --- /dev/null +++ b/tools/klee-replay/fd_init.c @@ -0,0 +1 @@ +#include "../../runtime/POSIX/fd_init.c" diff --git a/tools/klee-replay/file-creator.c b/tools/klee-replay/file-creator.c new file mode 100644 index 00000000..505fb8d7 --- /dev/null +++ b/tools/klee-replay/file-creator.c @@ -0,0 +1,532 @@ +//===-- file-creator.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-replay.h" + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <unistd.h> +#include <errno.h> +#include <sys/types.h> +#include <sys/stat.h> +#include <fcntl.h> +#include <termios.h> +#include <pty.h> +#include <time.h> +#include <sys/wait.h> +#include <sys/time.h> +#include <assert.h> + +static void create_file(int target_fd, + const char *target_name, + exe_disk_file_t *dfile, + const char *tmpdir); +static void check_file(int index, exe_disk_file_t *file); +static void delete_file(const char *path, int recurse); + + +#define __STDIN -1 +#define __STDOUT -2 + +static int create_link(const char *fname, + exe_disk_file_t *dfile, + const char *tmpdir) { + char buf[64]; + struct stat64 *s = dfile->stat; + + // XXX Broken, we want this path to be somewhere else most likely. + sprintf(buf, "%s.lnk", fname); + s->st_mode = (s->st_mode & ~S_IFMT) | S_IFREG; + create_file(-1, buf, dfile, tmpdir); + + int res = symlink(buf, fname); + if (res < 0) { + perror("symlink"); + } + + return open(fname, O_RDWR); +} + + +static int create_dir(const char *fname, exe_disk_file_t *dfile, + const char *tmpdir) { + int res = mkdir(fname, dfile->stat->st_mode); + if (res < 0) { + perror("mkdir"); + return -1; + } + return open(fname, O_RDWR); +} + +double getTime() { + struct timeval t; + gettimeofday(&t, NULL); + + return (double) t.tv_sec + ((double) t.tv_usec / 1000000.0); +} + +/// Return true if program exited, false if timed out. +int wait_for_timeout_or_exit(pid_t pid, const char *name, int *statusp) { + char *t = getenv("KLEE_REPLAY_TIMEOUT"); + int timeout = t ? atoi(t) : 5; + double wait = timeout * .5; + double start = getTime(); + fprintf(stderr, "note: %s: waiting %.2fs\n", name, wait); + while (getTime() - start < wait) { + struct timespec r = {0, 1000000}; + nanosleep(&r, 0); + int res = waitpid(pid, statusp, WNOHANG); + if (res==pid) + return 1; + } + + return 0; +} + +static int create_char_dev(const char *fname, exe_disk_file_t *dfile, + const char *tmpdir) { + struct stat64 *s = dfile->stat; + unsigned flen = dfile->size; + char* contents = dfile->contents; + + // Assume tty, kinda broken, need an actual device id or something + struct termios term, *ts=&term; + struct winsize win = { 24, 80, 0, 0 }; + /* 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'; + + { + char name[1024]; + int amaster, aslave; + int res = openpty(&amaster, &aslave, name, &term, &win); + if (res < 0) { + perror("openpty"); + exit(1); + } + + if (symlink(name, fname) == -1) { + fprintf(stderr, "unable to create sym link to tty\n"); + perror("symlink"); + } + + // pty will not be world writeable + s->st_mode &= ~02; + + pid_t pid = fork(); + if (pid < 0) { + perror("fork failed\n"); + exit(1); + } else if (pid == 0) { + close(amaster); + + fprintf(stderr, "note: pty slave: setting raw mode\n"); + { + struct termio mode; + + int res = ioctl(aslave, TCGETA, &mode); + assert(!res); + mode.c_iflag = IGNBRK; + mode.c_oflag &= ~(OLCUC | ONLCR | OCRNL | ONLRET); + mode.c_lflag = 0; + mode.c_cc[VMIN] = 1; + mode.c_cc[VTIME] = 0; + res = ioctl(aslave, TCSETA, &mode); + assert(res == 0); + } + + return aslave; + } else { + unsigned pos = 0; + int status; + fprintf(stderr, "note: pty master: starting\n"); + close(aslave); + + while (pos < flen) { + int res = write(amaster, &contents[pos], flen - pos); + if (res<0) { + if (errno != EINTR) { + fprintf(stderr, "note: pty master: write error\n"); + perror("errno"); + break; + } + } else if (res) { + fprintf(stderr, "note: pty master: wrote: %d (of %d)\n", res, flen); + pos += res; + } + } + + if (wait_for_timeout_or_exit(pid, "pty master", &status)) + goto pty_exit; + + fprintf(stderr, "note: pty master: closing & waiting\n"); + close(amaster); + while (1) { + int res = waitpid(pid, &status, 0); + if (res < 0) { + if (errno != EINTR) + break; + } else { + break; + } + } + + pty_exit: + close(amaster); + fprintf(stderr, "note: pty master: done\n"); + process_status(status, 0, "PTY MASTER"); + } + } +} + +static int create_pipe(const char *fname, exe_disk_file_t *dfile, + const char *tmpdir) { + //struct stat64 *s = dfile->stat; + unsigned flen = dfile->size; + char* contents = dfile->contents; + + // XXX what is direction ? need more data + pid_t pid; + int fds[2]; + int res = pipe(fds); + if (res < 0) { + perror("pipe"); + exit(1); + } + + pid = fork(); + if (pid < 0) { + perror("fork"); + exit(1); + } else if (pid == 0) { + close(fds[1]); + return fds[0]; + } else { + unsigned pos = 0; + int status; + fprintf(stderr, "note: pipe master: starting\n"); + close(fds[0]); + + while (pos < flen) { + int res = write(fds[1], &contents[pos], flen - pos); + if (res<0) { + if (errno != EINTR) + break; + } else if (res) { + pos += res; + } + } + + if (wait_for_timeout_or_exit(pid, "pipe master", &status)) + goto pipe_exit; + + fprintf(stderr, "note: pipe master: closing & waiting\n"); + close(fds[1]); + while (1) { + int res = waitpid(pid, &status, 0); + if (res < 0) { + if (errno != EINTR) + break; + } else { + break; + } + } + + pipe_exit: + close(fds[1]); + fprintf(stderr, "note: pipe master: done\n"); + process_status(status, 0, "PTY MASTER"); + } +} + + +static int create_reg_file(const char *fname, exe_disk_file_t *dfile, + const char *tmpdir) { + struct stat64 *s = dfile->stat; + char* contents = dfile->contents; + unsigned flen = dfile->size; + unsigned mode = s->st_mode & 0777; + + //fprintf(stderr, "Creating regular file\n"); + + // Open in RDWR just in case we have to end up using this fd. + + if (__exe_env.version == 0 && mode == 0) + mode = 0644; + + + int fd = open(fname, O_CREAT | O_RDWR, mode); + // int fd = open(fname, O_CREAT | O_WRONLY, s->st_mode&0777); + if (fd < 0) { + fprintf(stderr, "Cannot create file %s\n", fname); + exit(1); + } + + int r = write(fd, contents, flen); + if (r < 0 || (unsigned) r != flen) { + fprintf(stderr, "Cannot write file %s\n", fname); + exit(1); + } + + struct timeval tv[2]; + tv[0].tv_sec = s->st_atime; + tv[0].tv_usec = 0; + tv[1].tv_sec = s->st_mtime; + tv[1].tv_usec = 0; + futimes(fd, tv); + + // XXX: Now what we should do is reopen a new fd with the correct modes + // as they were given to the process. + lseek(fd, 0, SEEK_SET); + + return fd; +} + +static int delete_dir(const char *path, int recurse) { + if (recurse) { + DIR *d = opendir(path); + struct dirent *de; + + if (d) { + while ((de = readdir(d))) { + if (strcmp(de->d_name, ".")!=0 && strcmp(de->d_name, "..")!=0) { + char tmp[PATH_MAX]; + sprintf(tmp, "%s/%s", path, de->d_name); + delete_file(tmp, 0); + } + } + + closedir(d); + } + } + + if (rmdir(path) == -1) { + fprintf(stderr, "Cannot create file %s (exists, is dir, can't remove)\n", path); + perror("rmdir"); + return -1; + } + + return 0; +} + +static void delete_file(const char *path, int recurse) { + if (unlink(path) < 0 && errno != ENOENT) { + if (errno == EISDIR) { + delete_dir(path, 1); + } else { + fprintf(stderr, "Cannot create file %s (already exists)\n", path); + perror("unlink"); + } + } +} + +static void create_file(int target_fd, + const char *target_name, + exe_disk_file_t *dfile, + const char *tmpdir) { + struct stat64 *s = dfile->stat; + char tmpname[PATH_MAX]; + const char *target; + int fd; + + assert((target_fd == -1) ^ (target_name == NULL)); + + if (target_name) { + target = target_name; + } else { + sprintf(tmpname, "%s/fd%d", tmpdir, target_fd); + target = tmpname; + } + + delete_file(target, 1); + + // XXX get rid of me once a reasonable solution is found + s->st_uid = geteuid(); + s->st_gid = getegid(); + + if (S_ISLNK(s->st_mode)) { + fd = create_link(target, dfile, tmpdir); + } + else if (S_ISDIR(s->st_mode)) { + fd = create_dir(target, dfile, tmpdir); + } + else if (S_ISCHR(s->st_mode)) { + fd = create_char_dev(target, dfile, tmpdir); + } + else if (S_ISFIFO(s->st_mode) || + (target_fd==0 && (s->st_mode & S_IFMT) == 0)) { // XXX hack + fd = create_pipe(target, dfile, tmpdir); + } + else { + fd = create_reg_file(target, dfile, tmpdir); + } + + if (fd >= 0) { + if (target_fd != -1) { + close(target_fd); + if (dup2(fd, target_fd) < 0) { + fprintf(stderr, "note: dup2 failed for target: %d\n", target_fd); + perror("dup2"); + } + close(fd); + } else { + // Only worry about 1 vs !1 + if (s->st_nlink > 1) { + char tmp2[PATH_MAX]; + sprintf(tmp2, "%s/%s.link2", tmpdir, target_name); + if (link(target_name, tmp2) < 0) { + perror("link"); + exit(1); + } + } + + close(fd); + } + } +} + +void replay_create_files(exe_file_system_t *exe_fs) { + char tmpdir[PATH_MAX]; + unsigned k; + + if (!getcwd(tmpdir, PATH_MAX)) { + perror("getcwd"); + exit(1); + } + + strcat(tmpdir, ".temps"); + delete_file(tmpdir, 1); + mkdir(tmpdir, 0755); + + umask(0); + for (k=0; k < exe_fs->n_sym_files; k++) { + char name[2]; + sprintf(name, "%c", 'A' + k); + create_file(-1, name, &exe_fs->sym_files[k], tmpdir); + } + + if (exe_fs->sym_stdin) + create_file(0, NULL, exe_fs->sym_stdin, tmpdir); + + if (exe_fs->sym_stdout) + create_file(1, NULL, exe_fs->sym_stdout, tmpdir); + + if (exe_fs->sym_stdin) + check_file(__STDIN, exe_fs->sym_stdin); + + if (exe_fs->sym_stdout) + check_file(__STDOUT, exe_fs->sym_stdout); + + for (k=0; k<exe_fs->n_sym_files; ++k) + check_file(k, &exe_fs->sym_files[k]); +} + +static void check_file(int index, exe_disk_file_t *dfile) { + struct stat s; + int res; + char name[32]; + + switch (index) { + case __STDIN: + strcpy(name, "stdin"); + res = fstat(0, &s); + break; + case __STDOUT: + strcpy(name, "stdout"); + res = fstat(1, &s); + break; + default: + name[0] = 'A' + index; + name[1] = '\0'; + res = stat(name, &s); + break; + } + + if (res < 0) { + fprintf(stderr, "warning: check_file %d: stat failure\n", index); + return; + } + + if (s.st_dev != dfile->stat->st_dev) { + fprintf(stderr, "warning: check_file %s: dev mismatch: %d vs %d\n", + name, (int) s.st_dev, (int) dfile->stat->st_dev); + } +/* if (s.st_ino != dfile->stat->st_ino) { */ +/* fprintf(stderr, "warning: check_file %s: ino mismatch: %d vs %d\n", */ +/* name, (int) s.st_ino, (int) dfile->stat->st_ino); */ +/* } */ + if (s.st_mode != dfile->stat->st_mode) { + fprintf(stderr, "warning: check_file %s: mode mismatch: %#o vs %#o\n", + name, s.st_mode, dfile->stat->st_mode); + } + if (s.st_nlink != dfile->stat->st_nlink) { + fprintf(stderr, "warning: check_file %s: nlink mismatch: %d vs %d\n", + name, (int) s.st_nlink, (int) dfile->stat->st_nlink); + } + if (s.st_uid != dfile->stat->st_uid) { + fprintf(stderr, "warning: check_file %s: uid mismatch: %d vs %d\n", + name, s.st_uid, dfile->stat->st_uid); + } + if (s.st_gid != dfile->stat->st_gid) { + fprintf(stderr, "warning: check_file %s: gid mismatch: %d vs %d\n", + name, s.st_gid, dfile->stat->st_gid); + } + if (s.st_rdev != dfile->stat->st_rdev) { + fprintf(stderr, "warning: check_file %s: rdev mismatch: %d vs %d\n", + name, (int) s.st_rdev, (int) dfile->stat->st_rdev); + } + if (s.st_size != dfile->stat->st_size) { + fprintf(stderr, "warning: check_file %s: size mismatch: %d vs %d\n", + name, (int) s.st_size, (int) dfile->stat->st_size); + } + if (s.st_blksize != dfile->stat->st_blksize) { + fprintf(stderr, "warning: check_file %s: blksize mismatch: %d vs %d\n", + name, (int) s.st_blksize, (int) dfile->stat->st_blksize); + } + if (s.st_blocks != dfile->stat->st_blocks) { + fprintf(stderr, "warning: check_file %s: blocks mismatch: %d vs %d\n", + name, (int) s.st_blocks, (int) dfile->stat->st_blocks); + } +/* if (s.st_atime != dfile->stat->st_atime) { */ +/* fprintf(stderr, "warning: check_file %s: atime mismatch: %d vs %d\n", */ +/* name, (int) s.st_atime, (int) dfile->stat->st_atime); */ +/* } */ +/* if (s.st_mtime != dfile->stat->st_mtime) { */ +/* fprintf(stderr, "warning: check_file %s: mtime mismatch: %d vs %d\n", */ +/* name, (int) s.st_mtime, (int) dfile->stat->st_mtime); */ +/* } */ +/* if (s.st_ctime != dfile->stat->st_ctime) { */ +/* fprintf(stderr, "warning: check_file %s: ctime mismatch: %d vs %d\n", */ +/* name, (int) s.st_ctime, (int) dfile->stat->st_ctime); */ +/* } */ +} diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c new file mode 100644 index 00000000..1163eaaa --- /dev/null +++ b/tools/klee-replay/klee-replay.c @@ -0,0 +1,362 @@ +//===-- klee-replay.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-replay.h" + +#include "klee/Internal/ADT/KTest.h" + +#include <assert.h> +#include <stdio.h> +#include <stdlib.h> +#include <string.h> + +#include <errno.h> +#include <time.h> +#include <unistd.h> +#include <sys/signal.h> +#include <sys/wait.h> + +static void __emit_error(const char *msg); + +static KTest* input = NULL; +static unsigned obj_index = 0; + +static const char *progname = 0; +static unsigned monitored_pid = 0; +static unsigned monitored_timeout; + +static void stop_monitored(int process) { + fprintf(stderr, "TIMEOUT: ATTEMPTING GDB EXIT\n"); + int pid = fork(); + if (pid < 0) { + fprintf(stderr, "ERROR: gdb_exit: fork failed\n"); + } else if (pid == 0) { + /* Run gdb in a child process. */ + const char *gdbargs[] = { + "/usr/bin/gdb", + "--pid", "", + "-q", + "--batch", + "--eval-command=call exit(1)", + 0, + 0 + }; + char pids[64]; + sprintf(pids, "%d", process); + + gdbargs[2] = pids; + /* Make sure gdb doesn't talk to the user */ + close(0); + + fprintf(stderr, "RUNNING GDB: "); + unsigned i; + for (i = 0; i != 5; ++i) + fprintf(stderr, "%s ", gdbargs[i]); + fprintf(stderr, "\n"); + + execvp(gdbargs[0], (char * const *) gdbargs); + perror("execvp"); + _exit(66); + } else { + /* Parent process, wait for gdb to finish. */ + int res, status; + do { + res = waitpid(pid, &status, 0); + } while (res < 0 && errno == EINTR); + + if (res < 0) { + perror("waitpid"); + _exit(66); + } + } +} + +static void int_handler(int signal) { + fprintf(stderr, "%s: Received signal %d. Killing monitored process(es)\n", + progname, signal); + if (monitored_pid) { + stop_monitored(monitored_pid); + /* Kill the process group of monitored_pid. Since we called + setpgrp() for pid, this will not kill us, or any of our + ancestors */ + kill(-monitored_pid, SIGKILL); + } else { + _exit(99); + } +} +static void timeout_handler(int signal) { + fprintf(stderr, "EXIT STATUS: TIMED OUT (%d seconds)\n", monitored_timeout); + if (monitored_pid) { + stop_monitored(monitored_pid); + /* Kill the process group of monitored_pid. Since we called + setpgrp() for pid, this will not kill us, or any of our + ancestors */ + kill(-monitored_pid, SIGKILL); + } else { + _exit(88); + } +} + +void process_status(int status, + time_t elapsed, + const char *pfx) { + + if (pfx) + fprintf(stderr, "%s: ", pfx); + if (WIFSIGNALED(status)) { + fprintf(stderr, "EXIT STATUS: CRASHED signal %d (%d seconds)\n", + WTERMSIG(status), (int) elapsed); + _exit(77); + } else if (WIFEXITED(status)) { + int rc = WEXITSTATUS(status); + + char msg[64]; + if (rc == 0) { + strcpy(msg, "NORMAL"); + } else { + sprintf(msg, "ABNORMAL %d", rc); + } + fprintf(stderr, "EXIT STATUS: %s (%d seconds)\n", msg, (int) elapsed); + _exit(rc); + } else { + fprintf(stderr, "EXIT STATUS: NONE (%d seconds)\n", (int) elapsed); + _exit(0); + } +} + +static void run_monitored(char *executable, int argc, char **argv) { + int pid; + const char *t = getenv("KLEE_REPLAY_TIMEOUT"); + if (!t) + t = "10000000"; + monitored_timeout = atoi(t); + + if (monitored_timeout==0) { + fprintf(stderr, "ERROR: invalid timeout (%s)\n", t); + _exit(1); + } + + /* Kill monitored process(es) on SIGINT and SIGTERM */ + signal(SIGINT, int_handler); + signal(SIGTERM, int_handler); + + signal(SIGALRM, timeout_handler); + pid = fork(); + if (pid < 0) { + perror("fork"); + _exit(66); + } else if (pid == 0) { + /* This process actually executes the target program. + * + * Create a new process group for pid, and the process tree it may spawn. We + * do this, because later on we might want to kill pid _and_ all processes + * spawned by it and its descendants. + */ + setpgrp(); + + execv(executable, argv); + perror("execv"); + _exit(66); + } else { + /* Parent process which monitors the child. */ + int res, status; + time_t start = time(0); + sigset_t masked; + + sigemptyset(&masked); + sigaddset(&masked, SIGALRM); + + monitored_pid = pid; + alarm(monitored_timeout); + do { + res = waitpid(pid, &status, 0); + } while (res < 0 && errno == EINTR); + + if (res < 0) { + perror("waitpid"); + _exit(66); + } + + /* Just in case, kill the process group of pid. Since we called setpgrp() + for pid, this will not kill us, or any of our ancestors */ + kill(-pid, SIGKILL); + process_status(status, time(0) - start, 0); + } +} + + +int main(int argc, char** argv) { + int prg_argc; + char ** prg_argv; + + progname = argv[0]; + + if (argc != 3) { + fprintf(stderr, "Usage: %s <executable> <ktest-file>\n",argv[0]); + fprintf(stderr, " %s --create-files-only <ktest-file>\n", argv[0]); + fprintf(stderr, " Set KLEE_REPLAY_TIMEOUT environment variable to set a timeout (in seconds)\n"); + exit(1); + } + + /* Special case hack for only creating files and not actually executing the + * program. + */ + if (strcmp(argv[1], "--create-files-only") == 0) { + char* input_fname = argv[2]; + + input = kTest_fromFile(input_fname); + if (!input) { + fprintf(stderr, "%s: error: input file %s not valid.\n", progname, + input_fname); + exit(1); + } + + prg_argc = input->numArgs; + prg_argv = input->args; + prg_argv[0] = argv[1]; + klee_init_env(&prg_argc, &prg_argv); + + replay_create_files(&__exe_fs); + return 0; + } + + /* Normal execution path ... */ + + char* executable = argv[1]; + char* input_fname = argv[2]; + unsigned i; + + FILE *f = fopen(executable, "r"); + if (!f) { + fprintf(stderr, "Error: executable %s not found.\n", executable); + exit(1); + } + fclose(f); + + input = kTest_fromFile(input_fname); + if (!input) { + fprintf(stderr, "%s: error: input file %s not valid.\n", progname, + input_fname); + exit(1); + } + + prg_argc = input->numArgs; + prg_argv = input->args; + prg_argv[0] = argv[1]; + klee_init_env(&prg_argc, &prg_argv); + fprintf(stderr, "ARGS: "); + for (i=0; i != (unsigned) prg_argc; ++i) { + char *s = prg_argv[i]; + if (s[0]=='A' && s[1] && !s[2]) s[1] = '\0'; + fprintf(stderr, "\"%s\" ", prg_argv[i]); + } + fprintf(stderr, "\n"); + + replay_create_files(&__exe_fs); + + run_monitored(executable, prg_argc, prg_argv); + + return 0; +} + + +/* Klee functions */ + +int __fputc_unlocked(int c, FILE *f) { + return fputc_unlocked(c, f); +} + +int __fgetc_unlocked(FILE *f) { + return fgetc_unlocked(f); +} + +int klee_get_errno() { + return errno; +} + +void klee_warning(char *name) { + fprintf(stderr, "WARNING: %s\n", name); +} + +void klee_warning_once(char *name) { + fprintf(stderr, "WARNING: %s\n", name); +} + +int klee_assume(int x) { + if (!x) { + fprintf(stderr, "WARNING: klee_assume(0)!\n"); + } + return 0; +} + +int klee_is_symbolic(int x) { + return 0; +} + +void klee_prefer_cex(void *buffer, unsigned condition) { + ; +} + +void klee_make_symbolic(void *addr, unsigned nbytes, const char *name) { + /* XXX remove model version code once new tests gen'd */ + if (obj_index >= input->numObjects) { + if (strcmp("model_version", name) == 0) { + assert(nbytes == 4); + *((int*) addr) = 0; + } else { + __emit_error("ran out of appropriate inputs"); + } + } else { + KTestObject *boo = &input->objects[obj_index]; + + if (strcmp("model_version", name) == 0 && + strcmp("model_version", boo->name) != 0) { + assert(nbytes == 4); + *((int*) addr) = 0; + } else { + if (boo->numBytes != nbytes) { + fprintf(stderr, "make_symbolic mismatch, different sizes: " + "%d in input file, %d in code\n", boo->numBytes, nbytes); + exit(1); + } else { + memcpy(addr, boo->bytes, nbytes); + obj_index++; + } + } + } +} + +/* Redefined here so that we can check the value read. */ +int klee_range(int min, int max, const char* name) { + int r; + klee_make_symbolic(&r, sizeof r, name); + + if (r < min || r >= max) { + fprintf(stderr, "klee_range(%d, %d, %s) returned invalid result: %d\n", + min, max, name, r); + exit(1); + } + return r; +} + +void klee_report_error(const char *file, int line, + const char *message, const char *suffix) { + __emit_error(message); +} + +void klee_mark_global(void *object) { + ; +} + +/*** HELPER FUNCTIONS ***/ + +static void __emit_error(const char *msg) { + fprintf(stderr, "ERROR: %s\n", msg); + exit(1); +} diff --git a/tools/klee-replay/klee-replay.h b/tools/klee-replay/klee-replay.h new file mode 100644 index 00000000..668b5e3e --- /dev/null +++ b/tools/klee-replay/klee-replay.h @@ -0,0 +1,28 @@ +//===-- klee-replay.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 __KLEE_REPLAY_H__ +#define __KLEE_REPLAY_H__ + +#define _LARGEFILE64_SOURCE +#define _FILE_OFFSET_BITS 64 + +// FIXME: This is a hack. +#include "../../runtime/POSIX/fd.h" +#include <sys/time.h> + +void replay_create_files(exe_file_system_t *exe_fs); + +void process_status(int status, + time_t elapsed, + const char *pfx) + __attribute__((noreturn)); + +#endif + diff --git a/tools/klee-replay/klee_init_env.c b/tools/klee-replay/klee_init_env.c new file mode 100644 index 00000000..229fe43d --- /dev/null +++ b/tools/klee-replay/klee_init_env.c @@ -0,0 +1 @@ +#include "../../runtime/POSIX/klee_init_env.c" |