Clean up interfaces

Psychic now extract patch number directly from meta conditions.
Previously it was under the assumption that a patch is triggered
by multiple choices.  Now we allow a patch to have multiple hunks
and the possibility to combine multiple patches.

Internally, the code relevant diff test generation
is moved under Differentiator.

8 files changed, 147 insertions, 138 deletions

diff --git a/include/klee/klee.h b/include/klee/klee.h
index 04cb75c8..07528595 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -118,7 +118,6 @@ extern "C" {
   void klee_prefer_cex(void *object, uintptr_t condition);
   void klee_posix_prefer_cex(void *object, uintptr_t condition);
   void klee_mark_global(void *object);
-  void klee_mark_patch(uint64_t patch_number);
 
   /* Return a possible constant value for the input expression. This
      allows programs to forcibly concretize values on their own. */
diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp
index 20aa69c9..2609e832 100644
--- a/lib/Core/Differentiator.cpp
+++ b/lib/Core/Differentiator.cpp
@@ -11,12 +11,74 @@
 
 #include <spawn.h>
 
+#include <algorithm>
+#include <iostream>
+#include <sstream>
+
 llvm::cl::opt<std::string>
 InputProgram{llvm::cl::desc("<input program>"),
              llvm::cl::Positional, llvm::cl::Required};
 
 using namespace klee;
 
+bool
+isSymArg(const std::string& name)
+{
+  /// Match arg\d\d
+  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(const std::string& name)
+{
+  /// Match for out!.*\d
+  return (name[0] == 'o' && name[1] == 'u' && name[2] == 't' && name[3] == '!'
+          && '0' <= name[name.size() - 1] && name[name.size() - 1] <= '9');
+}
+
+std::pair<bool, std::uint64_t>
+Differentiator::extractPatchNumber(ref<Expr> e)
+{
+  if (e.get()->getKind() == Expr::And) {
+    const auto& et = dyn_cast<AndExpr>(e.get());
+    const auto& l = extractPatchNumber(et->left);
+    const auto& r = extractPatchNumber(et->right);
+    // Optimized if ((__choose\d+) == 0) {} else if (\1 == \d+)
+    assert(!(l.first && r.first));
+    return {l.first || r.first, l.first ? l.second : r.second};
+  }
+  if (e.get()->getKind() != Expr::Eq)
+    return {false, 0u}; // expecting __choose\d+ == \d+
+  const auto eq = dyn_cast<EqExpr>(e.get());
+  // Expr is unbalanced to the right, hence scalar must be on the left.
+  if (eq->left.get()->getKind() != Expr::Constant)
+    return {false, 0u};
+  const auto constant = dyn_cast<ConstantExpr>(eq->left.get());
+  if (constant->isFalse()) // negation
+    return {false, 0u}; // could only be !(__choose.+) anyway if meta
+
+  ReadExpr* read;
+  if (eq->right.get()->getKind() == Expr::Read) {
+    read = dyn_cast<ReadExpr>(eq->right.get());
+  } else {
+    if (eq->right.get()->getKind() != Expr::Concat)
+      return {false, 0u};
+    const auto concat = dyn_cast<ConcatExpr>(eq->right.get());
+    if (concat->getLeft().get()->getKind() != Expr::Read)
+      return {false, 0u};
+    read = dyn_cast<ReadExpr>(concat->getLeft().get());
+  }
+
+  const auto& name = read->updates.root->name;
+  // Skip when it is not __choose\d.*
+  if (name.substr(0, 8) != "__choose" || '0' > name[8] || name[8] > '9')
+    return {false, 0u};
+  return {true, constant->getZExtValue()};
+}
+
 ExprCmbnVisitor::ExprCmbnVisitor(char rev, ArrayCache& ac)
 : revision(rev), arrayCache(ac)
 {}
@@ -28,7 +90,7 @@ ExprCmbnVisitor::visitExprPost(const Expr& e)
     return ExprVisitor::Action::doChildren();
   const auto load = dyn_cast<ReadExpr>(&e);
   const auto orig = load->updates.root;
-  if (!Differentiator::isSymOut(orig->name))
+  if (!isSymOut(orig->name))
     return ExprVisitor::Action::doChildren();
   const auto a = this->arrayCache.CreateArray(
     orig->name + '!' + this->revision,
@@ -39,13 +101,50 @@ ExprCmbnVisitor::visitExprPost(const Expr& e)
   return ExprVisitor::Action::changeTo(replacement);
 }
 
-bool
-Differentiator::isSymArg(const std::string& name)
+Differentiator::Differentiator(std::unique_ptr<TimingSolver>* s,
+                               time::Span& t, ArrayCache& ac)
+: revisions{{0}}, prog{InputProgram.c_str()}, solver{s}, solverTimeout{t},
+  arrayCache{ac}, visitorA{'a', ac}, visitorB{'b', ac}
+{}
+
+Differentiator::Bytes
+run(const std::uint64_t rev, const char* prog,
+    const Differentiator::TestArgs& argv)
 {
-  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');
+  int fildes[2];
+  {
+    const 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);
+  {
+    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::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);
+    assert(!err);
+  }
+  close(fildes[1]);
+
+  char buffer[128]; // output buffer for concrete execution
+  Differentiator::Bytes result;
+  for (unsigned char n; n = read(fildes[0], buffer, sizeof(buffer));) {
+    assert(n >= 0);
+    for (unsigned char i = 0; i < n; ++i)
+      result.push_back(buffer[i]);
+  }
+  posix_spawn_file_actions_destroy(&action);
+  result.push_back(0); // null termination
+  return result;
 }
 
 bool
@@ -82,56 +181,26 @@ Differentiator::extract(ExecutionState* a, ExecutionState* b,
       }
     }
     uint8_t last = 0;
-    for (const auto& p : args) {
-      assert(p.first == last);
-      argv.push_back(p.second);
+    for (const auto& [rev, arg] : args) {
+      assert(rev == last);
+      argv.push_back(arg);
       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);
-  }
+  for (const auto& rev : this->revisions)
+    outputs[rev].second = run(rev, this->prog, argv);
   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
+  std::map<std::string, Clusters> revOut;
+  for (const auto& [rev, out] : outputs) {
+    const auto& [syms, concrete] = out;
+    for (const auto& [var, val] : syms)
+      revOut[var][val].insert(rev);
+    revOut[""][concrete].insert(rev);
   }
-
-  for (auto& vp : revOut)
-    for (auto& p : vp.second)
-      for (auto& q : vp.second) {
+  for (const auto& [_, clusters] : revOut)
+    for (const auto& p : clusters)
+      for (const auto& q : clusters) {
         if (&p == &q)
           continue;
         for (std::uint64_t i : p.second)
@@ -162,11 +231,11 @@ Differentiator::search(ExecutionState* latest)
       ConstraintSet cmbnSet;
       {
         std::set<ref<Expr>> combination;
-        for (auto const& constraint : state->constraints)
+        for (const auto& constraint : state->constraints)
           combination.insert(this->visitorA.visit(constraint));
-        for (auto const& constraint : latest->constraints)
+        for (const auto& constraint : latest->constraints)
           combination.insert(this->visitorB.visit(constraint));
-        for (auto const& constraint : combination)
+        for (const auto& constraint : combination)
           cmbnSet.push_back(constraint);
       }
 
@@ -191,8 +260,10 @@ Differentiator::search(ExecutionState* latest)
 
         // 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]));
+          const auto& b = this->visitorB.outVars[name].find(a.first);
+          if (b == this->visitorB.outVars[name].end())
+            continue;
+          const auto& ne = NotExpr::create(EqExpr::create(a.second, b->second));
           if (distinction.get() == nullptr)
             distinction = ne;
           else
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h
index 1927f8d7..3743743c 100644
--- a/lib/Core/Differentiator.h
+++ b/lib/Core/Differentiator.h
@@ -41,10 +41,8 @@ struct Differentiator {
   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&);
+  /// Extract revision number from given condition if any
+  static std::pair<bool, std::uint64_t> extractPatchNumber(ref<Expr> e);
 
   Differentiator(std::unique_ptr<TimingSolver>*, time::Span&, ArrayCache&);
   /// Extract differential test from concrete execution
@@ -56,11 +54,11 @@ struct Differentiator {
   /// Log patch differentiation result
   void log();
 
-  /// Environment variables corresponding to each revision
-  std::map<std::uint64_t, std::string> envs;
+  /// Program revision numbers
+  std::set<std::uint64_t> revisions;
 private:
   /// Program path for concrete execution.
-  std::string prog;
+  const char* prog;
   /// Exit states
   std::map<std::uint64_t,
            std::set<ExecutionState*,
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 95629d7c..4bde3ae8 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -111,7 +111,6 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     openMergeStack(state.openMergeStack),
     patchLocs(state.patchLocs),
     patchNo(state.patchNo),
-    metaEnvVar(state.metaEnvVar),
     steppedInstructions(state.steppedInstructions),
     instsSinceCovNew(state.instsSinceCovNew),
     unwindingInformation(state.unwindingInformation
@@ -391,59 +390,7 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
   }
 }
 
-std::string extractMetaEnvVar(ref<Expr> e) {
-  if (e.get()->getKind() == Expr::And) {
-    const auto et = dyn_cast<AndExpr>(e.get());
-    const auto& left = extractMetaEnvVar(et->left);
-    const auto& right = extractMetaEnvVar(et->right);
-    // Optimized if ((__choose\d+) == 0) {} else if (\1 == \d+)
-    assert(left.empty() || right.empty());
-    return left.empty() ? right : left;
-  }
-  if (e.get()->getKind() != Expr::Eq)
-    return ""; // expecting __choose\d+ == \d+
-  const auto eq = dyn_cast<EqExpr>(e.get());
-  // Expr is unbalanced to the right, hence scalar must be on the left.
-  if (eq->left.get()->getKind() != Expr::Constant)
-    return "";
-  const auto constant = dyn_cast<ConstantExpr>(eq->left.get());
-  if (constant->isFalse()) // negation
-    return ""; // could only be !(__choose.+) if has __choose
-
-  ReadExpr* read;
-  if (eq->right.get()->getKind() == Expr::Read) {
-    read = dyn_cast<ReadExpr>(eq->right.get());
-  } else {
-    if (eq->right.get()->getKind() != Expr::Concat)
-      return "";
-    const auto concat = dyn_cast<ConcatExpr>(eq->right.get());
-    if (concat->getLeft().get()->getKind() != Expr::Read)
-      return "";
-    read = dyn_cast<ReadExpr>(concat->getLeft().get());
-  }
-
-  const auto& name = read->updates.root->name;
-  // Skip when it is not __choose\d.*
-  if (name.substr(0, 8) != "__choose" || '0' > name[8] || name[8] > '9')
-    return "";
-  std::string value;
-  constant->toString(value);
-  unsigned char count = 1;
-  while (count < name.size() - 8 && name[count + 8] != '_')
-    ++count;
-  return "__SWITCH" + name.substr(8, count) + "=" + value;
-}
-
 void ExecutionState::addConstraint(ref<Expr> e) {
-  auto v = extractMetaEnvVar(e);
-  if (!v.empty()) {
-    this->patchLocs++;
-    if (!this->metaEnvVar.empty())
-      return; // one revision at once
-    if (v.substr(v.size() - 2) != "=0")
-      this->metaEnvVar = v;
-    return;
-  }
   ConstraintManager c(constraints);
   c.addConstraint(e);
 }
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 0af3c336..038c62e3 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -232,9 +232,6 @@ 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 The numbers of times this state has run through Executor::stepInstruction
   std::uint64_t steppedInstructions = 0;
 
@@ -316,6 +313,7 @@ struct ExecutionStatePathCondCompare {
            j = b->constraints.begin();
          i < a->constraints.end() && j < b->constraints.end(); ++i, ++j)
       return *i < *j;
+    return false;
   }
 };
 }
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 4dd486b6..279d5f3a 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1236,6 +1236,19 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
 }
 
 void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
+  const auto& [isMeta, patchNo] = Differentiator::extractPatchNumber(condition);
+  if (isMeta) {
+    if (state.patchNo && patchNo != state.patchNo) {
+      terminateStateEarly(state, "ignore patch combination",
+                          StateTerminationType::SilentExit);
+      return;
+    }
+    state.patchLocs++;
+    if (!state.patchNo)
+      differ.revisions.insert(state.patchNo = patchNo);
+    return;
+  }
+
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(condition)) {
     if (!CE->isTrue())
       llvm::report_fatal_error("attempt to add invalid constraint");
@@ -4002,7 +4015,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
     interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix);
   }
 
-  differ.search(&state);
+  differ.search(&state); // e.g. sanitiser error
   terminateState(state, terminationType);
 
   if (shouldExitOn(terminationType))
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index f80f6b65..b0c28fbc 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -109,7 +109,6 @@ static constexpr std::array handlerInfo = {
   add("klee_is_symbolic", handleIsSymbolic, true),
   add("klee_make_symbolic", handleMakeSymbolic, false),
   add("klee_mark_global", handleMarkGlobal, false),
-  add("klee_mark_patch", handleMarkPatch, false),
   add("klee_open_merge", handleOpenMerge, false),
   add("klee_close_merge", handleCloseMerge, false),
   add("klee_prefer_cex", handlePreferCex, false),
@@ -841,18 +840,3 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
     mo->isGlobal = true;
   }
 }
-
-void SpecialFunctionHandler::handleMarkPatch(ExecutionState &state,
-                                             KInstruction *target,
-                                             std::vector<ref<Expr>> &arguments) {
-  assert(arguments.size() == 1 &&
-         "invalid number of arguments to klee_mark_patch");
-  assert(isa<ConstantExpr>(arguments[0]) &&
-         "expect constant patch number argument to klee_mark_patch");
-  auto patchNo = cast<ConstantExpr>(arguments[0])->getLimitedValue();
-  if (state.patchNo && patchNo != state.patchNo)
-    executor.terminateStateEarly(state, "ignore patch combination",
-                                 StateTerminationType::SilentExit);
-  else
-    executor.differ.envs[state.patchNo = patchNo] = state.metaEnvVar;
-}
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index be0bc7d2..3fdbf8f8 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -101,7 +101,6 @@ namespace klee {
     HANDLER(handleMalloc);
     HANDLER(handleMemalign);
     HANDLER(handleMarkGlobal);
-    HANDLER(handleMarkPatch);
     HANDLER(handleOpenMerge);
     HANDLER(handleCloseMerge);
     HANDLER(handleNew);