Lay ground work for concrete execution

6 files changed, 81 insertions, 33 deletions

diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
index 04fdef88..8948bfce 100644
--- a/include/klee/Core/Interpreter.h
+++ b/include/klee/Core/Interpreter.h
@@ -129,6 +129,9 @@ public:
   // a user specified path. use null to reset.
   virtual void setReplayPath(const std::vector<bool> *path) = 0;
 
+  // supply path to the program for concrete execution.
+  virtual void setProgram(const std::string& path) = 0;
+
   // supply a set of symbolic bindings that will be used as "seeds"
   // for the search. use null to reset.
   virtual void useSeeds(const std::vector<struct KTest *> *seeds) = 0;
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 2a754acd..9f81c907 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -110,6 +110,7 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     arrayNames(state.arrayNames),
     openMergeStack(state.openMergeStack),
     patchNo(state.patchNo),
+    metaEnvVar(state.metaEnvVar),
     formula(state.formula),
     steppedInstructions(state.steppedInstructions),
     instsSinceCovNew(state.instsSinceCovNew),
@@ -390,35 +391,38 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
   }
 }
 
-bool isMetaConstraint(ref<Expr> e) {
+std::string extractMetaEnvVar(ref<Expr> e) {
   if (e.get()->getKind() != Expr::Eq)
-    return false;
+    return "";
   const auto eq = dyn_cast<EqExpr>(e.get());
   if (eq->left.get()->getKind() != Expr::Constant)
-    return false;
+    return "";
   const auto constant = dyn_cast<ConstantExpr>(eq->left.get());
   if (constant->isFalse()) // the else branch
-    return isMetaConstraint(eq->right);
+    return extractMetaEnvVar(eq->right);
 
   if (eq->right.get()->getKind() != Expr::Concat)
-    return false;
+    return "";
   const auto concat = dyn_cast<ConcatExpr>(eq->right.get());
   if (concat->getLeft().get()->getKind() != Expr::Read)
-    return false;
+    return "";
 
   const auto read = dyn_cast<ReadExpr>(concat->getLeft().get());
   const auto& name = read->updates.root->name;
   // string::starts_with requires C++20
   if (name.substr(0, 8) != "__choose")
-    return false;
+    return "";
   for (const auto c : name.substr(8))
     if ('0' > c || c > '9')
-      return false;
-  return true;
+      return "";
+  std::string value;
+  constant->toString(value);
+  return "__SWITCH" + name.substr(8, name.size() - 8) + "=" + value;
 }
 
 void ExecutionState::addConstraint(ref<Expr> e) {
-  if (isMetaConstraint(e))
+  this->metaEnvVar = extractMetaEnvVar(e);
+  if (!this->metaEnvVar.empty())
     return;
   ConstraintManager c(constraints);
   c.addConstraint(e);
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 5df7ad70..1a3f42e7 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -229,6 +229,9 @@ public:
   /// @ brief The patch number, starting from 1; 0 being the original.
   std::uint64_t patchNo = 0;
 
+  /// @ brief Environment variable for runtime metaprogram switching.
+  std::string metaEnvVar = "";
+
   /// @ brief Terminated on exit, awaiting comparison.
   std::string formula = "";
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index cfbe7357..e87caa97 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -91,6 +91,7 @@
 #include <iomanip>
 #include <iosfwd>
 #include <limits>
+#include <spawn.h>
 #include <sstream>
 #include <stdlib.h>
 #include <string>
@@ -3837,39 +3838,44 @@ void Executor::extractDifferentiator(uint64_t a, uint64_t b, const z3::model& m)
   this->diffTests.push_back(test);
 }
 
+std::string hash(std::string data) {
+  std::stringstream stream;
+  stream << std::hex << std::setw(16) << std::setfill('0')
+         << std::hash<std::string>{}(data);
+  return stream.str();
+}
+
 void Executor::searchDifferentiators(ExecutionState* latest) {
-  std::string last_smt2_name = "smt2.XXXXXX";
-  auto last_smt2_fd = mkstemp(last_smt2_name.data());
-  assert(last_smt2_fd != -1);
-  const auto written = write(last_smt2_fd, latest->formula.c_str(),
-                             latest->formula.size());
-  assert(written == latest->formula.size());
-  close(last_smt2_fd);
+  auto last_smt2_name = hash(latest->formula) + ".smt2";
+  std::ofstream last_smt2_file;
+  last_smt2_file.open(last_smt2_name);
+  last_smt2_file << latest->formula;
+  last_smt2_file.close();
   for (const auto& state : this->exitStates) {
     // TODO: skip moar and order
     if (state->patchNo == latest->patchNo)
       continue;
+    auto smt2_name = hash(state->formula) + ".smt2";
+    if (smt2_name == last_smt2_name)
+      continue;
 
     // File I/O is expensive but SMT solving is even more expensive (-;
     // Seriously though, FIXME: implement symbdiff natively
-    std::string smt2_name = "smt2.XXXXXX";
-    auto smt2_fd = mkstemp(smt2_name.data());
-    assert(smt2_fd != -1);
-    const auto written = write(smt2_fd, state->formula.c_str(),
-                               state->formula.size());
-    assert(written == state->formula.size());
-    close(smt2_fd);
+    std::ofstream smt2_file;
+    smt2_file.open(smt2_name);
+    smt2_file << state->formula;
+    smt2_file.close();
 
     auto command = "symbdiff " + smt2_name + " " + last_smt2_name;
     for (const auto& out : this->symOuts)
       command += " " + std::to_string(out.second);
-    const auto pipe = popen(command.c_str(), "r");
+    const auto out = popen(command.c_str(), "r");
     std::string formula;
     char buffer[128];
-    while (!feof(pipe))
-      if (fgets(buffer, 128, pipe) != NULL)
+    while (!feof(out))
+      if (fgets(buffer, 128, out) != NULL)
         formula += buffer;
-    assert(pclose(pipe) == 0);
+    assert(pclose(out) == 0);
     remove(smt2_name.c_str());
 
     static z3::context c;
@@ -3879,7 +3885,30 @@ void Executor::searchDifferentiators(ExecutionState* latest) {
     if (s.check() != z3::sat)
       continue;
     this->extractDifferentiator(latest->patchNo, state->patchNo, s.get_model());
-    llvm::errs() << this->diffTests.back() << "\n";
+    assert(!this->diffTests.empty());
+
+    pid_t pid;
+    std::vector<const char*> args {this->concreteProgram.c_str()};
+    uint8_t last = 0;
+    for (const auto& p : this->diffTests.back().args) {
+      assert(p.first == last);
+      args.push_back(p.second.c_str());
+      last++;
+    }
+    int fildes[2];
+    auto err = pipe(fildes);
+    if (err)
+      llvm::errs() << "failed creating pipe\n";
+    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);
+    char *const envp[] = {const_cast<char* const>(latest->metaEnvVar.c_str()),
+                          NULL};
+    auto status = posix_spawn(&pid, this->concreteProgram.c_str(),
+                              &action, NULL,
+                              const_cast<char* const *>(args.data()), envp);
+    break;
   }
   remove(last_smt2_name.c_str());
 }
@@ -3893,8 +3922,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
 
   interpreterHandler->incPathsCompleted();
   getConstraintLog(state, state.formula, Interpreter::SMTLIB2);
-  if (state.patchNo)
-    searchDifferentiators(&state);
+  searchDifferentiators(&state);
   exitStates.insert(&state);
   terminateState(state, StateTerminationType::Exit);
 }
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 5719c510..6a6b19c0 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -172,6 +172,9 @@ private:
   /// object.
   unsigned replayPosition;
 
+  /// Program path for concrete execution.
+  std::string concreteProgram;
+
   /// When non-null a list of "seed" inputs which will be used to
   /// drive execution.
   const std::vector<struct KTest *> *usingSeeds;  
@@ -554,6 +557,10 @@ public:
     replayPosition = 0;
   }
 
+  void setProgram(const std::string& path) override {
+    this->concreteProgram = path;
+  }
+
   llvm::Module *setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
                           const ModuleOptions &opts) override;
 
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 3c6c81ca..61455ef6 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -66,7 +66,10 @@ using namespace klee;
 
 namespace {
   cl::opt<std::string>
-  InputFile(cl::desc("<input bytecode>"), cl::Positional, cl::init("-"));
+  InputFile(cl::desc("<input bytecode>"), cl::Positional, cl::Required);
+
+  cl::opt<std::string>
+  InputProgram(cl::desc("<input program>"), cl::Positional, cl::Required);
 
   cl::list<std::string>
   InputArgv(cl::ConsumeAfter,
@@ -1418,8 +1421,8 @@ int main(int argc, char **argv, char **envp) {
   std::vector<bool> replayPath;
   if (!ReplayPathFile.empty()) {
     KleeHandler::loadPathFile(ReplayPathFile, replayPath);
-    interpreter->setReplayPath(&replayPath);
   }
+  interpreter->setProgram(InputProgram);
 
   auto startTime = std::time(nullptr);
   { // output clock info and start time