about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r--lib/Core/Executor.cpp204
1 files changed, 9 insertions, 195 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 056c6aad..22e4ac92 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -92,7 +92,6 @@
 #include <iomanip>
 #include <iosfwd>
 #include <limits>
-#include <spawn.h>
 #include <sstream>
 #include <stdlib.h>
 #include <string>
@@ -489,13 +488,12 @@ unsigned dumpStates = 0, dumpExecutionTree = 0;
 Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                    InterpreterHandler *ih)
     : Interpreter(opts), interpreterHandler(ih), searcher(0),
-      externalDispatcher(new ExternalDispatcher(ctx)),
-      metaEnvVars{{0, ""}}, statsTracker(0), pathWriter(0), symPathWriter(0),
-      specialFunctionHandler(0), timers{time::Span(TimerInterval)},
+      externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
+      pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)},
       replayKTest(0), replayPath(0), usingSeeds(0),
       atMemoryLimit(false), inhibitForking(false), haltExecution(false),
-      ivcEnabled(false), debugLogBuffer(debugBufferString),
-      visitorA{'a', arrayCache}, visitorB{'b', arrayCache} {
+      ivcEnabled(false), differ(&solver, coreSolverTimeout, arrayCache),
+      debugLogBuffer(debugBufferString) {
 
 
   const time::Span maxTime{MaxTime};
@@ -3661,16 +3659,6 @@ bool Executor::checkMemoryUsage() {
   return false;
 }
 
-std::string quoted(const char* s) {
-  std::stringstream ss;
-  ss << std::quoted(s);
-  return ss.str();
-}
-
-inline char hex(unsigned char c) {
-  return (c < 10) ? '0' + c : 'a' + c - 10;
-}
-
 void Executor::doDumpStates() {
   if (!DumpStatesOnHalt || states.empty()) {
     interpreterHandler->incPathsExplored(states.size());
@@ -3681,34 +3669,6 @@ void Executor::doDumpStates() {
   for (const auto &state : states)
     terminateStateEarly(*state, "Execution halting.", StateTerminationType::Interrupted);
   updateStates(nullptr);
-
-  std::set<uint64_t> revs;
-  for (const auto& p : this->metaEnvVars)
-    revs.insert(p.first);
-  for (const auto& t : this->diffTests) {
-    std::map<TestVal, std::set<std::uint64_t>> stdoutClusters;
-    std::map<std::pair<std::string, TestVal>,
-             std::set<std::uint64_t>> varClusters;
-    for (const auto& rev : t.second) {
-      for (const auto& var : rev.second.first)
-        varClusters[var].insert(rev.first);
-      stdoutClusters[rev.second.second].insert(rev.first);
-      // TODO: improve output format
-      if (stdoutClusters.size() > 1) {
-        llvm::errs() << "Args:";
-        for (const auto& s : t.first)
-          llvm::errs() << " \"" << quoted((const char *) s.data()) << '"';
-        llvm::errs() << '\n';
-        int i = 0;
-        for (const auto& so : stdoutClusters) {
-          llvm::errs() << i++ << " " << so.first.data();
-          for (const auto& r : so.second)
-            llvm::errs() << " " << r;
-          llvm::errs() << '\n';
-        }
-      }
-    }
-  }
 }
 
 void Executor::run(ExecutionState &initialState) {
@@ -3910,151 +3870,6 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {
   return ret;
 };
 
-void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
-                                     std::vector<const Array*> objects,
-                                     std::vector<TestVal> values) {
-  Executor::TestArgs argv;
-  Executor::TestOuts outputs;
-  {
-    std::map<std::uint8_t, TestVal> args;
-    for (unsigned i = 0; i < objects.size(); ++i) {
-      const auto& name = objects[i]->name;
-      if (isSymArg(name)) {
-        args[std::atoi(name.c_str() + 3)] = values[i];
-        args[std::atoi(name.c_str() + 3)].push_back(0); // null termination
-      } 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];
-      }
-    }
-    uint8_t last = 0;
-    for (const auto& p : args) {
-      assert(p.first == last);
-      argv.push_back(p.second);
-      last++;
-    }
-  }
-
-  char buffer[128]; // output buffer for concrete execution
-  for (const auto& rev : this->metaEnvVars) {
-    auto& envs = rev.second;
-    pid_t pid;
-    std::vector<const char*> argp {this->concreteProgram.c_str()};
-    for (const auto& v : argv)
-      argp.push_back((const char *) v.data());
-    argp.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 *>(argp.data()),
-                      envs.empty() ? NULL : envp);
-    assert(!err);
-    close(fildes[1]);
-    for (unsigned char n; n = read(fildes[0], buffer, sizeof(buffer));) {
-      assert(n >= 0);
-      for (unsigned char i = 0; i < n; ++i)
-        outputs[rev.first].second.push_back(buffer[i]);
-    }
-    outputs[rev.first].second.push_back(0); // null termination
-    posix_spawn_file_actions_destroy(&action);
-  }
-  this->diffTests[argv] = outputs;
-  // :var :val cluster
-  std::map<std::string, std::map<TestVal, std::set<std::uint64_t>>> revOut;
-  for (auto& o : outputs) {
-    for (auto& var : o.second.first)
-      revOut[var.first][var.second].insert(o.first);
-    revOut[""][o.second.second].insert(o.first); // stdout
-  }
-
-  for (auto& vp : revOut)
-    for (auto& p : vp.second)
-      for (auto& q : vp.second) {
-        if (&p == &q)
-          continue;
-        for (std::uint64_t i : p.second)
-          for (std::uint64_t j : q.second)
-            if (i < j)
-              this->decided.emplace(std::make_pair(i, j),
-                                    &this->diffTests[argv]);
-      }
-}
-
-void Executor::searchDifferentiators(ExecutionState* latest) {
-  for (const auto& rev : this->exitStates) {
-    if (rev.first == latest->patchNo)
-      continue;
-    if (rev.first < latest->patchNo) {
-      if (this->decided.find(std::make_pair(rev.first, latest->patchNo))
-          != this->decided.end())
-        continue;
-    } else {
-      if (this->decided.find(std::make_pair(latest->patchNo, rev.first))
-          != this->decided.end())
-        continue;
-    }
-    for (const auto& state : rev.second) {
-      ConstraintSet cmbnSet;
-      {
-        std::set<ref<Expr>> combination;
-        for (auto const& constraint : state->constraints)
-          combination.insert(this->visitorA.visit(constraint));
-        for (auto const& constraint : latest->constraints)
-          combination.insert(this->visitorB.visit(constraint));
-        for (auto const& constraint : combination)
-          cmbnSet.push_back(constraint);
-      }
-
-      std::vector<const Array*> objects;
-      // FIXME: what if diff symbolics
-      for (const auto& sym : state->symbolics) {
-        if (isSymArg(sym.second->name)) {
-          objects.push_back(sym.second);
-          continue;
-        }
-        if (!isSymOut(sym.second->name))
-          continue;
-        objects.push_back(arrayCache.CreateArray(sym.second->name + "!a",
-                                                 sym.second->size));
-        objects.push_back(arrayCache.CreateArray(sym.second->name + "!b",
-                                                 sym.second->size));
-
-        ref<Expr> distinction;
-        // FIXME: impossible to use visitor hash
-        for (const auto& a : this->visitorA.outVars[sym.second->name]) {
-          const auto ne = NotExpr::create(EqExpr::create(a.second,
-            this->visitorB.outVars[sym.second->name][a.first]));
-          if (distinction.get() == nullptr)
-            distinction = ne;
-          else
-            distinction = OrExpr::create(ne, distinction);
-        }
-        assert(distinction.get() != nullptr);
-        cmbnSet.push_back(distinction);
-      }
-
-      this->solver->setTimeout(coreSolverTimeout);
-      std::vector<TestVal> values;
-      bool success = this->solver->getInitialValues(cmbnSet, objects, values,
-                                                    state->queryMetaData);
-      solver->setTimeout(time::Span());
-      if (!success)
-        continue;
-      this->extractDifferentiator(latest, state, objects, values);
-      assert(!this->diffTests.empty());
-      llvm::errs() << latest->patchNo << ' ' << state->patchNo << '\n';
-      break; // one diff test per termination for now
-    }
-  }
-}
-
 void Executor::terminateStateOnExit(ExecutionState &state) {
   ++stats::terminationExit;
   if (shouldWriteTest(state) || (AlwaysOutputSeeds && seedMap.count(&state)))
@@ -4063,8 +3878,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
         terminationTypeFileExtension(StateTerminationType::Exit).c_str());
 
   interpreterHandler->incPathsCompleted();
-  if (exitStates[state.patchNo].insert(&state).second)
-    searchDifferentiators(&state);
+  differ.search(&state);
   terminateState(state, StateTerminationType::Exit);
 }
 
@@ -4190,8 +4004,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
     interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix);
   }
 
-  if (exitStates[state.patchNo].insert(&state).second)
-    searchDifferentiators(&state);
+  differ.search(&state);
   terminateState(state, terminationType);
 
   if (shouldExitOn(terminationType))
@@ -4882,10 +4695,10 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     bindObjectInState(state, mo, false, array);
     state.addSymbolic(mo, array);
 
-    if (isSymArg(uniqueName)) {
+    if (Differentiator::isSymArg(uniqueName)) {
       assert(std::atoi(name.c_str() + 3) == this->symArgs.size());
       this->symArgs.push_back(mo->size - 1); // string's null termination
-    } else if (isSymOut(uniqueName)) {
+    } else if (Differentiator::isSymOut(uniqueName)) {
       // assert(this->symOuts.find(uniqueName) == this->symOuts.end());
       this->symOuts[uniqueName] = mo->size;
     }
@@ -5042,6 +4855,7 @@ void Executor::runFunctionAsMain(Function *f,
   executionTree = createExecutionTree(
       *state, userSearcherRequiresInMemoryExecutionTree(), *interpreterHandler);
   run(*state);
+  differ.log();
   executionTree = nullptr;
 
   // hack to clear memory objects
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-06-02 22:32:25 +0000