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 ++++++ lib/Solver/DummySolver.cpp | 8 ++++---- lib/Solver/MetaSMTSolver.cpp | 2 +- lib/Solver/STPSolver.cpp | 2 +- lib/Solver/SolverStats.cpp | 1 + lib/Solver/Z3Solver.cpp | 2 +- 7 files changed, 37 insertions(+), 26 deletions(-) (limited to 'lib') 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(); diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp index 60a4fb51..a845f901 100644 --- a/lib/Solver/DummySolver.cpp +++ b/lib/Solver/DummySolver.cpp @@ -30,19 +30,19 @@ public: DummySolverImpl::DummySolverImpl() {} bool DummySolverImpl::computeValidity(const Query &, Solver::Validity &result) { - ++stats::queries; + ++stats::solverQueries; // FIXME: We should have stats::queriesFail; return false; } bool DummySolverImpl::computeTruth(const Query &, bool &isValid) { - ++stats::queries; + ++stats::solverQueries; // FIXME: We should have stats::queriesFail; return false; } bool DummySolverImpl::computeValue(const Query &, ref &result) { - ++stats::queries; + ++stats::solverQueries; ++stats::queryCounterexamples; return false; } @@ -50,7 +50,7 @@ bool DummySolverImpl::computeValue(const Query &, ref &result) { bool DummySolverImpl::computeInitialValues( const Query &, const std::vector &objects, std::vector > &values, bool &hasSolution) { - ++stats::queries; + ++stats::solverQueries; ++stats::queryCounterexamples; return false; } diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 0f78bb5b..37c22f0e 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -194,7 +194,7 @@ bool MetaSMTSolverImpl::computeInitialValues( TimerStatIncrementer t(stats::queryTime); assert(_builder); - ++stats::queries; + ++stats::solverQueries; ++stats::queryCounterexamples; bool success = true; diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 13536910..6e62b82b 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -387,7 +387,7 @@ bool STPSolverImpl::computeInitialValues( for (const auto &constraint : query.constraints) vc_assertFormula(vc, builder->construct(constraint)); - ++stats::queries; + ++stats::solverQueries; ++stats::queryCounterexamples; ExprHandle stp_e = builder->construct(query.expr); diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp index 40f0d53f..97b8902a 100644 --- a/lib/Solver/SolverStats.cpp +++ b/lib/Solver/SolverStats.cpp @@ -12,6 +12,7 @@ using namespace klee; Statistic stats::cexCacheTime("CexCacheTime", "CCtime"); +Statistic stats::solverQueries("SolverQueries", "SQ"); Statistic stats::queries("Queries", "Q"); Statistic stats::queriesInvalid("QueriesInvalid", "Qiv"); Statistic stats::queriesValid("QueriesValid", "Qv"); diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index b628b86b..8319e5f3 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -268,7 +268,7 @@ bool Z3SolverImpl::internalRunSolver( Z3_solver_assert(builder->ctx, theSolver, builder->construct(constraint)); constant_arrays_in_query.visit(constraint); } - ++stats::queries; + ++stats::solverQueries; if (objects) ++stats::queryCounterexamples; -- cgit 1.4.1