about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/CoreStats.cpp1
-rw-r--r--lib/Core/CoreStats.h3
-rw-r--r--lib/Core/ExternalDispatcher.cpp3
-rw-r--r--lib/Core/StatsTracker.cpp8
4 files changed, 13 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));