diff options
| -rw-r--r-- | lib/Core/CoreStats.cpp | 1 | ||||
| -rw-r--r-- | lib/Core/CoreStats.h | 3 | ||||
| -rw-r--r-- | lib/Core/ExternalDispatcher.cpp | 3 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 8 | ||||
| -rwxr-xr-x | tools/klee-stats/klee-stats | 1 |
5 files changed, 14 insertions, 2 deletions
diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp index 720fa1b2..06b8b930 100644 --- a/lib/Core/CoreStats.cpp +++ b/lib/Core/CoreStats.cpp @@ -13,6 +13,7 @@ using namespace klee; Statistic stats::allocations("Allocations", "Alloc"); Statistic stats::coveredInstructions("CoveredInstructions", "Icov"); +Statistic stats::externalCalls("ExternalCalls", "ExtC"); Statistic stats::falseBranches("FalseBranches", "Bf"); Statistic stats::forkTime("ForkTime", "Ftime"); Statistic stats::forks("Forks", "Forks"); diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h index b624d1aa..c0dcac7d 100644 --- a/lib/Core/CoreStats.h +++ b/lib/Core/CoreStats.h @@ -27,6 +27,9 @@ namespace stats { extern Statistic forkTime; extern Statistic solverTime; + /// The number of external calls. + extern Statistic externalCalls; + /// The number of process forks. extern Statistic forks; diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index d286bea9..d155798e 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -8,6 +8,8 @@ //===----------------------------------------------------------------------===// #include "ExternalDispatcher.h" + +#include "CoreStats.h" #include "klee/Config/Version.h" #include "klee/Module/KCallable.h" #include "klee/Module/KModule.h" @@ -158,6 +160,7 @@ ExternalDispatcherImpl::~ExternalDispatcherImpl() { bool ExternalDispatcherImpl::executeCall(KCallable *callable, Instruction *i, uint64_t *args) { + ++stats::externalCalls; dispatchers_ty::iterator it = dispatchers.find(i); if (it != dispatchers.end()) { // Code already JIT'ed for this diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 0cec4222..907aaa73 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -454,6 +454,7 @@ void StatsTracker::writeStatsHeader() { << "QueryCexCacheMisses INTEGER," << "QueryCexCacheHits INTEGER," << "InhibitedForks INTEGER," + << "ExternalCalls INTEGER," << "ArrayHashTime INTEGER" << ')'; char *zErrMsg = nullptr; @@ -490,6 +491,7 @@ void StatsTracker::writeStatsHeader() { << "QueryCexCacheMisses," << "QueryCexCacheHits," << "InhibitedForks," + << "ExternalCalls," << "ArrayHashTime" << ") VALUES (" << "?," @@ -514,6 +516,7 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," << "?," + << "?," << "? " << ')'; @@ -549,10 +552,11 @@ void StatsTracker::writeStatsLine() { sqlite3_bind_int64(insertStmt, 20, stats::queryCexCacheMisses); sqlite3_bind_int64(insertStmt, 21, stats::queryCexCacheHits); sqlite3_bind_int64(insertStmt, 22, stats::inhibitedForks); + sqlite3_bind_int64(insertStmt, 23, stats::externalCalls); #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 23, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, 24, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 23, -1LL); + sqlite3_bind_int64(insertStmt, 24, -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 b819f69b..be30a0ca 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -35,6 +35,7 @@ Legend = [ ('Branches', 'number of conditional branch (br) instructions in the LLVM bitcode', 'NumBranches'), ('FullBranches', 'number of fully-explored conditional branch (br) instructions in the LLVM bitcode', 'FullBranches'), ('PartialBranches', 'number of partially-explored conditional branch (br) instructions in the LLVM bitcode', 'PartialBranches'), + ('ExternalCalls', 'number of external calls', 'ExternalCalls'), # - time ('TUser(s)', 'total user time', "UserTime"), ('TResolve(s)', 'time spent in object resolution', "ResolveTime"), |