From 855d33173cae9fd43899a6a96a58f79563560cce Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 7 Jan 2022 16:09:10 +0000 Subject: stats: rename numQueries/Queries -> SolverQueries, add Queries --- lib/Core/StatsTracker.cpp | 42 +++++++++++++++++++++++------------------- lib/Core/TimingSolver.cpp | 6 ++++++ 2 files changed, 29 insertions(+), 19 deletions(-) (limited to 'lib/Core') diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 907aaa73..37a52fff 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -439,7 +439,8 @@ void StatsTracker::writeStatsHeader() { << "UserTime REAL," << "NumStates INTEGER," << "MallocUsage INTEGER," - << "NumQueries INTEGER," + << "Queries INTEGER," + << "SolverQueries INTEGER," << "NumQueryConstructs INTEGER," << "WallTime REAL," << "CoveredInstructions INTEGER," @@ -476,7 +477,8 @@ void StatsTracker::writeStatsHeader() { << "UserTime," << "NumStates," << "MallocUsage," - << "NumQueries," + << "Queries," + << "SolverQueries," << "NumQueryConstructs," << "WallTime," << "CoveredInstructions," @@ -517,6 +519,7 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," << "?," + << "?," << "? " << ')'; @@ -538,25 +541,26 @@ void StatsTracker::writeStatsLine() { sqlite3_bind_int64(insertStmt, 6, executor.states.size()); sqlite3_bind_int64(insertStmt, 7, util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize()); sqlite3_bind_int64(insertStmt, 8, stats::queries); - sqlite3_bind_int64(insertStmt, 9, stats::queryConstructs); - sqlite3_bind_int64(insertStmt, 10, elapsed().toMicroseconds()); - sqlite3_bind_int64(insertStmt, 11, stats::coveredInstructions); - sqlite3_bind_int64(insertStmt, 12, stats::uncoveredInstructions); - sqlite3_bind_int64(insertStmt, 13, stats::queryTime); - sqlite3_bind_int64(insertStmt, 14, stats::solverTime); - sqlite3_bind_int64(insertStmt, 15, stats::cexCacheTime); - sqlite3_bind_int64(insertStmt, 16, stats::forkTime); - sqlite3_bind_int64(insertStmt, 17, stats::resolveTime); - sqlite3_bind_int64(insertStmt, 18, stats::queryCacheMisses); - sqlite3_bind_int64(insertStmt, 19, stats::queryCacheHits); - 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); + sqlite3_bind_int64(insertStmt, 9, stats::solverQueries); + sqlite3_bind_int64(insertStmt, 10, stats::queryConstructs); + sqlite3_bind_int64(insertStmt, 11, elapsed().toMicroseconds()); + sqlite3_bind_int64(insertStmt, 12, stats::coveredInstructions); + sqlite3_bind_int64(insertStmt, 13, stats::uncoveredInstructions); + sqlite3_bind_int64(insertStmt, 14, stats::queryTime); + sqlite3_bind_int64(insertStmt, 15, stats::solverTime); + sqlite3_bind_int64(insertStmt, 16, stats::cexCacheTime); + sqlite3_bind_int64(insertStmt, 17, stats::forkTime); + sqlite3_bind_int64(insertStmt, 18, stats::resolveTime); + sqlite3_bind_int64(insertStmt, 19, stats::queryCacheMisses); + sqlite3_bind_int64(insertStmt, 10, stats::queryCacheHits); + sqlite3_bind_int64(insertStmt, 21, stats::queryCexCacheMisses); + sqlite3_bind_int64(insertStmt, 22, stats::queryCexCacheHits); + sqlite3_bind_int64(insertStmt, 23, stats::inhibitedForks); + sqlite3_bind_int64(insertStmt, 24, stats::externalCalls); #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 24, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, 25, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 24, -1LL); + sqlite3_bind_int64(insertStmt, 25, -1LL); #endif int errCode = sqlite3_step(insertStmt); if(errCode != SQLITE_DONE) klee_error("Error writing stats data: %s", sqlite3_errmsg(statsFile)); diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index fc31e72d..812357ce 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -15,6 +15,7 @@ #include "klee/Statistics/Statistics.h" #include "klee/Statistics/TimerStatIncrementer.h" #include "klee/Solver/Solver.h" +#include "klee/Solver/SolverStats.h" #include "CoreStats.h" @@ -26,6 +27,7 @@ using namespace llvm; bool TimingSolver::evaluate(const ConstraintSet &constraints, ref expr, Solver::Validity &result, SolverQueryMetaData &metaData) { + ++stats::queries; // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE->isTrue() ? Solver::True : Solver::False; @@ -46,6 +48,7 @@ bool TimingSolver::evaluate(const ConstraintSet &constraints, ref expr, bool TimingSolver::mustBeTrue(const ConstraintSet &constraints, ref expr, bool &result, SolverQueryMetaData &metaData) { + ++stats::queries; // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE->isTrue() ? true : false; @@ -90,6 +93,7 @@ bool TimingSolver::mayBeFalse(const ConstraintSet &constraints, ref expr, bool TimingSolver::getValue(const ConstraintSet &constraints, ref expr, ref &result, SolverQueryMetaData &metaData) { + ++stats::queries; // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE; @@ -112,6 +116,7 @@ bool TimingSolver::getInitialValues( const ConstraintSet &constraints, const std::vector &objects, std::vector> &result, SolverQueryMetaData &metaData) { + ++stats::queries; if (objects.empty()) return true; @@ -128,6 +133,7 @@ bool TimingSolver::getInitialValues( std::pair, ref> TimingSolver::getRange(const ConstraintSet &constraints, ref expr, SolverQueryMetaData &metaData) { + ++stats::queries; TimerStatIncrementer timer(stats::solverTime); auto result = solver->getRange(Query(constraints, expr)); metaData.queryCost += timer.delta(); -- cgit 1.4.1