about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/IncompleteSolver.h2
-rw-r--r--include/klee/Solver.h13
-rw-r--r--include/klee/SolverImpl.h9
-rw-r--r--lib/Core/TimingSolver.h6
-rw-r--r--lib/Solver/CachingSolver.cpp10
-rw-r--r--lib/Solver/CexCachingSolver.cpp10
-rw-r--r--lib/Solver/IncompleteSolver.cpp9
-rw-r--r--lib/Solver/IndependentSolver.cpp10
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp7
-rw-r--r--lib/Solver/QueryLoggingSolver.h3
-rw-r--r--lib/Solver/Solver.cpp28
-rw-r--r--tools/kleaver/main.cpp2
12 files changed, 94 insertions, 15 deletions
diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h
index 9a122c74..f589e3b3 100644
--- a/include/klee/IncompleteSolver.h
+++ b/include/klee/IncompleteSolver.h
@@ -102,6 +102,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 }
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 1af30870..8fe33c7c 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -194,6 +194,9 @@ namespace klee {
     //
     // FIXME: This should go into a helper class, and should handle failure.
     virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
+    
+    virtual char *getConstraintLog(const Query& query);
+    virtual void setCoreSolverTimeout(double timeout);
   };
 
   /// STPSolver - A complete solver based on STP.
@@ -207,15 +210,13 @@ namespace klee {
     /// be optimized into add/shift/multiply operations.
     STPSolver(bool useForkedSTP, bool optimizeDivides = true);
 
-    
-    
     /// getConstraintLog - Return the constraint log for the given state in CVC
     /// format.
-    char *getConstraintLog(const Query&);
-    
-    /// setTimeout - Set constraint solver timeout delay to the given value; 0
+    virtual char *getConstraintLog(const Query&);
+
+    /// setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0
     /// is off.
-    void setTimeout(double timeout);
+    virtual void setCoreSolverTimeout(double timeout);
   };
 
   /* *** */
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h
index e200205b..c17082a8 100644
--- a/include/klee/SolverImpl.h
+++ b/include/klee/SolverImpl.h
@@ -93,10 +93,17 @@ namespace klee {
     
     /// 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);
+
+    virtual char *getConstraintLog(const Query& query)  {
+        // dummy
+        return(NULL);
+    }
+
+    virtual void setCoreSolverTimeout(double timeout) {};
 };
 
 }
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index b13879df..2684e071 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -42,7 +42,11 @@ namespace klee {
     }
 
     void setTimeout(double t) {
-      stpSolver->setTimeout(t);
+      stpSolver->setCoreSolverTimeout(t);
+    }
+    
+    char *getConstraintLog(const Query& query) {
+      return solver->getConstraintLog(query);
     }
 
     bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 5911bbf3..674d4627 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -85,6 +85,8 @@ public:
                                               hasSolution);
   }
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 /** @returns the canonical version of the given query.  The reference
@@ -244,6 +246,14 @@ SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();
 }
 
+char *CachingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void CachingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 ///
 
 Solver *klee::createCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index b38df672..df7fffc5 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -83,6 +83,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query& query);
+  void setCoreSolverTimeout(double timeout);
 };
 
 ///
@@ -350,6 +352,14 @@ SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();
 }
 
+char *CexCachingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void CexCachingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 ///
 
 Solver *klee::createCexCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index 7bc8058d..dc2c9fd4 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -138,3 +138,12 @@ StagedSolverImpl::computeInitialValues(const Query& query,
 SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode() {
   return secondary->impl->getOperationStatusCode();
 }
+
+char *StagedSolverImpl::getConstraintLog(const Query& query) {
+  return secondary->impl->getConstraintLog(query);
+}
+
+void StagedSolverImpl::setCoreSolverTimeout(double timeout) {
+  secondary->impl->setCoreSolverTimeout(timeout);
+}
+
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index b3ef1e57..d9fc77dc 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -285,6 +285,8 @@ public:
                                               hasSolution);
   }
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
   
 bool IndependentSolver::computeValidity(const Query& query,
@@ -318,6 +320,14 @@ SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();      
 }
 
+char *IndependentSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void IndependentSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 Solver *klee::createIndependentSolver(Solver *s) {
   return new Solver(new IndependentSolver(s));
 }
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 245ad3bf..e7187fc3 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -183,4 +183,11 @@ SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() {
     return solver->impl->getOperationStatusCode();
 }
 
+char *QueryLoggingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void QueryLoggingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
 
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 527d075b..2c7d80e8 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -70,7 +70,8 @@ public:
                               std::vector< std::vector<unsigned char> > &values,
                               bool &hasSolution);
     SolverRunStatus getOperationStatusCode();
-
+    char *getConstraintLog(const Query&);
+    void setCoreSolverTimeout(double timeout);
 };
 
 #endif	/* KLEE_QUERYLOGGINGSOLVER_H */
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index b3d1613d..3414cda2 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -101,6 +101,14 @@ Solver::~Solver() {
   delete impl; 
 }
 
+char *Solver::getConstraintLog(const Query& query) {
+    return impl->getConstraintLog(query);
+}
+
+void Solver::setCoreSolverTimeout(double timeout) {
+    impl->setCoreSolverTimeout(timeout);
+}
+
 bool Solver::evaluate(const Query& query, Validity &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
@@ -307,6 +315,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 bool ValidatingSolver::computeTruth(const Query& query,
@@ -408,6 +418,14 @@ SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() {
     return solver->impl->getOperationStatusCode();
 }
 
+char *ValidatingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void ValidatingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
   return new Solver(new ValidatingSolver(s, oracle));
 }
@@ -466,9 +484,9 @@ private:
 public:
   STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
-
+  
   char *getConstraintLog(const Query&);
-  void setTimeout(double _timeout) { timeout = _timeout; }
+  void setCoreSolverTimeout(double _timeout) { timeout = _timeout; }
 
   bool computeTruth(const Query&, bool &isValid);
   bool computeValue(const Query&, ref<Expr> &result);
@@ -532,11 +550,11 @@ STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
 }
 
 char *STPSolver::getConstraintLog(const Query &query) {
-  return static_cast<STPSolverImpl*>(impl)->getConstraintLog(query);  
+  return impl->getConstraintLog(query);  
 }
 
-void STPSolver::setTimeout(double timeout) {
-  static_cast<STPSolverImpl*>(impl)->setTimeout(timeout);
+void STPSolver::setCoreSolverTimeout(double timeout) {
+    impl->setCoreSolverTimeout(timeout);
 }
 
 /***/
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 47c4f07f..6c2a29e5 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -216,7 +216,7 @@ static bool EvaluateInputAST(const char *Filename,
   if (!UseDummySolver) {
     STPSolver* stpSolver = new STPSolver(UseForkedCoreSolver);
     if (0 != MaxCoreSolverTime) {
-      stpSolver->setTimeout(MaxCoreSolverTime);    
+      stpSolver->setCoreSolverTimeout(MaxCoreSolverTime);    
     }
     STP = S = stpSolver;
   }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-26 18:39:30 +0000