aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/CachingSolver.cpp5
-rw-r--r--lib/Solver/CexCachingSolver.cpp5
-rw-r--r--lib/Solver/IncompleteSolver.cpp4
-rw-r--r--lib/Solver/IndependentSolver.cpp5
-rw-r--r--lib/Solver/PCLoggingSolver.cpp112
-rw-r--r--lib/Solver/SMTLIBLoggingSolver.cpp5
-rw-r--r--lib/Solver/Solver.cpp57
7 files changed, 148 insertions, 45 deletions
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index c0b77429..f7b88855 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -82,6 +82,7 @@ public:
return solver->impl->computeInitialValues(query, objects, values,
hasSolution);
}
+ bool hasTimeoutOccurred();
};
/** @returns the canonical version of the given query. The reference
@@ -234,6 +235,10 @@ bool CachingSolver::computeTruth(const Query& query,
return true;
}
+bool CachingSolver::hasTimeoutOccurred() {
+ return solver->impl->hasTimeoutOccurred();
+}
+
///
Solver *klee::createCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 19f16821..c84ae409 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -82,6 +82,7 @@ public:
const std::vector<const Array*> &objects,
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution);
+ bool hasTimeoutOccurred();
};
///
@@ -339,6 +340,10 @@ CexCachingSolver::computeInitialValues(const Query& query,
return true;
}
+bool CexCachingSolver::hasTimeoutOccurred() {
+ return solver->impl->hasTimeoutOccurred();
+}
+
///
Solver *klee::createCexCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index a565bab2..45e2ea9b 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -134,3 +134,7 @@ StagedSolverImpl::computeInitialValues(const Query& query,
return secondary->impl->computeInitialValues(query, objects, values,
hasSolution);
}
+
+bool StagedSolverImpl::hasTimeoutOccurred() {
+ return secondary->impl->hasTimeoutOccurred();
+}
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 70f3cab2..0eb86720 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -284,6 +284,7 @@ public:
return solver->impl->computeInitialValues(query, objects, values,
hasSolution);
}
+ bool hasTimeoutOccurred();
};
bool IndependentSolver::computeValidity(const Query& query,
@@ -313,6 +314,10 @@ 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();
+}
+
Solver *klee::createIndependentSolver(Solver *s) {
return new Solver(new IndependentSolver(s));
}
diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
index e7128982..0b31182e 100644
--- a/lib/Solver/PCLoggingSolver.cpp
+++ b/lib/Solver/PCLoggingSolver.cpp
@@ -19,7 +19,8 @@
#include "llvm/Support/CommandLine.h"
#include <fstream>
-
+#include <sstream>
+#include <iostream>
using namespace klee;
using namespace llvm;
using namespace klee::util;
@@ -29,9 +30,17 @@ using namespace klee::util;
class PCLoggingSolver : public SolverImpl {
Solver *solver;
std::ofstream os;
+ std::ostringstream logBuffer; // buffer to store logs before flushing to
+ // file
ExprPPrinter *printer;
unsigned queryCount;
+ int minQueryTimeToLog; // we log to file only those queries
+ // which take longer than specified time (ms);
+ // if this param is negative, log only those queries
+ // on which solver's timed out
+
double startTime;
+ double lastQueryTime;
void startQuery(const Query& query, const char *typeName,
const ref<Expr> *evalExprsBegin = 0,
@@ -40,30 +49,62 @@ class PCLoggingSolver : public SolverImpl {
const Array * const* evalArraysEnd = 0) {
Statistic *S = theStatisticManager->getStatisticByName("Instructions");
uint64_t instructions = S ? S->getValue() : 0;
- os << "# Query " << queryCount++ << " -- "
- << "Type: " << typeName << ", "
- << "Instructions: " << instructions << "\n";
- printer->printQuery(os, query.constraints, query.expr,
+
+ logBuffer << "# Query " << queryCount++ << " -- "
+ << "Type: " << typeName << ", "
+ << "Instructions: " << instructions << "\n";
+ printer->printQuery(logBuffer, query.constraints, query.expr,
evalExprsBegin, evalExprsEnd,
evalArraysBegin, evalArraysEnd);
-
+
startTime = getWallTime();
}
void finishQuery(bool success) {
- double delta = getWallTime() - startTime;
- os << "# " << (success ? "OK" : "FAIL") << " -- "
- << "Elapsed: " << delta << "\n";
+ lastQueryTime = getWallTime() - startTime;
+ logBuffer << "# " << (success ? "OK" : "FAIL") << " -- "
+ << "Elapsed: " << lastQueryTime << "\n";
+
+ if (true == solver->impl->hasTimeoutOccurred()) {
+ logBuffer << "\nSolver TIMEOUT detected\n";
+ }
+ }
+
+ /// flushBuffer - flushes the temporary logs buffer. Depending on threshold
+ /// settings, contents of the buffer are either discarded or written to a file.
+ void flushBuffer(void) {
+ logBuffer.flush();
+
+ if ((0 == minQueryTimeToLog) ||
+ (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) {
+ // we either do not limit logging queries or the query time
+ // is larger than threshold (in ms)
+
+ if ((minQueryTimeToLog >= 0) ||
+ (true == (solver->impl->hasTimeoutOccurred()))) {
+ // we do additional check here to log only timeouts in case
+ // user specified negative value for minQueryTimeToLog param
+ os << logBuffer.str();
+ }
+ }
+
+ // prepare the buffer for reuse
+ logBuffer.clear();
+ logBuffer.str("");
}
public:
- PCLoggingSolver(Solver *_solver, std::string path)
+ PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog)
: solver(_solver),
os(path.c_str(), std::ios::trunc),
- printer(ExprPPrinter::create(os)),
- queryCount(0) {
+ logBuffer(""),
+ printer(ExprPPrinter::create(logBuffer)),
+ queryCount(0),
+ minQueryTimeToLog(queryTimeToLog),
+ startTime(0.0f),
+ lastQueryTime(0.0f) {
}
- ~PCLoggingSolver() {
+ ~PCLoggingSolver() {
delete printer;
delete solver;
}
@@ -73,8 +114,11 @@ public:
bool success = solver->impl->computeTruth(query, isValid);
finishQuery(success);
if (success)
- os << "# Is Valid: " << (isValid ? "true" : "false") << "\n";
- os << "\n";
+ logBuffer << "# Is Valid: " << (isValid ? "true" : "false") << "\n";
+ logBuffer << "\n";
+
+ flushBuffer();
+
return success;
}
@@ -83,8 +127,11 @@ public:
bool success = solver->impl->computeValidity(query, result);
finishQuery(success);
if (success)
- os << "# Validity: " << result << "\n";
- os << "\n";
+ logBuffer << "# Validity: " << result << "\n";
+ logBuffer << "\n";
+
+ flushBuffer();
+
return success;
}
@@ -94,8 +141,11 @@ public:
bool success = solver->impl->computeValue(query, result);
finishQuery(success);
if (success)
- os << "# Result: " << result << "\n";
- os << "\n";
+ logBuffer << "# Result: " << result << "\n";
+ logBuffer << "\n";
+
+ flushBuffer();
+
return success;
}
@@ -115,7 +165,7 @@ public:
values, hasSolution);
finishQuery(success);
if (success) {
- os << "# Solvable: " << (hasSolution ? "true" : "false") << "\n";
+ logBuffer << "# Solvable: " << (hasSolution ? "true" : "false") << "\n";
if (hasSolution) {
std::vector< std::vector<unsigned char> >::iterator
values_it = values.begin();
@@ -123,23 +173,31 @@ public:
e = objects.end(); i != e; ++i, ++values_it) {
const Array *array = *i;
std::vector<unsigned char> &data = *values_it;
- os << "# " << array->name << " = [";
+ logBuffer << "# " << array->name << " = [";
for (unsigned j = 0; j < array->size; j++) {
- os << (int) data[j];
+ logBuffer << (int) data[j];
if (j+1 < array->size)
- os << ",";
+ logBuffer << ",";
}
- os << "]\n";
+ logBuffer << "]\n";
}
}
}
- os << "\n";
+ logBuffer << "\n";
+
+ flushBuffer();
+
return success;
}
+
+ bool hasTimeoutOccurred() {
+ return solver->impl->hasTimeoutOccurred();
+ }
};
///
-Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path) {
- return new Solver(new PCLoggingSolver(_solver, path));
+Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path,
+ int minQueryTimeToLog) {
+ return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog));
}
diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp
index 0fb09424..b3f7eb3b 100644
--- a/lib/Solver/SMTLIBLoggingSolver.cpp
+++ b/lib/Solver/SMTLIBLoggingSolver.cpp
@@ -158,6 +158,11 @@ class SMTLIBLoggingSolver : public SolverImpl
os << "\n";
return success;
}
+
+ bool hasTimeoutOccurred()
+ {
+ return solver->impl->hasTimeoutOccurred();
+ }
};
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 7430a58b..366a7b05 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -273,6 +273,7 @@ public:
const std::vector<const Array*> &objects,
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution);
+ bool hasTimeoutOccurred();
};
bool ValidatingSolver::computeTruth(const Query& query,
@@ -370,6 +371,10 @@ ValidatingSolver::computeInitialValues(const Query& query,
return true;
}
+bool ValidatingSolver::hasTimeoutOccurred() {
+ return solver->impl->hasTimeoutOccurred();
+}
+
Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
return new Solver(new ValidatingSolver(s, oracle));
}
@@ -403,6 +408,10 @@ public:
++stats::queryCounterexamples;
return false;
}
+ bool hasTimeoutOccurred() {
+ return false;
+ }
+
};
Solver *klee::createDummySolver() {
@@ -419,6 +428,7 @@ private:
STPBuilder *builder;
double timeout;
bool useForkedSTP;
+ bool timeoutOccurred;
public:
STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
@@ -433,6 +443,7 @@ public:
const std::vector<const Array*> &objects,
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution);
+ bool hasTimeoutOccurred();
};
static unsigned char *shared_memory_ptr;
@@ -449,7 +460,8 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim
vc(vc_createValidityChecker()),
builder(new STPBuilder(vc, _optimizeDivides)),
timeout(0.0),
- useForkedSTP(_useForkedSTP)
+ useForkedSTP(_useForkedSTP),
+ timeoutOccurred(false)
{
assert(vc && "unable to create validity checker");
assert(builder && "unable to create STPBuilder");
@@ -577,14 +589,14 @@ static void stpTimeoutHandler(int x) {
_exit(52);
}
-static bool 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 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
@@ -597,11 +609,11 @@ static bool runAndGetCexForked(::VC vc,
int pid = fork();
if (pid==-1) {
fprintf(stderr, "error: fork failed (for STP)");
- return false;
+ return SOLVER_RUN_STATUS_FORK_FAILED;
}
if (pid == 0) {
- if (timeout) {
+ if (timeout) {
::alarm(0); /* Turn off alarm so we can safely set signal handler */
::signal(SIGALRM, stpTimeoutHandler);
::alarm(std::max(1, (int)timeout));
@@ -629,7 +641,7 @@ static bool runAndGetCexForked(::VC vc,
if (res < 0) {
fprintf(stderr, "error: waitpid() for STP failed");
- return false;
+ return SOLVER_RUN_STATUS_WAITPID_FAILED;
}
// From timed_run.py: It appears that linux at least will on
@@ -637,7 +649,7 @@ static bool runAndGetCexForked(::VC vc,
// signal, so test signal first.
if (WIFSIGNALED(status) || !WIFEXITED(status)) {
fprintf(stderr, "error: STP did not return successfully");
- return false;
+ return SOLVER_RUN_STATUS_INTERRUPTED;
}
int exitcode = WEXITSTATUS(status);
@@ -647,10 +659,11 @@ static bool runAndGetCexForked(::VC vc,
hasSolution = false;
} else if (exitcode==52) {
fprintf(stderr, "error: STP timed out");
- return false;
+ // mark that a timeout occurred
+ return SOLVER_RUN_STATUS_TIMEOUT;
} else {
fprintf(stderr, "error: STP did not return a recognized code");
- return false;
+ return SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;
}
if (hasSolution) {
@@ -665,7 +678,7 @@ static bool runAndGetCexForked(::VC vc,
}
}
- return true;
+ return SOLVER_RUN_STATUS_SUCCESS;
}
}
@@ -676,6 +689,8 @@ STPSolverImpl::computeInitialValues(const Query &query,
std::vector< std::vector<unsigned char> >
&values,
bool &hasSolution) {
+ timeoutOccurred = false;
+
TimerStatIncrementer t(stats::queryTime);
vc_push(vc);
@@ -698,8 +713,10 @@ STPSolverImpl::computeInitialValues(const Query &query,
bool success;
if (useForkedSTP) {
- success = runAndGetCexForked(vc, builder, stp_e, objects, values,
- hasSolution, timeout);
+ SolverRunStatus runStatus = runAndGetCexForked(vc, builder, stp_e, objects, values,
+ hasSolution, timeout);
+ success = (SOLVER_RUN_STATUS_SUCCESS == runStatus);
+ timeoutOccurred = (SOLVER_RUN_STATUS_TIMEOUT == runStatus);
} else {
runAndGetCex(vc, builder, stp_e, objects, values, hasSolution);
success = true;
@@ -716,3 +733,7 @@ STPSolverImpl::computeInitialValues(const Query &query,
return success;
}
+
+bool STPSolverImpl::hasTimeoutOccurred() {
+ return timeoutOccurred;
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-25 19:37:42 +0000