Half-bake decision clustering

7 files changed, 77 insertions, 145 deletions

diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 534753eb..021c3ce7 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -12,7 +12,6 @@ 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
deleted file mode 100644
index c68ec6d1..00000000
--- a/lib/Core/Differentiator.cpp
+++ /dev/null
@@ -1,70 +0,0 @@
-//===-- Differentiator.cpp ------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "Differentiator.h"
-
-#include <iomanip>
-#include <sstream>
-
-using namespace klee;
-
-namespace klee {
-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');
-}
-
-std::string quoted(const std::string& 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 writeHex(llvm::raw_ostream& os, std::string s) {
-    for (const auto c : s)
-        os << "\\x" << hex(c >> 4) << hex(c & 0xf);
-}
-
-llvm::raw_ostream &operator<<(llvm::raw_ostream& os, const Differentiator& d) {
-  os << "{(";
-  uint8_t last = 0;
-  for (const auto& p : d.args) {
-    assert(p.first == last);
-    if (last)
-      os << " ";
-    os << quoted(p.second);
-    last++;
-  }
-  os << ") {";
-  last = 0;
-  for (const auto& p : d.outputs) {
-    os << (last ? " :" : ":") << p.first << " {"; os << d.revA << " ";
-    writeHex(os, p.second.first);
-    os << " " << d.revB << " ";
-    writeHex(os, p.second.second);
-    os << "}";
-    last++;
-  }
-  os << "}}";
-
-  return os;
-}
-}
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h
deleted file mode 100644
index 1f9c7766..00000000
--- a/lib/Core/Differentiator.h
+++ /dev/null
@@ -1,47 +0,0 @@
-//===-- Differentiator.h ----------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// Class to perform actual execution, hides implementation details from external
-// interpreter.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_DIFFERENTIATOR_H
-#define KLEE_DIFFERENTIATOR_H
-
-#include "llvm/Support/raw_ostream.h"
-
-#include <cstdint>
-#include <map>
-#include <string>
-
-namespace klee {
-
-/// Return if name matches arg\d\d
-bool isSymArg(std::string);
-
-/// Return if name matches out!.*\d
-bool isSymOut(std::string);
-
-struct Differentiator {
-  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;
-  // 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
-llvm::raw_ostream &operator<<(llvm::raw_ostream&, const Differentiator&);
-} // End klee namespace
-
-#endif /* KLEE_DIFFERENTIATOR_H */
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1906427e..b21ee913 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3605,8 +3605,34 @@ void Executor::doDumpStates() {
     terminateStateEarly(*state, "Execution halting.", StateTerminationType::Interrupted);
   updateStates(nullptr);
 
-  for (const auto& t : this->diffTests)
-    llvm::errs() << t << '\n';
+  std::set<uint64_t> revs;
+  for (const auto& p : this->metaEnvVars)
+    revs.insert(p.first);
+  for (const auto& t : this->diffTests) {
+    std::map<std::string, std::set<std::uint64_t>> stdoutClusters;
+    std::map<std::pair<std::string, std::string>,
+             std::set<std::uint64_t>> varClusters;
+    if (t.second.size() < this->metaEnvVars.size())
+      continue;
+    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() << " \"" << s << '"';
+        llvm::errs() << '\n';
+        int i = 0;
+        for (const auto& so : stdoutClusters) {
+          llvm::errs() << i++ << " " << so.first;
+          for (const auto& r : so.second)
+            llvm::errs() << " " << r;
+          llvm::errs() << '\n';
+        }
+      }
+    }
+  }
 }
 
 void Executor::run(ExecutionState &initialState) {
@@ -3810,17 +3836,18 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {
 
 void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
                                      const z3::model& m) {
-  auto test = Differentiator {a->patchNo, b->patchNo};
+  std::map<std::uint8_t, std::string> args;
+  Executor::TestOuts outputs;
   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] = "";
+      args[i] = "";
       const auto& expr = m.eval(m[k]());
       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);
+        args[i].push_back((unsigned char) c);
       }
     } else if (isSymOut(name.substr(0, name.size() - 2))) {
       // TODO: use arguments for all patches
@@ -3831,28 +3858,27 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
         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);
-        if (name[name.size() - 1] == 'a')
-          test.outputs[ident].first = binary;
-        else
-          test.outputs[ident].second = binary;
       }
+      const auto rev = ((name[name.size() - 1] == 'a') ? a : b)->patchNo;
+      outputs[rev].first[name.substr(4, name.size() - 6)] = binary;
     }
   }
-  llvm::errs() << test << '\n';
+  Executor::TestArgs argv;
+  uint8_t last = 0;
+  for (const auto& p : args) {
+    assert(p.first == last);
+    argv.push_back(p.second);
+    last++;
+  }
 
   char buffer[128];
-  for (auto& rev : this->metaEnvVars) {
+  for (const 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);
+    std::vector<const char*> argp {this->concreteProgram.c_str()};
+    for (const auto& s : argv)
+      argp.push_back(s.c_str());
+    argp.push_back(NULL);
 
     int fildes[2];
     auto err = pipe(fildes);
@@ -3863,7 +3889,7 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
     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()),
+                      const_cast<char* const *>(argp.data()),
                       envs.empty() ? NULL : envp);
     assert(!err);
     close(fildes[1]);
@@ -3873,11 +3899,10 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
       buffer[n] = 0;
       out += buffer;
     }
-    test.stdouts[rev.first] = out;
-    llvm::errs() << "rev " << rev.first << ' ' << out;
+    outputs[rev.first].second = out;
     posix_spawn_file_actions_destroy(&action);
   }
-  this->diffTests.push_back(test);
+  this->diffTests[argv] = outputs;
 }
 
 std::string hash(std::string data) {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 3b10fa27..4928a5ab 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -15,7 +15,6 @@
 #ifndef KLEE_EXECUTOR_H
 #define KLEE_EXECUTOR_H
 
-#include "Differentiator.h"
 #include "ExecutionState.h"
 #include "UserSearcher.h"
 
@@ -108,6 +107,12 @@ public:
   RNG theRNG;
 
 private:
+  typedef std::vector<std::string> TestArgs;
+  /// :rev (:var val) stdout
+  typedef std::map<std::uint64_t,
+                   std::pair<std::map<std::string, std::string>,
+                             std::string>> TestOuts;
+
   std::unique_ptr<KModule> kmodule;
   InterpreterHandler *interpreterHandler;
   Searcher *searcher;
@@ -118,7 +123,7 @@ private:
   std::set<ExecutionState*, ExecutionStateIDCompare> states;
   std::set<ExecutionState*, ExecutionStateIDCompare> exitStates;
   std::map<std::uint64_t, std::string> metaEnvVars;
-  std::vector<Differentiator> diffTests;
+  std::map<TestArgs, TestOuts> diffTests;
   StatsTracker *statsTracker;
   TreeStreamWriter *pathWriter, *symPathWriter;
   SpecialFunctionHandler *specialFunctionHandler;
@@ -610,6 +615,11 @@ public:
   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 09f58fd3..2c2c0018 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -274,4 +274,17 @@ namespace klee {
     llvm_unreachable("Unsupported expression in evalConstantExpr");
     return op1;
   }
+
+  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/shell.nix b/shell.nix
index 9d361a5f..570f39bd 100644
--- a/shell.nix
+++ b/shell.nix
@@ -3,6 +3,8 @@ let symbdiff = callPackage ./tools/symbdiff { };
 in mkShell {
   packages = [ clang symbdiff ];
   shellHook = ''
-    alias klang='clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone'
+    # clang -emit-llvm -c -DKLEE_RUNTIME metaprogram.c for bitcode
+    # clang -o metaprogram{,.c} for binary
+    alias clang='clang -g -O0 -Xclang -disable-O0-optnone'
  '';
 }