[wip] Add persistent list workaround

Author: ladisgin

CMakeLists.txt

@@ -302,6 +302,9 @@ else()
   message(STATUS "TCMalloc support disabled")
 endif()
 
+
+list(APPEND KLEE_COMPONENT_CXX_FLAGS "-gdwarf-4")
+
 ################################################################################
 # Detect SQLite3
 ################################################################################

lib/Core/ExecutionState.cpp

@@ -123,7 +123,7 @@ InfoStackFrame::InfoStackFrame(const InfoStackFrame &s)
 /***/
 ExecutionState::ExecutionState()
     : initPC(nullptr), pc(nullptr), prevPC(nullptr), incomingBBIndex(-1),
-      depth(0), ptreeNode(nullptr), steppedInstructions(0),
+      depth(0), ptreeNode(nullptr), symbolics(std::make_shared<PList>()), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false),
       forkDisabled(false), prevHistory_(TargetsHistory::create()),
@@ -133,7 +133,7 @@ ExecutionState::ExecutionState()
 
 ExecutionState::ExecutionState(KFunction *kf)
     : initPC(kf->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1),
-      depth(0), ptreeNode(nullptr), steppedInstructions(0),
+      depth(0), ptreeNode(nullptr), symbolics(std::make_shared<PList>()), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false),
       forkDisabled(false), prevHistory_(TargetsHistory::create()),
@@ -144,7 +144,7 @@ ExecutionState::ExecutionState(KFunction *kf)
 
 ExecutionState::ExecutionState(KFunction *kf, KBlock *kb)
     : initPC(kb->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1),
-      depth(0), ptreeNode(nullptr), steppedInstructions(0),
+      depth(0), ptreeNode(nullptr), symbolics(std::make_shared<PList>()), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false),
       forkDisabled(false), prevHistory_(TargetsHistory::create()),
@@ -194,8 +194,8 @@ ExecutionState *ExecutionState::branch() {
 }
 
 bool ExecutionState::inSymbolics(const MemoryObject *mo) const {
-  for (auto i : symbolics) {
-    if (mo->id == i.memoryObject->id) {
+  for (auto &symbolic : *symbolics) {
+    if (mo->id == symbolic.memoryObject->id) {
       return true;
     }
   }
@@ -255,13 +255,12 @@ void ExecutionState::popFrame() {
 
 void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array,
                                  KType *type) {
-  symbolics.emplace_back(ref<const MemoryObject>(mo), array, type);
+  symbolics->emplace_back(mo, array, type);
 }
 
 ref<const MemoryObject>
 ExecutionState::findMemoryObject(const Array *array) const {
-  for (unsigned i = 0; i != symbolics.size(); ++i) {
-    const auto &symbolic = symbolics[i];
+  for (const auto &symbolic : *symbolics) {
     if (array == symbolic.array) {
       return symbolic.memoryObject;
     }
@@ -368,7 +367,7 @@ bool ExecutionState::resolveOnSymbolics(const ref<ConstantExpr> &addr,
                                         IDType &result) const {
   uint64_t address = addr->getZExtValue();
 
-  for (const auto &res : symbolics) {
+  for (const auto &res : *symbolics) {
     const auto &mo = res.memoryObject;
     // Check if the provided address is between start and end of the object
     // [mo->address, mo->address + mo->size) or the object is a 0-sized object.

lib/Core/ExecutionState.h

@@ -41,6 +41,8 @@ DISABLE_WARNING_POP
 #include <utility>
 #include <vector>
 
+#include <list>
+
 namespace klee {
 class Array;
 class CallPathNode;
@@ -223,6 +225,85 @@ struct Symbolic {
   }
 };
 
+struct PList {
+private:
+  std::shared_ptr<const PList> prev;
+  size_t prev_len;
+  std::vector<Symbolic> curr;
+
+public:
+  size_t size() const { return prev_len + curr.size(); }
+
+  struct iterator {
+    const PList *curr;
+    std::unique_ptr<iterator> it;
+    size_t get;
+
+  public:
+    explicit iterator(const PList *p) : curr(p), it(nullptr), get(0) {
+      if (curr->prev.get()) {
+        it = std::make_unique<iterator>(curr->prev.get());
+      }
+    }
+
+    bool operator==(const iterator &b) const {
+      return curr == b.curr && get == b.get;
+    }
+    bool operator!=(const iterator &b) const { return !(*this == b); }
+
+    iterator &operator++() {
+      ++get;
+      if (get < curr->prev_len) {
+        return it->operator++();
+      }
+      return *this;
+    }
+
+    const Symbolic &operator*() const {
+      if (get < curr->prev_len) {
+        return it->operator*();
+      }
+      return curr->curr[get - curr->prev_len];
+    }
+
+    const Symbolic &operator->() const { return **this; }
+  };
+
+  [[nodiscard]] iterator begin() const { return iterator(this); }
+
+  [[nodiscard]] iterator end() const {
+    auto it = iterator(this);
+    it.get = size();
+    return it;
+  }
+
+  [[nodiscard]] iterator begin() { return iterator(this); }
+
+  [[nodiscard]] iterator end() {
+    auto it = iterator(this);
+    it.get = size();
+    return it;
+  }
+
+  void emplace_back(const MemoryObject *mo, const Array *array, KType *type) {
+    curr.emplace_back(ref<const MemoryObject>(mo), array, type);
+  }
+
+  PList() : prev(nullptr), prev_len(0), curr(){};
+  PList(std::shared_ptr<const PList> pr) : curr() {
+    while (pr && pr->prev && pr->prev_len == pr->prev->prev_len) {
+      pr = pr->prev;
+    }
+    if (pr && pr->size()) {
+      prev = pr;
+      prev_len = pr->size();
+    } else {
+      prev = nullptr;
+      prev_len = 0;
+    }
+  }
+};
+
 struct MemorySubobject {
   ref<Expr> address;
   unsigned size;
@@ -326,7 +407,7 @@ class ExecutionState {
   /// @brief Ordered list of symbolics: used to generate test cases.
   //
   // FIXME: Move to a shared list structure (not critical).
-  std::vector<Symbolic> symbolics;
+  std::shared_ptr<PList> symbolics;
 
   /// @brief map from memory accesses to accessed objects and access offsets.
   ExprHashMap<std::set<IDType>> resolvedPointers;

lib/Core/Executor.cpp

@@ -6900,10 +6900,10 @@ void Executor::logState(const ExecutionState &state, int id,
     *f << "Address memory object: " << object.first->address << "\n";
     *f << "Memory object size: " << object.first->size << "\n";
   }
-  *f << state.symbolics.size() << " symbolics total. "
+  *f << state.symbolics->size() << " symbolics total. "
      << "Symbolics:\n";
   size_t sc = 0;
-  for (auto &symbolic : state.symbolics) {
+  for (auto &symbolic : *state.symbolics) {
     *f << "Symbolic number " << sc++ << "\n";
     *f << "Associated memory object: " << symbolic.memoryObject.get()->id
        << "\n";
@@ -6924,12 +6924,12 @@ void Executor::setInitializationGraph(const ExecutionState &state,
   ExprHashMap<std::pair<IDType, ref<Expr>>> resolvedPointers;
 
   std::unordered_map<IDType, ref<const MemoryObject>> idToSymbolics;
-  for (const auto &symbolic : state.symbolics) {
+  for (const auto &symbolic : *state.symbolics) {
     ref<const MemoryObject> mo = symbolic.memoryObject;
     idToSymbolics[mo->id] = mo;
   }
 
-  for (const auto &symbolic : state.symbolics) {
+  for (const auto &symbolic : *state.symbolics) {
     KType *symbolicType = symbolic.type;
     if (!symbolicType->getRawType()) {
       continue;
@@ -6992,15 +6992,17 @@ void Executor::setInitializationGraph(const ExecutionState &state,
       // The objects have to be symbolic
       bool pointerFound = false, pointeeFound = false;
       size_t pointerIndex = 0, pointeeIndex = 0;
-      for (size_t i = 0; i < state.symbolics.size(); i++) {
-        if (state.symbolics[i].memoryObject == pointerResolution.first) {
+      size_t i = 0;
+      for (auto &symbolic : *state.symbolics) {
+        if (symbolic.memoryObject == pointerResolution.first) {
           pointerIndex = i;
           pointerFound = true;
         }
-        if (state.symbolics[i].memoryObject->id == pointer.second.first) {
+        if (symbolic.memoryObject->id == pointer.second.first) {
           pointeeIndex = i;
           pointeeFound = true;
         }
+        ++i;
       }
       if (pointerFound && pointeeFound) {
         ref<ConstantExpr> offset = model.evaluate(pointerResolution.second);
@@ -7087,8 +7089,9 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
 
   std::vector<SparseStorage<unsigned char>> values;
   std::vector<const Array *> objects;
-  for (unsigned i = 0; i != state.symbolics.size(); ++i)
-    objects.push_back(state.symbolics[i].array);
+  for (auto &symbolic : *state.symbolics) {
+    objects.push_back(symbolic.array);
+  }
   bool success = solver->getInitialValues(extendedConstraints.cs(), objects,
                                           values, state.queryMetaData);
   solver->setTimeout(time::Span());
@@ -7099,19 +7102,23 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
     return false;
   }
 
-  res.objects = new KTestObject[state.symbolics.size()];
-  res.numObjects = state.symbolics.size();
+  res.numObjects = state.symbolics->size();
+  res.objects = new KTestObject[res.numObjects];
 
-  for (unsigned i = 0; i != state.symbolics.size(); ++i) {
-    auto mo = state.symbolics[i].memoryObject;
-    KTestObject *o = &res.objects[i];
-    o->name = const_cast<char *>(mo->name.c_str());
-    o->address = mo->address;
-    o->numBytes = values[i].size();
-    o->bytes = new unsigned char[o->numBytes];
-    std::copy(values[i].begin(), values[i].end(), o->bytes);
-    o->numPointers = 0;
-    o->pointers = nullptr;
+  {
+    size_t i = 0;
+    for (auto &symbolic : *state.symbolics) {
+      auto mo = symbolic.memoryObject;
+      KTestObject *o = &res.objects[i];
+      o->name = const_cast<char *>(mo->name.c_str());
+      o->address = mo->address;
+      o->numBytes = values[i].size();
+      o->bytes = new unsigned char[o->numBytes];
+      std::copy(values[i].begin(), values[i].end(), o->bytes);
+      o->numPointers = 0;
+      o->pointers = nullptr;
+      ++i;
+    }
   }
 
   Assignment model = Assignment(objects, values, true);