Patch by Tomasz Kuchta adding more detailed information on query failures.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171391 91177308-0d34-0410-b5e6-96231b3b80d8

9 files changed, 128 insertions, 77 deletions

diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h
index 38ee4e28..9a122c74 100644
--- a/include/klee/IncompleteSolver.h
+++ b/include/klee/IncompleteSolver.h
@@ -101,7 +101,7 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
-  bool hasTimeoutOccurred();
+  SolverRunStatus getOperationStatusCode();
 };
 
 }
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 94e7d477..9e05967d 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -226,12 +226,6 @@ namespace klee {
   /// fails.
   Solver *createDummySolver();
   
-  enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS, 
-                         SOLVER_RUN_STATUS_TIMEOUT,
-                         SOLVER_RUN_STATUS_FORK_FAILED,
-                         SOLVER_RUN_STATUS_INTERRUPTED,
-                         SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE,
-                         SOLVER_RUN_STATUS_WAITPID_FAILED };
 }
 
 #endif
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h
index 080dfc54..09be849b 100644
--- a/include/klee/SolverImpl.h
+++ b/include/klee/SolverImpl.h
@@ -28,6 +28,15 @@ namespace klee {
     SolverImpl() {}
     virtual ~SolverImpl();
 
+    enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE,
+                           SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE,
+                           SOLVER_RUN_STATUS_FAILURE,
+                           SOLVER_RUN_STATUS_TIMEOUT,
+                           SOLVER_RUN_STATUS_FORK_FAILED,
+                           SOLVER_RUN_STATUS_INTERRUPTED,
+                           SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE,
+                           SOLVER_RUN_STATUS_WAITPID_FAILED };
+
     /// computeValidity - Compute a full validity result for the
     /// query.
     ///
@@ -57,8 +66,12 @@ namespace klee {
                                         &values,
                                       bool &hasSolution) = 0;
     
-    /// haveTimeOutOccurred - retrieve timeout status for the last query.
-    virtual bool hasTimeoutOccurred() = 0;
+    /// getOperationStatusCode - get the status of the last solver operation
+    virtual SolverRunStatus getOperationStatusCode() = 0;
+    
+    /// getOperationStatusString - get string representation of the operation
+    /// status code
+    static const char* getOperationStatusString(SolverRunStatus statusCode);
 };
 
 }
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index f7b88855..b6a93c7b 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -82,7 +82,7 @@ public:
     return solver->impl->computeInitialValues(query, objects, values, 
                                               hasSolution);
   }
-  bool hasTimeoutOccurred();
+  SolverRunStatus getOperationStatusCode();
 };
 
 /** @returns the canonical version of the given query.  The reference
@@ -235,8 +235,8 @@ bool CachingSolver::computeTruth(const Query& query,
   return true;
 }
 
-bool CachingSolver::hasTimeoutOccurred() {
-  return solver->impl->hasTimeoutOccurred();
+SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() {
+  return solver->impl->getOperationStatusCode();
 }
 
 ///
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index c84ae409..3d7a754c 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -82,7 +82,7 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
-  bool hasTimeoutOccurred();
+  SolverRunStatus getOperationStatusCode();
 };
 
 ///
@@ -340,8 +340,8 @@ CexCachingSolver::computeInitialValues(const Query& query,
   return true;
 }
 
-bool CexCachingSolver::hasTimeoutOccurred() {
-  return solver->impl->hasTimeoutOccurred();
+SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode() {
+  return solver->impl->getOperationStatusCode();
 }
 
 ///
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index 45e2ea9b..7bc8058d 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -135,6 +135,6 @@ StagedSolverImpl::computeInitialValues(const Query& query,
                                                hasSolution);
 }
 
-bool StagedSolverImpl::hasTimeoutOccurred() {
-  return secondary->impl->hasTimeoutOccurred();
+SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode() {
+  return secondary->impl->getOperationStatusCode();
 }
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 0eb86720..b3ef1e57 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -284,7 +284,7 @@ public:
     return solver->impl->computeInitialValues(query, objects, values,
                                               hasSolution);
   }
-  bool hasTimeoutOccurred();
+  SolverRunStatus getOperationStatusCode();
 };
   
 bool IndependentSolver::computeValidity(const Query& query,
@@ -314,8 +314,8 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) {
   return solver->impl->computeValue(Query(tmp, query.expr), result);
 }
 
-bool IndependentSolver::hasTimeoutOccurred() {
-  return solver->impl->hasTimeoutOccurred();
+SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() {
+  return solver->impl->getOperationStatusCode();      
 }
 
 Solver *klee::createIndependentSolver(Solver *s) {
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 366a7b05..abb70770 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -39,6 +39,48 @@ using namespace klee;
 
 /***/
 
+SolverImpl::~SolverImpl() {
+}
+
+bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) {
+  bool isTrue, isFalse;
+  if (!computeTruth(query, isTrue))
+    return false;
+  if (isTrue) {
+    result = Solver::True;
+  } else {
+    if (!computeTruth(query.negateExpr(), isFalse))
+      return false;
+    result = isFalse ? Solver::False : Solver::Unknown;
+  }
+  return true;
+}
+
+const char* SolverImpl::getOperationStatusString(SolverRunStatus statusCode)
+{
+    switch (statusCode)
+    {
+        case SOLVER_RUN_STATUS_SUCCESS_SOLVABLE:
+            return "OPERATION SUCCESSFUL, QUERY IS SOLVABLE";
+        case SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE:
+            return "OPERATION SUCCESSFUL, QUERY IS UNSOLVABLE";
+        case SOLVER_RUN_STATUS_FAILURE:
+            return "OPERATION FAILED";
+        case SOLVER_RUN_STATUS_TIMEOUT:
+            return "SOLVER TIMEOUT";
+        case SOLVER_RUN_STATUS_FORK_FAILED:
+            return "FORK FAILED";
+        case SOLVER_RUN_STATUS_INTERRUPTED:
+            return "SOLVER PROCESS INTERRUPTED";
+        case SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE:
+            return "UNEXPECTED SOLVER PROCESS EXIT CODE";
+        case SOLVER_RUN_STATUS_WAITPID_FAILED:
+            return "WAITPID FAILED FOR SOLVER PROCESS";
+        default:
+            return "UNRECOGNIZED OPERATION STATUS";        
+    }    
+}
+
 const char *Solver::validity_to_str(Validity v) {
   switch (v) {
   default:    return "Unknown";
@@ -51,9 +93,6 @@ Solver::~Solver() {
   delete impl; 
 }
 
-SolverImpl::~SolverImpl() {
-}
-
 bool Solver::evaluate(const Query& query, Validity &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
@@ -66,20 +105,6 @@ bool Solver::evaluate(const Query& query, Validity &result) {
   return impl->computeValidity(query, result);
 }
 
-bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) {
-  bool isTrue, isFalse;
-  if (!computeTruth(query, isTrue))
-    return false;
-  if (isTrue) {
-    result = Solver::True;
-  } else {
-    if (!computeTruth(query.negateExpr(), isFalse))
-      return false;
-    result = isFalse ? Solver::False : Solver::Unknown;
-  }
-  return true;
-}
-
 bool Solver::mustBeTrue(const Query& query, bool &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
@@ -273,7 +298,7 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
-  bool hasTimeoutOccurred();
+  SolverRunStatus getOperationStatusCode();
 };
 
 bool ValidatingSolver::computeTruth(const Query& query,
@@ -371,8 +396,8 @@ ValidatingSolver::computeInitialValues(const Query& query,
   return true;
 }
 
-bool ValidatingSolver::hasTimeoutOccurred() {
-    return solver->impl->hasTimeoutOccurred();
+SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() {
+    return solver->impl->getOperationStatusCode();
 }
 
 Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
@@ -408,8 +433,8 @@ public:
     ++stats::queryCounterexamples;
     return false; 
   }
-  bool hasTimeoutOccurred() {
-      return false;
+  SolverRunStatus getOperationStatusCode() {
+      return SOLVER_RUN_STATUS_FAILURE;
   }
   
 };
@@ -428,7 +453,7 @@ private:
   STPBuilder *builder;
   double timeout;
   bool useForkedSTP;
-  bool timeoutOccurred;
+  SolverRunStatus runStatusCode;
 
 public:
   STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
@@ -443,7 +468,7 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
-  bool hasTimeoutOccurred();
+  SolverRunStatus getOperationStatusCode();
 };
 
 static unsigned char *shared_memory_ptr;
@@ -461,7 +486,7 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim
     builder(new STPBuilder(vc, _optimizeDivides)),
     timeout(0.0),
     useForkedSTP(_useForkedSTP),
-    timeoutOccurred(false)
+    runStatusCode(SOLVER_RUN_STATUS_FAILURE)
 {
   assert(vc && "unable to create validity checker");
   assert(builder && "unable to create STPBuilder");
@@ -558,10 +583,10 @@ bool STPSolverImpl::computeValue(const Query& query,
   return true;
 }
 
-static void runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q,
-                   const std::vector<const Array*> &objects,
-                   std::vector< std::vector<unsigned char> > &values,
-                   bool &hasSolution) {
+static SolverImpl::SolverRunStatus runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q,
+                                                const std::vector<const Array*> &objects,
+                                                std::vector< std::vector<unsigned char> > &values,
+                                                bool &hasSolution) {
   // XXX I want to be able to timeout here, safely
   hasSolution = !vc_query(vc, q);
 
@@ -583,20 +608,27 @@ static void runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q,
       values.push_back(data);
     }
   }
+  
+  if (true == hasSolution) {
+    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+  }
+  else {
+    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;  
+  }
 }
 
 static void stpTimeoutHandler(int x) {
   _exit(52);
 }
 
-static SolverRunStatus runAndGetCexForked(::VC vc, 
-                                          STPBuilder *builder,
-                                          ::VCExpr q,
-                                          const std::vector<const Array*> &objects,
-                                          std::vector< std::vector<unsigned char> >
-                                          &values,
-                                          bool &hasSolution,
-                                          double timeout) {
+static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, 
+                                                      STPBuilder *builder,
+                                                      ::VCExpr q,
+                                                      const std::vector<const Array*> &objects,
+                                                      std::vector< std::vector<unsigned char> >
+                                                      &values,
+                                                      bool &hasSolution,
+                                                      double timeout) {
   unsigned char *pos = shared_memory_ptr;
   unsigned sum = 0;
   for (std::vector<const Array*>::const_iterator
@@ -609,7 +641,7 @@ static SolverRunStatus runAndGetCexForked(::VC vc,
   int pid = fork();
   if (pid==-1) {
     fprintf(stderr, "error: fork failed (for STP)");
-    return SOLVER_RUN_STATUS_FORK_FAILED;
+    return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED;
   }
 
   if (pid == 0) {
@@ -641,7 +673,7 @@ static SolverRunStatus runAndGetCexForked(::VC vc,
     
     if (res < 0) {
       fprintf(stderr, "error: waitpid() for STP failed");
-      return SOLVER_RUN_STATUS_WAITPID_FAILED;
+      return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED;
     }
     
     // From timed_run.py: It appears that linux at least will on
@@ -649,7 +681,7 @@ static SolverRunStatus runAndGetCexForked(::VC vc,
     // signal, so test signal first.
     if (WIFSIGNALED(status) || !WIFEXITED(status)) {
       fprintf(stderr, "error: STP did not return successfully");
-      return SOLVER_RUN_STATUS_INTERRUPTED;
+      return SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED;
     }
 
     int exitcode = WEXITSTATUS(status);
@@ -660,10 +692,10 @@ static SolverRunStatus runAndGetCexForked(::VC vc,
     } else if (exitcode==52) {
       fprintf(stderr, "error: STP timed out");
       // mark that a timeout occurred
-      return SOLVER_RUN_STATUS_TIMEOUT;
+      return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT;
     } else {
       fprintf(stderr, "error: STP did not return a recognized code");
-      return SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;
+      return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;
     }
     
     if (hasSolution) {
@@ -677,11 +709,16 @@ static SolverRunStatus runAndGetCexForked(::VC vc,
         pos += array->size;
       }
     }
-
-    return SOLVER_RUN_STATUS_SUCCESS;
+    
+    if (true == hasSolution) {
+      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+    }
+    else {        
+      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
+    }
   }
 }
-
+#include <iostream>
 bool
 STPSolverImpl::computeInitialValues(const Query &query,
                                     const std::vector<const Array*> 
@@ -689,7 +726,7 @@ STPSolverImpl::computeInitialValues(const Query &query,
                                     std::vector< std::vector<unsigned char> > 
                                       &values,
                                     bool &hasSolution) {
-  timeoutOccurred = false;
+  runStatusCode =  SOLVER_RUN_STATUS_FAILURE; 
     
   TimerStatIncrementer t(stats::queryTime);
 
@@ -713,12 +750,12 @@ STPSolverImpl::computeInitialValues(const Query &query,
 
   bool success;
   if (useForkedSTP) {
-    SolverRunStatus runStatus = runAndGetCexForked(vc, builder, stp_e, objects, values, 
-                                                   hasSolution, timeout);
-    success = (SOLVER_RUN_STATUS_SUCCESS == runStatus);
-    timeoutOccurred = (SOLVER_RUN_STATUS_TIMEOUT == runStatus);
+    runStatusCode = runAndGetCexForked(vc, builder, stp_e, objects, values, 
+                                       hasSolution, timeout);
+    success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == runStatusCode) ||
+               (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == runStatusCode));    
   } else {
-    runAndGetCex(vc, builder, stp_e, objects, values, hasSolution);
+    runStatusCode = runAndGetCex(vc, builder, stp_e, objects, values, hasSolution);    
     success = true;
   }
   
@@ -734,6 +771,6 @@ STPSolverImpl::computeInitialValues(const Query &query,
   return success;
 }
 
-bool STPSolverImpl::hasTimeoutOccurred() {
-    return timeoutOccurred;
+SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() {
+   return runStatusCode;
 }
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 16a0ea42..1a4663a1 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -8,6 +8,7 @@
 #include "klee/Expr.h"
 #include "klee/ExprBuilder.h"
 #include "klee/Solver.h"
+#include "klee/SolverImpl.h"
 #include "klee/Statistics.h"
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprVisitor.h"
@@ -93,7 +94,7 @@ namespace {
   UseFastCexSolver("use-fast-cex-solver",
 		   cl::init(false));
   
-  // FIXME: Command line argument duplicated in Executor.cpp of Klee. Different
+  // FIXME: Command line argument modified in Executor.cpp of Klee. Different
   // output file name used.
   cl::opt<bool>
   UseSTPQueryPCLog("use-stp-query-pc-log",
@@ -220,7 +221,9 @@ static bool EvaluateInputAST(const char *Filename,
                           result)) {
           std::cout << (result ? "VALID" : "INVALID");
         } else {
-          std::cout << "FAIL";
+          std::cout << "FAIL (reason: " 
+                    << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
+                    << ")";
         }
       } else if (!QC->Values.empty()) {
         assert(QC->Objects.empty() && 
@@ -236,7 +239,9 @@ static bool EvaluateInputAST(const char *Filename,
           std::cout << "INVALID\n";
           std::cout << "\tExpr 0:\t" << result;
         } else {
-          std::cout << "FAIL";
+          std::cout << "FAIL (reason: " 
+                    << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
+                    << ")";
         }
       } else {
         std::vector< std::vector<unsigned char> > result;
@@ -260,7 +265,9 @@ static bool EvaluateInputAST(const char *Filename,
               std::cout << "\n";
           }
         } else {
-          std::cout << "FAIL";
+          std::cout << "FAIL (reason: " 
+                    << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
+                    << ")";
         }
       }