about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/Core/CMakeLists.txt1
-rw-r--r--lib/Core/Differentiator.cpp23
-rw-r--r--lib/Core/Differentiator.h8
-rw-r--r--lib/Core/Executor.cpp73
-rw-r--r--lib/Core/Executor.h16
-rw-r--r--lib/Core/ExecutorUtil.cpp13
-rw-r--r--shell.nix4
7 files changed, 83 insertions, 55 deletions
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 5f392ec9..9005a1ff 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
   Executor.cpp
   ExecutorUtil.cpp
diff --git a/lib/Core/Differentiator.cpp b/lib/Core/Differentiator.cpp
index c68ec6d1..ea713ad4 100644
--- a/lib/Core/Differentiator.cpp
+++ b/lib/Core/Differentiator.cpp
@@ -15,18 +15,6 @@
 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;
@@ -46,22 +34,19 @@ void writeHex(llvm::raw_ostream& os, std::string s) {
 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)
+  for (const auto& s : d.args) {
+    if (last++)
       os << " ";
-    os << quoted(p.second);
-    last++;
+    os << quoted(s);
   }
   os << ") {";
   last = 0;
   for (const auto& p : d.outputs) {
-    os << (last ? " :" : ":") << p.first << " {"; os << d.revA << " ";
+    os << (last++ ? " :" : ":") << p.first << " {"; os << d.revA << " ";
     writeHex(os, p.second.first);
     os << " " << d.revB << " ";
     writeHex(os, p.second.second);
     os << "}";
-    last++;
   }
   os << "}}";
 
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h
index b9aa1ba4..70e83848 100644
--- a/lib/Core/Differentiator.h
+++ b/lib/Core/Differentiator.h
@@ -23,16 +23,10 @@
 
 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;
+  std::vector<std::string> args;
   // k => (out!k!a, out!k!b)
   std::map<std::string, std::pair<std::string, std::string>> outputs;
   // rev => stdout
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 2b2fcec9..78c3d8d5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3479,8 +3479,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) {
@@ -3681,17 +3707,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
@@ -3702,28 +3729,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);
@@ -3734,7 +3760,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]);
@@ -3744,11 +3770,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 af3a3778..89819157 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"
 
@@ -109,6 +108,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;
@@ -119,7 +124,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;
@@ -602,7 +607,12 @@ 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);
 } // End klee namespace
 
 #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'
  '';
 }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-08-13 22:19:17 +0000