diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 4 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 19 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 12 | ||||
| -rw-r--r-- | lib/Expr/ExprPPrinter.cpp | 22 | ||||
| -rw-r--r-- | lib/Module/PhiCleaner.cpp | 20 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 310 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 105 |
7 files changed, 252 insertions, 240 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 1724ea06..a0fbda03 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -61,8 +61,8 @@ UseForkedCoreSolver("use-forked-solver", llvm::cl::opt<bool> CoreSolverOptimizeDivides("solver-optimize-divides", - llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"), - llvm::cl::init(true)); + llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=off)"), + llvm::cl::init(false)); /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index dc9edf5f..3b2a860e 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -282,7 +282,7 @@ Executor::Executor(const InterpreterOptions &opts, symPathWriter(0), specialFunctionHandler(0), processTree(0), - replayOut(0), + replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), @@ -736,7 +736,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { } } } else if (res==Solver::Unknown) { - assert(!replayOut && "in replay mode, only one branch can be true."); + assert(!replayKTest && "in replay mode, only one branch can be true."); if ((MaxMemoryInhibit && atMemoryLimit) || current.forkDisabled || @@ -1926,8 +1926,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { count = Expr::createZExtToPointerWidth(count); size = MulExpr::create(size, count); } - bool isLocal = i->getOpcode()==Instruction::Alloca; - executeAlloc(state, size, isLocal, ki); + executeAlloc(state, size, true, ki); break; } @@ -2652,8 +2651,8 @@ std::string Executor::getAddressInfo(ExecutionState &state, } void Executor::terminateState(ExecutionState &state) { - if (replayOut && replayPosition!=replayOut->numObjects) { - klee_warning_once(replayOut, + if (replayKTest && replayPosition!=replayKTest->numObjects) { + klee_warning_once(replayKTest, "replay did not consume all objects in test input."); } @@ -2875,7 +2874,7 @@ void Executor::callExternalFunction(ExecutionState &state, ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, ref<Expr> e) { unsigned n = interpreterOpts.MakeConcreteSymbolic; - if (!n || replayOut || replayPath) + if (!n || replayKTest || replayPath) return e; // right now, we don't replace symbolics (is there any reason to?) @@ -3221,7 +3220,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo, const std::string &name) { // Create a new object state for the memory object (instead of a copy). - if (!replayOut) { + if (!replayKTest) { // Find a unique name for this array. First try the original name, // or if that fails try adding a unique identifier. unsigned id = 0; @@ -3281,10 +3280,10 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } } else { ObjectState *os = bindObjectInState(state, mo, false); - if (replayPosition >= replayOut->numObjects) { + if (replayPosition >= replayKTest->numObjects) { terminateStateOnError(state, "replay count mismatch", "user.err"); } else { - KTestObject *obj = &replayOut->objects[replayPosition++]; + KTestObject *obj = &replayKTest->objects[replayPosition++]; if (obj->numBytes != mo->size) { terminateStateOnError(state, "replay size mismatch", "user.err"); } else { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 8bfa278a..1997bad2 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -150,10 +150,10 @@ private: /// When non-null the bindings that will be used for calls to /// klee_make_symbolic in order replay. - const struct KTest *replayOut; + const struct KTest *replayKTest; /// When non-null a list of branch decisions to be used for replay. const std::vector<bool> *replayPath; - /// The index into the current \ref replayOut or \ref replayPath + /// The index into the current \ref replayKTest or \ref replayPath /// object. unsigned replayPosition; @@ -417,16 +417,16 @@ public: } virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) { symPathWriter = tsw; - } + } - virtual void setReplayOut(const struct KTest *out) { + virtual void setReplayKTest(const struct KTest *out) { assert(!replayPath && "cannot replay both buffer and path"); - replayOut = out; + replayKTest = out; replayPosition = 0; } virtual void setReplayPath(const std::vector<bool> *path) { - assert(!replayOut && "cannot replay both buffer and path"); + assert(!replayKTest && "cannot replay both buffer and path"); replayPath = path; replayPosition = 0; } diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index ddcc57a1..1682d9b5 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -457,6 +457,14 @@ void ExprPPrinter::printConstraints(llvm::raw_ostream &os, printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool)); } +namespace { + +struct ArrayPtrsByName { + bool operator()(const Array *a1, const Array *a2) const { + return a1->name < a2->name; + } +}; +} void ExprPPrinter::printQuery(llvm::raw_ostream &os, const ConstraintManager &constraints, @@ -482,13 +490,15 @@ void ExprPPrinter::printQuery(llvm::raw_ostream &os, if (printArrayDecls) { for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it) p.usedArrays.insert(*it); - for (std::set<const Array*>::iterator it = p.usedArrays.begin(), - ie = p.usedArrays.end(); it != ie; ++it) { + std::vector<const Array *> sortedArray(p.usedArrays.begin(), + p.usedArrays.end()); + std::sort(sortedArray.begin(), sortedArray.end(), ArrayPtrsByName()); + for (std::vector<const Array *>::iterator it = sortedArray.begin(), + ie = sortedArray.end(); + it != ie; ++it) { const Array *A = *it; - // FIXME: Print correct name, domain, and range. - PC << "array " << A->name - << "[" << A->size << "]" - << " : " << "w32" << " -> " << "w8" << " = "; + PC << "array " << A->name << "[" << A->size << "]" + << " : w" << A->domain << " -> w" << A->range << " = "; if (A->isSymbolicArray()) { PC << "symbolic"; } else { diff --git a/lib/Module/PhiCleaner.cpp b/lib/Module/PhiCleaner.cpp index 3d8d7867..2cf3ba4a 100644 --- a/lib/Module/PhiCleaner.cpp +++ b/lib/Module/PhiCleaner.cpp @@ -39,16 +39,16 @@ bool klee::PhiCleanerPass::runOnFunction(Function &f) { if (pi->getIncomingBlock(i) != reference->getIncomingBlock(i)) break; - if (i!=numBlocks) { - std::vector<Value*> values; - values.reserve(numBlocks); - for (unsigned i=0; i<numBlocks; i++) - values[i] = pi->getIncomingValueForBlock(reference->getIncomingBlock(i)); - for (unsigned i=0; i<numBlocks; i++) { - pi->setIncomingBlock(i, reference->getIncomingBlock(i)); - pi->setIncomingValue(i, values[i]); - } - changed = true; + if (i != numBlocks) { + std::vector<Value*> values; + values.reserve(numBlocks); + for (unsigned i = 0; i<numBlocks; i++) + values.push_back(pi->getIncomingValueForBlock(reference->getIncomingBlock(i))); + for (unsigned i = 0; i<numBlocks; i++) { + pi->setIncomingBlock(i, reference->getIncomingBlock(i)); + pi->setIncomingValue(i, values[i]); + } + changed = true; } // see if it uses any previously defined phi nodes diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 5484a319..f93bec3c 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -1,13 +1,4 @@ //===-- QueryLoggingSolver.cpp --------------------------------------------===// - -#include "QueryLoggingSolver.h" -#include "klee/Internal/System/Time.h" -#include "klee/Statistics.h" - -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) -#include "llvm/Support/FileSystem.h" -#endif - // // The KLEE Symbolic Virtual Machine // @@ -15,188 +6,203 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// +#include "QueryLoggingSolver.h" +#include "klee/Internal/System/Time.h" +#include "klee/Statistics.h" + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#include "llvm/Support/FileSystem.h" +#endif using namespace klee::util; -QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, - std::string path, - const std::string& commentSign, - int queryTimeToLog) +namespace { +llvm::cl::opt<bool> DumpPartialQueryiesEarly( + "log-partial-queries-early", llvm::cl::init(false), + llvm::cl::desc("Log queries before calling the solver (default=off)")); +} + +QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, + const std::string &commentSign, + int queryTimeToLog) : solver(_solver), #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) os(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text), #else os(path.c_str(), ErrorInfo), #endif - BufferString(""), - logBuffer(BufferString), - queryCount(0), - minQueryTimeToLog(queryTimeToLog), - startTime(0.0f), - lastQueryTime(0.0f), + BufferString(""), logBuffer(BufferString), queryCount(0), + minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f), queryCommentSign(commentSign) { - assert(0 != solver); + assert(0 != solver); } -QueryLoggingSolver::~QueryLoggingSolver() { - delete solver; +QueryLoggingSolver::~QueryLoggingSolver() { delete solver; } + +void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) { + logBuffer.flush(); + if (writeToFile) { + os << logBuffer.str(); + os.flush(); + } + // prepare the buffer for reuse + BufferString = ""; } -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::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); + + if (DumpPartialQueryiesEarly) { + flushBufferConditionally(true); + } + 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"; - } + 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(); - os.flush(); - } - } - - // prepare the buffer for reuse - BufferString = ""; + bool writeToFile = false; + + 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 + writeToFile = true; + } + } + + flushBufferConditionally(writeToFile); } -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::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::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 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 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"; - } +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; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() { - return solver->impl->getOperationStatusCode(); + return solver->impl->getOperationStatusCode(); } -char *QueryLoggingSolver::getConstraintLog(const Query& query) { +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 ad1722ca..bb266c67 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -1,4 +1,5 @@ -//===-- QueryLoggingSolver.h ---------------------------------------------------===// +//===-- QueryLoggingSolver.h +//---------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -8,75 +9,71 @@ //===----------------------------------------------------------------------===// #ifndef KLEE_QUERYLOGGINGSOLVER_H -#define KLEE_QUERYLOGGINGSOLVER_H +#define KLEE_QUERYLOGGINGSOLVER_H #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "llvm/Support/raw_ostream.h" -#include <fstream> -#include <sstream> using namespace klee; -/// This abstract class represents a solver that is capable of logging +/// This abstract class represents a solver that is capable of logging /// queries to a file. /// Derived classes might specialize this one by providing different formats /// for the query output. class QueryLoggingSolver : public SolverImpl { protected: - Solver *solver; - std::string ErrorInfo; - llvm::raw_fd_ostream os; - // @brief Buffer used by logBuffer - std::string BufferString; - // @brief buffer to store logs before flushing to file - llvm::raw_string_ostream logBuffer; - unsigned queryCount; - int minQueryTimeToLog; // we log to file only those queries - // which take longer than the specified time (ms); - // if this param is negative, log only those queries - // on which the solver has timed out + Solver *solver; + std::string ErrorInfo; + llvm::raw_fd_ostream os; + // @brief Buffer used by logBuffer + std::string BufferString; + // @brief buffer to store logs before flushing to file + llvm::raw_string_ostream logBuffer; + unsigned queryCount; + int minQueryTimeToLog; // we log to file only those queries + // which take longer than the specified time (ms); + // if this param is negative, log only those queries + // on which the solver has timed out - double startTime; - double lastQueryTime; - const std::string queryCommentSign; // sign representing commented lines - // in given a query format + double startTime; + double lastQueryTime; + const std::string queryCommentSign; // sign representing commented lines + // in given a query format + + virtual void startQuery(const Query &query, const char *typeName, + const Query *falseQuery = 0, + const std::vector<const Array *> *objects = 0); + + virtual void finishQuery(bool success); + + /// 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); + + virtual void printQuery(const Query &query, const Query *falseQuery = 0, + const std::vector<const Array *> *objects = 0) = 0; + void flushBufferConditionally(bool writeToFile); - virtual void startQuery(const Query& query, const char* typeName, - const Query* falseQuery = 0, - const std::vector<const Array*>* objects = 0); - - virtual void finishQuery(bool success); - - /// 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); - - virtual void printQuery(const Query& query, - const Query* falseQuery = 0, - const std::vector<const Array*>* objects = 0) = 0; - public: - QueryLoggingSolver(Solver *_solver, - std::string path, - const std::string& commentSign, - int queryTimeToLog); - - virtual ~QueryLoggingSolver(); + QueryLoggingSolver(Solver *_solver, std::string path, + const std::string &commentSign, int queryTimeToLog); - /// implementation of the SolverImpl interface - bool computeTruth(const Query& query, bool &isValid); - bool computeValidity(const Query& query, Solver::Validity &result); - bool computeValue(const Query& query, ref<Expr> &result); - bool computeInitialValues(const Query& query, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values, - bool &hasSolution); - SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query&); - void setCoreSolverTimeout(double timeout); -}; + virtual ~QueryLoggingSolver(); -#endif /* KLEE_QUERYLOGGINGSOLVER_H */ + /// implementation of the SolverImpl interface + bool computeTruth(const Query &query, bool &isValid); + bool computeValidity(const Query &query, Solver::Validity &result); + bool computeValue(const Query &query, ref<Expr> &result); + bool computeInitialValues(const Query &query, + const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double timeout); +}; +#endif /* KLEE_QUERYLOGGINGSOLVER_H */ |