about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2013-07-11 16:21:15 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2013-07-11 16:21:15 +0000
commitd47bf6b91faeab6c97a06108ed35b2b7ad0a45fc (patch)
tree2314b8f81c311f9077af964b9eb9872cfdede220 /lib/Solver
parente4ce97b38411de5d972ee4cf89cede342b7f82f0 (diff)
downloadklee-d47bf6b91faeab6c97a06108ed35b2b7ad0a45fc.tar.gz
Fixed and improved the stats on (cex)cache hits and misses.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186097 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/CachingSolver.cpp9
-rw-r--r--lib/Solver/CexCachingSolver.cpp8
-rw-r--r--lib/Solver/SolverStats.cpp2
-rw-r--r--lib/Solver/SolverStats.h2
4 files changed, 18 insertions, 3 deletions
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index b6a93c7b..5911bbf3 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/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/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 3d7a754c..497ccb4a 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/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/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp
index 1f85fe88..9d6963cf 100644
--- a/lib/Solver/SolverStats.cpp
+++ b/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/lib/Solver/SolverStats.h b/lib/Solver/SolverStats.h
index 56bdf999..a38c9826 100644
--- a/lib/Solver/SolverStats.h
+++ b/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;