[fear] Add PersistentHashMap

[feat] Use 'immer' data structures

[feat] Add `UseImmerStructures`

[feat] Add `FixedSizeStorageAdapter`

Author: misonijnik

.cirrus.yml

@@ -6,11 +6,11 @@ task:
   deps_script:
     - sed -i.bak -e 's/quarterly/latest/' /etc/pkg/FreeBSD.conf
     - env ASSUME_ALWAYS_YES=yes pkg update -f
-    - env ASSUME_ALWAYS_YES=yes pkg install -y llvm11 gmake z3 cmake pkgconf google-perftools python3 py39-sqlite3 py39-tabulate nlohmann-json bash coreutils
+    - env ASSUME_ALWAYS_YES=yes pkg install -y llvm11 gmake z3 cmake pkgconf google-perftools python3 py39-sqlite3 py39-tabulate nlohmann-json bash coreutils immer
   build_script:
     - mkdir build
     - cd build
-    - cmake -DLLVM_DIR=/usr/local/llvm11 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON ..
+    - cmake -DLLVM_DIR=/usr/local/llvm11 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON ..
     - gmake
   test_script:
     - sed -i.bak -e 's/lit\./lit11\./' test/lit.cfg

.github/workflows/build.yaml

@@ -32,6 +32,7 @@ env:
   SQLITE_VERSION: 3400100
   BITWUZLA_VERSION: 0.3.1
   JSON_VERSION: v3.11.3
+  IMMER_VERSION: v0.8.1
 
 jobs:
   Linux:

CMakeLists.txt

@@ -681,6 +681,7 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin
 include_directories("${CMAKE_BINARY_DIR}/include")
 include_directories("${CMAKE_SOURCE_DIR}/include")
 include_directories("${JSON_SRC_DIR}/include")
+include_directories("${IMMER_SRC_DIR}")
 # set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include)
 
 ################################################################################

Dockerfile

@@ -36,6 +36,7 @@ ENV USE_LIBCXX=1
 ENV KLEE_RUNTIME_BUILD="Debug+Asserts"
 ENV SQLITE_VERSION=3400100
 ENV JSON_VERSION=v3.11.3
+ENV IMMER_VERSION=v0.8.1
 LABEL maintainer="KLEE Developers"
 
 # TODO remove adding sudo package

build.sh

@@ -5,7 +5,7 @@
 
 # Base folder where dependencies and KLEE itself are installed
 BASE=$HOME/klee_build
-BUILD_SUFFIX="Release"
+BUILD_SUFFIX="Debug"
 
 ## KLEE Required options
 # Build type for KLEE. The options are:
@@ -26,7 +26,6 @@ USE_LIBCXX=1
 # Also required despite not being mentioned in the guide
 SQLITE_VERSION="3400100"
 
-
 ## LLVM Required options
 LLVM_VERSION=14
 ENABLE_OPTIMIZED=1
@@ -44,6 +43,9 @@ GTEST_VERSION=1.11.0
 ## json options
 JSON_VERSION=v3.11.3
 
+## immer options
+IMMER_VERSION=v0.8.1
+
 ## UClibC Required options
 UCLIBC_VERSION=klee_uclibc_v1.3
 # LLVM_VERSION is also required for UClibC
@@ -56,4 +58,4 @@ MINISAT_VERSION=master
 
 BITWUZLA_VERSION=0.3.1
 
-BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION ./scripts/build/build.sh klee --install-system-deps
+BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION ./scripts/build/build.sh klee --install-system-deps

include/klee/ADT/PersistentHashMap.h

@@ -0,0 +1,82 @@
+//===-- PersistentHashMap.h -------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_PRESISTENTHASHMAP_H
+#define KLEE_PRESISTENTHASHMAP_H
+
+#ifndef IMMER_NO_EXCEPTIONS
+#define IMMER_NO_EXCEPTIONS
+#endif /* IMMER_NO_EXCEPTIONS */
+
+#include <immer/map.hpp>
+
+namespace klee {
+
+template <class K, class D, class HASH = std::hash<K>,
+          class EQUAL = std::equal_to<K>>
+class PersistentHashMap {
+public:
+  typedef immer::map<K, D, HASH, EQUAL> Map;
+  typedef typename Map::iterator iterator;
+  typedef K key_type;
+  typedef std::pair<K, D> value_type;
+
+private:
+  Map elts;
+
+  PersistentHashMap(const Map &b) : elts(b) {}
+
+public:
+  PersistentHashMap() {}
+  PersistentHashMap(const PersistentHashMap &b) : elts(b.elts) {}
+  ~PersistentHashMap() {}
+
+  PersistentHashMap &operator=(const PersistentHashMap &b) {
+    elts = b.elts;
+    return *this;
+  }
+  bool operator==(const PersistentHashMap &b) const { return elts == b.elts; }
+  bool operator<(const PersistentHashMap &b) const { return elts < b.elts; }
+
+  bool empty() const { return elts.empty(); }
+  size_t count(const key_type &key) const { return elts.count(key); }
+  const D *lookup(const key_type &key) const { return elts.find(key); }
+  size_t size() const { return elts.size(); }
+
+  void insert(const value_type &value) {
+    if (!lookup(value.first)) {
+      elts = elts.insert(value);
+    }
+  }
+  void replace(const value_type &value) { elts = elts.insert(value); }
+  void remove(const key_type &key) { elts = elts.erase(key); }
+
+  iterator begin() const { return elts.begin(); }
+  iterator end() const { return elts.end(); }
+
+  const D &operator[](const key_type &key) {
+    return elts[key];
+    // auto value = lookup(key);
+    // if (value) {
+    //   return *value;
+    // } else {
+    //   value_type defVal;
+    //   defVal.first = key;
+    //   insert(defVal);
+    //   return *lookup(key);
+    // }
+  }
+
+  const D &at(const key_type &key) const { return elts.at(key); }
+
+  void clear() { elts = Map(); }
+};
+} // namespace klee
+
+#endif /* KLEE_PRESISTENTHASHMAP_H */

include/klee/ADT/PersistentVector.h

@@ -0,0 +1,66 @@
+//===-- PersistentVector.h --------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_PRESISTENTVECTOR_H
+#define KLEE_PRESISTENTVECTOR_H
+
+#ifndef IMMER_NO_EXCEPTIONS
+#define IMMER_NO_EXCEPTIONS
+#endif /* IMMER_NO_EXCEPTIONS */
+
+#include <immer/vector.hpp>
+
+namespace klee {
+
+template <class T> class PersistentVector {
+public:
+  using Vector = immer::vector<T>;
+  using iterator = typename Vector::iterator;
+  using value_type = T;
+
+private:
+  Vector elts;
+
+  PersistentVector(const Vector &b) : elts(b) {}
+
+public:
+  PersistentVector() {}
+  PersistentVector(const PersistentVector &b) : elts(b.elts) {}
+  ~PersistentVector() {}
+
+  PersistentVector &operator=(const PersistentVector &b) {
+    elts = b.elts;
+    return *this;
+  }
+
+  bool operator==(const PersistentVector &b) const { return elts == b.elts; }
+  bool operator!=(const PersistentVector &other) const {
+    return !(*this == other);
+  }
+  bool empty() const { return elts.empty(); }
+  size_t size() const { return elts.size(); }
+
+  void set(size_t index, const value_type &value) {
+    elts = elts.set(index, value);
+  }
+  void init(const size_t &n) { elts = Vector(n); }
+  void push_back(const value_type &value) { elts = elts.push_back(value); }
+  const value_type &back() const { return elts.back(); }
+  const value_type &front() const { return elts.front(); }
+  const value_type &operator[](const size_t &index) const {
+    return elts[index];
+  }
+  const value_type &at(const size_t &index) const { return elts[index]; }
+
+  iterator begin() const { return elts.begin(); }
+  iterator end() const { return elts.end(); }
+};
+} // namespace klee
+
+#endif /* KLEE_PRESISTENTVECTOR_H */