diff options
Diffstat (limited to 'runtime')
| -rw-r--r-- | runtime/POSIX/fd.h | 2 | ||||
| -rw-r--r-- | runtime/POSIX/fd_init.c | 9 | ||||
| -rw-r--r-- | runtime/POSIX/klee_init_env.c | 21 |
3 files changed, 20 insertions, 12 deletions
diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h index 87d967ee..24a350dc 100644 --- a/runtime/POSIX/fd.h +++ b/runtime/POSIX/fd.h @@ -103,7 +103,7 @@ extern exe_file_system_t __exe_fs; extern exe_sym_env_t __exe_env; void klee_init_fds(unsigned n_files, unsigned file_length, - unsigned stdin_length, int sym_stdout_flag, + unsigned stdin_length, unsigned stdout_length, 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 adb1d9f6..b93148ec 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -96,14 +96,13 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, } /* 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 + file_length: size in bytes of each symbolic file, including stdin/stdout 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, - unsigned stdin_length, int sym_stdout_flag, + unsigned stdin_length, unsigned stdout_length, int save_all_writes_flag, unsigned max_failures) { unsigned k; char name[7] = "?_data"; @@ -150,11 +149,11 @@ void klee_init_fds(unsigned n_files, unsigned file_length, } /* setting symbolic stdout */ - if (sym_stdout_flag) { + if (stdout_length) { __exe_fs.sym_stdout = malloc(sizeof(*__exe_fs.sym_stdout)); if (!__exe_fs.sym_stdout) klee_report_error(__FILE__, __LINE__, "out of memory in klee_init_env", "user.err"); - __create_new_dfile(__exe_fs.sym_stdout, 1024, "stdout", &s); + __create_new_dfile(__exe_fs.sym_stdout, stdout_length, "stdout", &s); __exe_env.fds[1].dfile = __exe_fs.sym_stdout; __exe_fs.stdout_writes = 0; } diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index aaee4c4e..50b36845 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -89,7 +89,7 @@ void klee_init_env(int *argcPtr, char ***argvPtr) { 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; + unsigned sym_stdout_len = 0; int save_all_writes_flag = 0; int fd_fail = 0; char **final_argv; @@ -109,7 +109,7 @@ usage: (klee_init_env) [options] [program arguments]\n\ -sym-files <NUM> <N> - Make NUM symbolic files ('A', 'B', 'C', etc.),\n\ each with size N\n\ -sym-stdin <N> - Make stdin symbolic with size N.\n\ - -sym-stdout - Make stdout symbolic.\n\ + -sym-stdout <N> - Make stdout symbolic with size N.\n\ -save-all-writes - Allow write operations to execute as expected\n\ even if they exceed the file size. If set to 0, all\n\ writes exceeding the initial file size are discarded.\n\ @@ -197,8 +197,11 @@ usage: (klee_init_env) [options] [program arguments]\n\ 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++; + const char *msg = + "--sym-stdout expects one integer argument <sym-stdout-len>"; + if (++k == argc) + __emit_error(msg); + sym_stdout_len = __str_to_int(argv[k++], msg); } else if (__streq(argv[k], "--save-all-writes") || __streq(argv[k], "-save-all-writes")) { save_all_writes_flag = 1; @@ -231,7 +234,7 @@ usage: (klee_init_env) [options] [program arguments]\n\ *argcPtr = new_argc; *argvPtr = final_argv; - klee_init_fds(sym_files, sym_file_len, sym_stdin_len, sym_stdout_flag, + klee_init_fds(sym_files, sym_file_len, sym_stdin_len, sym_stdout_len, save_all_writes_flag, fd_fail); } @@ -242,5 +245,11 @@ int __klee_posix_wrapped_main(int argc, char **argv, char **envp); /* This wrapper gets called instead of main if POSIX setup is used */ int __klee_posix_wrapper(int argcPtr, char **argvPtr, char** envp) { klee_init_env(&argcPtr, &argvPtr); - return __klee_posix_wrapped_main(argcPtr, argvPtr, envp); + int code = __klee_posix_wrapped_main(argcPtr, argvPtr, envp); + if (__exe_fs.sym_stdout) { + long long sym_stdout; + klee_make_symbolic(&sym_stdout, 8, "out!std!1"); + klee_assume(sym_stdout == *(long long *) __exe_fs.sym_stdout->contents); + } + return code; } |