Make symbolic stdout more flexible

6 files changed, 162 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;
 }
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] <input bytecode> <concrete program>
+    <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 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()