about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Solver/SolverStats.h1
-rw-r--r--lib/Core/StatsTracker.cpp42
-rw-r--r--lib/Core/TimingSolver.cpp6
-rw-r--r--lib/Solver/DummySolver.cpp8
-rw-r--r--lib/Solver/MetaSMTSolver.cpp2
-rw-r--r--lib/Solver/STPSolver.cpp2
-rw-r--r--lib/Solver/SolverStats.cpp1
-rw-r--r--lib/Solver/Z3Solver.cpp2
-rw-r--r--tools/kleaver/main.cpp2
-rwxr-xr-xtools/klee-stats/klee-stats5
-rw-r--r--tools/klee/main.cpp2
11 files changed, 43 insertions, 30 deletions
diff --git a/include/klee/Solver/SolverStats.h b/include/klee/Solver/SolverStats.h
index fe14d9e5..fd4a3ab6 100644
--- a/include/klee/Solver/SolverStats.h
+++ b/include/klee/Solver/SolverStats.h
@@ -16,6 +16,7 @@ namespace klee {
 namespace stats {
 
   extern Statistic cexCacheTime;
+  extern Statistic solverQueries;
   extern Statistic queries;
   extern Statistic queriesInvalid;
   extern Statistic queriesValid;
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;
 
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 22c23422..eed4e4c9 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -296,7 +296,7 @@ static bool EvaluateInputAST(const char *Filename,
 
   delete S;
 
-  if (uint64_t queries = *theStatisticManager->getStatisticByName("Queries")) {
+  if (uint64_t queries = *theStatisticManager->getStatisticByName("SolverQueries")) {
     llvm::outs()
       << "--\n"
       << "total queries = " << queries << '\n'
diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats
index be30a0ca..5e49587b 100755
--- a/tools/klee-stats/klee-stats
+++ b/tools/klee-stats/klee-stats
@@ -50,8 +50,9 @@ Legend = [
     ('AvgActiveStates', 'average number of active states', "AvgStates"),
     ('InhibitedForks', 'number of inhibited state forks due to e.g. memory pressure', "InhibitedForks"),
     # - constraint caching/solving
-    ('Queries', 'number of queries issued to the constraint solver', "NumQueries"),
-    ('QueryConstructs', 'number of query constructs for all queries send to the constraint solver', "NumQueryConstructs"),
+    ('Queries', 'number of queries issued to the solver chain', "Queries"),
+    ('SolverQueries', 'number of queries issued to the constraint solver', "SolverQueries"),
+    ('SolverQueryConstructs', 'number of query constructs for all queries send to the constraint solver', "NumQueryConstructs"),
     ('AvgSolverQuerySize', 'average number of query constructs per query issued to the constraint solver', "AvgQC"),
     ('QCacheMisses', 'Query cache misses', "QueryCacheMisses"),
     ('QCacheHits', 'Query cache hits', "QueryCacheHits"),
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 0b76e904..ddb1faec 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1547,7 +1547,7 @@ int main(int argc, char **argv, char **envp) {
   delete interpreter;
 
   uint64_t queries =
-    *theStatisticManager->getStatisticByName("Queries");
+    *theStatisticManager->getStatisticByName("SolverQueries");
   uint64_t queriesValid =
     *theStatisticManager->getStatisticByName("QueriesValid");
   uint64_t queriesInvalid =
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-21 22:40:53 +0000