diff options
| -rw-r--r-- | lib/Core/CoreStats.cpp | 1 | ||||
| -rw-r--r-- | lib/Core/CoreStats.h | 3 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 2 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 8 | ||||
| -rwxr-xr-x | tools/klee-stats/klee-stats | 1 |
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 ¤t, 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"), |