about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/ExecutionState.cpp24
-rw-r--r--lib/Core/ExecutionState.h3
-rw-r--r--lib/Core/Executor.cpp70
-rw-r--r--lib/Core/Executor.h7
4 files changed, 73 insertions, 31 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 4e9067fa..bb51974f 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -106,6 +106,7 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     arrayNames(state.arrayNames),
     openMergeStack(state.openMergeStack),
     patchNo(state.patchNo),
+    metaEnvVar(state.metaEnvVar),
     formula(state.formula),
     steppedInstructions(state.steppedInstructions),
     instsSinceCovNew(state.instsSinceCovNew),
@@ -374,35 +375,38 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
   }
 }
 
-bool isMetaConstraint(ref<Expr> e) {
+std::string extractMetaEnvVar(ref<Expr> e) {
   if (e.get()->getKind() != Expr::Eq)
-    return false;
+    return "";
   const auto eq = dyn_cast<EqExpr>(e.get());
   if (eq->left.get()->getKind() != Expr::Constant)
-    return false;
+    return "";
   const auto constant = dyn_cast<ConstantExpr>(eq->left.get());
   if (constant->isFalse()) // the else branch
-    return isMetaConstraint(eq->right);
+    return extractMetaEnvVar(eq->right);
 
   if (eq->right.get()->getKind() != Expr::Concat)
-    return false;
+    return "";
   const auto concat = dyn_cast<ConcatExpr>(eq->right.get());
   if (concat->getLeft().get()->getKind() != Expr::Read)
-    return false;
+    return "";
 
   const auto read = dyn_cast<ReadExpr>(concat->getLeft().get());
   const auto& name = read->updates.root->name;
   // string::starts_with requires C++20
   if (name.substr(0, 8) != "__choose")
-    return false;
+    return "";
   for (const auto c : name.substr(8))
     if ('0' > c || c > '9')
-      return false;
-  return true;
+      return "";
+  std::string value;
+  constant->toString(value);
+  return "__SWITCH" + name.substr(8, name.size() - 8) + "=" + value;
 }
 
 void ExecutionState::addConstraint(ref<Expr> e) {
-  if (isMetaConstraint(e))
+  this->metaEnvVar = extractMetaEnvVar(e);
+  if (!this->metaEnvVar.empty())
     return;
   ConstraintManager c(constraints);
   c.addConstraint(e);
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 2ae22284..25cf5ee2 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -229,6 +229,9 @@ 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 Terminated on exit, awaiting comparison.
   std::string formula = "";
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f28a363c..d8d0d0b3 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -89,6 +89,7 @@ typedef unsigned TypeSize;
 #include <iomanip>
 #include <iosfwd>
 #include <limits>
+#include <spawn.h>
 #include <sstream>
 #include <stdlib.h>
 #include <string>
@@ -3708,39 +3709,44 @@ void Executor::extractDifferentiator(uint64_t a, uint64_t b, const z3::model& m)
   this->diffTests.push_back(test);
 }
 
+std::string hash(std::string data) {
+  std::stringstream stream;
+  stream << std::hex << std::setw(16) << std::setfill('0')
+         << std::hash<std::string>{}(data);
+  return stream.str();
+}
+
 void Executor::searchDifferentiators(ExecutionState* latest) {
-  std::string last_smt2_name = "smt2.XXXXXX";
-  auto last_smt2_fd = mkstemp(last_smt2_name.data());
-  assert(last_smt2_fd != -1);
-  const auto written = write(last_smt2_fd, latest->formula.c_str(),
-                             latest->formula.size());
-  assert(written == latest->formula.size());
-  close(last_smt2_fd);
+  auto last_smt2_name = hash(latest->formula) + ".smt2";
+  std::ofstream last_smt2_file;
+  last_smt2_file.open(last_smt2_name);
+  last_smt2_file << latest->formula;
+  last_smt2_file.close();
   for (const auto& state : this->exitStates) {
     // TODO: skip moar and order
     if (state->patchNo == latest->patchNo)
       continue;
+    auto smt2_name = hash(state->formula) + ".smt2";
+    if (smt2_name == last_smt2_name)
+      continue;
 
     // File I/O is expensive but SMT solving is even more expensive (-;
     // Seriously though, FIXME: implement symbdiff natively
-    std::string smt2_name = "smt2.XXXXXX";
-    auto smt2_fd = mkstemp(smt2_name.data());
-    assert(smt2_fd != -1);
-    const auto written = write(smt2_fd, state->formula.c_str(),
-                               state->formula.size());
-    assert(written == state->formula.size());
-    close(smt2_fd);
+    std::ofstream smt2_file;
+    smt2_file.open(smt2_name);
+    smt2_file << state->formula;
+    smt2_file.close();
 
     auto command = "symbdiff " + smt2_name + " " + last_smt2_name;
     for (const auto& out : this->symOuts)
       command += " " + std::to_string(out.second);
-    const auto pipe = popen(command.c_str(), "r");
+    const auto out = popen(command.c_str(), "r");
     std::string formula;
     char buffer[128];
-    while (!feof(pipe))
-      if (fgets(buffer, 128, pipe) != NULL)
+    while (!feof(out))
+      if (fgets(buffer, 128, out) != NULL)
         formula += buffer;
-    assert(pclose(pipe) == 0);
+    assert(pclose(out) == 0);
     remove(smt2_name.c_str());
 
     static z3::context c;
@@ -3750,7 +3756,30 @@ void Executor::searchDifferentiators(ExecutionState* latest) {
     if (s.check() != z3::sat)
       continue;
     this->extractDifferentiator(latest->patchNo, state->patchNo, s.get_model());
-    llvm::errs() << this->diffTests.back() << "\n";
+    assert(!this->diffTests.empty());
+
+    pid_t pid;
+    std::vector<const char*> args {this->concreteProgram.c_str()};
+    uint8_t last = 0;
+    for (const auto& p : this->diffTests.back().args) {
+      assert(p.first == last);
+      args.push_back(p.second.c_str());
+      last++;
+    }
+    int fildes[2];
+    auto err = pipe(fildes);
+    if (err)
+      llvm::errs() << "failed creating pipe\n";
+    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>(latest->metaEnvVar.c_str()),
+                          NULL};
+    auto status = posix_spawn(&pid, this->concreteProgram.c_str(),
+                              &action, NULL,
+                              const_cast<char* const *>(args.data()), envp);
+    break;
   }
   remove(last_smt2_name.c_str());
 }
@@ -3764,8 +3793,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
 
   interpreterHandler->incPathsCompleted();
   getConstraintLog(state, state.formula, Interpreter::SMTLIB2);
-  if (state.patchNo)
-    searchDifferentiators(&state);
+  searchDifferentiators(&state);
   exitStates.insert(&state);
   terminateState(state);
 }
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 8f2850fd..59f41ea7 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -173,6 +173,9 @@ 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;  
@@ -547,6 +550,10 @@ 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;
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-08-15 14:46:12 +0000