aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/klee-replay/Makefile19
-rw-r--r--tools/klee-replay/fd_init.c1
-rw-r--r--tools/klee-replay/file-creator.c532
-rw-r--r--tools/klee-replay/klee-replay.c362
-rw-r--r--tools/klee-replay/klee-replay.h28
-rw-r--r--tools/klee-replay/klee_init_env.c1
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"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-25 03:21:19 +0000