From 09485583beee941f271aa0a4e5ed3765dd41aa5c Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <cnx@loang.net>
Date: Mon, 20 Nov 2023 00:26:03 +0900
Subject: Revert orphaned changes

---
 lib/Core/Executor.cpp | 10 ----------
 lib/Core/Executor.h   |  6 ------
 tools/klee/main.cpp   |  1 +
 3 files changed, 1 insertion(+), 16 deletions(-)

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 22e4ac92..4dd486b6 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -93,11 +93,9 @@
 #include <iosfwd>
 #include <limits>
 #include <sstream>
-#include <stdlib.h>
 #include <string>
 #include <sys/mman.h>
 #include <sys/resource.h>
-#include <unistd.h>
 #include <vector>
 
 using namespace llvm;
@@ -4695,14 +4693,6 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     bindObjectInState(state, mo, false, array);
     state.addSymbolic(mo, array);
 
-    if (Differentiator::isSymArg(uniqueName)) {
-      assert(std::atoi(name.c_str() + 3) == this->symArgs.size());
-      this->symArgs.push_back(mo->size - 1); // string's null termination
-    } else if (Differentiator::isSymOut(uniqueName)) {
-      // assert(this->symOuts.find(uniqueName) == this->symOuts.end());
-      this->symOuts[uniqueName] = mo->size;
-    }
-
     auto found = seedMap.find(&state);
     if (found != seedMap.end()) {
       // In seed mode we need to add this as binding
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index eae3a5b2..50446145 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -146,12 +146,6 @@ private:
   /// globals that have no representative object (e.g. aliases).
   std::map<const llvm::GlobalValue*, ref<ConstantExpr>> globalAddresses;
 
-  /// Size of symbolic arguments.
-  std::vector<size_t> symArgs;
-
-  /// Size of symbolic outputs.
-  std::map<std::string, size_t> symOuts;
-
   /// Map of legal function addresses to the corresponding Function.
   /// Used to validate and dereference function pointers.
   std::unordered_map<std::uint64_t, llvm::Function*> legalFunctions;
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index a1fd5b4a..56c932e8 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1418,6 +1418,7 @@ int main(int argc, char **argv, char **envp) {
   std::vector<bool> replayPath;
   if (!ReplayPathFile.empty()) {
     KleeHandler::loadPathFile(ReplayPathFile, replayPath);
+    interpreter->setReplayPath(&replayPath);
   }
 
   auto startTime = std::time(nullptr);
-- 
cgit 1.4.1