stats: add termination class stats

1 files changed, 32 insertions, 9 deletions

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)