Persistent ptree 3

.github/workflows/build.yaml

@@ -10,7 +10,7 @@ on:
 # Defaults for building KLEE
 env:
   BASE_IMAGE: ubuntu:jammy-20230126
-  REPOSITORY: klee
+  REPOSITORY: ghcr.io/klee
   COVERAGE: 0
   DISABLE_ASSERTIONS: 0
   ENABLE_DOXYGEN: 0

.github/workflows/differential-shellcheck.yml

@@ -0,0 +1,31 @@
+# Doc: https://github.com/redhat-plumbers-in-action/differential-shellcheck#usage
+---
+
+name: Differential ShellCheck
+on:
+  push:
+    branches: [master]
+  pull_request:
+    branches: [master]
+
+permissions:
+  contents: read
+
+jobs:
+  lint:
+    runs-on: ubuntu-latest
+
+    permissions:
+      security-events: write
+
+    steps:
+      - name: Repository checkout
+        uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+
+      - name: Differential ShellCheck
+        uses: redhat-plumbers-in-action/differential-shellcheck@v4
+        with:
+          severity: warning
+          token: ${{ secrets.GITHUB_TOKEN }}

CMakeLists.txt

@@ -90,8 +90,9 @@ list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules")
 option(ENABLE_KLEE_ASSERTS "Enable KLEE assertions" ON)
 if (ENABLE_KLEE_ASSERTS)
   message(STATUS "KLEE assertions enabled")
-  # We have to add the undefine to the flags, otherwise "-D-UDNDEBUG" will be added
-  list(APPEND KLEE_COMPONENT_CXX_FLAGS "-UDNDEBUG")
+  # We have to undefine `NDEBUG` (which CMake adds by default) using `FLAGS`
+  # and not `DEFINES` since `target_compile_definitions` does not support `-U`.
+  list(APPEND KLEE_COMPONENT_CXX_FLAGS "-UNDEBUG")
 else()
   message(STATUS "KLEE assertions disabled")
   list(APPEND KLEE_COMPONENT_CXX_DEFINES "-DNDEBUG")
@@ -319,6 +320,16 @@ if (NOT SQLITE3_FOUND)
   message( FATAL_ERROR "SQLite3 not found, please install" )
 endif()
 
+find_program(
+  SQLITE_CLI
+  NAMES "sqlite3"
+  DOC "Path to sqlite3 tool"
+)
+
+if (NOT SQLITE_CLI)
+  set(SQLITE_CLI "")
+endif()
+
 ################################################################################
 # Detect libcap
 ################################################################################

Dockerfile

@@ -1,11 +1,11 @@
-FROM klee/llvm:110_O_D_A_ubuntu_jammy-20230126 as llvm_base
-FROM klee/gtest:1.11.0_ubuntu_jammy-20230126 as gtest_base
-FROM klee/uclibc:klee_uclibc_v1.3_110_ubuntu_jammy-20230126 as uclibc_base
-FROM klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 as tcmalloc_base
-FROM klee/stp:2.3.3_ubuntu_jammy-20230126 as stp_base
-FROM klee/z3:4.8.15_ubuntu_jammy-20230126 as z3_base
-FROM klee/libcxx:110_ubuntu_jammy-20230126 as libcxx_base
-FROM klee/sqlite:3400100_ubuntu_jammy-20230126 as sqlite3_base
+FROM ghcr.io/klee/llvm:110_O_D_A_ubuntu_jammy-20230126 as llvm_base
+FROM ghcr.io/klee/gtest:1.11.0_ubuntu_jammy-20230126 as gtest_base
+FROM ghcr.io/klee/uclibc:klee_uclibc_v1.3_110_ubuntu_jammy-20230126 as uclibc_base
+FROM ghcr.io/klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 as tcmalloc_base
+FROM ghcr.io/klee/stp:2.3.3_ubuntu_jammy-20230126 as stp_base
+FROM ghcr.io/klee/z3:4.8.15_ubuntu_jammy-20230126 as z3_base
+FROM ghcr.io/klee/libcxx:110_ubuntu_jammy-20230126 as libcxx_base
+FROM ghcr.io/klee/sqlite:3400100_ubuntu_jammy-20230126 as sqlite3_base
 FROM llvm_base as intermediate
 COPY --from=gtest_base /tmp /tmp/
 COPY --from=uclibc_base /tmp /tmp/

include/klee/Core/BranchTypes.h

@@ -14,9 +14,9 @@
 
 /// \cond DO_NOT_DOCUMENT
 #define BRANCH_TYPES                                                           \
-  BTYPE(NONE, 0U)                                                              \
-  BTYPE(ConditionalBranch, 1U)                                                 \
-  BTYPE(IndirectBranch, 2U)                                                    \
+  BTYPEDEFAULT(NONE, 0U)                                                       \
+  BTYPE(Conditional, 1U)                                                       \
+  BTYPE(Indirect, 2U)                                                          \
   BTYPE(Switch, 3U)                                                            \
   BTYPE(Call, 4U)                                                              \
   BTYPE(MemOp, 5U)                                                             \
@@ -25,7 +25,7 @@
   BTYPE(Realloc, 8U)                                                           \
   BTYPE(Free, 9U)                                                              \
   BTYPE(GetVal, 10U)                                                           \
-  MARK(END, 10U)
+  BMARK(END, 10U)
 /// \endcond
 
 /** @enum BranchType
@@ -34,8 +34,8 @@
  *  | Value                           | Description                                                                                        |
  *  |---------------------------------|----------------------------------------------------------------------------------------------------|
  *  | `BranchType::NONE`              | default value (no branch)                                                                          |
- *  | `BranchType::ConditionalBranch` | branch caused by `br` instruction with symbolic condition                                          |
- *  | `BranchType::IndirectBranch`    | branch caused by `indirectbr` instruction with symbolic address                                    |
+ *  | `BranchType::Conditional`       | branch caused by `br` instruction with symbolic condition                                          |
+ *  | `BranchType::Indirect`          | branch caused by `indirectbr` instruction with symbolic address                                    |
  *  | `BranchType::Switch`            | branch caused by `switch` instruction with symbolic value                                          |
  *  | `BranchType::Call`              | branch caused by `call` with symbolic function pointer                                             |
  *  | `BranchType::MemOp`             | branch caused by memory operation with symbolic address (e.g. multiple resolutions, out-of-bounds) |
@@ -46,13 +46,20 @@
  *  | `BranchType::GetVal`            | branch caused by user-invoked concretization while seeding                                         |
  */
 enum class BranchType : std::uint8_t {
-/// \cond DO_NOT_DOCUMENT
-#define BTYPE(N,I) N = (I),
-#define MARK(N,I) N = (I),
+  /// \cond DO_NOT_DOCUMENT
+  #define BTYPEDEFAULT(N,I) N = (I),
+  #define BTYPE(N,I) N = (I),
+  #define BMARK(N,I) N = (I),
   BRANCH_TYPES
-#undef BTYPE
-#undef MARK
-/// \endcond
+  /// \endcond
 };
 
-#endif
+
+#undef BTYPEDEFAULT
+#undef BTYPE
+#undef BMARK
+#define BTYPEDEFAULT(N,I)
+#define BTYPE(N,I)
+#define BMARK(N,I)
+
+#endif

include/klee/Core/Interpreter.h

@@ -9,6 +9,7 @@
 #ifndef KLEE_INTERPRETER_H
 #define KLEE_INTERPRETER_H
 
+#include <cstdint>
 #include <map>
 #include <memory>
 #include <set>

include/klee/Core/TerminationTypes.h

@@ -12,51 +12,85 @@
 
 #include <cstdint>
 
+
+#define TERMINATION_CLASSES                                                    \
+  TCLASS(Exit, 1U)                                                             \
+  TCLASS(Early, 2U)                                                            \
+  TCLASS(SolverError, 3U)                                                      \
+  TCLASS(ProgramError, 4U)                                                     \
+  TCLASS(UserError, 5U)                                                        \
+  TCLASS(ExecutionError, 6U)                                                   \
+  TCLASS(EarlyAlgorithm, 7U)                                                   \
+  TCLASS(EarlyUser, 8U)
+
+///@brief Termination classes categorize termination types
+enum class StateTerminationClass : std::uint8_t {
+  /// \cond DO_NOT_DOCUMENT
+  #define TCLASS(N,I) N = (I),
+  TERMINATION_CLASSES
+  /// \endcond
+};
+
+
+// (Name, ID, file suffix)
 #define TERMINATION_TYPES                                                      \
   TTYPE(RUNNING, 0U, "")                                                       \
   TTYPE(Exit, 1U, "")                                                          \
-  MARK(NORMAL, 1U)                                                             \
-  TTYPE(Interrupted, 2U, "early")                                              \
-  TTYPE(MaxDepth, 3U, "early")                                                 \
-  TTYPE(OutOfMemory, 4U, "early")                                              \
-  TTYPE(OutOfStackMemory, 5U, "early")                                         \
-  MARK(EARLY, 5U)                                                              \
-  TTYPE(Solver, 8U, "solver.err")                                              \
-  MARK(SOLVERERR, 8U)                                                          \
-  TTYPE(Abort, 10U, "abort.err")                                               \
-  TTYPE(Assert, 11U, "assert.err")                                             \
-  TTYPE(BadVectorAccess, 12U, "bad_vector_access.err")                         \
-  TTYPE(Free, 13U, "free.err")                                                 \
-  TTYPE(Model, 14U, "model.err")                                               \
-  TTYPE(Overflow, 15U, "overflow.err")                                         \
-  TTYPE(Ptr, 16U, "ptr.err")                                                   \
-  TTYPE(ReadOnly, 17U, "read_only.err")                                        \
-  TTYPE(ReportError, 18U, "report_error.err")                                  \
-  TTYPE(InvalidBuiltin, 19U, "invalid_builtin_use.err")                        \
-  TTYPE(ImplicitTruncation, 20U, "implicit_truncation.err")                    \
-  TTYPE(ImplicitConversion, 21U, "implicit_conversion.err")                    \
-  TTYPE(UnreachableCall, 22U, "unreachable_call.err")                          \
-  TTYPE(MissingReturn, 23U, "missing_return.err")                              \
-  TTYPE(InvalidLoad, 24U, "invalid_load.err")                                  \
-  TTYPE(NullableAttribute, 25U, "nullable_attribute.err")                      \
-  MARK(PROGERR, 25U)                                                           \
-  TTYPE(User, 33U, "user.err")                                                 \
-  MARK(USERERR, 33U)                                                           \
-  TTYPE(Execution, 35U, "exec.err")                                            \
-  TTYPE(External, 36U, "external.err")                                         \
-  MARK(EXECERR, 36U)                                                           \
-  TTYPE(Replay, 37U, "")                                                       \
-  TTYPE(Merge, 38U, "")                                                        \
-  TTYPE(SilentExit, 39U, "")                                                   \
-  MARK(END, 39U)
+  TTMARK(EXIT, 1U)                                                             \
+  TTYPE(Interrupted, 10U, "early")                                             \
+  TTYPE(MaxDepth, 11U, "early")                                                \
+  TTYPE(OutOfMemory, 12U, "early")                                             \
+  TTYPE(OutOfStackMemory, 13U, "early")                                        \
+  TTMARK(EARLY, 13U)                                                           \
+  TTYPE(Solver, 20U, "solver.err")                                             \
+  TTMARK(SOLVERERR, 20U)                                                       \
+  TTYPE(Abort, 30U, "abort.err")                                               \
+  TTYPE(Assert, 31U, "assert.err")                                             \
+  TTYPE(BadVectorAccess, 32U, "bad_vector_access.err")                         \
+  TTYPE(Free, 33U, "free.err")                                                 \
+  TTYPE(Model, 34U, "model.err")                                               \
+  TTYPE(Overflow, 35U, "overflow.err")                                         \
+  TTYPE(Ptr, 36U, "ptr.err")                                                   \
+  TTYPE(ReadOnly, 37U, "read_only.err")                                        \
+  TTYPE(ReportError, 38U, "report_error.err")                                  \
+  TTYPE(InvalidBuiltin, 39U, "invalid_builtin_use.err")                        \
+  TTYPE(ImplicitTruncation, 40U, "implicit_truncation.err")                    \
+  TTYPE(ImplicitConversion, 41U, "implicit_conversion.err")                    \
+  TTYPE(UnreachableCall, 42U, "unreachable_call.err")                          \
+  TTYPE(MissingReturn, 43U, "missing_return.err")                              \
+  TTYPE(InvalidLoad, 44U, "invalid_load.err")                                  \
+  TTYPE(NullableAttribute, 45U, "nullable_attribute.err")                      \
+  TTMARK(PROGERR, 45U)                                                         \
+  TTYPE(User, 50U, "user.err")                                                 \
+  TTMARK(USERERR, 50U)                                                         \
+  TTYPE(Execution, 60U, "exec.err")                                            \
+  TTYPE(External, 61U, "external.err")                                         \
+  TTMARK(EXECERR, 61U)                                                         \
+  TTYPE(Replay, 70U, "")                                                       \
+  TTYPE(Merge, 71U, "")                                                        \
+  TTMARK(EARLYALGORITHM, 71U)                                                  \
+  TTYPE(SilentExit, 80U, "")                                                   \
+  TTMARK(EARLYUSER, 80U)                                                       \
+  TTMARK(END, 80U)
+
 
 ///@brief Reason an ExecutionState got terminated.
 enum class StateTerminationType : std::uint8_t {
-#define TTYPE(N,I,S) N = (I),
-#define MARK(N,I) N = (I),
+  /// \cond DO_NOT_DOCUMENT
+  #define TTYPE(N,I,S) N = (I),
+  #define TTMARK(N,I) N = (I),
   TERMINATION_TYPES
-#undef TTYPE
-#undef MARK
+  /// \endcond
 };
 
+
+// reset definitions
+
+#undef TCLASS
+#undef TTYPE
+#undef TTMARK
+#define TCLASS(N,I)
+#define TTYPE(N,I,S)
+#define TTMARK(N,I)
+
 #endif

include/klee/Solver/SolverStats.h

@@ -16,6 +16,7 @@ namespace klee {
 namespace stats {
 
   extern Statistic cexCacheTime;
+  extern Statistic solverQueries;
   extern Statistic queries;
   extern Statistic queriesInvalid;
   extern Statistic queriesValid;

include/klee/Statistics/Statistic.h

@@ -10,6 +10,7 @@
 #ifndef KLEE_STATISTIC_H
 #define KLEE_STATISTIC_H
 
+#include <cstdint>
 #include <string>
 
 namespace klee {