about summary refs log tree commit diff homepage
path: root/lib/Core/Differentiator.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/Differentiator.cpp')
-rw-r--r--lib/Core/Differentiator.cpp183
1 files changed, 127 insertions, 56 deletions
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-06-02 21:53:01 +0000