Refine support for stdio capture psychic

4 files changed, 38 insertions, 30 deletions

diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp
index 95c08bda..553df337 100644
--- a/lib/Core/Differentiator.cpp
+++ b/lib/Core/Differentiator.cpp
@@ -109,35 +109,41 @@ Differentiator::Differentiator(std::unique_ptr<TimingSolver>* s,
 
 Differentiator::Bytes
 run(const std::uint64_t rev, const char* prog,
-    const Differentiator::TestArgs& argv)
+    const Differentiator::TestInps& inputs)
 {
-  int fildes[2];
+  int ind[2], outd[2];
   {
-    const auto err = pipe(fildes);
+    auto err = pipe(ind);
+    assert(!err);
+    err = pipe(outd);
     assert(!err);
   }
   posix_spawn_file_actions_t action;
   posix_spawn_file_actions_init(&action);
-  posix_spawn_file_actions_addclose(&action, fildes[0]);
-  posix_spawn_file_actions_adddup2(&action, fildes[1], 1);
+  posix_spawn_file_actions_adddup2(&action, ind[0], 0);
+  posix_spawn_file_actions_addclose(&action, ind[1]);
+  posix_spawn_file_actions_addclose(&action, outd[0]);
+  posix_spawn_file_actions_adddup2(&action, outd[1], 1);
   {
     pid_t pid;
-    std::vector<const char*> argp {prog};
-    for (const auto& v : argv)
-      argp.push_back((const char *) v.data());
-    argp.push_back(NULL);
+    std::vector<const char*> argv {prog};
+    for (const auto& v : inputs.first)
+      argv.push_back((const char *) v.data());
+    argv.push_back(NULL);
     std::ostringstream env;
     env << "KLEE_META=" << rev;
     char *const envp[] = {const_cast<char* const>(env.str().c_str()), NULL};
     const auto err = posix_spawn(&pid, prog, &action, NULL,
-                                 const_cast<char* const *>(argp.data()), envp);
+                                 const_cast<char* const *>(argv.data()), envp);
     assert(!err);
   }
-  close(fildes[1]);
+  write(ind[0], inputs.second.data(), inputs.second.size());
+  close(ind[0]);
+  close(outd[1]);
 
   char buffer[128]; // output buffer for concrete execution
   Differentiator::Bytes result;
-  for (unsigned char n; n = read(fildes[0], buffer, sizeof(buffer));) {
+  for (unsigned char n; n = read(outd[0], buffer, sizeof(buffer));) {
     assert(n >= 0);
     for (unsigned char i = 0; i < n; ++i)
       result.push_back(buffer[i]);
@@ -156,14 +162,14 @@ logBytes(const Differentiator::Bytes& buffer)
 }
 
 void
-logArgs(const Differentiator::TestArgs& args)
+logInputs(const Differentiator::TestInps& inputs)
 {
   llvm::errs() << "Args:";
-  for (const auto& s : args) {
+  for (const auto& s : inputs.first) {
     llvm::errs() << ' ';
     logBytes(s);
   }
-  llvm::errs() << '\n';
+  llvm::errs() << "\nStdin: " << inputs.second.data() << '\n';
 }
 
 void
@@ -188,7 +194,7 @@ Differentiator::extract(ExecutionState* a, ExecutionState* b,
                         const std::vector<const Array*>& objects,
                         const std::vector<Bytes>& values)
 {
-  TestArgs argv;
+  TestInps inputs;
   TestOuts outputs;
   {
     std::map<std::uint8_t, Bytes> args;
@@ -200,18 +206,20 @@ Differentiator::extract(ExecutionState* a, ExecutionState* b,
       } else if (isSymOut(name.substr(0, name.size() - 2))) {
         const auto rev = ((name[name.size() - 1] == 'a') ? a : b)->patchNo;
         outputs[rev].first[name.substr(4, name.size() - 6)] = values[i];
+      } else if (name == "stdin") {
+          inputs.second = values[i];
       }
     }
     uint8_t last = 0;
     for (const auto& [rev, arg] : args) {
       assert(rev == last);
-      argv.push_back(arg);
+      inputs.first.push_back(arg);
       last++;
     }
   }
   for (const auto& rev : this->revisions)
-    outputs[rev].second = run(rev, this->prog, argv);
-  this->tests[argv] = outputs;
+    outputs[rev].second = run(rev, this->prog, inputs);
+  this->tests[inputs] = outputs;
 
   std::map<std::string, Clusters> revOut;
   for (const auto& [rev, out] : outputs) {
@@ -228,7 +236,7 @@ Differentiator::extract(ExecutionState* a, ExecutionState* b,
         for (std::uint64_t i : p.second)
           for (std::uint64_t j : q.second)
             if (i < j)
-              this->done.emplace(std::make_pair(i, j), &this->tests[argv]);
+              this->done.emplace(std::make_pair(i, j), &this->tests[inputs]);
       }
 }
 
@@ -314,7 +322,7 @@ Differentiator::search(ExecutionState* latest)
 void
 Differentiator::log()
 {
-  std::vector<std::pair<const TestArgs, const Clusters>> clusterings;
+  std::vector<std::pair<const TestInps, const Clusters>> clusterings;
   for (auto& t : this->tests) {
     Clusters clusters;
     for (const auto& rev : this->revisions) {
@@ -327,8 +335,8 @@ Differentiator::log()
     if (clusters.size() > 1)
       clusterings.push_back({std::move(t.first), std::move(clusters)});
   }
-  for (const auto& [args, clusters] : clusterings) {
-    logArgs(args);
+  for (const auto& [inputs, clusters] : clusterings) {
+    logInputs(inputs);
     logClusters(clusters);
     llvm::errs() << '\n';
   }
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h
index 11225ac7..98c15e92 100644
--- a/lib/Core/Differentiator.h
+++ b/lib/Core/Differentiator.h
@@ -35,8 +35,8 @@ private:
 struct Differentiator {
   /// Buffer of bytes
   typedef std::vector<unsigned char> Bytes;
-  /// CLI arguments
-  typedef std::vector<Bytes> TestArgs;
+  /// argv stdin
+  typedef std::pair<std::vector<Bytes>, Bytes> TestInps;
   /// :rev (:var val) stdout
   typedef std::map<std::uint64_t,
                    std::pair<std::map<std::string, Bytes>,
@@ -59,6 +59,8 @@ struct Differentiator {
 
   /// Program revision numbers
   std::set<std::uint64_t> revisions;
+  /// Differentiated pairs
+  std::map<std::pair<std::uint64_t, std::uint64_t>, TestOuts*> done;
 private:
   /// Program path for concrete execution.
   const char* prog;
@@ -67,7 +69,7 @@ private:
            std::set<ExecutionState*,
                     ExecutionStatePathCondCompare>> exits;
   /// Differential tests
-  std::map<TestArgs, TestOuts> tests;
+  std::map<TestInps, TestOuts> tests;
   /// SMT solver "borrowed" from Executor
   std::unique_ptr<TimingSolver>* solver;
   /// SMT solving timeout
@@ -76,8 +78,6 @@ private:
   ArrayCache& arrayCache;
   /// Symbolic output renamers
   ExprCmbnVisitor visitorA, visitorB;
-  /// Differentiated pairs
-  std::map<std::pair<std::uint64_t, std::uint64_t>, TestOuts*> done;
 };
 
 } // namespace klee
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 465100f4..34b3d7b8 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1104,7 +1104,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
 
   // Fix branch in only-replay-seed mode, if we don't have both true
   // and false seeds.
-  if (isSeeding && 
+  if (isSeeding && !Differentiator::extractPatchNumber(condition).first &&
       (current.forkDisabled || OnlyReplaySeeds) && 
       res == Solver::Unknown) {
     bool trueSeed=false, falseSeed=false;
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c
index b93148ec..90c04a73 100644
--- a/runtime/POSIX/fd_init.c
+++ b/runtime/POSIX/fd_init.c
@@ -153,7 +153,7 @@ void klee_init_fds(unsigned n_files, unsigned file_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, stdout_length, "stdout", &s);
+    __create_new_dfile(__exe_fs.sym_stdout, stdout_length, "out!stdout!0", &s);
     __exe_env.fds[1].dfile = __exe_fs.sym_stdout;
     __exe_fs.stdout_writes = 0;
   }