From 3a1965c62540ef3fa3ec857f2b7d055cbbb68939 Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Tue, 11 Jan 2022 09:09:44 +0000
Subject: stats: add termination class stats

---
 lib/Core/StatsTracker.cpp | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'lib/Core/StatsTracker.cpp')

diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 80723f8a..9f92a127 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -12,6 +12,7 @@
 #include "ExecutionState.h"
 
 #include "klee/Config/Version.h"
+#include "klee/Core/TerminationTypes.h"
 #include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
@@ -432,6 +433,8 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue,
 void StatsTracker::writeStatsHeader() {
   #undef BTYPE
   #define BTYPE(Name,I) << "Branches" #Name " INTEGER,"
+  #undef TCLASS
+  #define TCLASS(Name,I) << "Termination" #Name " INTEGER,"
   std::ostringstream create, insert;
   create << "CREATE TABLE stats ("
          << "Instructions INTEGER,"
@@ -461,6 +464,7 @@ void StatsTracker::writeStatsHeader() {
          << "Allocations INTEGER,"
          << "States INTEGER,"
          BRANCH_TYPES
+         TERMINATION_CLASSES
          << "ArrayHashTime INTEGER"
          << ')';
   char *zErrMsg = nullptr;
@@ -476,6 +480,8 @@ void StatsTracker::writeStatsHeader() {
    */
   #undef BTYPE
   #define BTYPE(Name, I) << "Branches" #Name ","
+  #undef TCLASS
+  #define TCLASS(Name, I) << "Termination" #Name ","
   insert << "INSERT OR FAIL INTO stats ("
          << "Instructions,"
          << "FullBranches,"
@@ -504,10 +510,13 @@ void StatsTracker::writeStatsHeader() {
          << "Allocations,"
          << "States,"
          BRANCH_TYPES
+         TERMINATION_CLASSES
          << "ArrayHashTime"
          << ')';
   #undef BTYPE
   #define BTYPE(Name, I) << "?,"
+  #undef TCLASS
+  #define TCLASS(Name, I) << "?,"
   insert << " VALUES ("
          << "?,"
          << "?,"
@@ -536,6 +545,7 @@ void StatsTracker::writeStatsHeader() {
          << "?,"
          << "?,"
          BRANCH_TYPES
+         TERMINATION_CLASSES
          << "? "
          << ')';
 
@@ -551,6 +561,8 @@ time::Span StatsTracker::elapsed() {
 void StatsTracker::writeStatsLine() {
   #undef BTYPE
   #define BTYPE(Name,I) sqlite3_bind_int64(insertStmt, arg++, stats::branches ## Name);
+  #undef TCLASS
+  #define TCLASS(Name,I) sqlite3_bind_int64(insertStmt, arg++, stats::termination ## Name);
   int arg = 1;
   sqlite3_bind_int64(insertStmt, arg++, stats::instructions);
   sqlite3_bind_int64(insertStmt, arg++, fullBranches);
@@ -579,6 +591,7 @@ void StatsTracker::writeStatsLine() {
   sqlite3_bind_int64(insertStmt, arg++, stats::allocations);
   sqlite3_bind_int64(insertStmt, arg++, ExecutionState::getLastID());
   BRANCH_TYPES
+  TERMINATION_CLASSES
 #ifdef KLEE_ARRAY_DEBUG
   sqlite3_bind_int64(insertStmt, arg++, stats::arrayHashTime);
 #else
-- 
cgit 1.4.1