Conclude concrete execution impl

5 files changed, 70 insertions, 39 deletions

diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp
index b0fc8caf..c68ec6d1 100644
--- a/lib/Core/Differentiator.cpp
+++ b/lib/Core/Differentiator.cpp
@@ -34,7 +34,7 @@ std::string quoted(const std::string& s) {
   return ss.str();
 }
 
-inline char hex(char c) {
+inline char hex(unsigned char c) {
     return (c < 10) ? '0' + c : 'a' + c - 10;
 }
 
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h
index 54a12ac7..1f9c7766 100644
--- a/lib/Core/Differentiator.h
+++ b/lib/Core/Differentiator.h
@@ -30,10 +30,14 @@ bool isSymArg(std::string);
 bool isSymOut(std::string);
 
 struct Differentiator {
-  uint64_t revA, revB;
-  std::map<uint8_t, std::string> args;
+  std::uint64_t revA, revB;
+  // arg_k => v
+  std::map<std::uint8_t, std::string> args;
+  // k => (out!k!a, out!k!b)
   std::map<std::string, std::pair<std::string, std::string>> outputs;
-  Differentiator(uint64_t a, uint64_t b) : revA{a}, revB{b} {}
+  // rev => stdout
+  std::map<std::uint64_t, std::string> stdouts;
+  Differentiator(std::uint64_t a, std::uint64_t b) : revA{a}, revB{b} {}
 };
 
 /// Write convenient representation for debugging
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 9f81c907..b614f6e4 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -421,9 +421,12 @@ std::string extractMetaEnvVar(ref<Expr> e) {
 }
 
 void ExecutionState::addConstraint(ref<Expr> e) {
-  this->metaEnvVar = extractMetaEnvVar(e);
-  if (!this->metaEnvVar.empty())
+  auto v = extractMetaEnvVar(e);
+  if (!v.empty()) {
+    if (v.substr(v.size() - 2) != "=0")
+      this->metaEnvVar = v;
     return;
+  }
   ConstraintManager c(constraints);
   c.addConstraint(e);
 }
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e87caa97..1906427e 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3604,6 +3604,9 @@ void Executor::doDumpStates() {
   for (const auto &state : states)
     terminateStateEarly(*state, "Execution halting.", StateTerminationType::Interrupted);
   updateStates(nullptr);
+
+  for (const auto& t : this->diffTests)
+    llvm::errs() << t << '\n';
 }
 
 void Executor::run(ExecutionState &initialState) {
@@ -3805,16 +3808,17 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {
   return ret;
 };
 
-void Executor::extractDifferentiator(uint64_t a, uint64_t b, const z3::model& m) {
-  auto test = Differentiator {a, b};
+void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
+                                     const z3::model& m) {
+  auto test = Differentiator {a->patchNo, b->patchNo};
   for (auto k = m.size(); k--;) {
     const auto& name = m[k].name().str();
     if (isSymArg(name)) {
       const uint8_t i = std::atoi(name.c_str() + 3);
       test.args[i] = "";
       const auto& expr = m.eval(m[k]());
-      for (uint8_t b = 0; b < this->symArgs[i]; ++b) {
-        const auto c = z3::select(expr, b).simplify().as_uint64();
+      for (uint8_t i = 0; i < this->symArgs[i]; ++i) {
+        const auto c = z3::select(expr, i).simplify().as_uint64();
         assert(c <= std::numeric_limits<unsigned char>::max());
         test.args[i].push_back((unsigned char) c);
       }
@@ -3823,8 +3827,8 @@ void Executor::extractDifferentiator(uint64_t a, uint64_t b, const z3::model& m)
       const auto& expr = m.eval(m[k]());
       std::string binary {""};
       const auto size = this->symOuts[name.substr(0, name.size() - 2)];
-      for (uint8_t b = 0; b < size; ++b) {
-        const auto c = z3::select(expr, b).simplify().as_uint64();
+      for (uint8_t i = 0; i < size; ++i) {
+        const auto c = z3::select(expr, i).simplify().as_uint64();
         assert(c <= std::numeric_limits<unsigned char>::max());
         binary.push_back((unsigned char) c);
         const auto& ident = name.substr(4, name.size() - 6);
@@ -3835,6 +3839,44 @@ void Executor::extractDifferentiator(uint64_t a, uint64_t b, const z3::model& m)
       }
     }
   }
+  llvm::errs() << test << '\n';
+
+  char buffer[128];
+  for (auto& rev : this->metaEnvVars) {
+    auto& envs = rev.second;
+    pid_t pid;
+    std::vector<const char*> args {this->concreteProgram.c_str()};
+    uint8_t last = 0;
+    for (const auto& p : test.args) {
+      assert(p.first == last);
+      args.push_back(p.second.c_str());
+      last++;
+    }
+    args.push_back(NULL);
+
+    int fildes[2];
+    auto err = pipe(fildes);
+    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);
+    char *const envp[] = {const_cast<char* const>(envs.c_str()), NULL};
+    err = posix_spawn(&pid, this->concreteProgram.c_str(), &action, NULL,
+                      const_cast<char* const *>(args.data()),
+                      envs.empty() ? NULL : envp);
+    assert(!err);
+    close(fildes[1]);
+    std::string out = "";
+    for (ssize_t n; n = read(fildes[0], buffer, 127);) {
+      assert(n >= 0);
+      buffer[n] = 0;
+      out += buffer;
+    }
+    test.stdouts[rev.first] = out;
+    llvm::errs() << "rev " << rev.first << ' ' << out;
+    posix_spawn_file_actions_destroy(&action);
+  }
   this->diffTests.push_back(test);
 }
 
@@ -3869,14 +3911,15 @@ void Executor::searchDifferentiators(ExecutionState* latest) {
     auto command = "symbdiff " + smt2_name + " " + last_smt2_name;
     for (const auto& out : this->symOuts)
       command += " " + std::to_string(out.second);
-    const auto out = popen(command.c_str(), "r");
+    const auto out = popen((command + " 2> /dev/null").c_str(), "r");
     std::string formula;
     char buffer[128];
     while (!feof(out))
-      if (fgets(buffer, 128, out) != NULL)
+      if (fgets(buffer, 127, out) != NULL)
         formula += buffer;
-    assert(pclose(out) == 0);
     remove(smt2_name.c_str());
+    if (pclose(out))
+      continue;
 
     static z3::context c;
     static z3::solver s {c};
@@ -3884,30 +3927,8 @@ void Executor::searchDifferentiators(ExecutionState* latest) {
     s.from_string(formula.c_str());
     if (s.check() != z3::sat)
       continue;
-    this->extractDifferentiator(latest->patchNo, state->patchNo, s.get_model());
+    this->extractDifferentiator(latest, state, s.get_model());
     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());
@@ -3921,6 +3942,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
         terminationTypeFileExtension(StateTerminationType::Exit).c_str());
 
   interpreterHandler->incPathsCompleted();
+  metaEnvVars[state.patchNo] = state.metaEnvVar;
   getConstraintLog(state, state.formula, Interpreter::SMTLIB2);
   searchDifferentiators(&state);
   exitStates.insert(&state);
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 6a6b19c0..3b10fa27 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -117,6 +117,7 @@ private:
   std::unique_ptr<MemoryManager> memory;
   std::set<ExecutionState*, ExecutionStateIDCompare> states;
   std::set<ExecutionState*, ExecutionStateIDCompare> exitStates;
+  std::map<std::uint64_t, std::string> metaEnvVars;
   std::vector<Differentiator> diffTests;
   StatsTracker *statsTracker;
   TreeStreamWriter *pathWriter, *symPathWriter;
@@ -432,7 +433,8 @@ private:
       llvm::Instruction** lastInstruction);
 
   /// Extract differencial test from SMT model
-  void extractDifferentiator(uint64_t, uint64_t, const z3::model&);
+  void extractDifferentiator(ExecutionState*, ExecutionState*,
+                             const z3::model&);
 
   /// Compare with other exit states for possible differencial tests
   void searchDifferentiators(ExecutionState *state);