[wip] Uninitialized Memory

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

@@ -1,6 +1,8 @@
 #ifndef KLEE_SPARSESTORAGE_H
 #define KLEE_SPARSESTORAGE_H
 
+#include "klee/ADT/Ref.h"
+#include <algorithm>
 #include <cassert>
 #include <cstddef>
 #include <iterator>
@@ -12,31 +14,47 @@ namespace llvm {
 class raw_ostream;
 };
 
+
 namespace klee {
 
+enum class Density {
+  Sparse,
+  Dense,
+};
+
 template <typename ValueType> class SparseStorage {
 private:
   std::unordered_map<size_t, ValueType> internalStorage;
   ValueType defaultValue;
-  size_t rangeSize = 0;
 
   bool contains(size_t key) const { return internalStorage.count(key) != 0; }
 
 public:
   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);
+    }
+  }
+
   SparseStorage(const std::vector<ValueType> &values,
                 const ValueType &defaultValue = ValueType())
       : defaultValue(defaultValue) {
     for (size_t idx = 0; idx < values.size(); ++idx) {
-      internalStorage[idx] = values[idx];
+      store(idx, values[idx]);
     }
   }
 
   void store(size_t idx, const ValueType &value) {
+    if (value == defaultValue) {
+      internalStorage.erase(idx);
+    } else {
       internalStorage[idx] = value;
-      rangeSize = std::max(rangeSize, idx + 1);
+    }
   }
 
   template <typename InputIterator>
@@ -52,12 +70,15 @@ template <typename ValueType> class SparseStorage {
   }
 
   size_t sizeOfSetRange() const {
-    return rangeSize;
+    size_t sizeOfRange = 0;
+    for (auto i : internalStorage) {
+      sizeOfRange = std::max(i.first, sizeOfRange);
+    }
+    return sizeOfRange;
   }
 
   bool operator==(const SparseStorage<ValueType> &another) const {
-    return defaultValue == another.defaultValue &&
-        compare(another) == 0;
+    return defaultValue == another.defaultValue && compare(another) == 0;
   }
 
   bool operator!=(const SparseStorage<ValueType> &another) const {
@@ -73,46 +94,56 @@ template <typename ValueType> class SparseStorage {
   }
 
   int compare(const SparseStorage<ValueType> &other) const {
-    std::map<size_t, ValueType> thisMap;
-    std::map<size_t, ValueType> otherMap;
-    for (auto i : internalStorage) {
-      thisMap.insert(i);
-    }
-    for (auto i : other.internalStorage) {
-      otherMap.insert(i);
-    }
-    if (thisMap == otherMap) {
+    auto ordered = calculateOrderedStorage();
+    auto otherOrdered = other.calculateOrderedStorage();
+
+    if (ordered == otherOrdered) {
       return 0;
     } else {
-      return thisMap < otherMap ? -1 : 1;
+      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();
-    rangeSize = 0;
   }
 
   void reset(ValueType newDefault) {
     defaultValue = newDefault;
     internalStorage.clear();
-    rangeSize = 0;
   }
 
   // Specialized for unsigned char in .cpp
-  void print(llvm::raw_ostream &os) const;
+  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/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,14 @@ 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);
@@ -27,6 +32,7 @@ class SourceBuilder {
                                          int _index, KModule *km);
   static ref<SymbolicSource> value(const llvm::Value &_allocSite, int _index,
                                    KModule *km);
+  static ref<SymbolicSource> global(const llvm::GlobalVariable &name);
   static ref<SymbolicSource> irreproducible(const std::string &name);
 };