Commit 39bfc329 authored by Cristian Cadar's avatar Cristian Cadar Committed by Daniel Liew
Browse files

This is a combination of 3 commits. I did this because some commit woulds not compile.

The first commit's message is:
Patch by Tomasz Kuchta that refactors the logging code, by introducing a new logging class hierarchy.

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

Conflicts:

	test/Feature/ExprLogging.c

This is the 2nd commit message:

Forgot to add QueryLoggingSolver in patch 171387 from Tomasz Kuchta.

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

This is the 3rd commit message:

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

Conflicts:

	lib/Solver/Solver.cpp
parent 341e484a
......@@ -101,7 +101,7 @@ public:
const std::vector<const Array*> &objects,
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution);
bool hasTimeoutOccurred();
SolverRunStatus getOperationStatusCode();
};
}
......
......@@ -225,18 +225,13 @@ namespace klee {
/// createSMTLIBLoggingSolver - Create a solver which will forward all queries
/// after writing them to the given path in .smt2 format.
Solver *createSMTLIBLoggingSolver(Solver *s, std::string path);
Solver *createSMTLIBLoggingSolver(Solver *s, std::string path,
int minQueryTimeToLog);
/// createDummySolver - Create a dummy solver implementation which always
/// 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
......@@ -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);
};
}
......
......@@ -333,7 +333,8 @@ Solver *constructSolverChain(STPSolver *stpSolver,
if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB))
{
solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath);
solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath,
MinQueryTimeToLog);
klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str());
}
......@@ -365,7 +366,8 @@ Solver *constructSolverChain(STPSolver *stpSolver,
if (optionIsSet(queryLoggingOptions,ALL_SMTLIB))
{
solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath);
solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
MinQueryTimeToLog);
klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str());
}
......
......@@ -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();
}
///
......
......@@ -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();
}
///
......
......@@ -58,7 +58,10 @@ public:
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution);
virtual bool hasTimeoutOccurred() { return solver->impl->hasTimeoutOccurred(); }
virtual SolverImpl::SolverRunStatus getOperationStatusCode() {
return solver->impl->getOperationStatusCode();
}
};
enum MinMax { mmUnknown, mmMin, mmMax };
......
......@@ -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();
}
......@@ -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) {
......
......@@ -7,192 +7,57 @@
//
//===----------------------------------------------------------------------===//
#include "klee/Solver.h"
#include "QueryLoggingSolver.h"
#include "klee/Expr.h"
#include "klee/SolverImpl.h"
#include "klee/Statistics.h"
#include "klee/util/ExprPPrinter.h"
#include "klee/Internal/Support/QueryLog.h"
#include "klee/Internal/System/Time.h"
#include "llvm/Support/CommandLine.h"
#include <fstream>
#include <sstream>
#include <iostream>
using namespace klee;
using namespace llvm;
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,
const ref<Expr> *evalExprsEnd = 0,
const Array * const* evalArraysBegin = 0,
const Array * const* evalArraysEnd = 0) {
Statistic *S = theStatisticManager->getStatisticByName("Instructions");
uint64_t instructions = S ? S->getValue() : 0;
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) {
lastQueryTime = getWallTime() - startTime;
logBuffer << "# " << (success ? "OK" : "FAIL") << " -- "
<< "Elapsed: " << lastQueryTime << "\n";
if (true == solver->impl->hasTimeoutOccurred()) {
logBuffer << "\nSolver TIMEOUT detected\n";
class PCLoggingSolver : public QueryLoggingSolver {
private :
ExprPPrinter *printer;
virtual void printQuery(const Query& query,
const Query* falseQuery = 0,
const std::vector<const Array*>* objects = 0) {
const ref<Expr>* evalExprsBegin = 0;
const ref<Expr>* evalExprsEnd = 0;
if (0 != falseQuery) {
evalExprsBegin = &query.expr;
evalExprsEnd = &query.expr + 1;
}
const Array* const *evalArraysBegin = 0;
const Array* const *evalArraysEnd = 0;
if ((0 != objects) && (false == objects->empty())) {
evalArraysBegin = &((*objects)[0]);
evalArraysEnd = &((*objects)[0]) + objects->size();
}
const Query* q = (0 == falseQuery) ? &query : falseQuery;
printer->printQuery(logBuffer, q->constraints, q->expr,
evalExprsBegin, evalExprsEnd,
evalArraysBegin, evalArraysEnd);
}
}
/// 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, int queryTimeToLog)
: solver(_solver),
os(path.c_str(), std::ios::trunc),
logBuffer(""),
printer(ExprPPrinter::create(logBuffer)),
queryCount(0),
minQueryTimeToLog(queryTimeToLog),
startTime(0.0f),
lastQueryTime(0.0f) {
}
~PCLoggingSolver() {
delete printer;
delete solver;
}
bool computeTruth(const Query& query, bool &isValid) {
startQuery(query, "Truth");
bool success = solver->impl->computeTruth(query, isValid);
finishQuery(success);
if (success)
logBuffer << "# Is Valid: " << (isValid ? "true" : "false") << "\n";
logBuffer << "\n";
flushBuffer();
PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog)
: QueryLoggingSolver(_solver, path, "#", queryTimeToLog),
printer(ExprPPrinter::create(logBuffer)) {
}
return success;
}
bool computeValidity(const Query& query, Solver::Validity &result) {
startQuery(query, "Validity");
bool success = solver->impl->computeValidity(query, result);
finishQuery(success);
if (success)
logBuffer << "# Validity: " << result << "\n";
logBuffer << "\n";
flushBuffer();
return success;
}
bool computeValue(const Query& query, ref<Expr> &result) {
startQuery(query.withFalse(), "Value",
&query.expr, &query.expr + 1);
bool success = solver->impl->computeValue(query, result);
finishQuery(success);
if (success)
logBuffer << "# Result: " << result << "\n";
logBuffer << "\n";
flushBuffer();
return success;
}
bool computeInitialValues(const Query& query,
const std::vector<const Array*> &objects,
std::vector< std::vector<unsigned char> > &values,
bool &hasSolution) {
if (objects.empty()) {
startQuery(query, "InitialValues",
0, 0);
} else {
startQuery(query, "InitialValues",
0, 0,
&objects[0], &objects[0] + objects.size());
}
bool success = solver->impl->computeInitialValues(query, objects,
values, hasSolution);
finishQuery(success);
if (success) {
logBuffer << "# Solvable: " << (hasSolution ? "true" : "false") << "\n";
if (hasSolution) {
std::vector< std::vector<unsigned char> >::iterator
values_it = values.begin();
for (std::vector<const Array*>::const_iterator i = objects.begin(),
e = objects.end(); i != e; ++i, ++values_it) {
const Array *array = *i;
std::vector<unsigned char> &data = *values_it;
logBuffer << "# " << array->name << " = [";
for (unsigned j = 0; j < array->size; j++) {
logBuffer << (int) data[j];
if (j+1 < array->size)
logBuffer << ",";
}
logBuffer << "]\n";
}
}
}
logBuffer << "\n";
flushBuffer();
return success;
}
bool hasTimeoutOccurred() {
return solver->impl->hasTimeoutOccurred();
}
virtual ~PCLoggingSolver() {
delete printer;
}
};
///
......
//===-- QueryLoggingSolver.cpp --------------------------------------------===//
#include "QueryLoggingSolver.h"
#include "klee/Internal/System/Time.h"
#include "klee/Statistics.h"
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
using namespace klee::util;
QueryLoggingSolver::QueryLoggingSolver(Solver *_solver,
std::string path,
const std::string& commentSign,
int queryTimeToLog)
: solver(_solver),
os(path.c_str(), std::ios::trunc),
logBuffer(""),
queryCount(0),
minQueryTimeToLog(queryTimeToLog),
startTime(0.0f),
lastQueryTime(0.0f),
queryCommentSign(commentSign) {
assert(0 != solver);
}
QueryLoggingSolver::~QueryLoggingSolver() {
delete solver;
}
void QueryLoggingSolver::startQuery(const Query& query, const char* typeName,
const Query* falseQuery,
const std::vector<const Array*> *objects) {
Statistic *S = theStatisticManager->getStatisticByName("Instructions");
uint64_t instructions = S ? S->getValue() : 0;
logBuffer << queryCommentSign << " Query " << queryCount++ << " -- "
<< "Type: " << typeName << ", "
<< "Instructions: " << instructions << "\n";
printQuery(query, falseQuery, objects);
startTime = getWallTime();
}
void QueryLoggingSolver::finishQuery(bool success) {
lastQueryTime = getWallTime() - startTime;
logBuffer << queryCommentSign << " " << (success ? "OK" : "FAIL") << " -- "
<< "Elapsed: " << lastQueryTime << "\n";
if (false == success) {
logBuffer << queryCommentSign << " Failure reason: "
<< SolverImpl::getOperationStatusString(solver->impl->getOperationStatusCode())
<< "\n";
}
}
void QueryLoggingSolver::flushBuffer() {
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) ||
(SOLVER_RUN_STATUS_TIMEOUT == (solver->impl->getOperationStatusCode()))) {
// 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("");
}
bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) {
startQuery(query, "Truth");
bool success = solver->impl->computeTruth(query, isValid);
finishQuery(success);
if (success) {
logBuffer << queryCommentSign << " Is Valid: "
<< (isValid ? "true" : "false") << "\n";
}
logBuffer << "\n";
flushBuffer();
return success;
}
bool QueryLoggingSolver::computeValidity(const Query& query,
Solver::Validity& result) {
startQuery(query, "Validity");
bool success = solver->impl->computeValidity(query, result);
finishQuery(success);
if (success) {
logBuffer << queryCommentSign << " Validity: "
<< result << "\n";
}
logBuffer << "\n";
flushBuffer();
return success;
}
bool QueryLoggingSolver::computeValue(const Query& query, ref<Expr>& result) {
Query withFalse = query.withFalse();
startQuery(query, "Value", &withFalse);
bool success = solver->impl->computeValue(query, result);
finishQuery(success);
if (success) {
logBuffer << queryCommentSign << " Result: " << result << "\n";
}
logBuffer << "\n";
flushBuffer();
return success;
}
bool QueryLoggingSolver::computeInitialValues(const Query& query,
const std::vector<const Array*>& objects,
std::vector<std::vector<unsigned char> >& values,
bool& hasSolution) {
startQuery(query, "InitialValues", 0, &objects);
bool success = solver->impl->computeInitialValues(query, objects,
values, hasSolution);
finishQuery(success);
if (success) {
logBuffer << queryCommentSign << " Solvable: "
<< (hasSolution ? "true" : "false") << "\n";
if (hasSolution) {
std::vector< std::vector<unsigned char> >::iterator
values_it = values.begin();
for (std::vector<const Array*>::const_iterator i = objects.begin(),
e = objects.end(); i != e; ++i, ++values_it) {
const Array *array = *i;
std::vector<unsigned char> &data = *values_it;
logBuffer << queryCommentSign << " " << array->name << " = [";
for (unsigned j = 0; j < array->size; j++) {
logBuffer << (int) data[j];
if (j+1 < array->size) {
logBuffer << ",";
}
}
logBuffer << "]\n";
}
}
}
logBuffer << "\n";
flushBuffer();
return success;
}
SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() {
return solver->impl->getOperationStatusCode();
}
//===-- QueryLoggingSolver.h ---------------------------------------------------===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#ifndef KLEE_QUERYLOGGINGSOLVER_H
#define KLEE_QUERYLOGGINGSOLVER_H
#include "klee/Solver.h"
#include "klee/SolverImpl.h"
#include <fstream>
#include <sstream>
using namespace klee;
/// This abstract class represents a solver that is capable of logging