stats: rename numQueries/Queries -> SolverQueries, add Queries

2 files changed, 29 insertions, 19 deletions

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> expr,
                             Solver::Validity &result,
                             SolverQueryMetaData &metaData) {
+  ++stats::queries;
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE->isTrue() ? Solver::True : Solver::False;
@@ -46,6 +48,7 @@ bool TimingSolver::evaluate(const ConstraintSet &constraints, ref<Expr> expr,
 
 bool TimingSolver::mustBeTrue(const ConstraintSet &constraints, ref<Expr> expr,
                               bool &result, SolverQueryMetaData &metaData) {
+  ++stats::queries;
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE->isTrue() ? true : false;
@@ -90,6 +93,7 @@ bool TimingSolver::mayBeFalse(const ConstraintSet &constraints, ref<Expr> expr,
 bool TimingSolver::getValue(const ConstraintSet &constraints, ref<Expr> expr,
                             ref<ConstantExpr> &result,
                             SolverQueryMetaData &metaData) {
+  ++stats::queries;
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE;
@@ -112,6 +116,7 @@ bool TimingSolver::getInitialValues(
     const ConstraintSet &constraints, const std::vector<const Array *> &objects,
     std::vector<std::vector<unsigned char>> &result,
     SolverQueryMetaData &metaData) {
+  ++stats::queries;
   if (objects.empty())
     return true;
 
@@ -128,6 +133,7 @@ bool TimingSolver::getInitialValues(
 std::pair<ref<Expr>, ref<Expr>>
 TimingSolver::getRange(const ConstraintSet &constraints, ref<Expr> expr,
                        SolverQueryMetaData &metaData) {
+  ++stats::queries;
   TimerStatIncrementer timer(stats::solverTime);
   auto result = solver->getRange(Query(constraints, expr));
   metaData.queryCost += timer.delta();