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

7 files changed, 37 insertions, 26 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();
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<Expr> &result) {
-  ++stats::queries;
+  ++stats::solverQueries;
   ++stats::queryCounterexamples;
   return false;
 }
@@ -50,7 +50,7 @@ bool DummySolverImpl::computeValue(const Query &, ref<Expr> &result) {
 bool DummySolverImpl::computeInitialValues(
     const Query &, const std::vector<const Array *> &objects,
     std::vector<std::vector<unsigned char> > &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<SolverContext>::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;