diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
| -rw-r--r-- | lib/Core/Executor.cpp | 184 |
1 files changed, 115 insertions, 69 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ef55f21f..f31d6aeb 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -47,6 +47,7 @@ #include "klee/Internal/Module/KModule.h" #include "klee/Internal/Support/FloatEvaluation.h" #include "klee/Internal/System/Time.h" +#include "klee/Internal/System/MemoryUsage.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) #include "llvm/IR/Function.h" @@ -85,8 +86,8 @@ #include <cassert> #include <algorithm> -#include <iostream> #include <iomanip> +#include <iosfwd> #include <fstream> #include <sstream> #include <vector> @@ -163,6 +164,11 @@ namespace { SimplifySymIndices("simplify-sym-indices", cl::init(false)); + cl::opt<bool> + EqualitySubstitution("equality-substitution", + cl::init(true), + cl::desc("Simplify equality expressions before querying the solver (default=on).")); + cl::opt<unsigned> MaxSymArraySize("max-sym-array-size", cl::init(0)); @@ -315,7 +321,7 @@ Executor::Executor(const InterpreterOptions &opts, assert(false); break; }; - std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; } else { coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); @@ -332,7 +338,7 @@ Executor::Executor(const InterpreterOptions &opts, interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); - this->solver = new TimingSolver(solver); + this->solver = new TimingSolver(solver, EqualitySubstitution); memory = new MemoryManager(); } @@ -1104,12 +1110,13 @@ Executor::toConstant(ExecutionState &state, bool success = solver->getValue(state, e, value); assert(success && "FIXME: Unhandled solver failure"); (void) success; - - std::ostringstream os; - os << "silently concretizing (reason: " << reason << ") expression " << e - << " to value " << value - << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")"; - + + std::string str; + llvm::raw_string_ostream os(str); + os << "silently concretizing (reason: " << reason << ") expression " << e + << " to value " << value << " (" << (*(state.pc)).info->file << ":" + << (*(state.pc)).info->line << ")"; + if (AllExternalWarnings) klee_warning(reason, os.str().c_str()); else @@ -1166,7 +1173,7 @@ void Executor::executeGetValue(ExecutionState &state, void Executor::stepInstruction(ExecutionState &state) { if (DebugPrintInstructions) { printFileLine(state, state.pc); - std::cerr << std::setw(10) << stats::instructions << " "; + llvm::errs().indent(10) << stats::instructions << " "; llvm::errs() << *(state.pc->inst) << '\n'; } @@ -1350,10 +1357,10 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src, void Executor::printFileLine(ExecutionState &state, KInstruction *ki) { const InstructionInfo &ii = *ki->info; - if (ii.file != "") - std::cerr << " " << ii.file << ":" << ii.line << ":"; + if (ii.file != "") + llvm::errs() << " " << ii.file << ":" << ii.line << ":"; else - std::cerr << " [no debug info]:"; + llvm::errs() << " [no debug info]:"; } /// Compute the true target of a function call, resolving LLVM and KLEE aliases @@ -2584,11 +2591,7 @@ void Executor::run(ExecutionState &initialState) { // We need to avoid calling GetMallocUsage() often because it // is O(elts on freelist). This is really bad since we start // to pummel the freelist once we hit the memory cap. -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) - unsigned mbs = sys::Process::GetMallocUsage() >> 20; -#else - unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20; -#endif + unsigned mbs = util::GetTotalMallocUsage() >> 20; if (mbs > MaxMemory) { if (mbs > MaxMemory + 100) { // just guess at how many to kill @@ -2627,7 +2630,7 @@ void Executor::run(ExecutionState &initialState) { dump: if (DumpStatesOnHalt && !states.empty()) { - std::cerr << "KLEE: halting execution, dumping remaining states\n"; + llvm::errs() << "KLEE: halting execution, dumping remaining states\n"; for (std::set<ExecutionState*>::iterator it = states.begin(), ie = states.end(); it != ie; ++it) { @@ -2641,7 +2644,8 @@ void Executor::run(ExecutionState &initialState) { std::string Executor::getAddressInfo(ExecutionState &state, ref<Expr> address) const{ - std::ostringstream info; + std::string Str; + llvm::raw_string_ostream info(Str); info << "\taddress: " << address << "\n"; uint64_t example; if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) { @@ -2729,29 +2733,74 @@ void Executor::terminateStateOnExit(ExecutionState &state) { terminateState(state); } +const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state, + Instruction ** lastInstruction) { + // unroll the stack of the applications state and find + // the last instruction which is not inside a KLEE internal function + ExecutionState::stack_ty::const_reverse_iterator it = state.stack.rbegin(), + itE = state.stack.rend(); + + // don't check beyond the outermost function (i.e. main()) + itE--; + + const InstructionInfo * ii = 0; + if (kmodule->internalFunctions.count(it->kf->function) == 0){ + ii = state.prevPC->info; + *lastInstruction = state.prevPC->inst; + // Cannot return yet because even though + // it->function is not an internal function it might of + // been called from an internal function. + } + + // Wind up the stack and check if we are in a KLEE internal function. + // We visit the entire stack because we want to return a CallInstruction + // that was not reached via any KLEE internal functions. + for (;it != itE; ++it) { + // check calling instruction and if it is contained in a KLEE internal function + const Function * f = (*it->caller).inst->getParent()->getParent(); + if (kmodule->internalFunctions.count(f)){ + ii = 0; + continue; + } + if (!ii){ + ii = (*it->caller).info; + *lastInstruction = (*it->caller).inst; + } + } + + if (!ii) { + // something went wrong, play safe and return the current instruction info + *lastInstruction = state.prevPC->inst; + return *state.prevPC->info; + } + return *ii; +} void Executor::terminateStateOnError(ExecutionState &state, const llvm::Twine &messaget, const char *suffix, const llvm::Twine &info) { std::string message = messaget.str(); static std::set< std::pair<Instruction*, std::string> > emittedErrors; - const InstructionInfo &ii = *state.prevPC->info; + Instruction * lastInst; + const InstructionInfo &ii = getLastNonKleeInternalInstruction(state, &lastInst); if (EmitAllErrors || - emittedErrors.insert(std::make_pair(state.prevPC->inst, message)).second) { + emittedErrors.insert(std::make_pair(lastInst, message)).second) { if (ii.file != "") { klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str()); } else { - klee_message("ERROR: %s", message.c_str()); + klee_message("ERROR: (location information missing) %s", message.c_str()); } if (!EmitAllErrors) klee_message("NOTE: now ignoring this error at this location"); - - std::ostringstream msg; + + std::string MsgString; + llvm::raw_string_ostream msg(MsgString); msg << "Error: " << message << "\n"; if (ii.file != "") { msg << "File: " << ii.file << "\n"; msg << "Line: " << ii.line << "\n"; + msg << "assembly.ll line: " << ii.assemblyLine << "\n"; } msg << "Stack: \n"; state.dumpStack(msg); @@ -2759,6 +2808,7 @@ void Executor::terminateStateOnError(ExecutionState &state, std::string info_str = info.str(); if (info_str != "") msg << "Info: \n" << info_str; + interpreterHandler->processTestCase(state, msg.str().c_str(), suffix); } @@ -2783,8 +2833,8 @@ void Executor::callExternalFunction(ExecutionState &state, return; if (NoExternals && !okExternals.count(function->getName())) { - std::cerr << "KLEE:ERROR: Calling not-OK external function : " - << function->getName().str() << "\n"; + llvm::errs() << "KLEE:ERROR: Calling not-OK external function : " + << function->getName().str() << "\n"; terminateStateOnError(state, "externals disallowed", "user.err"); return; } @@ -2823,7 +2873,9 @@ void Executor::callExternalFunction(ExecutionState &state, state.addressSpace.copyOutConcretes(); if (!SuppressExternalWarnings) { - std::ostringstream os; + + std::string TmpStr; + llvm::raw_string_ostream os(TmpStr); os << "calling external: " << function->getName().str() << "("; for (unsigned i=0; i<arguments.size(); i++) { os << arguments[i]; @@ -2867,11 +2919,11 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, if (!n || replayOut || replayPath) return e; - // right now, we don't replace symbolics (is there any reason too?) + // right now, we don't replace symbolics (is there any reason to?) if (!isa<ConstantExpr>(e)) return e; - if (n != 1 && random() % n) + if (n != 1 && random() % n) return e; // create a new fresh location, assert it is equal to concrete value in e @@ -2882,7 +2934,7 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, Expr::getMinBytesForWidth(e->getWidth())); ref<Expr> res = Expr::createTempRead(array, e->getWidth()); ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res)); - std::cerr << "Making symbolic: " << eq << "\n"; + llvm::errs() << "Making symbolic: " << eq << "\n"; state.addConstraint(eq); return res; } @@ -2994,7 +3046,9 @@ void Executor::executeAlloc(ExecutionState &state, } if (hugeSize.second) { - std::ostringstream info; + + std::string Str; + llvm::raw_string_ostream info(Str); ExprPPrinter::printOne(info, " size expr", size); info << " concretization : " << example << "\n"; info << " unbound example: " << tmp << "\n"; @@ -3392,48 +3446,41 @@ unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) { return state.symPathOS.getID(); } -void Executor::getConstraintLog(const ExecutionState &state, - std::string &res, +void Executor::getConstraintLog(const ExecutionState &state, std::string &res, Interpreter::LogType logFormat) { std::ostringstream info; - switch(logFormat) - { - case STP: - { - Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - char *log = solver->getConstraintLog(query); - res = std::string(log); - free(log); - } - break; - - case KQUERY: - { - std::ostringstream info; - ExprPPrinter::printConstraints(info, state.constraints); - res = info.str(); - } - break; - - case SMTLIB2: - { - std::ostringstream info; - ExprSMTLIBPrinter* printer = createSMTLIBPrinter(); - printer->setOutput(info); - Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - printer->setQuery(query); - printer->generateOutput(); - res = info.str(); - delete printer; - } - break; + switch (logFormat) { + case STP: { + Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); + char *log = solver->getConstraintLog(query); + res = std::string(log); + free(log); + } break; + + case KQUERY: { + std::string Str; + llvm::raw_string_ostream info(Str); + ExprPPrinter::printConstraints(info, state.constraints); + res = info.str(); + } break; + + case SMTLIB2: { + std::string Str; + llvm::raw_string_ostream info(Str); + ExprSMTLIBPrinter *printer = createSMTLIBPrinter(); + printer->setOutput(info); + Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); + printer->setQuery(query); + printer->generateOutput(); + res = info.str(); + delete printer; + } break; default: - klee_warning("Executor::getConstraintLog() : Log format not supported!"); + klee_warning("Executor::getConstraintLog() : Log format not supported!"); } - } bool Executor::getSymbolicSolution(const ExecutionState &state, @@ -3468,8 +3515,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, solver->setTimeout(0); if (!success) { klee_warning("unable to compute initial values (invalid constraints?)!"); - ExprPPrinter::printQuery(std::cerr, - state.constraints, + ExprPPrinter::printQuery(llvm::errs(), state.constraints, ConstantExpr::alloc(0, Expr::Bool)); return false; } |