stats: add termination class stats

7 files changed, 162 insertions, 73 deletions

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