diff options
author | Timotej Kapus <tk1713@ic.ac.uk> | 2020-02-21 16:55:11 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-09-17 18:17:25 +0100 |
commit | 52dfb5246697dc68f007e058f817b23310cae708 (patch) | |
tree | 8bd9ff6f2935e0b0530474102bafc089b490de59 | |
parent | 7bd9582967636f9f4f9acecadd26ab8faef74323 (diff) | |
download | klee-52dfb5246697dc68f007e058f817b23310cae708.tar.gz |
Add klee-zesti a ZESTI like wrapper script
klee-zesti takes concrete arguments, files and stdin of the program under tests converts them to a seed and then runs klee with that seed. This emulates the interface of ZESTI.
-rw-r--r-- | tools/CMakeLists.txt | 1 | ||||
-rw-r--r-- | tools/klee-zesti/CMakeLists.txt | 13 | ||||
-rwxr-xr-x | tools/klee-zesti/klee-zesti | 129 |
3 files changed, 143 insertions, 0 deletions
diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index 6fe153d7..a400569b 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -12,4 +12,5 @@ add_subdirectory(kleaver) add_subdirectory(klee) add_subdirectory(klee-replay) add_subdirectory(klee-stats) +add_subdirectory(klee-zesti) add_subdirectory(ktest-tool) diff --git a/tools/klee-zesti/CMakeLists.txt b/tools/klee-zesti/CMakeLists.txt new file mode 100644 index 00000000..20ad1ad0 --- /dev/null +++ b/tools/klee-zesti/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-zesti DESTINATION bin) + +# Copy into the build directory's binary directory +# so system tests can find it +configure_file(klee-zesti "${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/klee-zesti" COPYONLY) diff --git a/tools/klee-zesti/klee-zesti b/tools/klee-zesti/klee-zesti new file mode 100755 index 00000000..c4331403 --- /dev/null +++ b/tools/klee-zesti/klee-zesti @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +import sys +import os +import subprocess +import tempfile +import select +import shutil +HELP="""OVERVIEW: ZESTI like wrapper of KLEE + +USAGE: klee-zesti [klee-options] <input bytecode> <concrete program arguments> + +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 <concrete program arguments> 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 split_args(): + prog = None + prog_args = [] + klee_args = [] + is_progargs = False + for a in sys.argv[1:]: + if is_progargs: + prog_args += [a] + elif a.startswith("-"): + klee_args += [a] + else: + prog = a + is_progargs = True + return klee_args, prog, prog_args + +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(): + klee_args, prog, prog_args = split_args() + if len(sys.argv) == 1 or prog is None: + 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) + klee_args += ["-seed-file=" + ktest_file] + + proc = subprocess.Popen([KLEE] + klee_args + [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() + + |