stats: add termination class stats

9 files changed, 243 insertions, 111 deletions

diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h
index 4fe5583a..25e5ef4a 100644
--- a/include/klee/Core/TerminationTypes.h
+++ b/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
diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp
index 54a9a697..48eb1e85 100644
--- a/lib/Core/CoreStats.cpp
+++ b/lib/Core/CoreStats.cpp
@@ -8,7 +8,6 @@
 //===----------------------------------------------------------------------===//
 
 #include "CoreStats.h"
-
 #include "klee/Support/ErrorHandling.h"
 
 
@@ -49,3 +48,10 @@ void stats::incBranchStat(BranchType reason, std::uint32_t value) {
                static_cast<std::uint8_t>(reason));
   }
 }
+
+
+// termination types
+
+#undef TCLASS
+#define TCLASS(Name,I) Statistic stats::termination ## Name("Termination"#Name, "Trm"#Name);
+TERMINATION_CLASSES
diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h
index 15850354..609e976a 100644
--- a/lib/Core/CoreStats.h
+++ b/lib/Core/CoreStats.h
@@ -11,6 +11,7 @@
 #define KLEE_CORESTATS_H
 
 #include "klee/Core/BranchTypes.h"
+#include "klee/Core/TerminationTypes.h"
 #include "klee/Statistics/Statistic.h"
 
 namespace klee {
@@ -55,6 +56,11 @@ namespace stats {
   #define BTYPE(Name,I) extern Statistic branches ## Name;
   BRANCH_TYPES
 
+  /// Count termination types.
+  #undef TCLASS
+  #define TCLASS(Name,I) extern Statistic termination ## Name;
+  TERMINATION_CLASSES
+
   /// Increase a branch statistic for the given reason by value.
   void incBranchStat(BranchType reason, std::uint32_t value);
 }
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e3af7348..a3f91f20 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -436,6 +436,7 @@ llvm::cl::bits<PrintDebugInstructionsType> DebugPrintInstructions(
                    "Log all instructions to file "
                    "instructions.txt in format [src, "
                    "inst_id]"),
+
         clEnumValN(FILE_COMPACT, "compact:file",
                    "Log all instructions to file instructions.txt in format "
                    "[inst_id]")),
@@ -953,7 +954,7 @@ void Executor::branch(ExecutionState &state,
     if (OnlyReplaySeeds) {
       for (unsigned i=0; i<N; ++i) {
         if (result[i] && !seedMap.count(result[i])) {
-          terminateStateEarly(*result[i], "Unseeded path during replay", StateTerminationType::Replay);
+          terminateStateEarlyAlgorithm(*result[i], "Unseeded path during replay", StateTerminationType::Replay);
           result[i] = nullptr;
         }
       }
@@ -3167,8 +3168,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     if (iIdx >= vt->getNumElements()) {
       // Out of bounds write
-      terminateStateOnError(state, "Out of bounds write when inserting element",
-                            StateTerminationType::BadVectorAccess);
+      terminateStateOnProgramError(state,
+                                   "Out of bounds write when inserting element",
+                                   StateTerminationType::BadVectorAccess);
       return;
     }
 
@@ -3208,8 +3210,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     if (iIdx >= vt->getNumElements()) {
       // Out of bounds read
-      terminateStateOnError(state, "Out of bounds read when extracting element",
-                            StateTerminationType::BadVectorAccess);
+      terminateStateOnProgramError(state,
+                                   "Out of bounds read when extracting element",
+                                   StateTerminationType::BadVectorAccess);
       return;
     }
 
@@ -3658,17 +3661,18 @@ static bool shouldWriteTest(const ExecutionState &state) {
 
 static std::string terminationTypeFileExtension(StateTerminationType type) {
   std::string ret;
-#define TTYPE(N,I,S) case StateTerminationType::N: ret = (S); break;
-#define MARK(N,I)
+  #undef TTYPE
+  #undef TTMARK
+  #define TTYPE(N,I,S) case StateTerminationType::N: ret = (S); break;
+  #define TTMARK(N,I)
   switch (type) {
-  TERMINATION_TYPES
+    TERMINATION_TYPES
   }
-#undef TTYPE
-#undef MARK
   return ret;
 };
 
 void Executor::terminateStateOnExit(ExecutionState &state) {
+  ++stats::terminationExit;
   if (shouldWriteTest(state) || (AlwaysOutputSeeds && seedMap.count(&state)))
     interpreterHandler->processTestCase(
         state, nullptr,
@@ -3679,20 +3683,35 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
 }
 
 void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
-                                   StateTerminationType terminationType) {
-  if ((terminationType <= StateTerminationType::EXECERR &&
-       shouldWriteTest(state)) ||
+                                   StateTerminationType reason) {
+  if (reason <= StateTerminationType::EARLY) {
+    assert(reason > StateTerminationType::EXIT);
+    ++stats::terminationEarly;
+  }
+
+  if ((reason <= StateTerminationType::EARLY && shouldWriteTest(state)) ||
       (AlwaysOutputSeeds && seedMap.count(&state))) {
     interpreterHandler->processTestCase(
         state, (message + "\n").str().c_str(),
-        terminationTypeFileExtension(terminationType).c_str());
+        terminationTypeFileExtension(reason).c_str());
   }
 
   terminateState(state);
 }
 
-void Executor::terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message) {
-  terminateStateOnError(state, message, StateTerminationType::User, "");
+void Executor::terminateStateEarlyAlgorithm(ExecutionState &state,
+                                            const llvm::Twine &message,
+                                            StateTerminationType reason) {
+  assert(reason > StateTerminationType::EXECERR &&
+         reason <= StateTerminationType::EARLYALGORITHM);
+  ++stats::terminationEarlyAlgorithm;
+  terminateStateEarly(state, message, reason);
+}
+
+void Executor::terminateStateEarlyUser(ExecutionState &state,
+                                       const llvm::Twine &message) {
+  ++stats::terminationEarlyUser;
+  terminateStateEarly(state, message, StateTerminationType::SilentExit);
 }
 
 const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
@@ -3793,15 +3812,36 @@ void Executor::terminateStateOnError(ExecutionState &state,
 
 void Executor::terminateStateOnExecError(ExecutionState &state,
                                          const llvm::Twine &message,
-                                         const llvm::Twine &info) {
-  terminateStateOnError(state, message, StateTerminationType::Execution, info);
+                                         StateTerminationType reason) {
+  assert(reason > StateTerminationType::USERERR &&
+         reason <= StateTerminationType::EXECERR);
+  ++stats::terminationExecutionError;
+  terminateStateOnError(state, message, reason, "");
+}
+
+void Executor::terminateStateOnProgramError(ExecutionState &state,
+                                            const llvm::Twine &message,
+                                            StateTerminationType reason,
+                                            const llvm::Twine &info,
+                                            const char *suffix) {
+  assert(reason > StateTerminationType::SOLVERERR &&
+         reason <= StateTerminationType::PROGERR);
+  ++stats::terminationProgramError;
+  terminateStateOnError(state, message, reason, info, suffix);
 }
 
 void Executor::terminateStateOnSolverError(ExecutionState &state,
                                            const llvm::Twine &message) {
+  ++stats::terminationSolverError;
   terminateStateOnError(state, message, StateTerminationType::Solver, "");
 }
 
+void Executor::terminateStateOnUserError(ExecutionState &state,
+                                         const llvm::Twine &message) {
+  ++stats::terminationUserError;
+  terminateStateOnError(state, message, StateTerminationType::User, "");
+}
+
 // XXX shoot me
 static const char *okExternalsList[] = { "printf", 
                                          "fprintf", 
@@ -3945,14 +3985,15 @@ void Executor::callExternalFunction(ExecutionState &state,
 
   bool success = externalDispatcher->executeCall(callable, target->inst, args);
   if (!success) {
-    terminateStateOnError(state, "failed external call: " + callable->getName(),
-                          StateTerminationType::External);
+    terminateStateOnExecError(state,
+                              "failed external call: " + callable->getName(),
+                              StateTerminationType::External);
     return;
   }
 
   if (!state.addressSpace.copyInConcretes()) {
-    terminateStateOnError(state, "external modified read-only object",
-                          StateTerminationType::External);
+    terminateStateOnExecError(state, "external modified read-only object",
+                              StateTerminationType::External);
     return;
   }
 
@@ -4135,8 +4176,9 @@ void Executor::executeAlloc(ExecutionState &state,
           ExprPPrinter::printOne(info, "  size expr", size);
           info << "  concretization : " << example << "\n";
           info << "  unbound example: " << tmp << "\n";
-          terminateStateOnError(*hugeSize.second, "concretized symbolic size",
-                                StateTerminationType::Model, info.str());
+          terminateStateOnProgramError(*hugeSize.second,
+                                       "concretized symbolic size",
+                                       StateTerminationType::Model, info.str());
         }
       }
     }
@@ -4165,13 +4207,13 @@ void Executor::executeFree(ExecutionState &state,
            ie = rl.end(); it != ie; ++it) {
       const MemoryObject *mo = it->first.first;
       if (mo->isLocal) {
-        terminateStateOnError(*it->second, "free of alloca",
-                              StateTerminationType::Free,
-                              getAddressInfo(*it->second, address));
+        terminateStateOnProgramError(*it->second, "free of alloca",
+                                     StateTerminationType::Free,
+                                     getAddressInfo(*it->second, address));
       } else if (mo->isGlobal) {
-        terminateStateOnError(*it->second, "free of global",
-                              StateTerminationType::Free,
-                              getAddressInfo(*it->second, address));
+        terminateStateOnProgramError(*it->second, "free of global",
+                                     StateTerminationType::Free,
+                                     getAddressInfo(*it->second, address));
       } else {
         it->second->deallocate(mo);
         it->second->addressSpace.unbindObject(mo);
@@ -4215,14 +4257,15 @@ void Executor::resolveExact(ExecutionState &state,
       auto locinfo = unbound->heapAllocator.location_info(ptr, 1);
       if (locinfo == LocationInfo::LI_AllocatedOrQuarantined &&
           locinfo.getBaseAddress() == ptr && name == "free") {
-        terminateStateOnError(*unbound, "memory error: double free",
-                              StateTerminationType::Ptr,
-                              getAddressInfo(*unbound, p));
+        terminateStateOnProgramError(*unbound, "memory error: double free",
+                                     StateTerminationType::Ptr,
+                                     getAddressInfo(*unbound, p));
         return;
       }
     }
-    terminateStateOnError(*unbound, "memory error: invalid pointer: " + name,
-                          StateTerminationType::Ptr, getAddressInfo(*unbound, p));
+    terminateStateOnProgramError(
+        *unbound, "memory error: invalid pointer: " + name,
+        StateTerminationType::Ptr, getAddressInfo(*unbound, p));
   }
 }
 
@@ -4280,8 +4323,8 @@ void Executor::executeMemoryOperation(ExecutionState &state,
       const ObjectState *os = op.second;
       if (isWrite) {
         if (os->readOnly) {
-          terminateStateOnError(state, "memory error: object read only",
-                                StateTerminationType::ReadOnly);
+          terminateStateOnProgramError(state, "memory error: object read only",
+                                       StateTerminationType::ReadOnly);
         } else {
           ObjectState *wos = state.addressSpace.getWriteable(mo, os);
           wos->write(offset, value);
@@ -4324,8 +4367,8 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     if (bound) {
       if (isWrite) {
         if (os->readOnly) {
-          terminateStateOnError(*bound, "memory error: object read only",
-                                StateTerminationType::ReadOnly);
+          terminateStateOnProgramError(*bound, "memory error: object read only",
+                                       StateTerminationType::ReadOnly);
         } else {
           ObjectState *wos = bound->addressSpace.getWriteable(mo, os);
           wos->write(mo->getOffsetExpr(address), value);
@@ -4350,9 +4393,9 @@ void Executor::executeMemoryOperation(ExecutionState &state,
         std::uintptr_t ptrval = CE->getZExtValue();
         auto ptr = reinterpret_cast<void *>(ptrval);
         if (ptrval < MemoryManager::pageSize) {
-          terminateStateOnError(*unbound, "memory error: null page access",
-                                StateTerminationType::Ptr,
-                                getAddressInfo(*unbound, address));
+          terminateStateOnProgramError(
+              *unbound, "memory error: null page access",
+              StateTerminationType::Ptr, getAddressInfo(*unbound, address));
           return;
         } else if (MemoryManager::isDeterministic) {
           using kdalloc::LocationInfo;
@@ -4364,17 +4407,17 @@ void Executor::executeMemoryOperation(ExecutionState &state,
             auto baseExpr = Expr::createPointer(base);
             ObjectPair op;
             if (!unbound->addressSpace.resolveOne(baseExpr, op)) {
-              terminateStateOnError(*unbound, "memory error: use after free",
-                                    StateTerminationType::Ptr,
-                                    getAddressInfo(*unbound, address));
+              terminateStateOnProgramError(
+                  *unbound, "memory error: use after free",
+                  StateTerminationType::Ptr, getAddressInfo(*unbound, address));
               return;
             }
           }
         }
       }
-      terminateStateOnError(*unbound, "memory error: out of bound pointer",
-                            StateTerminationType::Ptr,
-                            getAddressInfo(*unbound, address));
+      terminateStateOnProgramError(
+          *unbound, "memory error: out of bound pointer",
+          StateTerminationType::Ptr, getAddressInfo(*unbound, address));
     }
   }
 }
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index c821b987..28a7d56d 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -410,7 +410,8 @@ private:
   const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state,
       llvm::Instruction** lastInstruction);
 
-  /// Remove state from queue and delete state
+  /// Remove state from queue and delete state. This function should only be
+  /// used in the termination functions below.
   void terminateState(ExecutionState &state);
 
   /// Call exit handler and terminate state normally
@@ -420,21 +421,43 @@ private:
   /// Call exit handler and terminate state early
   /// (e.g. due to state merging or memory pressure)
   void terminateStateEarly(ExecutionState &state, const llvm::Twine &message,
-                           StateTerminationType terminationType);
+                           StateTerminationType reason);
+
+  /// Call exit handler and terminate state early
+  /// (e.g. caused by the applied algorithm as in state merging or replaying)
+  void terminateStateEarlyAlgorithm(ExecutionState &state,
+                                    const llvm::Twine &message,
+                                    StateTerminationType reason);
+
+  /// Call exit handler and terminate state early
+  /// (e.g. due to klee_silent_exit issued by user)
+  void terminateStateEarlyUser(ExecutionState &state,
+                               const llvm::Twine &message);
+
+  /// Call error handler and terminate state in case of errors.
+  /// The underlying function of all error-handling termination functions
+  /// below. This function should only be used in the termination functions
+  /// below.
+  void terminateStateOnError(ExecutionState &state,
+                                    const llvm::Twine &message,
+                                    StateTerminationType reason,
+                                    const llvm::Twine &longMessage = "",
+                                    const char *suffix = nullptr);
 
   /// Call error handler and terminate state in case of program errors
   /// (e.g. free()ing globals, out-of-bound accesses)
-  void terminateStateOnError(ExecutionState &state, const llvm::Twine &message,
-                             StateTerminationType terminationType,
-                             const llvm::Twine &longMessage = "",
-                             const char *suffix = nullptr);
+  void terminateStateOnProgramError(ExecutionState &state,
+                                    const llvm::Twine &message,
+                                    StateTerminationType reason,
+                                    const llvm::Twine &longMessage = "",
+                                    const char *suffix = nullptr);
 
   /// Call error handler and terminate state in case of execution errors
   /// (things that should not be possible, like illegal instruction or
   /// unlowered intrinsic, or unsupported intrinsics, like inline assembly)
-  void terminateStateOnExecError(ExecutionState &state,
-                                 const llvm::Twine &message,
-                                 const llvm::Twine &info = "");
+  void terminateStateOnExecError(
+      ExecutionState &state, const llvm::Twine &message,
+      StateTerminationType = StateTerminationType::Execution);
 
   /// Call error handler and terminate state in case of solver errors
   /// (solver error or timeout)
diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp
index 00677541..3034dd74 100644
--- a/lib/Core/MergeHandler.cpp
+++ b/lib/Core/MergeHandler.cpp
@@ -106,7 +106,7 @@ void MergeHandler::addClosedState(ExecutionState *es,
 
     for (auto& mState: cpv) {
       if (mState->merge(*es)) {
-        executor->terminateStateEarly(*es, "merged state.", StateTerminationType::Merge);
+        executor->terminateStateEarlyAlgorithm(*es, "merged state.", StateTerminationType::Merge);
         executor->mergingSearcher->inCloseMerge.erase(es);
         mergedSuccessful = true;
         break;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index f4b09f36..7996499c 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -286,8 +286,8 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state,
                                          KInstruction *target,
                                          std::vector<ref<Expr>> &arguments) {
   assert(arguments.size() == 0 && "invalid number of arguments to abort");
-  executor.terminateStateOnError(state, "abort failure",
-                                 StateTerminationType::Abort);
+  executor.terminateStateOnProgramError(state, "abort failure",
+                                        StateTerminationType::Abort);
 }
 
 void SpecialFunctionHandler::handleExit(ExecutionState &state,
@@ -301,14 +301,14 @@ void SpecialFunctionHandler::handleSilentExit(
     ExecutionState &state, KInstruction *target,
     std::vector<ref<Expr>> &arguments) {
   assert(arguments.size() == 1 && "invalid number of arguments to exit");
-  executor.terminateStateEarly(state, "", StateTerminationType::SilentExit);
+  executor.terminateStateEarlyUser(state, "");
 }
 
 void SpecialFunctionHandler::handleAssert(ExecutionState &state,
                                           KInstruction *target,
                                           std::vector<ref<Expr>> &arguments) {
   assert(arguments.size() == 3 && "invalid number of arguments to _assert");
-  executor.terminateStateOnError(
+  executor.terminateStateOnProgramError(
       state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
       StateTerminationType::Assert);
 }
@@ -318,7 +318,7 @@ void SpecialFunctionHandler::handleAssertFail(
     std::vector<ref<Expr>> &arguments) {
   assert(arguments.size() == 4 &&
          "invalid number of arguments to __assert_fail");
-  executor.terminateStateOnError(
+  executor.terminateStateOnProgramError(
       state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
       StateTerminationType::Assert);
 }
@@ -330,7 +330,7 @@ void SpecialFunctionHandler::handleReportError(
          "invalid number of arguments to klee_report_error");
 
   // arguments[0,1,2,3] are file, line, message, suffix
-  executor.terminateStateOnError(
+  executor.terminateStateOnProgramError(
       state, readStringAtAddress(state, arguments[2]),
       StateTerminationType::ReportError, "",
       readStringAtAddress(state, arguments[3]).c_str());
@@ -759,19 +759,17 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
     ObjectPair op;
 
     if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) {
-      executor.terminateStateOnError(state,
-                                     "check_memory_access: memory error",
-                                     StateTerminationType::Ptr,
-                                     executor.getAddressInfo(state, address));
+      executor.terminateStateOnProgramError(
+          state, "check_memory_access: memory error", StateTerminationType::Ptr,
+          executor.getAddressInfo(state, address));
     } else {
       ref<Expr> chk = 
         op.first->getBoundsCheckPointer(address, 
                                         cast<ConstantExpr>(size)->getZExtValue());
       if (!chk->isTrue()) {
-        executor.terminateStateOnError(state,
-                                       "check_memory_access: memory error",
-                                       StateTerminationType::Ptr,
-                                       executor.getAddressInfo(state, address));
+        executor.terminateStateOnProgramError(
+            state, "check_memory_access: memory error",
+            StateTerminationType::Ptr, executor.getAddressInfo(state, address));
       }
     }
   }
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 80723f8a..9f92a127 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -12,6 +12,7 @@
 #include "ExecutionState.h"
 
 #include "klee/Config/Version.h"
+#include "klee/Core/TerminationTypes.h"
 #include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
@@ -432,6 +433,8 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue,
 void StatsTracker::writeStatsHeader() {
   #undef BTYPE
   #define BTYPE(Name,I) << "Branches" #Name " INTEGER,"
+  #undef TCLASS
+  #define TCLASS(Name,I) << "Termination" #Name " INTEGER,"
   std::ostringstream create, insert;
   create << "CREATE TABLE stats ("
          << "Instructions INTEGER,"
@@ -461,6 +464,7 @@ void StatsTracker::writeStatsHeader() {
          << "Allocations INTEGER,"
          << "States INTEGER,"
          BRANCH_TYPES
+         TERMINATION_CLASSES
          << "ArrayHashTime INTEGER"
          << ')';
   char *zErrMsg = nullptr;
@@ -476,6 +480,8 @@ void StatsTracker::writeStatsHeader() {
    */
   #undef BTYPE
   #define BTYPE(Name, I) << "Branches" #Name ","
+  #undef TCLASS
+  #define TCLASS(Name, I) << "Termination" #Name ","
   insert << "INSERT OR FAIL INTO stats ("
          << "Instructions,"
          << "FullBranches,"
@@ -504,10 +510,13 @@ void StatsTracker::writeStatsHeader() {
          << "Allocations,"
          << "States,"
          BRANCH_TYPES
+         TERMINATION_CLASSES
          << "ArrayHashTime"
          << ')';
   #undef BTYPE
   #define BTYPE(Name, I) << "?,"
+  #undef TCLASS
+  #define TCLASS(Name, I) << "?,"
   insert << " VALUES ("
          << "?,"
          << "?,"
@@ -536,6 +545,7 @@ void StatsTracker::writeStatsHeader() {
          << "?,"
          << "?,"
          BRANCH_TYPES
+         TERMINATION_CLASSES
          << "? "
          << ')';
 
@@ -551,6 +561,8 @@ time::Span StatsTracker::elapsed() {
 void StatsTracker::writeStatsLine() {
   #undef BTYPE
   #define BTYPE(Name,I) sqlite3_bind_int64(insertStmt, arg++, stats::branches ## Name);
+  #undef TCLASS
+  #define TCLASS(Name,I) sqlite3_bind_int64(insertStmt, arg++, stats::termination ## Name);
   int arg = 1;
   sqlite3_bind_int64(insertStmt, arg++, stats::instructions);
   sqlite3_bind_int64(insertStmt, arg++, fullBranches);
@@ -579,6 +591,7 @@ void StatsTracker::writeStatsLine() {
   sqlite3_bind_int64(insertStmt, arg++, stats::allocations);
   sqlite3_bind_int64(insertStmt, arg++, ExecutionState::getLastID());
   BRANCH_TYPES
+  TERMINATION_CLASSES
 #ifdef KLEE_ARRAY_DEBUG
   sqlite3_bind_int64(insertStmt, arg++, stats::arrayHashTime);
 #else
diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats
index 20d75adb..f681a06f 100755
--- a/tools/klee-stats/klee-stats
+++ b/tools/klee-stats/klee-stats
@@ -75,6 +75,15 @@ Legend = [
     ('BrRealloc', 'number of forks caused by symbolic reallocation size', "BranchesRealloc"),
     ('BrFree', 'number of forks caused by freeing a symbolic pointer', "BranchesFree"),
     ('BrGetVal', 'number of forks caused by user-invoked concretization while seeding', "BranchesGetVal"),
+    # - termination classes
+    ('TermExit', 'number of states that reached end of execution path', "TerminationExit"),
+    ('TermEarly', 'number of early terminated states (e.g. due to memory pressure, state limt)', "TerminationEarly"),
+    ('TermSolverErr', 'number of states terminated due to solver errors', "TerminationSolverError"),
+    ('TermProgrErr', 'number of states terminated due to program errors (e.g. division by zero)', "TerminationProgramError"),
+    ('TermUserErr', 'number of states terminated due to user errors (e.g. misuse of KLEE API)', "TerminationUserError"),
+    ('TermExecErr', 'number of states terminated due to execution errors (e.g. unsupported intrinsics)', "TerminationExecutionError"),
+    ('TermEarlyAlgo', 'number of state terminations required by algorithm (e.g. state merging or replaying)', "TerminationEarlyAlgorithm"),
+    ('TermEarlyUser', 'number of states terminated via klee_silent_exit()', "TerminationEarlyUser"),
     # - debugging
     ('TArrayHash(s)', 'time spent hashing arrays (if KLEE_ARRAY_DEBUG enabled, otherwise -1)', "ArrayHashTime"),
     ('TFork(s)', 'time spent forking states', "ForkTime"),