Implement native path condition combination

3 files changed, 66 insertions, 32 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e0ab9f84..e5a6bc9c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -488,7 +488,8 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)},
       replayKTest(0), replayPath(0), usingSeeds(0),
       atMemoryLimit(false), inhibitForking(false), haltExecution(false),
-      ivcEnabled(false), debugLogBuffer(debugBufferString) {
+      ivcEnabled(false), debugLogBuffer(debugBufferString),
+      visitorA{'a', arrayCache}, visitorB{'b', arrayCache} {
 
 
   const time::Span maxTime{MaxTime};
@@ -3953,6 +3954,13 @@ void Executor::searchDifferentiators(ExecutionState* latest) {
         continue;
     }
     for (const auto& state : rev.second) {
+      // TODO: implement symbdiff natively
+      std::set<ref<Expr>> combination;
+      for (auto const& constraint : state->constraints)
+        combination.insert(this->visitorA.visit(constraint));
+      for (auto const& constraint : latest->constraints)
+        combination.insert(this->visitorB.visit(constraint));
+
       auto hashPair = std::make_pair(hashFn(state->formula),
                                      hashFn(latest->formula));
       if (hashPair.first == hashPair.second || this->compared[hashPair])
@@ -3964,7 +3972,6 @@ void Executor::searchDifferentiators(ExecutionState* latest) {
       this->compared[hashPair] = true;
 
       // File I/O is expensive but SMT solving is even more expensive (-;
-      // Seriously though, FIXME: implement symbdiff natively
       const auto& smt2_name = hash(state->formula) + ".smt2";
       std::ofstream smt2_file;
       smt2_file.open(smt2_name);
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index bb65b9ad..fcb8fd80 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -24,6 +24,7 @@
 #include "klee/Core/TerminationTypes.h"
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/ArrayExprOptimizer.h"
+#include "klee/Expr/ExprVisitor.h"
 #include "klee/Module/Cell.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
@@ -60,36 +61,44 @@ namespace llvm {
   class Value;
 }
 
-namespace klee {
-class Array;
-struct Cell;
-class ExecutionState;
-class ExternalDispatcher;
-class Expr;
-class InstructionInfoTable;
-class KCallable;
-struct KFunction;
-struct KInstruction;
-class KInstIterator;
-class KModule;
-class MemoryManager;
-class MemoryObject;
-class ObjectState;
-class ExecutionTree;
-class Searcher;
-class SeedInfo;
-class SpecialFunctionHandler;
-struct StackFrame;
-class StatsTracker;
-class TimingSolver;
-class TreeStreamWriter;
-class MergeHandler;
-class MergingSearcher;
-template <class T> class ref;
-
-/// \todo Add a context object to keep track of data only live
-/// during an instruction step. Should contain addedStates,
-/// removedStates, and haltExecution, among others.
+namespace klee {  
+  class Array;
+  struct Cell;
+  class ExecutionState;
+  class ExecutionTree;
+  class ExternalDispatcher;
+  class Expr;
+  class ExprVisitor;
+  class InstructionInfoTable;
+  class KCallable;
+  struct KFunction;
+  struct KInstruction;
+  class KInstIterator;
+  class KModule;
+  class MemoryManager;
+  class MemoryObject;
+  class ObjectState;
+  class Searcher;
+  class SeedInfo;
+  class SpecialFunctionHandler;
+  struct StackFrame;
+  class StatsTracker;
+  class TimingSolver;
+  class TreeStreamWriter;
+  class MergeHandler;
+  class MergingSearcher;
+  template<class T> class ref;
+
+  /// \todo Add a context object to keep track of data only live
+  /// during an instruction step. Should contain addedStates,
+  /// removedStates, and haltExecution, among others.
+
+struct ExprCmbnVisitor : ExprVisitor {
+  char revision;
+  ArrayCache& arrayCache;
+  ExprCmbnVisitor(char rev, ArrayCache& ac) : revision(rev), arrayCache(ac) {}
+  Action visitExprPost(const Expr& e) override;
+};
 
 class Executor : public Interpreter {
   friend class OwningSearcher;
@@ -233,6 +242,9 @@ private:
   /// Typeids used during exception handling
   std::vector<ref<Expr>> eh_typeids;
 
+  /// Symbolic output renamers
+  ExprCmbnVisitor visitorA, visitorB;
+
   /// Return the typeid corresponding to a certain `type_info`
   ref<ConstantExpr> getEhTypeidFor(ref<Expr> type_info);
 
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 2c2c0018..af4f7b88 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -275,6 +275,21 @@ namespace klee {
     return op1;
   }
 
+  ExprVisitor::Action ExprCmbnVisitor::visitExprPost(const Expr& e) {
+    if (e.getKind() != Expr::Read)
+      return ExprVisitor::Action::doChildren();
+    const auto load = dyn_cast<ReadExpr>(&e);
+
+    const auto orig = load->updates.root;
+    if (orig->name.substr(0, 4) != "out!")
+      return ExprVisitor::Action::doChildren();
+    const auto a = this->arrayCache.CreateArray(
+      orig->name + '!' + this->revision,
+      orig->size, 0, 0, orig->domain, orig->range);
+    return ExprVisitor::Action::changeTo(
+      ReadExpr::create({a, load->updates.head}, load->index));
+  }
+
   bool isSymArg(std::string name) {
     return (name.size() == 5 // string::starts_with requires C++20
             && name[0] == 'a' && name[1] == 'r' && name[2] == 'g'