diff options
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/ExecutionState.cpp | 66 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 117 | ||||
-rw-r--r-- | lib/Core/ExecutorTimers.cpp | 6 | ||||
-rw-r--r-- | lib/Core/ExecutorUtil.cpp | 3 | ||||
-rw-r--r-- | lib/Core/ExternalDispatcher.cpp | 3 | ||||
-rw-r--r-- | lib/Core/ImpliedValue.cpp | 3 | ||||
-rw-r--r-- | lib/Core/Memory.cpp | 19 | ||||
-rw-r--r-- | lib/Core/PTree.cpp | 3 | ||||
-rw-r--r-- | lib/Core/PTree.h | 6 | ||||
-rw-r--r-- | lib/Core/Searcher.cpp | 23 | ||||
-rw-r--r-- | lib/Core/Searcher.h | 27 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 34 | ||||
-rw-r--r-- | lib/Core/StatsTracker.cpp | 13 | ||||
-rw-r--r-- | lib/Core/StatsTracker.h | 4 | ||||
-rw-r--r-- | lib/Core/UserSearcher.cpp | 2 |
15 files changed, 163 insertions, 166 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index b2c2a737..e81c776c 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -23,9 +23,10 @@ #include "llvm/Function.h" #endif #include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" -#include <iostream> #include <iomanip> +#include <sstream> #include <cassert> #include <map> #include <set> @@ -177,7 +178,7 @@ void ExecutionState::removeFnAlias(std::string fn) { /**/ -std::ostream &klee::operator<<(std::ostream &os, const MemoryMap &mm) { +llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, const MemoryMap &mm) { os << "{"; MemoryMap::iterator it = mm.begin(); MemoryMap::iterator ie = mm.end(); @@ -192,8 +193,8 @@ std::ostream &klee::operator<<(std::ostream &os, const MemoryMap &mm) { bool ExecutionState::merge(const ExecutionState &b) { if (DebugLogStateMerge) - std::cerr << "-- attempting merge of A:" - << this << " with B:" << &b << "--\n"; + llvm::errs() << "-- attempting merge of A:" << this << " with B:" << &b + << "--\n"; if (pc != b.pc) return false; @@ -230,21 +231,24 @@ bool ExecutionState::merge(const ExecutionState &b) { commonConstraints.begin(), commonConstraints.end(), std::inserter(bSuffix, bSuffix.end())); if (DebugLogStateMerge) { - std::cerr << "\tconstraint prefix: ["; - for (std::set< ref<Expr> >::iterator it = commonConstraints.begin(), - ie = commonConstraints.end(); it != ie; ++it) - std::cerr << *it << ", "; - std::cerr << "]\n"; - std::cerr << "\tA suffix: ["; - for (std::set< ref<Expr> >::iterator it = aSuffix.begin(), - ie = aSuffix.end(); it != ie; ++it) - std::cerr << *it << ", "; - std::cerr << "]\n"; - std::cerr << "\tB suffix: ["; - for (std::set< ref<Expr> >::iterator it = bSuffix.begin(), - ie = bSuffix.end(); it != ie; ++it) - std::cerr << *it << ", "; - std::cerr << "]\n"; + llvm::errs() << "\tconstraint prefix: ["; + for (std::set<ref<Expr> >::iterator it = commonConstraints.begin(), + ie = commonConstraints.end(); + it != ie; ++it) + llvm::errs() << *it << ", "; + llvm::errs() << "]\n"; + llvm::errs() << "\tA suffix: ["; + for (std::set<ref<Expr> >::iterator it = aSuffix.begin(), + ie = aSuffix.end(); + it != ie; ++it) + llvm::errs() << *it << ", "; + llvm::errs() << "]\n"; + llvm::errs() << "\tB suffix: ["; + for (std::set<ref<Expr> >::iterator it = bSuffix.begin(), + ie = bSuffix.end(); + it != ie; ++it) + llvm::errs() << *it << ", "; + llvm::errs() << "]\n"; } // We cannot merge if addresses would resolve differently in the @@ -257,9 +261,9 @@ bool ExecutionState::merge(const ExecutionState &b) { // and not the other if (DebugLogStateMerge) { - std::cerr << "\tchecking object states\n"; - std::cerr << "A: " << addressSpace.objects << "\n"; - std::cerr << "B: " << b.addressSpace.objects << "\n"; + llvm::errs() << "\tchecking object states\n"; + llvm::errs() << "A: " << addressSpace.objects << "\n"; + llvm::errs() << "B: " << b.addressSpace.objects << "\n"; } std::set<const MemoryObject*> mutated; @@ -271,22 +275,22 @@ bool ExecutionState::merge(const ExecutionState &b) { if (ai->first != bi->first) { if (DebugLogStateMerge) { if (ai->first < bi->first) { - std::cerr << "\t\tB misses binding for: " << ai->first->id << "\n"; + llvm::errs() << "\t\tB misses binding for: " << ai->first->id << "\n"; } else { - std::cerr << "\t\tA misses binding for: " << bi->first->id << "\n"; + llvm::errs() << "\t\tA misses binding for: " << bi->first->id << "\n"; } } return false; } if (ai->second != bi->second) { if (DebugLogStateMerge) - std::cerr << "\t\tmutated: " << ai->first->id << "\n"; + llvm::errs() << "\t\tmutated: " << ai->first->id << "\n"; mutated.insert(ai->first); } } if (ai!=ae || bi!=be) { if (DebugLogStateMerge) - std::cerr << "\t\tmappings differ\n"; + llvm::errs() << "\t\tmappings differ\n"; return false; } @@ -348,7 +352,7 @@ bool ExecutionState::merge(const ExecutionState &b) { return true; } -void ExecutionState::dumpStack(std::ostream &out) const { +void ExecutionState::dumpStack(llvm::raw_ostream &out) const { unsigned idx = 0; const KInstruction *target = prevPC; for (ExecutionState::stack_ty::const_reverse_iterator @@ -357,9 +361,11 @@ void ExecutionState::dumpStack(std::ostream &out) const { const StackFrame &sf = *it; Function *f = sf.kf->function; const InstructionInfo &ii = *target->info; - out << "\t#" << idx++ - << " " << std::setw(8) << std::setfill('0') << ii.assemblyLine - << " in " << f->getName().str() << " ("; + out << "\t#" << idx++; + std::stringstream AssStream; + AssStream << std::setw(8) << std::setfill('0') << ii.assemblyLine; + out << AssStream.str(); + out << " in " << f->getName().str() << " ("; // Yawn, we could go up and print varargs if we wanted to. unsigned index = 0; for (Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end(); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index abb023eb..3a07138d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -86,8 +86,8 @@ #include <cassert> #include <algorithm> -#include <iostream> #include <iomanip> +#include <iosfwd> #include <fstream> #include <sstream> #include <vector> @@ -316,7 +316,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); @@ -1105,12 +1105,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 @@ -1167,7 +1168,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'; } @@ -1351,10 +1352,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 @@ -2624,7 +2625,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) { @@ -2638,7 +2639,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)) { @@ -2786,8 +2788,9 @@ void Executor::terminateStateOnError(ExecutionState &state, } 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"; @@ -2800,7 +2803,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); + interpreterHandler->processTestCase(state, MsgString.c_str(), suffix); } terminateState(state); @@ -2824,8 +2827,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; } @@ -2864,7 +2867,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]; @@ -2923,7 +2928,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; } @@ -3035,7 +3040,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"; @@ -3433,48 +3440,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, @@ -3509,8 +3509,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; } diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index 06fd4be7..e4622d85 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -53,7 +53,7 @@ public: ~HaltTimer() {} void run() { - std::cerr << "KLEE: HaltTimer invoked\n"; + llvm::errs() << "KLEE: HaltTimer invoked\n"; executor->setHaltExecution(true); } }; @@ -122,7 +122,7 @@ void Executor::processTimers(ExecutionState *current, if (dumpPTree) { char name[32]; sprintf(name, "ptree%08d.dot", (int) stats::instructions); - std::ostream *os = interpreterHandler->openOutputFile(name); + llvm::raw_ostream *os = interpreterHandler->openOutputFile(name); if (os) { processTree->dump(*os); delete os; @@ -132,7 +132,7 @@ void Executor::processTimers(ExecutionState *current, } if (dumpStates) { - std::ostream *os = interpreterHandler->openOutputFile("states.txt"); + llvm::raw_ostream *os = interpreterHandler->openOutputFile("states.txt"); if (os) { for (std::set<ExecutionState*>::const_iterator it = states.begin(), diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 0d828ec4..f6b3dd5e 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -41,7 +41,6 @@ #include "llvm/Support/CallSite.h" -#include <iostream> #include <cassert> using namespace klee; @@ -62,7 +61,7 @@ namespace klee { switch (ce->getOpcode()) { default : ce->dump(); - std::cerr << "error: unknown ConstantExpr type\n" + llvm::errs() << "error: unknown ConstantExpr type\n" << "opcode: " << ce->getOpcode() << "\n"; abort(); diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 2dc16767..4c1e2b86 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -42,7 +42,6 @@ #endif #include <setjmp.h> #include <signal.h> -#include <iostream> using namespace llvm; using namespace klee; @@ -92,7 +91,7 @@ ExternalDispatcher::ExternalDispatcher() { std::string error; executionEngine = ExecutionEngine::createJIT(dispatchModule, &error); if (!executionEngine) { - std::cerr << "unable to make jit: " << error << "\n"; + llvm::errs() << "unable to make jit: " << error << "\n"; abort(); } diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index 56c1d1a9..c8342df1 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -18,7 +18,6 @@ #include "klee/util/ExprUtil.h" -#include <iostream> #include <map> #include <set> @@ -246,7 +245,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e, } else { if (it!=found.end()) { ref<Expr> binding = it->second; - std::cerr << "checkForImpliedValues: " << e << " = " << value << "\n" + llvm::errs() << "checkForImpliedValues: " << e << " = " << value << "\n" << "\t\t implies " << var << " == " << binding << " (error)\n"; assert(0); diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 4bcdd9f7..b6f225d1 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -32,7 +32,6 @@ #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" -#include <iostream> #include <cassert> #include <sstream> @@ -585,23 +584,23 @@ void ObjectState::write64(unsigned offset, uint64_t value) { } void ObjectState::print() { - std::cerr << "-- ObjectState --\n"; - std::cerr << "\tMemoryObject ID: " << object->id << "\n"; - std::cerr << "\tRoot Object: " << updates.root << "\n"; - std::cerr << "\tSize: " << size << "\n"; + llvm::errs() << "-- ObjectState --\n"; + llvm::errs() << "\tMemoryObject ID: " << object->id << "\n"; + llvm::errs() << "\tRoot Object: " << updates.root << "\n"; + llvm::errs() << "\tSize: " << size << "\n"; - std::cerr << "\tBytes:\n"; + llvm::errs() << "\tBytes:\n"; for (unsigned i=0; i<size; i++) { - std::cerr << "\t\t["<<i<<"]" + llvm::errs() << "\t\t["<<i<<"]" << " concrete? " << isByteConcrete(i) << " known-sym? " << isByteKnownSymbolic(i) << " flushed? " << isByteFlushed(i) << " = "; ref<Expr> e = read8(i); - std::cerr << e << "\n"; + llvm::errs() << e << "\n"; } - std::cerr << "\tUpdates:\n"; + llvm::errs() << "\tUpdates:\n"; for (const UpdateNode *un=updates.head; un; un=un->next) { - std::cerr << "\t\t[" << un->index << "] = " << un->value << "\n"; + llvm::errs() << "\t\t[" << un->index << "] = " << un->value << "\n"; } } diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index 349761cd..f0e7ab51 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -13,7 +13,6 @@ #include <klee/util/ExprPPrinter.h> #include <vector> -#include <iostream> using namespace klee; @@ -51,7 +50,7 @@ void PTree::remove(Node *n) { } while (n && !n->left && !n->right); } -void PTree::dump(std::ostream &os) { +void PTree::dump(llvm::raw_ostream &os) { ExprPPrinter *pp = ExprPPrinter::create(os); pp->setNewline("\\l"); os << "digraph G {\n"; diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index 6accc8e2..11d3f48c 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -12,10 +12,6 @@ #include <klee/Expr.h> -#include <utility> -#include <cassert> -#include <iostream> - namespace klee { class ExecutionState; @@ -34,7 +30,7 @@ namespace klee { const data_type &rightData); void remove(Node *n); - void dump(std::ostream &os); + void dump(llvm::raw_ostream &os); }; class PTreeNode { diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 8c3e26bc..2610f17e 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -411,17 +411,17 @@ ExecutionState &MergingSearcher::selectState() { } if (DebugLogMerge) - std::cerr << "-- all at merge --\n"; + llvm::errs() << "-- all at merge --\n"; for (std::map<Instruction*, std::vector<ExecutionState*> >::iterator it = merges.begin(), ie = merges.end(); it != ie; ++it) { if (DebugLogMerge) { - std::cerr << "\tmerge: " << it->first << " ["; + llvm::errs() << "\tmerge: " << it->first << " ["; for (std::vector<ExecutionState*>::iterator it2 = it->second.begin(), ie2 = it->second.end(); it2 != ie2; ++it2) { ExecutionState *state = *it2; - std::cerr << state << ", "; + llvm::errs() << state << ", "; } - std::cerr << "]\n"; + llvm::errs() << "]\n"; } // merge states @@ -440,13 +440,13 @@ ExecutionState &MergingSearcher::selectState() { } } if (DebugLogMerge && !toErase.empty()) { - std::cerr << "\t\tmerged: " << base << " with ["; + llvm::errs() << "\t\tmerged: " << base << " with ["; for (std::set<ExecutionState*>::iterator it = toErase.begin(), ie = toErase.end(); it != ie; ++it) { - if (it!=toErase.begin()) std::cerr << ", "; - std::cerr << *it; + if (it!=toErase.begin()) llvm::errs() << ", "; + llvm::errs() << *it; } - std::cerr << "]\n"; + llvm::errs() << "]\n"; } for (std::set<ExecutionState*>::iterator it = toErase.begin(), ie = toErase.end(); it != ie; ++it) { @@ -464,7 +464,7 @@ ExecutionState &MergingSearcher::selectState() { } if (DebugLogMerge) - std::cerr << "-- merge complete, continuing --\n"; + llvm::errs() << "-- merge complete, continuing --\n"; return selectState(); } @@ -512,7 +512,8 @@ ExecutionState &BatchingSearcher::selectState() { if (lastState) { double delta = util::getWallTime()-lastStartTime; if (delta>timeBudget*1.1) { - std::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n"; + llvm::errs() << "KLEE: increased time budget from " << timeBudget + << " to " << delta << "\n"; timeBudget = delta; } } @@ -578,7 +579,7 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, if (baseSearcher->empty()) { time *= 2; - std::cerr << "KLEE: increasing time budget to: " << time << "\n"; + llvm::errs() << "KLEE: increasing time budget to: " << time << "\n"; baseSearcher->update(0, pausedStates, std::set<ExecutionState*>()); pausedStates.clear(); } diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 3944d4b4..d866f521 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -10,18 +10,17 @@ #ifndef KLEE_SEARCHER_H #define KLEE_SEARCHER_H +#include "llvm/Support/raw_ostream.h" #include <vector> #include <set> #include <map> #include <queue> -// FIXME: Move out of header, use llvm streams. -#include <ostream> - namespace llvm { class BasicBlock; class Function; class Instruction; + class raw_ostream; } namespace klee { @@ -43,7 +42,7 @@ namespace klee { // prints name of searcher as a klee_message() // TODO: could probably make prettier or more flexible - virtual void printName(std::ostream &os) { + virtual void printName(llvm::raw_ostream &os) { os << "<unnamed searcher>\n"; } @@ -90,7 +89,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty() { return states.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; } }; @@ -104,7 +103,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty() { return states.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "BFSSearcher\n"; } }; @@ -118,7 +117,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty() { return states.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "RandomSearcher\n"; } }; @@ -150,7 +149,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty(); - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "WeightedRandomSearcher::"; switch(type) { case Depth : os << "Depth\n"; return; @@ -176,7 +175,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty(); - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "RandomPathSearcher\n"; } }; @@ -199,7 +198,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "MergingSearcher\n"; } }; @@ -222,7 +221,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "BumpMergingSearcher\n"; } }; @@ -247,7 +246,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty() { return baseSearcher->empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "<BatchingSearcher> timeBudget: " << timeBudget << ", instructionBudget: " << instructionBudget << ", baseSearcher:\n"; @@ -270,7 +269,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty() { return baseSearcher->empty() && pausedStates.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "IterativeDeepeningTimeSearcher\n"; } }; @@ -290,7 +289,7 @@ namespace klee { const std::set<ExecutionState*> &addedStates, const std::set<ExecutionState*> &removedStates); bool empty() { return searchers[0]->empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "<InterleavedSearcher> containing " << searchers.size() << " searchers:\n"; for (searchers_ty::iterator it = searchers.begin(), ie = searchers.end(); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index ca9f7b63..a7a1b32e 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -27,6 +27,7 @@ #include "llvm/Module.h" #endif #include "llvm/ADT/Twine.h" +#include "llvm/Support/Debug.h" #include <errno.h> @@ -251,7 +252,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state, //XXX:DRE:TAINT if(state.underConstrained) { - std::cerr << "TAINT: skipping abort fail\n"; + llvm::errs() << "TAINT: skipping abort fail\n"; executor.terminateState(state); } else { executor.terminateStateOnError(state, "abort failure", "abort.err"); @@ -279,7 +280,8 @@ void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state, "invalid number of arguments to klee_alias_function"); std::string old_fn = readStringAtAddress(state, arguments[0]); std::string new_fn = readStringAtAddress(state, arguments[1]); - //std::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n"; + DEBUG_WITH_TYPE("alias_handling", llvm::errs() << "Replacing " << old_fn + << "() with " << new_fn << "()\n"); if (old_fn == new_fn) state.removeFnAlias(old_fn); else state.addFnAlias(old_fn, new_fn); @@ -292,8 +294,8 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state, //XXX:DRE:TAINT if(state.underConstrained) { - std::cerr << "TAINT: skipping assertion:" - << readStringAtAddress(state, arguments[0]) << "\n"; + llvm::errs() << "TAINT: skipping assertion:" + << readStringAtAddress(state, arguments[0]) << "\n"; executor.terminateState(state); } else executor.terminateStateOnError(state, @@ -308,8 +310,8 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, //XXX:DRE:TAINT if(state.underConstrained) { - std::cerr << "TAINT: skipping assertion:" - << readStringAtAddress(state, arguments[0]) << "\n"; + llvm::errs() << "TAINT: skipping assertion:" + << readStringAtAddress(state, arguments[0]) << "\n"; executor.terminateState(state); } else executor.terminateStateOnError(state, @@ -326,9 +328,9 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state, //XXX:DRE:TAINT if(state.underConstrained) { - std::cerr << "TAINT: skipping klee_report_error:" - << readStringAtAddress(state, arguments[2]) << ":" - << readStringAtAddress(state, arguments[3]) << "\n"; + llvm::errs() << "TAINT: skipping klee_report_error:" + << readStringAtAddress(state, arguments[2]) << ":" + << readStringAtAddress(state, arguments[3]) << "\n"; executor.terminateState(state); } else executor.terminateStateOnError(state, @@ -444,7 +446,7 @@ void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state, "invalid number of arguments to klee_print_expr"); std::string msg_str = readStringAtAddress(state, arguments[0]); - std::cerr << msg_str << ":" << arguments[1] << "\n"; + llvm::errs() << msg_str << ":" << arguments[1] << "\n"; } void SpecialFunctionHandler::handleSetForking(ExecutionState &state, @@ -466,7 +468,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, void SpecialFunctionHandler::handleStackTrace(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - state.dumpStack(std::cout); + state.dumpStack(outs()); } void SpecialFunctionHandler::handleWarning(ExecutionState &state, @@ -497,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, "invalid number of arguments to klee_print_range"); std::string msg_str = readStringAtAddress(state, arguments[0]); - std::cerr << msg_str << ":" << arguments[1]; + llvm::errs() << msg_str << ":" << arguments[1]; if (!isa<ConstantExpr>(arguments[1])) { // FIXME: Pull into a unique value method? ref<ConstantExpr> value; @@ -509,15 +511,15 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, res); assert(success && "FIXME: Unhandled solver failure"); if (res) { - std::cerr << " == " << value; + llvm::errs() << " == " << value; } else { - std::cerr << " ~= " << value; + llvm::errs() << " ~= " << value; std::pair< ref<Expr>, ref<Expr> > res = executor.solver->getRange(state, arguments[1]); - std::cerr << " (in [" << res.first << ", " << res.second <<"])"; + llvm::errs() << " (in [" << res.first << ", " << res.second <<"])"; } } - std::cerr << "\n"; + llvm::errs() << "\n"; } void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state, diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 4709a5bc..0946d2ba 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -46,12 +46,10 @@ #endif #include "llvm/Support/CommandLine.h" #include "llvm/Support/CFG.h" -#include "llvm/Support/raw_os_ostream.h" #include "llvm/Support/Process.h" #include "llvm/Support/Path.h" #include "llvm/Support/FileSystem.h" -#include <iostream> #include <fstream> #include <unistd.h> @@ -432,11 +430,12 @@ void StatsTracker::updateStateStatistics(uint64_t addend) { void StatsTracker::writeIStats() { Module *m = executor.kmodule->module; uint64_t istatsMask = 0; - std::ostream &of = *istatsFile; + llvm::raw_fd_ostream &of = *istatsFile; - of.seekp(0, std::ios::end); - unsigned istatsSize = of.tellp(); - of.seekp(0); + // We assume that we didn't move the file pointer + unsigned istatsSize = of.tell(); + + of.seek(0); of << "version: 1\n"; of << "creator: klee\n"; @@ -564,7 +563,7 @@ void StatsTracker::writeIStats() { updateStateStatistics((uint64_t)-1); // Clear then end of the file if necessary (no truncate op?). - unsigned pos = of.tellp(); + unsigned pos = of.tell(); for (unsigned i=pos; i<istatsSize; ++i) of << '\n'; diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h index 8f3a01a2..629a723d 100644 --- a/lib/Core/StatsTracker.h +++ b/lib/Core/StatsTracker.h @@ -12,13 +12,13 @@ #include "CallPathManager.h" -#include <iostream> #include <set> namespace llvm { class BranchInst; class Function; class Instruction; + class raw_fd_ostream; } namespace klee { @@ -36,7 +36,7 @@ namespace klee { Executor &executor; std::string objectFilename; - std::ostream *statsFile, *istatsFile; + llvm::raw_fd_ostream *statsFile, *istatsFile; double startWallTime; unsigned numBranches; diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 2c75f796..72f3351f 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -129,7 +129,7 @@ Searcher *klee::constructUserSearcher(Executor &executor) { searcher = new IterativeDeepeningTimeSearcher(searcher); } - std::ostream &os = executor.getHandler().getInfoStream(); + llvm::raw_ostream &os = executor.getHandler().getInfoStream(); os << "BEGIN searcher description\n"; searcher->printName(os); |