[fix] Fix memory consumption

`using path_ty = std::vector<KBlock *>` -> `using path_ty = ImmutableList<KBlock *>`

include/klee/ADT/ImmutableList.h

@@ -10,6 +10,7 @@
 #ifndef KLEE_IMMUTABLELIST_H
 #define KLEE_IMMUTABLELIST_H
 
+#include <cassert>
 #include <memory>
 #include <vector>
 
@@ -96,6 +97,22 @@ template <typename T> class ImmutableList {
     node->values.push_back(std::move(value));
   }
 
+  void push_back(const T &value) {
+    if (!node) {
+      node = std::make_shared<ImmutableListNode>();
+    }
+    node->values.push_back(value);
+  }
+
+  bool empty() { return size() == 0; }
+
+  const T &back() {
+    assert(node && "requiers not empty list");
+    auto it = iterator(node.get());
+    it.get = size() - 1;
+    return *it;
+  }
+
   ImmutableList() : node(){};
   ImmutableList(const ImmutableList<T> &il)
       : node(std::make_shared<ImmutableListNode>(il)) {}

include/klee/Expr/Constraints.h

@@ -12,6 +12,7 @@
 
 #include "klee/ADT/Ref.h"
 
+#include "klee/ADT/PersistentMap.h"
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprHashMap.h"
@@ -91,7 +92,7 @@ class ConstraintSet {
 class PathConstraints {
 public:
   using ordered_constraints_ty =
-      std::map<Path::PathIndex, constraints_ty, Path::PathIndexCompare>;
+      PersistentMap<Path::PathIndex, constraints_ty, Path::PathIndexCompare>;
 
   void advancePath(KInstruction *ki);
   void advancePath(const Path &path);

include/klee/Expr/Path.h

@@ -1,6 +1,8 @@
 #ifndef KLEE_PATH_H
 #define KLEE_PATH_H
 
+#include "klee/ADT/ImmutableList.h"
+
 #include <stack>
 #include <string>
 #include <vector>
@@ -16,7 +18,7 @@ using stackframe_ty = std::pair<KInstruction *, KFunction *>;
 
 class Path {
 public:
-  using path_ty = std::vector<KBlock *>;
+  using path_ty = ImmutableList<KBlock *>;
   enum class TransitionKind { StepInto, StepOut, None };
 
   struct PathIndex {
@@ -38,23 +40,6 @@ class Path {
 
   void advance(KInstruction *ki);
 
-  friend bool operator==(const Path &lhs, const Path &rhs) {
-    return lhs.KBlocks == rhs.KBlocks &&
-           lhs.firstInstruction == rhs.firstInstruction &&
-           lhs.lastInstruction == rhs.lastInstruction;
-  }
-  friend bool operator!=(const Path &lhs, const Path &rhs) {
-    return !(lhs == rhs);
-  }
-
-  friend bool operator<(const Path &lhs, const Path &rhs) {
-    return lhs.KBlocks < rhs.KBlocks ||
-           (lhs.KBlocks == rhs.KBlocks &&
-            (lhs.firstInstruction < rhs.firstInstruction ||
-             (lhs.firstInstruction == rhs.firstInstruction &&
-              lhs.lastInstruction < rhs.lastInstruction)));
-  }
-
   unsigned KBlockSize() const;
   const path_ty &getBlocks() const;
   unsigned getFirstIndex() const;
@@ -64,7 +49,6 @@ class Path {
 
   std::vector<stackframe_ty> getStack(bool reversed) const;
 
-  std::vector<std::pair<KFunction *, BlockRange>> asFunctionRanges() const;
   std::string toString() const;
 
   static Path concat(const Path &l, const Path &r);
@@ -73,7 +57,7 @@ class Path {
 
   Path() = default;
 
-  Path(unsigned firstInstruction, std::vector<KBlock *> kblocks,
+  Path(unsigned firstInstruction, const path_ty &kblocks,
        unsigned lastInstruction)
       : KBlocks(kblocks), firstInstruction(firstInstruction),
         lastInstruction(lastInstruction) {}

lib/Core/ExecutionState.h

@@ -290,7 +290,7 @@ class ExecutionState {
   std::uint32_t depth = 0;
 
   /// @brief Exploration level, i.e., number of times KLEE cycled for this state
-  std::set<KBlock *, KBlockCompare> level;
+  PersistentSet<KBlock *, KBlockCompare> level;
 
   /// @brief Address space used by this state (e.g. Global and Heap)
   AddressSpace addressSpace;

lib/Expr/Constraints.cpp

@@ -330,10 +330,6 @@ PathConstraints::orderedCS() const {
 
 void PathConstraints::advancePath(KInstruction *ki) { _path.advance(ki); }
 
-void PathConstraints::advancePath(const Path &path) {
-  _path = Path::concat(_path, path);
-}
-
 ExprHashSet PathConstraints::addConstraint(ref<Expr> e, const Assignment &delta,
                                            Path::PathIndex currIndex) {
   auto expr = Simplificator::simplifyExpr(constraints, e);
@@ -352,7 +348,9 @@ ExprHashSet PathConstraints::addConstraint(ref<Expr> e, const Assignment &delta,
       added.insert(expr);
       pathIndexes.insert({expr, currIndex});
       _simplificationMap[expr].insert(expr);
-      orderedConstraints[currIndex].insert(expr);
+      auto indexConstraints = orderedConstraints[currIndex].second;
+      indexConstraints.insert(expr);
+      orderedConstraints.replace({currIndex, indexConstraints});
       constraints.addConstraint(expr, delta);
     }
   }
@@ -389,29 +387,6 @@ void PathConstraints::rewriteConcretization(const Assignment &a) {
   constraints.rewriteConcretization(a);
 }
 
-PathConstraints PathConstraints::concat(const PathConstraints &l,
-                                        const PathConstraints &r) {
-  // TODO : How to handle symcretes and concretization?
-  PathConstraints path = l;
-  path._path = Path::concat(l._path, r._path);
-  auto offset = l._path.KBlockSize();
-  for (const auto &i : r._original) {
-    path._original.insert(i);
-    auto index = r.pathIndexes.at(i);
-    index.block += offset;
-    path.pathIndexes.insert({i, index});
-    path.orderedConstraints[index].insert(i);
-  }
-  for (const auto &i : r.constraints.cs()) {
-    path.constraints.addConstraint(i, {});
-    if (r._simplificationMap.count(i)) {
-      path._simplificationMap.insert({i, r._simplificationMap.at(i)});
-    }
-  }
-  // Run the simplificator on the newly constructed set?
-  return path;
-}
-
 Simplificator::ExprResult
 Simplificator::simplifyExpr(const constraints_ty &constraints,
                             const ref<Expr> &expr) {

lib/Expr/Path.cpp

@@ -39,67 +39,6 @@ Path::PathIndex Path::getCurrentIndex() const {
   return {KBlocks.size() - 1, lastInstruction};
 }
 
-std::vector<stackframe_ty> Path::getStack(bool reversed) const {
-  std::vector<stackframe_ty> stack;
-  for (unsigned i = 0; i < KBlocks.size(); i++) {
-    auto current = reversed ? KBlocks[KBlocks.size() - 1 - i] : KBlocks[i];
-    // Previous for reversed is the next
-    KBlock *prev = nullptr;
-    if (i != 0) {
-      prev = reversed ? KBlocks[KBlocks.size() - i] : KBlocks[i - 1];
-    }
-    if (i == 0) {
-      stack.push_back({nullptr, current->parent});
-      continue;
-    }
-    if (reversed) {
-      auto kind = getTransitionKind(current, prev);
-      if (kind == TransitionKind::StepInto) {
-        if (!stack.empty()) {
-          stack.pop_back();
-        }
-      } else if (kind == TransitionKind::StepOut) {
-        assert(isa<KCallBlock>(prev));
-        stack.push_back({prev->getFirstInstruction(), current->parent});
-      }
-    } else {
-      auto kind = getTransitionKind(prev, current);
-      if (kind == TransitionKind::StepInto) {
-        stack.push_back({prev->getFirstInstruction(), current->parent});
-      } else if (kind == TransitionKind::StepOut) {
-        if (!stack.empty()) {
-          stack.pop_back();
-        }
-      }
-    }
-  }
-  return stack;
-}
-
-std::vector<std::pair<KFunction *, Path::BlockRange>>
-Path::asFunctionRanges() const {
-  assert(!KBlocks.empty());
-  std::vector<std::pair<KFunction *, BlockRange>> ranges;
-  BlockRange range{0, 0};
-  KFunction *function = KBlocks[0]->parent;
-  for (unsigned i = 1; i < KBlocks.size(); i++) {
-    if (getTransitionKind(KBlocks[i - 1], KBlocks[i]) == TransitionKind::None) {
-      if (i == KBlocks.size() - 1) {
-        range.last = i;
-        ranges.push_back({function, range});
-        return ranges;
-      } else {
-        continue;
-      }
-    }
-    range.last = i - 1;
-    ranges.push_back({function, range});
-    range.first = i;
-    function = KBlocks[i]->parent;
-  }
-  llvm_unreachable("asFunctionRanges reached the end of the for!");
-}
-
 Path Path::concat(const Path &l, const Path &r) {
   Path path = l;
   for (auto block : r.KBlocks) {
@@ -112,11 +51,16 @@ Path Path::concat(const Path &l, const Path &r) {
 std::string Path::toString() const {
   std::string blocks = "";
   unsigned depth = 0;
-  for (unsigned i = 0; i < KBlocks.size(); i++) {
-    auto current = KBlocks[i];
+  std::vector<KBlock *> KBlocksVector;
+  KBlocksVector.reserve(KBlocks.size());
+  for (auto kblock : KBlocks) {
+    KBlocksVector.push_back(kblock);
+  }
+  for (size_t i = 0; i < KBlocksVector.size(); i++) {
+    auto current = KBlocksVector[i];
     KBlock *prev = nullptr;
     if (i != 0) {
-      prev = KBlocks[i - 1];
+      prev = KBlocksVector[i - 1];
     }
     auto kind =
         i == 0 ? TransitionKind::StepInto : getTransitionKind(prev, current);