From 61434a77783c0f72df2df4799dd700ff25e22ad9 Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Thu, 22 Jun 2023 16:06:57 +0900 Subject: Make symbolic stdout more flexible --- runtime/POSIX/fd.h | 2 +- runtime/POSIX/fd_init.c | 9 ++- runtime/POSIX/klee_init_env.c | 21 +++++-- tools/CMakeLists.txt | 1 + tools/klee-psychic/CMakeLists.txt | 13 ++++ tools/klee-psychic/klee-psychic | 128 ++++++++++++++++++++++++++++++++++++++ 6 files changed, 162 insertions(+), 12 deletions(-) create mode 100644 tools/klee-psychic/CMakeLists.txt create mode 100755 tools/klee-psychic/klee-psychic 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 - Make NUM symbolic files ('A', 'B', 'C', etc.),\n\ each with size N\n\ -sym-stdin - Make stdin symbolic with size N.\n\ - -sym-stdout - Make stdout symbolic.\n\ + -sym-stdout - 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 "; + 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; } diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index 8c9128b4..2da5fc96 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -14,4 +14,5 @@ add_subdirectory(klee-exec-tree) add_subdirectory(klee-replay) add_subdirectory(klee-stats) add_subdirectory(klee-zesti) +add_subdirectory(klee-psychic) add_subdirectory(ktest-tool) diff --git a/tools/klee-psychic/CMakeLists.txt b/tools/klee-psychic/CMakeLists.txt new file mode 100644 index 00000000..78d62c04 --- /dev/null +++ b/tools/klee-psychic/CMakeLists.txt @@ -0,0 +1,13 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +install(PROGRAMS klee-psychic DESTINATION bin) + +# Copy into the build directory's binary directory +# so system tests can find it +configure_file(klee-psychic "${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/klee-psychic" COPYONLY) diff --git a/tools/klee-psychic/klee-psychic b/tools/klee-psychic/klee-psychic new file mode 100755 index 00000000..09d9b398 --- /dev/null +++ b/tools/klee-psychic/klee-psychic @@ -0,0 +1,128 @@ +#!/usr/bin/env python3 +import sys +import os +import subprocess +import tempfile +import select +import shutil +from itertools import dropwhile, takewhile +from pathlib import Path + +HELP="""OVERVIEW: ZESTI like wrapper of KLEE/Psychic + +USAGE: klee-psychic [klee-options] + + +WARNING this script is not equivalent to ZESTI in ICSE 2012. It just provides a similar interface to KLEE. Namely it first explores the path of and then continues symbolic execution from that point. Most importantly it does not implement the ZESTI searcher. +""" + + +KLEE="klee" +GEN_BOUT="gen-bout" + +def find_klee_bin_dir(): + global KLEE + global GEN_BOUT + bin_dir = os.path.dirname(os.path.realpath(__file__)) + KLEE = bin_dir + "/klee" + GEN_BOUT = bin_dir + "/gen-bout" + if not os.path.isfile(KLEE): + print("WARNING can't find klee at " + KLEE) + KLEE= shutil.which("klee") + print("Using klee in PATH", KLEE) + if not os.path.isfile(GEN_BOUT): + print("WARNING can't find gen-bout at " + GEN_BOUT) + GEN_BOUT= shutil.which("gen-bout") + print("Using gen-bout in PATH", GEN_BOUT) + if GEN_BOUT is None or KLEE is None: + print("Failed to find KLEE at this script location or in PATH. Quitting ...") + sys.exit(1) + print("Using", KLEE) + + +def is_option(arg): + """Check if argument is optional.""" + return arg.startswith('-') + + +def split_args(): + """Return KLEE options, bitcode, executable and its arguments.""" + klee_args = tuple(takewhile(is_option, sys.argv[1:])) + rest = dropwhile(is_option, sys.argv[1:]) + return klee_args, next(rest), next(rest), tuple(rest) + + +def maybe_file_size(name): + try: + return os.path.getsize(name) + except: + return None + +def get_stdin_file(tmpdir): + stdin = "" + stdin_size = 0 + if sys.stdin in select.select([sys.stdin], [], [], 0)[0]: + stdin += sys.stdin.readline() + if stdin == "": + return None, stdin_size + stdin_file_name = tmpdir.name + "/stdin.file" + with open(stdin_file_name, 'w') as f: + stdin_size = f.write(stdin) + return stdin_file_name, stdin_size + + + +def prog_args_to_posix(prog_args): + posix_args = [] + sym_file = 'A' + sym_file_sizes = [] + gen_out_args = [] + for parg in prog_args: + file_size = maybe_file_size(parg) + if file_size is None: + posix_args += ['--sym-arg', str(len(parg))] + gen_out_args += [parg] + else: + sym_file_sizes += [file_size] + posix_args += [sym_file] + sym_file = chr(ord(sym_file) + 1) + gen_out_args += ['--sym-file', parg] + + if ord(sym_file) - ord('A') > 0: + posix_args += ['--sym-files', str(ord(sym_file) - ord('A')), str(max(sym_file_sizes))] + return posix_args, gen_out_args + +def create_ktest_file(gen_out_args, tmpdir): + out_file=tmpdir + "/test.ktest" + subprocess.run([GEN_BOUT, "--bout-file", out_file] + gen_out_args, check=True) + return out_file + + +def main(): + try: + klee_args, bc, prog, prog_args = split_args() + except StopIteration: + print(HELP) + return + find_klee_bin_dir() + tmpdir = tempfile.TemporaryDirectory() + stdin_file, stdin_size = get_stdin_file(tmpdir) + posix_args, gen_out_args = prog_args_to_posix(prog_args) + if stdin_file is not None: + gen_out_args += ["--sym-stdin", stdin_file] + posix_args += ["--sym-stdin", str(stdin_size)] + ktest_file = create_ktest_file(gen_out_args,tmpdir.name) + Path('test.ktest').write_bytes(Path(ktest_file).read_bytes()) + proc = subprocess.Popen([KLEE, *klee_args, f'-seed-file={ktest_file}', + bc, prog, *posix_args], + stdout=sys.stdout, stderr=sys.stderr) + while proc.returncode is None: + try: + proc.wait() + except KeyboardInterrupt: + pass # This is expected when stopping KLEE, so we wait for KLEE to finish + sys.exit(proc.returncode) + + +if __name__ == "__main__": + main() -- cgit 1.4.1