Merge pull request #397 from andreamattavelli/refactoring_stdin

Distinct options for symbolic files and symbolic stdin

5 files changed, 28 insertions, 18 deletions

diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h
index cb86295c..4a6fbc15 100644
--- a/runtime/POSIX/fd.h
+++ b/runtime/POSIX/fd.h
@@ -71,9 +71,9 @@ typedef struct {
 extern exe_file_system_t __exe_fs;
 extern exe_sym_env_t __exe_env;
 
-void klee_init_fds(unsigned n_files, unsigned file_length, 
-		   int sym_stdout_flag, int do_all_writes_flag, 
-		   unsigned max_failures);
+void klee_init_fds(unsigned n_files, unsigned file_length,
+                   unsigned stdin_length, int sym_stdout_flag,
+                   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 8b69fd04..9184b7ea 100644
--- a/runtime/POSIX/fd_init.c
+++ b/runtime/POSIX/fd_init.c
@@ -107,9 +107,9 @@ static unsigned __sym_uint32(const char *name) {
                          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, 
-		   int sym_stdout_flag, int save_all_writes_flag,
-		   unsigned max_failures) {
+void klee_init_fds(unsigned n_files, unsigned file_length,
+                   unsigned stdin_length, int sym_stdout_flag,
+                   int save_all_writes_flag, unsigned max_failures) {
   unsigned k;
   char name[7] = "?-data";
   struct stat64 s;
@@ -124,9 +124,9 @@ void klee_init_fds(unsigned n_files, unsigned file_length,
   }
   
   /* setting symbolic stdin */
-  if (file_length) {
+  if (stdin_length) {
     __exe_fs.sym_stdin = malloc(sizeof(*__exe_fs.sym_stdin));
-    __create_new_dfile(__exe_fs.sym_stdin, file_length, "stdin", &s);
+    __create_new_dfile(__exe_fs.sym_stdin, stdin_length, "stdin", &s);
     __exe_env.fds[0].dfile = __exe_fs.sym_stdin;
   }
   else __exe_fs.sym_stdin = NULL;
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index cbcf31f4..8e578cf0 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -90,6 +90,7 @@ void klee_init_env(int* argcPtr, char*** argvPtr) {
   char* new_argv[1024];
   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;
   int save_all_writes_flag = 0;
   int fd_fail = 0;
@@ -102,13 +103,14 @@ void klee_init_env(int* argcPtr, char*** argvPtr) {
 
   // Recognize --help when it is the sole argument.
   if (argc == 2 && __streq(argv[1], "--help")) {
-  __emit_error("klee_init_env\n\n\
+    __emit_error("klee_init_env\n\n\
 usage: (klee_init_env) [options] [program arguments]\n\
   -sym-arg <N>              - Replace by a symbolic argument with length N\n\
   -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most\n\
                               MAX arguments, each with maximum length N\n\
-  -sym-files <NUM> <N>      - Make stdin and up to NUM symbolic files, each\n\
-                              with maximum size N.\n\
+  -sym-files <NUM> <N>      - Make up to NUM symbolic files, each\n\
+                                with maximum size N.\n\
+  -sym-stdin <N>            - Make stdin symbolic with maximum size N.\n\
   -sym-stdout               - Make stdout symbolic.\n\
   -max-fail <N>             - Allow up to <N> injected failures\n\
   -fd-fail                  - Shortcut for '-max-fail 1'\n\n");
@@ -156,8 +158,17 @@ usage: (klee_init_env) [options] [program arguments]\n\
       sym_files = __str_to_int(argv[k++], msg);
       sym_file_len = __str_to_int(argv[k++], msg);
 
-    }
-    else if (__streq(argv[k], "--sym-stdout") || __streq(argv[k], "-sym-stdout")) {
+    } else if (__streq(argv[k], "--sym-stdin") ||
+               __streq(argv[k], "-sym-stdin")) {
+      const char *msg =
+          "--sym-stdin expects one integer argument <sym-stdin-len>";
+
+      if (++k == argc)
+        __emit_error(msg);
+
+      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++;
     }
@@ -190,8 +201,7 @@ usage: (klee_init_env) [options] [program arguments]\n\
   *argcPtr = new_argc;
   *argvPtr = final_argv;
 
-  klee_init_fds(sym_files, sym_file_len, 
-		sym_stdout_flag, save_all_writes_flag, 
-		fd_fail);
+  klee_init_fds(sym_files, sym_file_len, sym_stdin_len, sym_stdout_flag,
+                save_all_writes_flag, fd_fail);
 }
 
diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c
index 241c5cbb..fdfc6ceb 100644
--- a/test/Runtime/POSIX/Isatty.c
+++ b/test/Runtime/POSIX/Isatty.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout > %t.log 2>&1
+// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-stdin 10 --sym-stdout > %t.log 2>&1
 // RUN: test -f %t.klee-out/test000001.ktest
 // RUN: test -f %t.klee-out/test000002.ktest
 // RUN: test -f %t.klee-out/test000003.ktest
diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c
index ebf16405..09eed6d2 100644
--- a/test/Runtime/POSIX/Stdin.c
+++ b/test/Runtime/POSIX/Stdin.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log
+// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-stdin 4 > %t.log
 // RUN: grep "mode:file" %t.log
 // RUN: grep "mode:dir" %t.log
 // RUN: grep "mode:chr" %t.log