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()
+
+