diff options
| author | Frank Busse <bb0xfb@gmail.com> | 2022-01-11 09:09:44 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-03-23 17:41:08 +0000 |
| commit | 3a1965c62540ef3fa3ec857f2b7d055cbbb68939 (patch) | |
| tree | 09dc3af2c442bbae80331b9a968d9d8f83558384 /lib/Core/StatsTracker.cpp | |
| parent | a6f0612026cac27a1c997517420bfe5c9d254944 (diff) | |
| download | klee-3a1965c62540ef3fa3ec857f2b7d055cbbb68939.tar.gz | |
stats: add termination class stats
Diffstat (limited to 'lib/Core/StatsTracker.cpp')
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
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 |