stats: add branch type stats

4 files changed, 157 insertions, 112 deletions

diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp
index 06b8b930..54a9a697 100644
--- a/lib/Core/CoreStats.cpp
+++ b/lib/Core/CoreStats.cpp
@@ -9,6 +9,9 @@
 
 #include "CoreStats.h"
 
+#include "klee/Support/ErrorHandling.h"
+
+
 using namespace klee;
 
 Statistic stats::allocations("Allocations", "Alloc");
@@ -28,3 +31,21 @@ Statistic stats::solverTime("SolverTime", "Stime");
 Statistic stats::states("States", "States");
 Statistic stats::trueBranches("TrueBranches", "Bt");
 Statistic stats::uncoveredInstructions("UncoveredInstructions", "Iuncov");
+
+
+// branch stats and setter
+
+#undef BTYPE
+#define BTYPE(Name,I) Statistic stats::branches ## Name("Branches"#Name, "Br"#Name);
+BRANCH_TYPES
+
+void stats::incBranchStat(BranchType reason, std::uint32_t value) {
+#undef BTYPE
+#define BTYPE(N,I) case BranchType::N : stats::branches ## N += value; break;
+  switch (reason) {
+    BRANCH_TYPES
+  default:
+    klee_error("Illegal branch type in incBranchStat(): %hhu",
+               static_cast<std::uint8_t>(reason));
+  }
+}
diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h
index c0dcac7d..15850354 100644
--- a/lib/Core/CoreStats.h
+++ b/lib/Core/CoreStats.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_CORESTATS_H
 #define KLEE_CORESTATS_H
 
+#include "klee/Core/BranchTypes.h"
 #include "klee/Statistics/Statistic.h"
 
 namespace klee {
@@ -49,6 +50,13 @@ namespace stats {
   /// distance to a function return.
   extern Statistic minDistToReturn;
 
+  /// Count branch types in execution tree. Inhibited branches are ignored.
+  #undef BTYPE
+  #define BTYPE(Name,I) extern Statistic branches ## Name;
+  BRANCH_TYPES
+
+  /// 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 c3a10144..e3af7348 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -900,6 +900,7 @@ void Executor::branch(ExecutionState &state,
     stats::inhibitedForks += N - 1;
   } else {
     stats::forks += N-1;
+    stats::incBranchStat(reason, N-1);
 
     // XXX do proper balance or keep random?
     result.push_back(&state);
@@ -1180,6 +1181,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
     }
 
     processTree->attach(current.ptreeNode, falseState, trueState, reason);
+    stats::incBranchStat(reason, 1);
 
     if (pathWriter) {
       // Need to update the pathOS.id field of falseState, otherwise the same id
@@ -2196,7 +2198,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       ref<Expr> cond = eval(ki, 0, state).value;
 
       cond = optimizer.optimizeExpr(cond, false);
-      Executor::StatePair branches = fork(state, cond, false, BranchType::ConditionalBranch);
+      Executor::StatePair branches = fork(state, cond, false, BranchType::Conditional);
 
       // NOTE: There is a hidden dependency here, markBranchVisited
       // requires that we still be in the context of the branch
@@ -2269,7 +2271,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     // fork states
     std::vector<ExecutionState *> branches;
-    branch(state, expressions, branches, BranchType::IndirectBranch);
+    branch(state, expressions, branches, BranchType::Indirect);
 
     // terminate error state
     if (result) {
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 51a0b73c..80723f8a 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -430,35 +430,38 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue,
 }
 
 void StatsTracker::writeStatsHeader() {
+  #undef BTYPE
+  #define BTYPE(Name,I) << "Branches" #Name " INTEGER,"
   std::ostringstream create, insert;
   create << "CREATE TABLE stats ("
-             << "Instructions INTEGER,"
-             << "FullBranches INTEGER,"
-             << "PartialBranches INTEGER,"
-             << "NumBranches INTEGER,"
-             << "UserTime REAL,"
-             << "NumStates INTEGER,"
-             << "MallocUsage INTEGER,"
-             << "Queries INTEGER,"
-             << "SolverQueries INTEGER,"
-             << "NumQueryConstructs INTEGER,"
-             << "WallTime REAL,"
-             << "CoveredInstructions INTEGER,"
-             << "UncoveredInstructions INTEGER,"
-             << "QueryTime INTEGER,"
-             << "SolverTime INTEGER,"
-             << "CexCacheTime INTEGER,"
-             << "ForkTime INTEGER,"
-             << "ResolveTime INTEGER,"
-             << "QueryCacheMisses INTEGER,"
-             << "QueryCacheHits INTEGER,"
-             << "QueryCexCacheMisses INTEGER,"
-             << "QueryCexCacheHits INTEGER,"
-             << "InhibitedForks INTEGER,"
-             << "ExternalCalls INTEGER,"
-             << "Allocations INTEGER,"
-             << "States INTEGER,"
-             << "ArrayHashTime INTEGER"
+         << "Instructions INTEGER,"
+         << "FullBranches INTEGER,"
+         << "PartialBranches INTEGER,"
+         << "NumBranches INTEGER,"
+         << "UserTime REAL,"
+         << "NumStates INTEGER,"
+         << "MallocUsage INTEGER,"
+         << "Queries INTEGER,"
+         << "SolverQueries INTEGER,"
+         << "NumQueryConstructs INTEGER,"
+         << "WallTime REAL,"
+         << "CoveredInstructions INTEGER,"
+         << "UncoveredInstructions INTEGER,"
+         << "QueryTime INTEGER,"
+         << "SolverTime INTEGER,"
+         << "CexCacheTime INTEGER,"
+         << "ForkTime INTEGER,"
+         << "ResolveTime INTEGER,"
+         << "QueryCacheMisses INTEGER,"
+         << "QueryCacheHits INTEGER,"
+         << "QueryCexCacheMisses INTEGER,"
+         << "QueryCexCacheHits INTEGER,"
+         << "InhibitedForks INTEGER,"
+         << "ExternalCalls INTEGER,"
+         << "Allocations INTEGER,"
+         << "States INTEGER,"
+         BRANCH_TYPES
+         << "ArrayHashTime INTEGER"
          << ')';
   char *zErrMsg = nullptr;
   if(sqlite3_exec(statsFile, create.str().c_str(), nullptr, nullptr, &zErrMsg)) {
@@ -471,62 +474,69 @@ void StatsTracker::writeStatsHeader() {
    * happen, but if it does this statement will fail with SQLITE_CONSTRAINT error. If this happens you should either
    * remove the constraints or consider using `IGNORE` mode.
    */
+  #undef BTYPE
+  #define BTYPE(Name, I) << "Branches" #Name ","
   insert << "INSERT OR FAIL INTO stats ("
-             << "Instructions,"
-             << "FullBranches,"
-             << "PartialBranches,"
-             << "NumBranches,"
-             << "UserTime,"
-             << "NumStates,"
-             << "MallocUsage,"
-             << "Queries,"
-             << "SolverQueries,"
-             << "NumQueryConstructs,"
-             << "WallTime,"
-             << "CoveredInstructions,"
-             << "UncoveredInstructions,"
-             << "QueryTime,"
-             << "SolverTime,"
-             << "CexCacheTime,"
-             << "ForkTime,"
-             << "ResolveTime,"
-             << "QueryCacheMisses,"
-             << "QueryCacheHits,"
-             << "QueryCexCacheMisses,"
-             << "QueryCexCacheHits,"
-             << "InhibitedForks,"
-             << "ExternalCalls,"
-             << "Allocations,"
-             << "States,"
-             << "ArrayHashTime"
-         << ") VALUES ("
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "?,"
-             << "? "
+         << "Instructions,"
+         << "FullBranches,"
+         << "PartialBranches,"
+         << "NumBranches,"
+         << "UserTime,"
+         << "NumStates,"
+         << "MallocUsage,"
+         << "Queries,"
+         << "SolverQueries,"
+         << "NumQueryConstructs,"
+         << "WallTime,"
+         << "CoveredInstructions,"
+         << "UncoveredInstructions,"
+         << "QueryTime,"
+         << "SolverTime,"
+         << "CexCacheTime,"
+         << "ForkTime,"
+         << "ResolveTime,"
+         << "QueryCacheMisses,"
+         << "QueryCacheHits,"
+         << "QueryCexCacheMisses,"
+         << "QueryCexCacheHits,"
+         << "InhibitedForks,"
+         << "ExternalCalls,"
+         << "Allocations,"
+         << "States,"
+         BRANCH_TYPES
+         << "ArrayHashTime"
+         << ')';
+  #undef BTYPE
+  #define BTYPE(Name, I) << "?,"
+  insert << " VALUES ("
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         << "?,"
+         BRANCH_TYPES
+         << "? "
          << ')';
 
   if(sqlite3_prepare_v2(statsFile, insert.str().c_str(), -1, &insertStmt, nullptr) != SQLITE_OK) {
@@ -539,36 +549,40 @@ time::Span StatsTracker::elapsed() {
 }
 
 void StatsTracker::writeStatsLine() {
-  sqlite3_bind_int64(insertStmt, 1, stats::instructions);
-  sqlite3_bind_int64(insertStmt, 2, fullBranches);
-  sqlite3_bind_int64(insertStmt, 3, partialBranches);
-  sqlite3_bind_int64(insertStmt, 4, numBranches);
-  sqlite3_bind_int64(insertStmt, 5, time::getUserTime().toMicroseconds());
-  sqlite3_bind_int64(insertStmt, 6, executor.states.size());
-  sqlite3_bind_int64(insertStmt, 7, util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize());
-  sqlite3_bind_int64(insertStmt, 8, stats::queries);
-  sqlite3_bind_int64(insertStmt, 9, stats::solverQueries);
-  sqlite3_bind_int64(insertStmt, 10, stats::queryConstructs);
-  sqlite3_bind_int64(insertStmt, 11, elapsed().toMicroseconds());
-  sqlite3_bind_int64(insertStmt, 12, stats::coveredInstructions);
-  sqlite3_bind_int64(insertStmt, 13, stats::uncoveredInstructions);
-  sqlite3_bind_int64(insertStmt, 14, stats::queryTime);
-  sqlite3_bind_int64(insertStmt, 15, stats::solverTime);
-  sqlite3_bind_int64(insertStmt, 16, stats::cexCacheTime);
-  sqlite3_bind_int64(insertStmt, 17, stats::forkTime);
-  sqlite3_bind_int64(insertStmt, 18, stats::resolveTime);
-  sqlite3_bind_int64(insertStmt, 19, stats::queryCacheMisses);
-  sqlite3_bind_int64(insertStmt, 10, stats::queryCacheHits);
-  sqlite3_bind_int64(insertStmt, 21, stats::queryCexCacheMisses);
-  sqlite3_bind_int64(insertStmt, 22, stats::queryCexCacheHits);
-  sqlite3_bind_int64(insertStmt, 23, stats::inhibitedForks);
-  sqlite3_bind_int64(insertStmt, 24, stats::externalCalls);
-  sqlite3_bind_int64(insertStmt, 25, stats::allocations);
-  sqlite3_bind_int64(insertStmt, 26, ExecutionState::getLastID());
+  #undef BTYPE
+  #define BTYPE(Name,I) sqlite3_bind_int64(insertStmt, arg++, stats::branches ## Name);
+  int arg = 1;
+  sqlite3_bind_int64(insertStmt, arg++, stats::instructions);
+  sqlite3_bind_int64(insertStmt, arg++, fullBranches);
+  sqlite3_bind_int64(insertStmt, arg++, partialBranches);
+  sqlite3_bind_int64(insertStmt, arg++, numBranches);
+  sqlite3_bind_int64(insertStmt, arg++, time::getUserTime().toMicroseconds());
+  sqlite3_bind_int64(insertStmt, arg++, executor.states.size());
+  sqlite3_bind_int64(insertStmt, arg++, util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize());
+  sqlite3_bind_int64(insertStmt, arg++, stats::queries);
+  sqlite3_bind_int64(insertStmt, arg++, stats::solverQueries);
+  sqlite3_bind_int64(insertStmt, arg++, stats::queryConstructs);
+  sqlite3_bind_int64(insertStmt, arg++, elapsed().toMicroseconds());
+  sqlite3_bind_int64(insertStmt, arg++, stats::coveredInstructions);
+  sqlite3_bind_int64(insertStmt, arg++, stats::uncoveredInstructions);
+  sqlite3_bind_int64(insertStmt, arg++, stats::queryTime);
+  sqlite3_bind_int64(insertStmt, arg++, stats::solverTime);
+  sqlite3_bind_int64(insertStmt, arg++, stats::cexCacheTime);
+  sqlite3_bind_int64(insertStmt, arg++, stats::forkTime);
+  sqlite3_bind_int64(insertStmt, arg++, stats::resolveTime);
+  sqlite3_bind_int64(insertStmt, arg++, stats::queryCacheMisses);
+  sqlite3_bind_int64(insertStmt, arg++, stats::queryCacheHits);
+  sqlite3_bind_int64(insertStmt, arg++, stats::queryCexCacheMisses);
+  sqlite3_bind_int64(insertStmt, arg++, stats::queryCexCacheHits);
+  sqlite3_bind_int64(insertStmt, arg++, stats::inhibitedForks);
+  sqlite3_bind_int64(insertStmt, arg++, stats::externalCalls);
+  sqlite3_bind_int64(insertStmt, arg++, stats::allocations);
+  sqlite3_bind_int64(insertStmt, arg++, ExecutionState::getLastID());
+  BRANCH_TYPES
 #ifdef KLEE_ARRAY_DEBUG
-  sqlite3_bind_int64(insertStmt, 27, stats::arrayHashTime);
+  sqlite3_bind_int64(insertStmt, arg++, stats::arrayHashTime);
 #else
-  sqlite3_bind_int64(insertStmt, 27, -1LL);
+  sqlite3_bind_int64(insertStmt, arg++, -1LL);
 #endif
   int errCode = sqlite3_step(insertStmt);
   if(errCode != SQLITE_DONE) klee_error("Error writing stats data: %s", sqlite3_errmsg(statsFile));