[feat] Uninitialized Memory [feat] Sizeless ObjectState

[feat] STP symsize array support

Author: ocelaiwo

include/klee/ADT/KTest.h

@@ -46,6 +46,7 @@ struct KTest {
 
   unsigned numObjects;
   KTestObject *objects;
+  unsigned uninitCoeff;
 };
 
 /* returns the current .ktest file format version */

include/klee/ADT/Ref.h

@@ -205,7 +205,13 @@ template <class T> class ref {
 
   // assumes non-null arguments
   bool equals(const ref &rhs) const {
-    assert(!isNull() && !rhs.isNull() && "Invalid call to compare()");
+    if (isNull() && rhs.isNull()) {
+      return true;
+    }
+    if (isNull() || rhs.isNull()) {
+      return false;
+    }
+    // assert(!isNull() && !rhs.isNull() && "Invalid call to compare()");
     return get()->equals(*rhs.get());
   }
 

include/klee/ADT/SparseStorage.h

@@ -5,65 +5,51 @@
 #include <cstddef>
 #include <iterator>
 #include <map>
+#include <unordered_map>
 #include <vector>
 
+namespace llvm {
+class raw_ostream;
+};
+
 namespace klee {
 
+enum class Density {
+  Sparse,
+  Dense,
+};
+
 template <typename ValueType> class SparseStorage {
 private:
-  size_t capacity;
-  std::map<size_t, ValueType> internalStorage;
+  std::unordered_map<size_t, ValueType> internalStorage;
   ValueType defaultValue;
 
   bool contains(size_t key) const { return internalStorage.count(key) != 0; }
 
 public:
-  struct Iterator {
-    using iterator_category = std::input_iterator_tag;
-    using difference_type = std::ptrdiff_t;
-    using value_type = ValueType;
-    using pointer = ValueType *;
-    using reference = ValueType &;
-
-  private:
-    size_t idx;
-    const SparseStorage *owner;
-
-  public:
-    Iterator(size_t idx, const SparseStorage *owner) : idx(idx), owner(owner) {}
-
-    value_type operator*() const { return owner->load(idx); }
-
-    Iterator &operator++() {
-      ++idx;
-      return *this;
-    }
-
-    Iterator operator++(int) {
-      Iterator snap = *this;
-      ++(*this);
-      return snap;
+  SparseStorage(const ValueType &defaultValue = ValueType())
+      : defaultValue(defaultValue) {}
+
+  SparseStorage(const std::unordered_map<size_t, ValueType> &internalStorage,
+                const ValueType &defaultValue)
+      : defaultValue(defaultValue) {
+    for (auto &[index, value] : internalStorage) {
+      store(index, value);
     }
-
-    bool operator==(const Iterator &other) const { return idx == other.idx; }
-
-    bool operator!=(const Iterator &other) const { return !(*this == other); }
-  };
-
-  SparseStorage(size_t capacity = 0,
-                const ValueType &defaultValue = ValueType())
-      : capacity(capacity), defaultValue(defaultValue) {}
+  }
 
   SparseStorage(const std::vector<ValueType> &values,
                 const ValueType &defaultValue = ValueType())
-      : capacity(values.capacity()), defaultValue(defaultValue) {
-    for (size_t idx = 0; idx < values.capacity(); ++idx) {
-      internalStorage[idx] = values[idx];
+      : defaultValue(defaultValue) {
+    for (size_t idx = 0; idx < values.size(); ++idx) {
+      store(idx, values[idx]);
     }
   }
 
   void store(size_t idx, const ValueType &value) {
-    if (idx < capacity) {
+    if (value == defaultValue) {
+      internalStorage.erase(idx);
+    } else {
       internalStorage[idx] = value;
     }
   }
@@ -77,55 +63,82 @@ template <typename ValueType> class SparseStorage {
   }
 
   ValueType load(size_t idx) const {
-    assert(idx < capacity && idx >= 0);
     return contains(idx) ? internalStorage.at(idx) : defaultValue;
   }
 
-  size_t size() const { return capacity; }
-
-  void resize(size_t newCapacity) {
-    assert(newCapacity >= 0);
-    // Free to extend
-    if (newCapacity >= capacity) {
-      capacity = newCapacity;
-      return;
-    }
-
-    // Truncate unnessecary elements
-    auto iterOnNewSize = internalStorage.lower_bound(newCapacity);
-    while (iterOnNewSize != internalStorage.end()) {
-      iterOnNewSize = internalStorage.erase(iterOnNewSize);
+  size_t sizeOfSetRange() const {
+    size_t sizeOfRange = 0;
+    for (auto i : internalStorage) {
+      sizeOfRange = std::max(i.first, sizeOfRange);
     }
-
-    capacity = newCapacity;
+    return sizeOfRange;
   }
 
   bool operator==(const SparseStorage<ValueType> &another) const {
-    return size() == another.size() && defaultValue == another.defaultValue &&
-           internalStorage == another.internalStorage;
+    return defaultValue == another.defaultValue && compare(another) == 0;
   }
 
   bool operator!=(const SparseStorage<ValueType> &another) const {
     return !(*this == another);
   }
 
   bool operator<(const SparseStorage &another) const {
-    return internalStorage < another.internalStorage;
+    return compare(another) == -1;
   }
 
   bool operator>(const SparseStorage &another) const {
-    return internalStorage > another.internalStorage;
+    return compare(another) == 1;
+  }
+
+  int compare(const SparseStorage<ValueType> &other) const {
+    auto ordered = calculateOrderedStorage();
+    auto otherOrdered = other.calculateOrderedStorage();
+
+    if (ordered == otherOrdered) {
+      return 0;
+    } else {
+      return ordered < otherOrdered ? -1 : 1;
+    }
+  }
+
+  std::map<size_t, ValueType> calculateOrderedStorage() const {
+    std::map<size_t, ValueType> ordered;
+    for (const auto &i : internalStorage) {
+      ordered.insert(i);
+    }
+    return ordered;
+  }
+
+  std::vector<ValueType> getFirstNIndexes(size_t n) const {
+    std::vector<ValueType> vectorized(n);
+    for (size_t i = 0; i < n; i++) {
+      vectorized[i] = load(i);
+    }
+    return vectorized;
+  }
+
+  const std::unordered_map<size_t, ValueType> &storage() const {
+    return internalStorage;
+  };
+
+  const ValueType &defaultV() const { return defaultValue; };
+
+  void reset() { internalStorage.clear(); }
+
+  void reset(ValueType newDefault) {
+    defaultValue = newDefault;
+    internalStorage.clear();
   }
 
-  Iterator begin() const { return Iterator(0, this); }
-  Iterator end() const { return Iterator(size(), this); }
+  // Specialized for unsigned char in .cpp
+  void print(llvm::raw_ostream &os, Density) const;
 };
 
 template <typename U>
 SparseStorage<unsigned char> sparseBytesFromValue(const U &value) {
   const unsigned char *valueUnsignedCharIterator =
       reinterpret_cast<const unsigned char *>(&value);
-  SparseStorage<unsigned char> result(sizeof(value));
+  SparseStorage<unsigned char> result;
   result.store(0, valueUnsignedCharIterator,
                valueUnsignedCharIterator + sizeof(value));
   return result;

include/klee/Expr/ArrayCache.h

@@ -64,6 +64,9 @@ class ArrayCache {
   typedef std::vector<const Array *> ArrayPtrVec;
   ArrayPtrVec concreteArrays;
 
+  // Number of arrays of each source allocated
+  std::unordered_map<SymbolicSource::Kind, unsigned> allocatedCount;
+
   unsigned getNextID() const;
 };
 } // namespace klee

include/klee/Expr/Assignment.h

@@ -95,8 +95,10 @@ class AssignmentEvaluator : public ExprEvaluator {
 inline ref<Expr> Assignment::evaluate(const Array *array, unsigned index,
                                       bool allowFreeValues) const {
   assert(array);
+  auto sizeExpr = evaluate(array->size);
   bindings_ty::iterator it = bindings.find(array);
-  if (it != bindings.end() && index < it->second.size()) {
+  if (it != bindings.end() && isa<ConstantExpr>(sizeExpr) &&
+      index < cast<ConstantExpr>(sizeExpr)->getZExtValue()) {
     return ConstantExpr::alloc(it->second.load(index), array->getRange());
   } else {
     if (allowFreeValues) {

include/klee/Expr/Expr.h

@@ -629,10 +629,7 @@ class Array {
 
 public:
   bool isSymbolicArray() const { return !isConstantArray(); }
-  bool isConstantArray() const {
-    return isa<ConstantSource>(source) ||
-           isa<SymbolicSizeConstantSource>(source);
-  }
+  bool isConstantArray() const;
 
   const std::string getName() const { return source->toString(); }
   const std::string getIdentifier() const {

include/klee/Expr/Parser/Lexer.h

@@ -32,6 +32,8 @@ struct Token {
     KWFalse,    ///< 'false'
     KWQuery,    ///< 'query'
     KWPath,     ///< 'path'
+    KWDV,       ///< 'DV'
+    KWNull,     ///< 'null'
     KWReserved, ///< fp[0-9]+([.].*)?, i[0-9]+
     KWSymbolic, ///< 'symbolic'
     KWTrue,     ///< 'true'

include/klee/Expr/SourceBuilder.h

@@ -2,6 +2,7 @@
 #define KLEE_SOURCEBUILDER_H
 
 #include "klee/ADT/Ref.h"
+#include "klee/ADT/SparseStorage.h"
 #include "klee/Expr/SymbolicSource.h"
 #include "klee/Module/KModule.h"
 
@@ -12,10 +13,13 @@ class SourceBuilder {
   SourceBuilder() = delete;
 
   static ref<SymbolicSource>
-  constant(const std::vector<ref<ConstantExpr>> &constantValues);
-  static ref<SymbolicSource> symbolicSizeConstant(unsigned defaultValue);
-  static ref<SymbolicSource> symbolicSizeConstantAddress(unsigned defaultValue,
-                                                         unsigned version);
+  constant(SparseStorage<ref<ConstantExpr>> constantValues);
+
+  static ref<SymbolicSource> uninitialized(unsigned version,
+                                           const KInstruction *allocSite);
+  static ref<SymbolicSource>
+  symbolicSizeConstantAddress(unsigned version, const KInstruction *allocSite,
+                              ref<Expr> size);
   static ref<SymbolicSource> makeSymbolic(const std::string &name,
                                           unsigned version);
   static ref<SymbolicSource> lazyInitializationAddress(ref<Expr> pointer);