Move differentiator to separate module

9 files changed, 349 insertions, 281 deletions

diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
index 8948bfce..04fdef88 100644
--- a/include/klee/Core/Interpreter.h
+++ b/include/klee/Core/Interpreter.h
@@ -129,9 +129,6 @@ 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/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 021c3ce7..534753eb 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -12,6 +12,7 @@ add_library(kleeCore
   CallPathManager.cpp
   Context.cpp
   CoreStats.cpp
+  Differentiator.cpp
   ExecutionState.cpp
   ExecutionTree.cpp
   ExecutionTreeWriter.cpp
diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp
new file mode 100644
index 00000000..20aa69c9
--- /dev/null
+++ b/lib/Core/Differentiator.cpp
@@ -0,0 +1,250 @@
+// Metaprogram's revision differentiator implementation
+// Copyright 2023  Nguyễn Gia Phong
+//
+// This file is distributed under the University of Illinois
+// Open Source License.  See LICENSE.TXT for details.
+
+#include "Differentiator.h"
+
+#include "llvm/Support/ErrorHandling.h"
+#include "llvm/Support/CommandLine.h"
+
+#include <spawn.h>
+
+llvm::cl::opt<std::string>
+InputProgram{llvm::cl::desc("<input program>"),
+             llvm::cl::Positional, llvm::cl::Required};
+
+using namespace klee;
+
+ExprCmbnVisitor::ExprCmbnVisitor(char rev, ArrayCache& ac)
+: revision(rev), arrayCache(ac)
+{}
+
+ExprVisitor::Action
+ExprCmbnVisitor::visitExprPost(const Expr& e)
+{
+  if (e.getKind() != Expr::Read)
+    return ExprVisitor::Action::doChildren();
+  const auto load = dyn_cast<ReadExpr>(&e);
+  const auto orig = load->updates.root;
+  if (!Differentiator::isSymOut(orig->name))
+    return ExprVisitor::Action::doChildren();
+  const auto a = this->arrayCache.CreateArray(
+    orig->name + '!' + this->revision,
+    orig->size, 0, 0, orig->domain, orig->range);
+  const auto replacement = ReadExpr::create({a, load->updates.head},
+                                            load->index);
+  this->outVars[orig->name][load->index] = dyn_cast<ReadExpr>(replacement.get());
+  return ExprVisitor::Action::changeTo(replacement);
+}
+
+bool
+Differentiator::isSymArg(const std::string& name)
+{
+  return (name.size() == 5 // string::starts_with requires C++20
+          && name[0] == 'a' && name[1] == 'r' && name[2] == 'g'
+          && '0' <= name[3] && name[3] <= '9'
+          && '0' <= name[4] && name[4] <= '9');
+}
+
+bool
+Differentiator::isSymOut(const std::string& name)
+{
+  // string::starts_with requires C++20
+  return (name[0] == 'o' && name[1] == 'u' && name[2] == 't' && name[3] == '!'
+          && '0' <= name[name.size() - 1] && name[name.size() - 1] <= '9');
+}
+
+Differentiator::Differentiator(std::unique_ptr<TimingSolver>* s,
+                               time::Span& t, ArrayCache& ac)
+: envs{{0, ""}}, prog{InputProgram}, solver{s}, solverTimeout{t},
+  arrayCache{ac}, visitorA{'a', ac}, visitorB{'b', ac}
+{}
+
+void
+Differentiator::extract(ExecutionState* a, ExecutionState* b,
+                        const std::vector<const Array*>& objects,
+                        const std::vector<Bytes>& values)
+{
+  TestArgs argv;
+  TestOuts outputs;
+  {
+    std::map<std::uint8_t, Bytes> 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->envs) {
+    auto& envs = rev.second;
+    pid_t pid;
+    std::vector<const char*> argp {this->prog.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->prog.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->tests[argv] = outputs;
+
+  // :var :val cluster
+  std::map<std::string, std::map<Bytes, 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->done.emplace(std::make_pair(i, j), &this->tests[argv]);
+      }
+}
+
+void
+Differentiator::search(ExecutionState* latest)
+{
+  if (!this->exits[latest->patchNo].insert(latest).second)
+    return; // skip when seen before
+  for (const auto& rev : this->exits) {
+    if (rev.first == latest->patchNo)
+      continue;
+    if (rev.first < latest->patchNo) {
+      if (this->done.find(std::make_pair(rev.first, latest->patchNo))
+          != this->done.end())
+        continue;
+    } else {
+      if (this->done.find(std::make_pair(latest->patchNo, rev.first))
+          != this->done.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;
+      ref<Expr> distinction;
+      for (const auto& sym : state->symbolics) {
+        if (isSymArg(sym.second->name)) {
+          objects.push_back(sym.second);
+          continue;
+        }
+        if (!isSymOut(sym.second->name))
+          continue;
+        unsigned char i = sym.second->name.size() - 1;
+        while (sym.second->name[i] != '!' && sym.second->name[i] != '_')
+          --i;
+        const auto& name = sym.second->name[i] == '_'
+                         ? sym.second->name.substr(0, i) : sym.second->name;
+        objects.push_back(arrayCache.CreateArray(name + "!a",
+                                                 sym.second->size));
+        objects.push_back(arrayCache.CreateArray(name + "!b",
+                                                 sym.second->size));
+
+        // FIXME: impossible to use visitor hash
+        for (const auto& a : this->visitorA.outVars[name]) {
+          const auto ne = NotExpr::create(EqExpr::create(a.second,
+            this->visitorB.outVars[name][a.first]));
+          if (distinction.get() == nullptr)
+            distinction = ne;
+          else
+            distinction = OrExpr::create(ne, distinction);
+        }
+      }
+
+      if (distinction.get() == nullptr)
+        continue; // no common symbolic
+      cmbnSet.push_back(distinction);
+      std::vector<Bytes> values;
+      std::unique_ptr<TimingSolver>& solver = *this->solver; // do judge!
+      solver->setTimeout(solverTimeout);
+      bool success = solver->getInitialValues(cmbnSet, objects, values,
+                                              state->queryMetaData);
+      solver->setTimeout(time::Span());
+      if (!success)
+        continue;
+      this->extract(latest, state, objects, values);
+      assert(!this->tests.empty());
+      break; // one diff test per termination for now
+    }
+  }
+}
+
+void
+Differentiator::log()
+{
+  for (const auto& t : this->tests) {
+    std::map<Bytes, std::set<std::uint64_t>> stdoutClusters;
+    std::map<std::pair<std::string, Bytes>,
+             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);
+      if (stdoutClusters.size() > 1) {
+        llvm::errs() << "Args:";
+        for (const auto& s : t.first) {
+          llvm::errs() << ' ';
+          for (const auto c : s)
+            llvm::errs() << (int) c << '.';
+        }
+        llvm::errs() << '\n';
+        for (const auto& so : stdoutClusters) {
+          llvm::errs() << "Revisions:";
+          for (const auto& r : so.second)
+            llvm::errs() << ' ' << r;
+          llvm::errs() << '\n' << std::string((const char*) so.first.data());
+        }
+        llvm::errs() << '\n';
+      }
+    }
+  }
+}
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h
new file mode 100644
index 00000000..1927f8d7
--- /dev/null
+++ b/lib/Core/Differentiator.h
@@ -0,0 +1,84 @@
+// Metaprogram's revision differentiator structure
+// Copyright 2023  Nguyễn Gia Phong
+//
+// This file is distributed under the University of Illinois
+// Open Source License.  See LICENSE.TXT for details.
+
+#ifndef KLEE_DIFFERENTIATOR_H
+#define KLEE_DIFFERENTIATOR_H
+
+#include "ExecutionState.h"
+
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprVisitor.h"
+#include "klee/System/Time.h"
+
+#include <cstdint>
+#include <map>
+#include <set>
+#include <string>
+
+namespace klee {
+
+struct ExprCmbnVisitor : ExprVisitor {
+  ExprCmbnVisitor(char, ArrayCache&);
+  Action visitExprPost(const Expr& e) override;
+
+  /// Recorded output variables
+  std::map<std::string, std::map<ref<Expr>, ref<ReadExpr>>> outVars;
+private:
+  char revision;
+  ArrayCache& arrayCache;
+};
+
+struct Differentiator {
+  /// Buffer of bytes
+  typedef std::vector<unsigned char> Bytes;
+  /// CLI arguments
+  typedef std::vector<Bytes> TestArgs;
+  /// :rev (:var val) stdout
+  typedef std::map<std::uint64_t, std::pair<std::map<std::string, Bytes>,
+                                            Bytes>> TestOuts;
+
+  /// Return if name matches arg\d\d
+  static bool isSymArg(const std::string&);
+  /// Return if name matches out!.*\d
+  static bool isSymOut(const std::string&);
+
+  Differentiator(std::unique_ptr<TimingSolver>*, time::Span&, ArrayCache&);
+  /// Extract differential test from concrete execution
+  void extract(ExecutionState*, ExecutionState*,
+               const std::vector<const Array*>&,
+               const std::vector<Bytes>&);
+  /// Compare with other exit states for possible differential tests
+  void search(ExecutionState*);
+  /// Log patch differentiation result
+  void log();
+
+  /// Environment variables corresponding to each revision
+  std::map<std::uint64_t, std::string> envs;
+private:
+  /// Program path for concrete execution.
+  std::string prog;
+  /// Exit states
+  std::map<std::uint64_t,
+           std::set<ExecutionState*,
+                    ExecutionStatePathCondCompare>> exits;
+  /// Differential tests
+  std::map<TestArgs, TestOuts> tests;
+  /// SMT solver "borrowed" from Executor
+  std::unique_ptr<TimingSolver>* solver;
+  /// SMT solving timeout
+  time::Span solverTimeout;
+  /// Symbolic memory array
+  ArrayCache& arrayCache;
+  /// Symbolic output renamers
+  ExprCmbnVisitor visitorA, visitorB;
+  /// Differentiated pairs
+  std::map<std::pair<std::uint64_t, std::uint64_t>, TestOuts*> done;
+};
+
+} // namespace klee
+
+#endif // KLEE_DIFFERENTIATOR_H
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
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 870e5801..eae3a5b2 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -16,6 +16,7 @@
 #define KLEE_EXECUTOR_H
 
 #include "ExecutionState.h"
+#include "Differentiator.h"
 #include "UserSearcher.h"
 
 #include "klee/ADT/RNG.h"
@@ -24,7 +25,6 @@
 #include "klee/Core/TerminationTypes.h"
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/ArrayExprOptimizer.h"
-#include "klee/Expr/ExprVisitor.h"
 #include "klee/Module/Cell.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
@@ -33,9 +33,6 @@
 #include "llvm/ADT/Twine.h"
 #include "llvm/Support/raw_ostream.h"
 
-#include <z3.h>
-#include <z3++.h>
-
 #include <map>
 #include <memory>
 #include <set>
@@ -68,7 +65,6 @@ namespace klee {
   class ExecutionTree;
   class ExternalDispatcher;
   class Expr;
-  class ExprVisitor;
   class InstructionInfoTable;
   class KCallable;
   struct KFunction;
@@ -93,14 +89,6 @@ namespace klee {
   /// during an instruction step. Should contain addedStates,
   /// removedStates, and haltExecution, among others.
 
-struct ExprCmbnVisitor : ExprVisitor {
-  char revision;
-  ArrayCache& arrayCache;
-  std::map<std::string, std::map<ref<Expr>, ref<ReadExpr>>> outVars;
-  ExprCmbnVisitor(char rev, ArrayCache& ac) : revision(rev), arrayCache(ac) {}
-  Action visitExprPost(const Expr& e) override;
-};
-
 class Executor : public Interpreter {
   friend class OwningSearcher;
   friend class WeightedRandomSearcher;
@@ -117,12 +105,6 @@ public:
   RNG theRNG;
 
 private:
-  typedef std::vector<unsigned char> TestVal;
-  typedef std::vector<TestVal> TestArgs;
-  /// :rev (:var val) stdout
-  typedef std::map<std::uint64_t, std::pair<std::map<std::string, TestVal>,
-                                            TestVal>> TestOuts;
-
   std::unique_ptr<KModule> kmodule;
   InterpreterHandler *interpreterHandler;
   Searcher *searcher;
@@ -131,13 +113,6 @@ private:
   std::unique_ptr<TimingSolver> solver;
   std::unique_ptr<MemoryManager> memory;
   std::set<ExecutionState*, ExecutionStateIDCompare> states;
-  std::map<std::uint64_t,
-           std::set<ExecutionState*,
-                    ExecutionStatePathCondCompare>> exitStates;
-  std::map<std::uint64_t, std::string> metaEnvVars;
-  std::map<TestArgs, TestOuts> diffTests;
-  std::map<std::pair<std::uint64_t, std::uint64_t>, TestOuts*> decided;
-  std::map<std::pair<std::size_t, std::size_t>, bool> compared;
   StatsTracker *statsTracker;
   TreeStreamWriter *pathWriter, *symPathWriter;
   SpecialFunctionHandler *specialFunctionHandler;
@@ -192,9 +167,6 @@ 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;  
@@ -224,6 +196,9 @@ private:
   /// Assumes ownership of the created array objects
   ArrayCache arrayCache;
 
+  /// Metaprogram's revision differentiator
+  Differentiator differ;
+
   /// File to print executed instructions to
   std::unique_ptr<llvm::raw_ostream> debugInstFile;
 
@@ -243,9 +218,6 @@ private:
   /// Typeids used during exception handling
   std::vector<ref<Expr>> eh_typeids;
 
-  /// Symbolic output renamers
-  ExprCmbnVisitor visitorA, visitorB;
-
   /// Return the typeid corresponding to a certain `type_info`
   ref<ConstantExpr> getEhTypeidFor(ref<Expr> type_info);
 
@@ -458,13 +430,6 @@ private:
   const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state,
       llvm::Instruction** lastInstruction);
 
-  /// Extract differencial test from concrete execution
-  void extractDifferentiator(ExecutionState*, ExecutionState*,
-                             std::vector<const Array*>, std::vector<TestVal>);
-
-  /// Compare with other exit states for possible differencial tests
-  void searchDifferentiators(ExecutionState *state);
-
   /// Remove state from queue and delete state. This function should only be
   /// used in the termination functions below.
   void terminateState(ExecutionState &state, StateTerminationType reason);
@@ -585,10 +550,6 @@ 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;
 
@@ -635,12 +596,6 @@ public:
   MergingSearcher *getMergingSearcher() const { return mergingSearcher; };
   void setMergingSearcher(MergingSearcher *ms) { mergingSearcher = ms; };
 };
-
-/// Return if name matches arg\d\d
-bool isSymArg(std::string);
-
-/// Return if name matches out!.*\d
-bool isSymOut(std::string);
 } // namespace klee
 
 #endif /* KLEE_EXECUTOR_H */
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index df13d2fd..09f58fd3 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -274,33 +274,4 @@ namespace klee {
     llvm_unreachable("Unsupported expression in evalConstantExpr");
     return op1;
   }
-
-  ExprVisitor::Action ExprCmbnVisitor::visitExprPost(const Expr& e) {
-    if (e.getKind() != Expr::Read)
-      return ExprVisitor::Action::doChildren();
-    const auto load = dyn_cast<ReadExpr>(&e);
-    const auto orig = load->updates.root;
-    if (!isSymOut(orig->name))
-      return ExprVisitor::Action::doChildren();
-    const auto a = this->arrayCache.CreateArray(
-      orig->name + '!' + this->revision,
-      orig->size, 0, 0, orig->domain, orig->range);
-    const auto replacement = ReadExpr::create({a, load->updates.head},
-                                              load->index);
-    this->outVars[orig->name][load->index] = dyn_cast<ReadExpr>(replacement.get());
-    return ExprVisitor::Action::changeTo(replacement);
-  }
-
-  bool isSymArg(std::string name) {
-    return (name.size() == 5 // string::starts_with requires C++20
-            && name[0] == 'a' && name[1] == 'r' && name[2] == 'g'
-            && '0' <= name[3] && name[3] <= '9'
-            && '0' <= name[4] && name[4] <= '9');
-  }
-
-  bool isSymOut(std::string name) {
-    // string::starts_with requires C++20
-    return (name[0] == 'o' && name[1] == 'u' && name[2] == 't' && name[3] == '!'
-            && '0' <= name[name.size() - 1] && name[name.size() - 1] <= '9');
-  }
 }
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 8484a8a7..f80f6b65 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -854,5 +854,5 @@ void SpecialFunctionHandler::handleMarkPatch(ExecutionState &state,
     executor.terminateStateEarly(state, "ignore patch combination",
                                  StateTerminationType::SilentExit);
   else
-    executor.metaEnvVars[state.patchNo = patchNo] = state.metaEnvVar;
+    executor.differ.envs[state.patchNo = patchNo] = state.metaEnvVar;
 }
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 61455ef6..a1fd5b4a 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -68,9 +68,6 @@ namespace {
   cl::opt<std::string>
   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,
             cl::desc("<program arguments>..."));
@@ -1422,7 +1419,6 @@ int main(int argc, char **argv, char **envp) {
   if (!ReplayPathFile.empty()) {
     KleeHandler::loadPathFile(ReplayPathFile, replayPath);
   }
-  interpreter->setProgram(InputProgram);
 
   auto startTime = std::time(nullptr);
   { // output clock info and start time