Fully symbolic memory, multiplex entry points, fair searcher

.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

@@ -11,6 +11,7 @@ on:
 env:
   BASE_IMAGE: ubuntu:jammy-20230126
   REPOSITORY: ghcr.io/klee
+  BUILD_SUFFIX: "default"
   COVERAGE: 0
   DISABLE_ASSERTIONS: 0
   ENABLE_DOXYGEN: 0
@@ -31,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

@@ -17,6 +17,7 @@ COPY --from=sqlite3_base /tmp /tmp/
 ENV COVERAGE=0
 ENV USE_TCMALLOC=1
 ENV BASE=/tmp
+ENV BUILD_SUFFIX="default"
 ENV LLVM_VERSION=13.0
 ENV ENABLE_DOXYGEN=1
 ENV ENABLE_OPTIMIZED=1
@@ -35,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
@@ -71,4 +73,4 @@ ENV LD_LIBRARY_PATH /home/klee/klee_build/lib/
 RUN /bin/bash -c 'ln -s ${BASE}/klee_src /home/klee/ && ln -s ${BASE}/klee_build* /home/klee/klee_build'
 
 # TODO Remove when STP is fixed
-RUN /bin/bash -c 'echo "export LD_LIBRARY_PATH=$(cd ${BASE}/metaSMT-*-deps/stp-git-basic/lib/ && pwd):$LD_LIBRARY_PATH" >> /home/klee/.bashrc'
+RUN /bin/bash -c 'echo "export LD_LIBRARY_PATH=$(cd ${BASE}/metaSMT-*-deps/stp-git-basic/lib/ && pwd):$LD_LIBRARY_PATH" >> /home/klee/.bashrc'

build.sh

@@ -5,6 +5,7 @@
 
 # Base folder where dependencies and KLEE itself are installed
 BASE=$HOME/klee_build
+BUILD_SUFFIX="Release"
 
 ## KLEE Required options
 # Build type for KLEE. The options are:
@@ -14,8 +15,7 @@ BASE=$HOME/klee_build
 # Release+Debug+Asserts
 # Debug
 # Debug+Asserts
-# KLEE_RUNTIME_BUILD="Debug+Asserts"
-KLEE_RUNTIME_BUILD="Release" # "Debug+Asserts"
+KLEE_RUNTIME_BUILD="Release"
 
 COVERAGE=0
 ENABLE_DOXYGEN=0
@@ -25,7 +25,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
@@ -43,6 +42,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
@@ -55,4 +57,17 @@ MINISAT_VERSION=master
 
 BITWUZLA_VERSION=0.3.1
 
-BASE="$BASE" 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
+KEEP_PARSE="true"
+while [ $KEEP_PARSE = "true" ]; do
+if [ "$1" = "--debug" ] || [ "$1" = "-g" ]; then
+    BUILD_SUFFIX="Debug"
+    ENABLE_OPTIMIZED=0
+    ENABLE_DEBUG=1
+    KLEE_RUNTIME_BUILD="Debug+Asserts"
+    shift 1
+else
+    KEEP_PARSE="false"
+fi
+done
+
+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 SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ./scripts/build/build.sh klee --install-system-deps

configs/options.json

@@ -29,7 +29,7 @@
                 "--output-istats=false",
                 "--output-stats=false",
                 "--max-time=${maxTime}s",
-                "--max-sym-alloc=${maxSymAlloc}",
+                "--max-sym-size-alloc=${maxSymAlloc}",
                 "--max-forks=${maxForks}",
                 "--max-solver-time=${maxSolverTime}s",
                 "--smart-resolve-entry-function",

include/klee/ADT/DisjointSetUnion.h

@@ -32,7 +32,7 @@ class DisjointSetUnion {
   using internal_storage_ty = std::unordered_set<ValueType, HASH, PRED>;
   using disjoint_sets_ty =
       std::unordered_map<ValueType, ref<const SetType>, HASH, PRED>;
-  using iterator = typename internal_storage_ty::iterator;
+  using iterator = typename internal_storage_ty::const_iterator;
 
 protected:
   std::unordered_map<ValueType, ValueType, HASH, PRED> parent;