Fixed and improved the stats on (cex)cache hits and misses.

4 files changed, 18 insertions, 3 deletions

diff --git a/klee/lib/Solver/CachingSolver.cpp b/klee/lib/Solver/CachingSolver.cpp
index b6a93c7b0ca..5911bbf3d45 100644
--- a/klee/lib/Solver/CachingSolver.cpp
+++ b/klee/lib/Solver/CachingSolver.cpp
@@ -73,12 +73,14 @@ public:
   bool computeValidity(const Query&, Solver::Validity &result);
   bool computeTruth(const Query&, bool &isValid);
   bool computeValue(const Query& query, ref<Expr> &result) {
+    ++stats::queryCacheMisses;
     return solver->impl->computeValue(query, result);
   }
   bool computeInitialValues(const Query& query,
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution) {
+    ++stats::queryCacheMisses;
     return solver->impl->computeInitialValues(query, objects, values, 
                                               hasSolution);
   }
@@ -141,19 +143,21 @@ bool CachingSolver::computeValidity(const Query& query,
   bool tmp, cacheHit = cacheLookup(query, cachedResult);
   
   if (cacheHit) {
-    ++stats::queryCacheHits;
-
     switch(cachedResult) {
     case IncompleteSolver::MustBeTrue:   
       result = Solver::True;
+      ++stats::queryCacheHits;
       return true;
     case IncompleteSolver::MustBeFalse:  
       result = Solver::False;
+      ++stats::queryCacheHits;
       return true;
     case IncompleteSolver::TrueOrFalse:  
       result = Solver::Unknown;
+      ++stats::queryCacheHits;
       return true;
     case IncompleteSolver::MayBeTrue: {
+      ++stats::queryCacheMisses;
       if (!solver->impl->computeTruth(query, tmp))
         return false;
       if (tmp) {
@@ -167,6 +171,7 @@ bool CachingSolver::computeValidity(const Query& query,
       }
     }
     case IncompleteSolver::MayBeFalse: {
+      ++stats::queryCacheMisses;
       if (!solver->impl->computeTruth(query.negateExpr(), tmp))
         return false;
       if (tmp) {
diff --git a/klee/lib/Solver/CexCachingSolver.cpp b/klee/lib/Solver/CexCachingSolver.cpp
index 3d7a754c9a3..497ccb4a945 100644
--- a/klee/lib/Solver/CexCachingSolver.cpp
+++ b/klee/lib/Solver/CexCachingSolver.cpp
@@ -185,13 +185,19 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
     if (CE->isFalse()) {
       result = (Assignment*) 0;
+      ++stats::queryCexCacheHits;
       return true;
     }
   } else {
     key.insert(neg);
   }
 
-  return searchForAssignment(key, result);
+  bool found = searchForAssignment(key, result);
+  if (found)
+    ++stats::queryCexCacheHits;
+  else ++stats::queryCexCacheMisses;
+    
+  return found;
 }
 
 bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
diff --git a/klee/lib/Solver/SolverStats.cpp b/klee/lib/Solver/SolverStats.cpp
index 1f85fe88b52..9d6963cfb02 100644
--- a/klee/lib/Solver/SolverStats.cpp
+++ b/klee/lib/Solver/SolverStats.cpp
@@ -17,6 +17,8 @@ Statistic stats::queriesInvalid("QueriesInvalid", "Qiv");
 Statistic stats::queriesValid("QueriesValid", "Qv");
 Statistic stats::queryCacheHits("QueryCacheHits", "QChits") ;
 Statistic stats::queryCacheMisses("QueryCacheMisses", "QCmisses");
+Statistic stats::queryCexCacheHits("QueryCexCacheHits", "QCexHits") ;
+Statistic stats::queryCexCacheMisses("QueryCexCacheMisses", "QCexMisses");
 Statistic stats::queryConstructTime("QueryConstructTime", "QBtime") ;
 Statistic stats::queryConstructs("QueriesConstructs", "QB");
 Statistic stats::queryCounterexamples("QueriesCEX", "Qcex");
diff --git a/klee/lib/Solver/SolverStats.h b/klee/lib/Solver/SolverStats.h
index 56bdf999726..a38c9826525 100644
--- a/klee/lib/Solver/SolverStats.h
+++ b/klee/lib/Solver/SolverStats.h
@@ -21,6 +21,8 @@ namespace stats {
   extern Statistic queriesValid;
   extern Statistic queryCacheHits;
   extern Statistic queryCacheMisses;
+  extern Statistic queryCexCacheHits;
+  extern Statistic queryCexCacheMisses;
   extern Statistic queryConstructTime;
   extern Statistic queryConstructs;
   extern Statistic queryCounterexamples;