stats: add InhibitedForks

5 files changed, 13 insertions, 2 deletions

diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp
index 2589d7da..720fa1b2 100644
--- a/lib/Core/CoreStats.cpp
+++ b/lib/Core/CoreStats.cpp
@@ -16,6 +16,7 @@ Statistic stats::coveredInstructions("CoveredInstructions", "Icov");
 Statistic stats::falseBranches("FalseBranches", "Bf");
 Statistic stats::forkTime("ForkTime", "Ftime");
 Statistic stats::forks("Forks", "Forks");
+Statistic stats::inhibitedForks("InhibitedForks", "InhibForks");
 Statistic stats::instructionRealTime("InstructionRealTimes", "Ireal");
 Statistic stats::instructionTime("InstructionTimes", "Itime");
 Statistic stats::instructions("Instructions", "I");
diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h
index 354706f5..b624d1aa 100644
--- a/lib/Core/CoreStats.h
+++ b/lib/Core/CoreStats.h
@@ -30,6 +30,9 @@ namespace stats {
   /// The number of process forks.
   extern Statistic forks;
 
+  /// Number of inhibited forks.
+  extern Statistic inhibitedForks;
+
   /// Number of states, this is a "fake" statistic used by istats, it
   /// isn't normally up-to-date.
   extern Statistic states;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 9322f50a..c3a10144 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -897,6 +897,7 @@ void Executor::branch(ExecutionState &state,
         result.push_back(nullptr);
       }
     }
+    stats::inhibitedForks += N - 1;
   } else {
     stats::forks += N-1;
 
@@ -1074,6 +1075,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
           addConstraint(current, Expr::createIsZero(condition));
           res = Solver::False;
         }
+        ++stats::inhibitedForks;
       }
     }
   }
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 539b913c..18c0a691 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -451,6 +451,7 @@ void StatsTracker::writeStatsHeader() {
              << "ResolveTime INTEGER,"
              << "QueryCexCacheMisses INTEGER,"
              << "QueryCexCacheHits INTEGER,"
+             << "InhibitedForks INTEGER,"
              << "ArrayHashTime INTEGER"
          << ')';
   char *zErrMsg = nullptr;
@@ -484,6 +485,7 @@ void StatsTracker::writeStatsHeader() {
              << "ResolveTime,"
              << "QueryCexCacheMisses,"
              << "QueryCexCacheHits,"
+             << "InhibitedForks,"
              << "ArrayHashTime"
          << ") VALUES ("
              << "?,"
@@ -505,6 +507,7 @@ void StatsTracker::writeStatsHeader() {
              << "?,"
              << "?,"
              << "?,"
+             << "?,"
              << "? "
          << ')';
 
@@ -537,10 +540,11 @@ void StatsTracker::writeStatsLine() {
   sqlite3_bind_int64(insertStmt, 17, stats::resolveTime);
   sqlite3_bind_int64(insertStmt, 18, stats::queryCexCacheMisses);
   sqlite3_bind_int64(insertStmt, 19, stats::queryCexCacheHits);
+  sqlite3_bind_int64(insertStmt, 20, stats::inhibitedForks);
 #ifdef KLEE_ARRAY_DEBUG
-  sqlite3_bind_int64(insertStmt, 20, stats::arrayHashTime);
+  sqlite3_bind_int64(insertStmt, 21, stats::arrayHashTime);
 #else
-  sqlite3_bind_int64(insertStmt, 20, -1LL);
+  sqlite3_bind_int64(insertStmt, 21, -1LL);
 #endif
   int errCode = sqlite3_step(insertStmt);
   if(errCode != SQLITE_DONE) klee_error("Error writing stats data: %s", sqlite3_errmsg(statsFile));
diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats
index 22cdaf43..18fbe595 100755
--- a/tools/klee-stats/klee-stats
+++ b/tools/klee-stats/klee-stats
@@ -47,6 +47,7 @@ Legend = [
     ('ActiveStates', 'number of currently active states (0 after successful termination)', "NumStates"),
     ('MaxActiveStates', 'maximum number of active states', "MaxStates"),
     ('AvgActiveStates', 'average number of active states', "AvgStates"),
+    ('InhibitedForks', 'number of inhibited state forks due to e.g. memory pressure', "InhibitedForks"),
     # - constraint caching/solving
     ('Queries', 'number of queries issued to the constraint solver', "NumQueries"),
     ('QueryConstructs', 'number of query constructs for all queries send to the constraint solver', "NumQueryConstructs"),