Introduce termination categories

Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.

5 files changed, 296 insertions, 261 deletions

diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h
new file mode 100644
index 00000000..592cd3cb
--- /dev/null
+++ b/include/klee/Core/TerminationTypes.h
@@ -0,0 +1,55 @@
+//===-- TerminationTypes.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_TERMINATIONTYPES_H
+#define KLEE_TERMINATIONTYPES_H
+
+#include <cstdint>
+
+#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")                                  \
+  MARK(PROGERR, 18U)                                                           \
+  TTYPE(User, 23U, "user.err")                                                 \
+  MARK(USERERR, 23U)                                                           \
+  TTYPE(Execution, 25U, "exec.err")                                            \
+  TTYPE(External, 26U, "external.err")                                         \
+  MARK(EXECERR, 26U)                                                           \
+  TTYPE(Replay, 27U, "")                                                       \
+  TTYPE(Merge, 28U, "")                                                        \
+  TTYPE(SilentExit, 29U, "")                                                   \
+  MARK(END, 29U)
+
+///@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),
+  TERMINATION_TYPES
+#undef TTYPE
+#undef MARK
+};
+
+#endif
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 3d6ea4ae..fdb8e3b8 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -267,35 +267,34 @@ cl::opt<std::string>
 
 /*** Termination criteria options ***/
 
-cl::list<Executor::TerminateReason> ExitOnErrorType(
+cl::list<StateTerminationType> ExitOnErrorType(
     "exit-on-error-type",
-    cl::desc(
-        "Stop execution after reaching a specified condition (default=false)"),
+    cl::desc("Stop execution after reaching a specified condition (default=false)"),
     cl::values(
-        clEnumValN(Executor::Abort, "Abort", "The program crashed"),
-        clEnumValN(Executor::Assert, "Assert", "An assertion was hit"),
-        clEnumValN(Executor::BadVectorAccess, "BadVectorAccess",
+        clEnumValN(StateTerminationType::Abort, "Abort",
+                   "The program crashed (reached abort()/klee_abort())"),
+        clEnumValN(StateTerminationType::Assert, "Assert",
+                   "An assertion was hit"),
+        clEnumValN(StateTerminationType::BadVectorAccess, "BadVectorAccess",
                    "Vector accessed out of bounds"),
-        clEnumValN(Executor::Exec, "Exec",
+        clEnumValN(StateTerminationType::Execution, "Execution",
                    "Trying to execute an unexpected instruction"),
-        clEnumValN(Executor::External, "External",
+        clEnumValN(StateTerminationType::External, "External",
                    "External objects referenced"),
-        clEnumValN(Executor::Free, "Free", "Freeing invalid memory"),
-        clEnumValN(Executor::Model, "Model", "Memory model limit hit"),
-        clEnumValN(Executor::Overflow, "Overflow", "An overflow occurred"),
-        clEnumValN(Executor::Ptr, "Ptr", "Pointer error"),
-        clEnumValN(Executor::ReadOnly, "ReadOnly", "Write to read-only memory"),
-        clEnumValN(Executor::ReportError, "ReportError",
+        clEnumValN(StateTerminationType::Free, "Free",
+                   "Freeing invalid memory"),
+        clEnumValN(StateTerminationType::Model, "Model",
+                   "Memory model limit hit"),
+        clEnumValN(StateTerminationType::Overflow, "Overflow",
+                   "An overflow occurred"),
+        clEnumValN(StateTerminationType::Ptr, "Ptr", "Pointer error"),
+        clEnumValN(StateTerminationType::ReadOnly, "ReadOnly",
+                   "Write to read-only memory"),
+        clEnumValN(StateTerminationType::ReportError, "ReportError",
                    "klee_report_error called"),
-        clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"),
-#ifdef SUPPORT_KLEE_EH_CXX
-        clEnumValN(Executor::UncaughtException, "UncaughtException",
-                   "Exception was not caught"),
-        clEnumValN(Executor::UnexpectedException, "UnexpectedException",
-                   "An unexpected exception was thrown"),
-#endif
-        clEnumValN(Executor::Unhandled, "Unhandled",
-                   "Unhandled instruction hit") KLEE_LLVM_CL_VAL_END),
+        clEnumValN(StateTerminationType::User, "User",
+                   "Wrong klee_* functions invocation")
+        KLEE_LLVM_CL_VAL_END),
     cl::ZeroOrMore,
     cl::cat(TerminationCat));
 
@@ -436,27 +435,6 @@ cl::opt<bool> DebugCheckForImpliedValues(
 extern "C" unsigned dumpStates, dumpPTree;
 unsigned dumpStates = 0, dumpPTree = 0;
 
-const char *Executor::TerminateReasonNames[] = {
-  [ Abort ] = "abort",
-  [ Assert ] = "assert",
-  [ BadVectorAccess ] = "bad_vector_access",
-  [ Exec ] = "exec",
-  [ External ] = "external",
-  [ Free ] = "free",
-  [ Model ] = "model",
-  [ Overflow ] = "overflow",
-  [ Ptr ] = "ptr",
-  [ ReadOnly ] = "readonly",
-  [ ReportError ] = "reporterror",
-  [ User ] = "user",
-#ifdef SUPPORT_KLEE_EH_CXX
-  [ UncaughtException ] = "uncaught_exception",
-  [ UnexpectedException ] = "unexpected_exception",
-#endif
-  [ Unhandled ] = "xxx",
-};
-
-
 Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                    InterpreterHandler *ih)
     : Interpreter(opts), interpreterHandler(ih), searcher(0),
@@ -960,10 +938,10 @@ void Executor::branch(ExecutionState &state,
     if (OnlyReplaySeeds) {
       for (unsigned i=0; i<N; ++i) {
         if (result[i] && !seedMap.count(result[i])) {
-          terminateState(*result[i]);
-          result[i] = NULL;
+          terminateStateEarly(*result[i], "Unseeded path during replay", StateTerminationType::Replay);
+          result[i] = nullptr;
         }
-      } 
+      }
     }
   }
 
@@ -1047,7 +1025,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
   solver->setTimeout(time::Span());
   if (!success) {
     current.pc = current.prevPC;
-    terminateStateEarly(current, "Query timed out (fork).");
+    terminateStateOnSolverError(current, "Query timed out (fork).");
     return StatePair(nullptr, nullptr);
   }
 
@@ -1210,8 +1188,8 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
 
     // Kinda gross, do we even really still want this option?
     if (MaxDepth && MaxDepth<=trueState->depth) {
-      terminateStateEarly(*trueState, "max-depth exceeded.");
-      terminateStateEarly(*falseState, "max-depth exceeded.");
+      terminateStateEarly(*trueState, "max-depth exceeded.", StateTerminationType::MaxDepth);
+      terminateStateEarly(*falseState, "max-depth exceeded.", StateTerminationType::MaxDepth);
       return StatePair(nullptr, nullptr);
     }
 
@@ -1489,9 +1467,8 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state,
       } else if (current_clause->isNullValue()) {
         ti_addr = 0;
       } else {
-        terminateStateOnError(
-            state, "Internal: Clause is not a bitcast or null (catch-all)",
-            Exec);
+        terminateStateOnExecError(
+            state, "Internal: Clause is not a bitcast or null (catch-all)");
         stateTerminated = true;
         return nullptr;
       }
@@ -1515,8 +1492,8 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state,
 
         if (num_elements >=
             std::numeric_limits<decltype(serialized_num_elements)>::max()) {
-          terminateStateOnError(
-              state, "Internal: too many elements in landingpad filter", Exec);
+          terminateStateOnExecError(
+              state, "Internal: too many elements in landingpad filter");
           stateTerminated = true;
           return nullptr;
         }
@@ -1529,10 +1506,9 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state,
           llvm::BitCastOperator const *bitcast =
               dyn_cast<llvm::BitCastOperator>(v);
           if (!bitcast) {
-            terminateStateOnError(state,
-                                  "Internal: expected value inside a "
-                                  "filter-clause to be a bitcast",
-                                  Exec);
+            terminateStateOnExecError(state,
+                                      "Internal: expected value inside a "
+                                      "filter-clause to be a bitcast");
             stateTerminated = true;
             return nullptr;
           }
@@ -1540,10 +1516,9 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state,
           llvm::GlobalValue const *clause_value =
               dyn_cast<GlobalValue>(bitcast->getOperand(0));
           if (!clause_value) {
-            terminateStateOnError(state,
-                                  "Internal: expected value inside a "
-                                  "filter-clause bitcast to be a GlobalValue",
-                                  Exec);
+            terminateStateOnExecError(state,
+                                      "Internal: expected value inside a "
+                                      "filter-clause bitcast to be a GlobalValue");
             stateTerminated = true;
             return nullptr;
           }
@@ -1876,7 +1851,7 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       // well.
     default:
       klee_warning("unimplemented intrinsic: %s", f->getName().data());
-      terminateStateOnError(state, "unimplemented intrinsic", Unhandled);
+      terminateStateOnExecError(state, "unimplemented intrinsic");
       return;
     }
 
@@ -1887,7 +1862,7 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
     // Check if maximum stack size was reached.
     // We currently only count the number of stack frames
     if (RuntimeMaxStackFrames && state.stack.size() > RuntimeMaxStackFrames) {
-      terminateStateEarly(state, "Maximum stack size reached.");
+      terminateStateEarly(state, "Maximum stack size reached.", StateTerminationType::OutOfStackMemory);
       klee_warning("Maximum stack size reached.");
       return;
     }
@@ -1913,14 +1888,12 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
         klee_warning_once(f, "calling %s with extra arguments.",
                           f->getName().data());
       } else if (callingArgs < funcArgs) {
-        terminateStateOnError(state, "calling function with too few arguments",
-                              User);
+        terminateStateOnUserError(state, "calling function with too few arguments");
         return;
       }
     } else {
       if (callingArgs < funcArgs) {
-        terminateStateOnError(state, "calling function with too few arguments",
-                              User);
+        terminateStateOnUserError(state, "calling function with too few arguments");
         return;
       }
 
@@ -3198,9 +3171,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     ConstantExpr *cIdx = dyn_cast<ConstantExpr>(idx);
     if (cIdx == NULL) {
-      terminateStateOnError(
-          state, "InsertElement, support for symbolic index not implemented",
-          Unhandled);
+      terminateStateOnExecError(
+          state, "InsertElement, support for symbolic index not implemented");
       return;
     }
     uint64_t iIdx = cIdx->getZExtValue();
@@ -3214,7 +3186,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (iIdx >= vt->getNumElements()) {
       // Out of bounds write
       terminateStateOnError(state, "Out of bounds write when inserting element",
-                            BadVectorAccess);
+                            StateTerminationType::BadVectorAccess);
       return;
     }
 
@@ -3240,9 +3212,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     ConstantExpr *cIdx = dyn_cast<ConstantExpr>(idx);
     if (cIdx == NULL) {
-      terminateStateOnError(
-          state, "ExtractElement, support for symbolic index not implemented",
-          Unhandled);
+      terminateStateOnExecError(
+          state, "ExtractElement, support for symbolic index not implemented");
       return;
     }
     uint64_t iIdx = cIdx->getZExtValue();
@@ -3256,7 +3227,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (iIdx >= vt->getNumElements()) {
       // Out of bounds read
       terminateStateOnError(state, "Out of bounds read when extracting element",
-                            BadVectorAccess);
+                            StateTerminationType::BadVectorAccess);
       return;
     }
 
@@ -3509,7 +3480,7 @@ bool Executor::checkMemoryUsage() {
       idx = theRNG.getInt32() % N;
 
     std::swap(arr[idx], arr[N - 1]);
-    terminateStateEarly(*arr[N - 1], "Memory limit exceeded.");
+    terminateStateEarly(*arr[N - 1], "Memory limit exceeded.", StateTerminationType::OutOfMemory);
   }
 
   return false;
@@ -3523,7 +3494,7 @@ void Executor::doDumpStates() {
 
   klee_message("halting execution, dumping remaining states");
   for (const auto &state : states)
-    terminateStateEarly(*state, "Execution halting.");
+    terminateStateEarly(*state, "Execution halting.", StateTerminationType::Interrupted);
   updateStates(nullptr);
 }
 
@@ -3707,23 +3678,49 @@ void Executor::terminateState(ExecutionState &state) {
   }
 }
 
-void Executor::terminateStateEarly(ExecutionState &state, 
-                                   const Twine &message) {
-  if (!OnlyOutputStatesCoveringNew || state.coveredNew ||
-      (AlwaysOutputSeeds && seedMap.count(&state)))
-    interpreterHandler->processTestCase(state, (message + "\n").str().c_str(),
-                                        "early");
-  terminateState(state);
+static bool shouldWriteTest(const ExecutionState &state) {
+  return !OnlyOutputStatesCoveringNew || state.coveredNew;
 }
 
+static std::string terminationTypeFileExtension(StateTerminationType type) {
+  std::string ret;
+#define TTYPE(N,I,S) case StateTerminationType::N: ret = (S); break;
+#define MARK(N,I)
+  switch (type) {
+  TERMINATION_TYPES
+  }
+#undef TTYPE
+#undef MARK
+  return ret;
+};
+
 void Executor::terminateStateOnExit(ExecutionState &state) {
-  if (!OnlyOutputStatesCoveringNew || state.coveredNew || 
-      (AlwaysOutputSeeds && seedMap.count(&state)))
-    interpreterHandler->processTestCase(state, 0, 0);
+  if (shouldWriteTest(state) || (AlwaysOutputSeeds && seedMap.count(&state)))
+    interpreterHandler->processTestCase(
+        state, nullptr,
+        terminationTypeFileExtension(StateTerminationType::Exit).c_str());
+
   interpreterHandler->incPathsCompleted();
   terminateState(state);
 }
 
+void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
+                                   StateTerminationType terminationType) {
+  if ((terminationType <= StateTerminationType::EXECERR &&
+       shouldWriteTest(state)) ||
+      (AlwaysOutputSeeds && seedMap.count(&state))) {
+    interpreterHandler->processTestCase(
+        state, (message + "\n").str().c_str(),
+        terminationTypeFileExtension(terminationType).c_str());
+  }
+
+  terminateState(state);
+}
+
+void Executor::terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message) {
+  terminateStateOnError(state, message, StateTerminationType::User, "");
+}
+
 const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
     Instruction ** lastInstruction) {
   // unroll the stack of the applications state and find
@@ -3767,30 +3764,24 @@ const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const Execut
   return *ii;
 }
 
-bool Executor::shouldExitOn(enum TerminateReason termReason) {
-  std::vector<TerminateReason>::iterator s = ExitOnErrorType.begin();
-  std::vector<TerminateReason>::iterator e = ExitOnErrorType.end();
-
-  for (; s != e; ++s)
-    if (termReason == *s)
-      return true;
-
-  return false;
+bool shouldExitOn(StateTerminationType reason) {
+  auto it = std::find(ExitOnErrorType.begin(), ExitOnErrorType.end(), reason);
+  return it != ExitOnErrorType.end();
 }
 
 void Executor::terminateStateOnError(ExecutionState &state,
                                      const llvm::Twine &messaget,
-                                     enum TerminateReason termReason,
-                                     const char *suffix,
-                                     const llvm::Twine &info) {
+                                     StateTerminationType terminationType,
+                                     const llvm::Twine &info,
+                                     const char *suffix) {
   std::string message = messaget.str();
   static std::set< std::pair<Instruction*, std::string> > emittedErrors;
   Instruction * lastInst;
   const InstructionInfo &ii = getLastNonKleeInternalInstruction(state, &lastInst);
-  
+
   if (EmitAllErrors ||
       emittedErrors.insert(std::make_pair(lastInst, message)).second) {
-    if (ii.file != "") {
+    if (!ii.file.empty()) {
       klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str());
     } else {
       klee_message("ERROR: (location information missing) %s", message.c_str());
@@ -3801,7 +3792,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
     std::string MsgString;
     llvm::raw_string_ostream msg(MsgString);
     msg << "Error: " << message << '\n';
-    if (ii.file != "") {
+    if (!ii.file.empty()) {
       msg << "File: " << ii.file << '\n'
           << "Line: " << ii.line << '\n'
           << "assembly.ll line: " << ii.assemblyLine << '\n'
@@ -3811,25 +3802,32 @@ void Executor::terminateStateOnError(ExecutionState &state,
     state.dumpStack(msg);
 
     std::string info_str = info.str();
-    if (info_str != "")
+    if (!info_str.empty())
       msg << "Info: \n" << info_str;
 
-    std::string suffix_buf;
-    if (!suffix) {
-      suffix_buf = TerminateReasonNames[termReason];
-      suffix_buf += ".err";
-      suffix = suffix_buf.c_str();
-    }
-
-    interpreterHandler->processTestCase(state, msg.str().c_str(), suffix);
+    const std::string ext = terminationTypeFileExtension(terminationType);
+    // use user provided suffix from klee_report_error()
+    const char * file_suffix = suffix ? suffix : ext.c_str();
+    interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix);
   }
-    
+
   terminateState(state);
 
-  if (shouldExitOn(termReason))
+  if (shouldExitOn(terminationType))
     haltExecution = true;
 }
 
+void Executor::terminateStateOnExecError(ExecutionState &state,
+                                         const llvm::Twine &message,
+                                         const llvm::Twine &info) {
+  terminateStateOnError(state, message, StateTerminationType::Execution, info);
+}
+
+void Executor::terminateStateOnSolverError(ExecutionState &state,
+                                           const llvm::Twine &message) {
+  terminateStateOnError(state, message, StateTerminationType::Solver, "");
+}
+
 // XXX shoot me
 static const char *okExternalsList[] = { "printf", 
                                          "fprintf", 
@@ -3851,7 +3849,7 @@ void Executor::callExternalFunction(ExecutionState &state,
       !okExternals.count(function->getName().str())) {
     klee_warning("Disallowed call to external function: %s\n",
                function->getName().str().c_str());
-    terminateStateOnError(state, "external calls disallowed", User);
+    terminateStateOnUserError(state, "external calls disallowed");
     return;
   }
 
@@ -3886,8 +3884,8 @@ void Executor::callExternalFunction(ExecutionState &state,
         ce->toMemory(&args[wordIndex]);
         wordIndex += (ce->getWidth()+63)/64;
       } else {
-        terminateStateOnExecError(state, 
-                                  "external call with symbolic argument: " + 
+        terminateStateOnExecError(state,
+                                  "external call with symbolic argument: " +
                                   function->getName());
         return;
       }
@@ -3938,13 +3936,13 @@ void Executor::callExternalFunction(ExecutionState &state,
   bool success = externalDispatcher->executeCall(function, target->inst, args);
   if (!success) {
     terminateStateOnError(state, "failed external call: " + function->getName(),
-                          External);
+                          StateTerminationType::External);
     return;
   }
 
   if (!state.addressSpace.copyInConcretes()) {
     terminateStateOnError(state, "external modified read-only object",
-                          External);
+                          StateTerminationType::External);
     return;
   }
 
@@ -4118,7 +4116,7 @@ void Executor::executeAlloc(ExecutionState &state,
           info << "  concretization : " << example << "\n";
           info << "  unbound example: " << tmp << "\n";
           terminateStateOnError(*hugeSize.second, "concretized symbolic size",
-                                Model, NULL, info.str());
+                                StateTerminationType::Model, info.str());
         }
       }
     }
@@ -4146,10 +4144,12 @@ 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", Free, NULL,
+        terminateStateOnError(*it->second, "free of alloca",
+                              StateTerminationType::Free,
                               getAddressInfo(*it->second, address));
       } else if (mo->isGlobal) {
-        terminateStateOnError(*it->second, "free of global", Free, NULL,
+        terminateStateOnError(*it->second, "free of global",
+                              StateTerminationType::Free,
                               getAddressInfo(*it->second, address));
       } else {
         it->second->addressSpace.unbindObject(mo);
@@ -4186,7 +4186,7 @@ void Executor::resolveExact(ExecutionState &state,
 
   if (unbound) {
     terminateStateOnError(*unbound, "memory error: invalid pointer: " + name,
-                          Ptr, NULL, getAddressInfo(*unbound, p));
+                          StateTerminationType::Ptr, getAddressInfo(*unbound, p));
   }
 }
 
@@ -4236,7 +4236,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     solver->setTimeout(time::Span());
     if (!success) {
       state.pc = state.prevPC;
-      terminateStateEarly(state, "Query timed out (bounds check).");
+      terminateStateOnSolverError(state, "Query timed out (bounds check).");
       return;
     }
 
@@ -4245,7 +4245,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
       if (isWrite) {
         if (os->readOnly) {
           terminateStateOnError(state, "memory error: object read only",
-                                ReadOnly);
+                                StateTerminationType::ReadOnly);
         } else {
           ObjectState *wos = state.addressSpace.getWriteable(mo, os);
           wos->write(offset, value);
@@ -4289,7 +4289,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
       if (isWrite) {
         if (os->readOnly) {
           terminateStateOnError(*bound, "memory error: object read only",
-                                ReadOnly);
+                                StateTerminationType::ReadOnly);
         } else {
           ObjectState *wos = bound->addressSpace.getWriteable(mo, os);
           wos->write(mo->getOffsetExpr(address), value);
@@ -4308,10 +4308,11 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   // XXX should we distinguish out of bounds and overlapped cases?
   if (unbound) {
     if (incomplete) {
-      terminateStateEarly(*unbound, "Query timed out (resolve).");
+      terminateStateOnSolverError(*unbound, "Query timed out (resolve).");
     } else {
-      terminateStateOnError(*unbound, "memory error: out of bound pointer", Ptr,
-                            NULL, getAddressInfo(*unbound, address));
+      terminateStateOnError(*unbound, "memory error: out of bound pointer",
+                            StateTerminationType::Ptr,
+                            getAddressInfo(*unbound, address));
     }
   }
 }
@@ -4346,8 +4347,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
             std::vector<unsigned char> &values = si.assignment.bindings[array];
             values = std::vector<unsigned char>(mo->size, '\0');
           } else if (!AllowSeedExtension) {
-            terminateStateOnError(state, "ran out of inputs during seeding",
-                                  User);
+            terminateStateOnUserError(state, "ran out of inputs during seeding");
             break;
           }
         } else {
@@ -4361,7 +4361,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
 		<< " vs " << obj->name << "[" << obj->numBytes << "]"
 		<< " in test\n";
 
-            terminateStateOnError(state, msg.str(), User);
+            terminateStateOnUserError(state, msg.str());
             break;
           } else {
             std::vector<unsigned char> &values = si.assignment.bindings[array];
@@ -4378,11 +4378,11 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
   } else {
     ObjectState *os = bindObjectInState(state, mo, false);
     if (replayPosition >= replayKTest->numObjects) {
-      terminateStateOnError(state, "replay count mismatch", User);
+      terminateStateOnUserError(state, "replay count mismatch");
     } else {
       KTestObject *obj = &replayKTest->objects[replayPosition++];
       if (obj->numBytes != mo->size) {
-        terminateStateOnError(state, "replay size mismatch", User);
+        terminateStateOnUserError(state, "replay size mismatch");
       } else {
         for (unsigned i=0; i<mo->size; i++)
           os->write8(i, obj->bytes[i]);
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 987edf47..e9763547 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -20,6 +20,7 @@
 
 #include "klee/ADT/RNG.h"
 #include "klee/Core/Interpreter.h"
+#include "klee/Core/TerminationTypes.h"
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/ArrayExprOptimizer.h"
 #include "klee/Module/Cell.h"
@@ -98,32 +99,10 @@ class Executor : public Interpreter {
 public:
   typedef std::pair<ExecutionState*,ExecutionState*> StatePair;
 
-  enum TerminateReason {
-    Abort,
-    Assert,
-    BadVectorAccess,
-    Exec,
-    External,
-    Free,
-    Model,
-    Overflow,
-    Ptr,
-    ReadOnly,
-    ReportError,
-    User,
-#ifdef SUPPORT_KLEE_EH_CXX
-    UncaughtException,
-    UnexpectedException,
-#endif
-    Unhandled,
-  };
-
   /// The random number generator.
   RNG theRNG;
 
 private:
-  static const char *TerminateReasonNames[];
-
   std::unique_ptr<KModule> kmodule;
   InterpreterHandler *interpreterHandler;
   Searcher *searcher;
@@ -430,28 +409,41 @@ private:
   const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state,
       llvm::Instruction** lastInstruction);
 
-  bool shouldExitOn(enum TerminateReason termReason);
-
-  // remove state from queue and delete
+  /// Remove state from queue and delete state
   void terminateState(ExecutionState &state);
-  // call exit handler and terminate state
-  void terminateStateEarly(ExecutionState &state, const llvm::Twine &message);
-  // call exit handler and terminate state
+
+  /// Call exit handler and terminate state normally
+  /// (end of execution path)
   void terminateStateOnExit(ExecutionState &state);
-  // call error handler and terminate state
+
+  /// 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);
+
+  /// 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,
-                             enum TerminateReason termReason,
-                             const char *suffix = NULL,
-                             const llvm::Twine &longMessage = "");
-
-  // call error handler and terminate state, for execution errors
-  // (things that should not be possible, like illegal instruction or
-  // unlowered instrinsic, or are unsupported, like inline assembly)
-  void terminateStateOnExecError(ExecutionState &state, 
+                             StateTerminationType terminationType,
+                             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="") {
-    terminateStateOnError(state, message, Exec, NULL, info);
-  }
+                                 const llvm::Twine &info = "");
+
+  /// Call error handler and terminate state in case of solver errors
+  /// (solver error or timeout)
+  void terminateStateOnSolverError(ExecutionState &state,
+                                   const llvm::Twine &message);
+
+  /// Call error handler and terminate state for user errors
+  /// (e.g. wrong usage of klee.h API)
+  void terminateStateOnUserError(ExecutionState &state,
+                                 const llvm::Twine &message);
 
   /// bindModuleConstants - Initialize the module constant table.
   void bindModuleConstants();
diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp
index 578b1b51..00677541 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->terminateState(*es);
+        executor->terminateStateEarly(*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 94c4dc3c..5c0246b3 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -246,16 +246,14 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
   ObjectPair op;
   addressExpr = executor.toUnique(state, addressExpr);
   if (!isa<ConstantExpr>(addressExpr)) {
-    executor.terminateStateOnError(
-        state, "Symbolic string pointer passed to one of the klee_ functions",
-        Executor::TerminateReason::User);
+    executor.terminateStateOnUserError(
+        state, "Symbolic string pointer passed to one of the klee_ functions");
     return "";
   }
   ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr);
   if (!state.addressSpace.resolveOne(address, op)) {
-    executor.terminateStateOnError(
-        state, "Invalid string pointer passed to one of the klee_ functions",
-        Executor::TerminateReason::User);
+    executor.terminateStateOnUserError(
+        state, "Invalid string pointer passed to one of the klee_ functions");
     return "";
   }
   const MemoryObject *mo = op.first;
@@ -292,54 +290,57 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
 /****/
 
 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", Executor::Abort);
+                                         KInstruction *target,
+                                         std::vector<ref<Expr>> &arguments) {
+  assert(arguments.size() == 0 && "invalid number of arguments to abort");
+  executor.terminateStateOnError(state, "abort failure",
+                                 StateTerminationType::Abort);
 }
 
 void SpecialFunctionHandler::handleExit(ExecutionState &state,
-                           KInstruction *target,
-                           std::vector<ref<Expr> > &arguments) {
-  assert(arguments.size()==1 && "invalid number of arguments to exit");
+                                        KInstruction *target,
+                                        std::vector<ref<Expr>> &arguments) {
+  assert(arguments.size() == 1 && "invalid number of arguments to exit");
   executor.terminateStateOnExit(state);
 }
 
-void SpecialFunctionHandler::handleSilentExit(ExecutionState &state,
-                                              KInstruction *target,
-                                              std::vector<ref<Expr> > &arguments) {
-  assert(arguments.size()==1 && "invalid number of arguments to exit");
-  executor.terminateState(state);
+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);
 }
 
 void SpecialFunctionHandler::handleAssert(ExecutionState &state,
                                           KInstruction *target,
-                                          std::vector<ref<Expr> > &arguments) {
-  assert(arguments.size()==3 && "invalid number of arguments to _assert");  
-  executor.terminateStateOnError(state,
-				 "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
-				 Executor::Assert);
+                                          std::vector<ref<Expr>> &arguments) {
+  assert(arguments.size() == 3 && "invalid number of arguments to _assert");
+  executor.terminateStateOnError(
+      state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
+      StateTerminationType::Assert);
 }
 
-void SpecialFunctionHandler::handleAssertFail(ExecutionState &state,
-                                              KInstruction *target,
-                                              std::vector<ref<Expr> > &arguments) {
-  assert(arguments.size()==4 && "invalid number of arguments to __assert_fail");
-  executor.terminateStateOnError(state,
-				 "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
-				 Executor::Assert);
+void SpecialFunctionHandler::handleAssertFail(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
+  assert(arguments.size() == 4 &&
+         "invalid number of arguments to __assert_fail");
+  executor.terminateStateOnError(
+      state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
+      StateTerminationType::Assert);
 }
 
-void SpecialFunctionHandler::handleReportError(ExecutionState &state,
-                                               KInstruction *target,
-                                               std::vector<ref<Expr> > &arguments) {
-  assert(arguments.size()==4 && "invalid number of arguments to klee_report_error");
-  
-  // arguments[0], arguments[1] are file, line
-  executor.terminateStateOnError(state,
-				 readStringAtAddress(state, arguments[2]),
-				 Executor::ReportError,
-				 readStringAtAddress(state, arguments[3]).c_str());
+void SpecialFunctionHandler::handleReportError(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
+  assert(arguments.size() == 4 &&
+         "invalid number of arguments to klee_report_error");
+
+  // arguments[0,1,2,3] are file, line, message, suffix
+  executor.terminateStateOnError(
+      state, readStringAtAddress(state, arguments[2]),
+      StateTerminationType::ReportError, "",
+      readStringAtAddress(state, arguments[3]).c_str());
 }
 
 void SpecialFunctionHandler::handleOpenMerge(ExecutionState &state,
@@ -431,9 +432,8 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state,
                                             KInstruction *target,
                                             std::vector<ref<Expr>> &arguments) {
   if (arguments.size() != 2) {
-    executor.terminateStateOnError(state,
-      "Incorrect number of arguments to memalign(size_t alignment, size_t size)",
-      Executor::User);
+    executor.terminateStateOnUserError(state,
+      "Incorrect number of arguments to memalign(size_t alignment, size_t size)");
     return;
   }
 
@@ -444,9 +444,7 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state,
   auto alignmentConstExpr = dyn_cast<ConstantExpr>(alignmentExpr);
 
   if (!alignmentConstExpr) {
-    executor.terminateStateOnError(state,
-      "Could not determine size of symbolic alignment",
-      Executor::User);
+    executor.terminateStateOnUserError(state, "Could not determine size of symbolic alignment");
     return;
   }
 
@@ -470,10 +468,8 @@ void SpecialFunctionHandler::handleEhUnwindRaiseExceptionImpl(
          "invalid number of arguments to _klee_eh_Unwind_RaiseException_impl");
 
   ref<ConstantExpr> exceptionObject = dyn_cast<ConstantExpr>(arguments[0]);
-  if (!exceptionObject) {
-    executor.terminateStateOnError(state,
-                                   "Internal error: Symbolic exception pointer",
-                                   Executor::Unhandled);
+  if (!exceptionObject.get()) {
+    executor.terminateStateOnExecError(state, "Internal error: Symbolic exception pointer");
     return;
   }
 
@@ -520,9 +516,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state,
     if (SilentKleeAssume) {
       executor.terminateState(state);
     } else {
-      executor.terminateStateOnError(state,
-                                     "invalid klee_assume call (provably false)",
-                                     Executor::User);
+      executor.terminateStateOnUserError(
+          state, "invalid klee_assume call (provably false)");
     }
   } else {
     executor.addConstraint(state, e);
@@ -579,9 +574,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
     state.forkDisabled = CE->isZero();
   } else {
-    executor.terminateStateOnError(state, 
-                                   "klee_set_forking requires a constant arg",
-                                   Executor::User);
+    executor.terminateStateOnUserError(state, "klee_set_forking requires a constant arg");
   }
 }
 
@@ -678,8 +671,7 @@ void SpecialFunctionHandler::handleGetErrno(ExecutionState &state,
   bool resolved = state.addressSpace.resolveOne(
       ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result);
   if (!resolved)
-    executor.terminateStateOnError(state, "Could not resolve address for errno",
-                                   Executor::User);
+    executor.terminateStateOnUserError(state, "Could not resolve address for errno");
   executor.bindLocal(target, state, result.second->read(0, Expr::Int32));
 }
 
@@ -770,16 +762,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
   ref<Expr> address = executor.toUnique(state, arguments[0]);
   ref<Expr> size = executor.toUnique(state, arguments[1]);
   if (!isa<ConstantExpr>(address) || !isa<ConstantExpr>(size)) {
-    executor.terminateStateOnError(state, 
-                                   "check_memory_access requires constant args",
-				   Executor::User);
+    executor.terminateStateOnUserError(state, "check_memory_access requires constant args");
   } else {
     ObjectPair op;
 
     if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) {
       executor.terminateStateOnError(state,
                                      "check_memory_access: memory error",
-				     Executor::Ptr, NULL,
+                                     StateTerminationType::Ptr,
                                      executor.getAddressInfo(state, address));
     } else {
       ref<Expr> chk = 
@@ -788,7 +778,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
       if (!chk->isTrue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
-				       Executor::Ptr, NULL,
+                                       StateTerminationType::Ptr,
                                        executor.getAddressInfo(state, address));
       }
     }
@@ -827,7 +817,8 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
   std::string name;
 
   if (arguments.size() != 3) {
-    executor.terminateStateOnError(state, "Incorrect number of arguments to klee_make_symbolic(void*, size_t, char*)", Executor::User);
+    executor.terminateStateOnUserError(state,
+        "Incorrect number of arguments to klee_make_symbolic(void*, size_t, char*)");
     return;
   }
 
@@ -850,8 +841,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
     ExecutionState *s = it->second;
     
     if (old->readOnly) {
-      executor.terminateStateOnError(*s, "cannot make readonly object symbolic",
-                                     Executor::User);
+      executor.terminateStateOnUserError(*s, "cannot make readonly object symbolic");
       return;
     } 
 
@@ -868,9 +858,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
     if (res) {
       executor.executeMakeSymbolic(*s, mo, name);
     } else {      
-      executor.terminateStateOnError(*s, 
-                                     "wrong size given to klee_make_symbolic[_name]", 
-                                     Executor::User);
+      executor.terminateStateOnUserError(*s, "wrong size given to klee_make_symbolic[_name]");
     }
   }
 }
@@ -892,30 +880,30 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
   }
 }
 
-void SpecialFunctionHandler::handleAddOverflow(ExecutionState &state,
-                                               KInstruction *target,
-                                               std::vector<ref<Expr> > &arguments) {
+void SpecialFunctionHandler::handleAddOverflow(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
   executor.terminateStateOnError(state, "overflow on addition",
-                                 Executor::Overflow);
+                                 StateTerminationType::Overflow);
 }
 
-void SpecialFunctionHandler::handleSubOverflow(ExecutionState &state,
-                                               KInstruction *target,
-                                               std::vector<ref<Expr> > &arguments) {
+void SpecialFunctionHandler::handleSubOverflow(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
   executor.terminateStateOnError(state, "overflow on subtraction",
-                                 Executor::Overflow);
+                                 StateTerminationType::Overflow);
 }
 
-void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state,
-                                               KInstruction *target,
-                                               std::vector<ref<Expr> > &arguments) {
+void SpecialFunctionHandler::handleMulOverflow(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
   executor.terminateStateOnError(state, "overflow on multiplication",
-                                 Executor::Overflow);
+                                 StateTerminationType::Overflow);
 }
 
-void SpecialFunctionHandler::handleDivRemOverflow(ExecutionState &state,
-                                               KInstruction *target,
-                                               std::vector<ref<Expr> > &arguments) {
+void SpecialFunctionHandler::handleDivRemOverflow(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr>> &arguments) {
   executor.terminateStateOnError(state, "overflow on division or remainder",
-                                 Executor::Overflow);
+                                 StateTerminationType::Overflow);
 }