diff options
| -rw-r--r-- | runtime/POSIX/fd.h | 6 | ||||
| -rw-r--r-- | runtime/POSIX/fd_init.c | 10 | ||||
| -rw-r--r-- | runtime/POSIX/klee_init_env.c | 26 | ||||
| -rw-r--r-- | test/Runtime/POSIX/Isatty.c | 2 | ||||
| -rw-r--r-- | test/Runtime/POSIX/Stdin.c | 2 |
5 files changed, 28 insertions, 18 deletions
diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h index cb86295c..4a6fbc15 100644 --- a/runtime/POSIX/fd.h +++ b/runtime/POSIX/fd.h @@ -71,9 +71,9 @@ typedef struct { 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_fds(unsigned n_files, unsigned file_length, + unsigned stdin_length, int sym_stdout_flag, + int do_all_writes_flag, unsigned max_failures); void klee_init_env(int *argcPtr, char ***argvPtr); /* *** */ diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index 8b69fd04..9184b7ea 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -107,9 +107,9 @@ static unsigned __sym_uint32(const char *name) { 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) { +void klee_init_fds(unsigned n_files, unsigned file_length, + unsigned stdin_length, int sym_stdout_flag, + int save_all_writes_flag, unsigned max_failures) { unsigned k; char name[7] = "?-data"; struct stat64 s; @@ -124,9 +124,9 @@ void klee_init_fds(unsigned n_files, unsigned file_length, } /* setting symbolic stdin */ - if (file_length) { + if (stdin_length) { __exe_fs.sym_stdin = malloc(sizeof(*__exe_fs.sym_stdin)); - __create_new_dfile(__exe_fs.sym_stdin, file_length, "stdin", &s); + __create_new_dfile(__exe_fs.sym_stdin, stdin_length, "stdin", &s); __exe_env.fds[0].dfile = __exe_fs.sym_stdin; } else __exe_fs.sym_stdin = NULL; diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index cbcf31f4..8e578cf0 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -90,6 +90,7 @@ void klee_init_env(int* argcPtr, char*** argvPtr) { char* new_argv[1024]; unsigned max_len, min_argvs, max_argvs; unsigned sym_files = 0, sym_file_len = 0; + unsigned sym_stdin_len = 0; int sym_stdout_flag = 0; int save_all_writes_flag = 0; int fd_fail = 0; @@ -102,13 +103,14 @@ void klee_init_env(int* argcPtr, char*** argvPtr) { // Recognize --help when it is the sole argument. if (argc == 2 && __streq(argv[1], "--help")) { - __emit_error("klee_init_env\n\n\ + __emit_error("klee_init_env\n\n\ usage: (klee_init_env) [options] [program arguments]\n\ -sym-arg <N> - Replace by a symbolic argument with length N\n\ -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most\n\ MAX arguments, each with maximum length N\n\ - -sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each\n\ - with maximum size N.\n\ + -sym-files <NUM> <N> - Make up to NUM symbolic files, each\n\ + with maximum size N.\n\ + -sym-stdin <N> - Make stdin symbolic with maximum size N.\n\ -sym-stdout - Make stdout symbolic.\n\ -max-fail <N> - Allow up to <N> injected failures\n\ -fd-fail - Shortcut for '-max-fail 1'\n\n"); @@ -156,8 +158,17 @@ usage: (klee_init_env) [options] [program arguments]\n\ 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")) { + } else if (__streq(argv[k], "--sym-stdin") || + __streq(argv[k], "-sym-stdin")) { + const char *msg = + "--sym-stdin expects one integer argument <sym-stdin-len>"; + + if (++k == argc) + __emit_error(msg); + + sym_stdin_len = __str_to_int(argv[k++], msg); + } else if (__streq(argv[k], "--sym-stdout") || + __streq(argv[k], "-sym-stdout")) { sym_stdout_flag = 1; k++; } @@ -190,8 +201,7 @@ usage: (klee_init_env) [options] [program arguments]\n\ *argcPtr = new_argc; *argvPtr = final_argv; - klee_init_fds(sym_files, sym_file_len, - sym_stdout_flag, save_all_writes_flag, - fd_fail); + klee_init_fds(sym_files, sym_file_len, sym_stdin_len, sym_stdout_flag, + save_all_writes_flag, fd_fail); } diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c index 241c5cbb..fdfc6ceb 100644 --- a/test/Runtime/POSIX/Isatty.c +++ b/test/Runtime/POSIX/Isatty.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout > %t.log 2>&1 +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-stdin 10 --sym-stdout > %t.log 2>&1 // RUN: test -f %t.klee-out/test000001.ktest // RUN: test -f %t.klee-out/test000002.ktest // RUN: test -f %t.klee-out/test000003.ktest diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c index ebf16405..09eed6d2 100644 --- a/test/Runtime/POSIX/Stdin.c +++ b/test/Runtime/POSIX/Stdin.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-stdin 4 > %t.log // RUN: grep "mode:file" %t.log // RUN: grep "mode:dir" %t.log // RUN: grep "mode:chr" %t.log |