From d934d983692c8952cdb887cbcd59f2df0001b9c0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:15:59 +0200 Subject: Refactoring from std::ostream to llvm::raw_ostream According to LLVM: lightweight and simpler implementation of streams. --- lib/Basic/ConstructSolverChain.cpp | 18 +++--- lib/Core/ExecutionState.cpp | 66 +++++++++++--------- lib/Core/Executor.cpp | 117 ++++++++++++++++++------------------ lib/Core/ExecutorTimers.cpp | 6 +- lib/Core/ExecutorUtil.cpp | 2 +- lib/Core/ExternalDispatcher.cpp | 2 +- lib/Core/ImpliedValue.cpp | 2 +- lib/Core/Memory.cpp | 18 +++--- lib/Core/PTree.cpp | 2 +- lib/Core/PTree.h | 2 +- lib/Core/Searcher.cpp | 23 +++---- lib/Core/Searcher.h | 23 +++---- lib/Core/SpecialFunctionHandler.cpp | 33 +++++----- lib/Core/StatsTracker.cpp | 11 ++-- lib/Core/StatsTracker.h | 3 +- lib/Core/UserSearcher.cpp | 2 +- lib/Expr/Expr.cpp | 11 ++-- lib/Expr/ExprPPrinter.cpp | 15 ++--- lib/Expr/ExprSMTLIBLetPrinter.cpp | 2 +- lib/Expr/ExprSMTLIBPrinter.cpp | 39 ++++++------ lib/Expr/Parser.cpp | 26 ++++---- lib/Module/KModule.cpp | 24 +++----- lib/Module/Optimize.cpp | 2 +- lib/SMT/SMTParser.cpp | 9 ++- lib/SMT/smtlib.y | 2 +- lib/Solver/FastCexSolver.cpp | 36 ++++++----- lib/Solver/IndependentSolver.cpp | 33 +++++----- lib/Solver/MetaSMTBuilder.h | 6 +- lib/Solver/QueryLoggingSolver.cpp | 10 +-- lib/Solver/QueryLoggingSolver.h | 10 ++- lib/Support/TreeStream.cpp | 19 +++--- 31 files changed, 297 insertions(+), 277 deletions(-) (limited to 'lib') diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index c0d0ef61..59790551 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -10,9 +10,9 @@ /* * This file groups declarations that are common to both KLEE and Kleaver. */ -#include #include "klee/Common.h" #include "klee/CommandLine.h" +#include "llvm/Support/raw_ostream.h" namespace klee { @@ -29,8 +29,8 @@ namespace klee solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath, MinQueryTimeToLog); - std::cerr << "Logging queries that reach solver in .pc format to " - << baseSolverQueryPCLogPath.c_str() << std::endl; + llvm::errs() << "Logging queries that reach solver in .pc format to " + << baseSolverQueryPCLogPath.c_str() << "\n"; } if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) @@ -38,8 +38,8 @@ namespace klee solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, MinQueryTimeToLog); - std::cerr << "Logging queries that reach solver in .smt2 format to " - << baseSolverQuerySMT2LogPath.c_str() << std::endl; + llvm::errs() << "Logging queries that reach solver in .smt2 format to " + << baseSolverQuerySMT2LogPath.c_str() << "\n"; } if (UseFastCexSolver) @@ -62,16 +62,16 @@ namespace klee solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog); - std::cerr << "Logging all queries in .pc format to " - << queryPCLogPath.c_str() << std::endl; + llvm::errs() << "Logging all queries in .pc format to " + << queryPCLogPath.c_str() << "\n"; } if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) { solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath, MinQueryTimeToLog); - std::cerr << "Logging all queries in .smt2 format to " - << querySMT2LogPath.c_str() << std::endl; + llvm::errs() << "Logging all queries in .smt2 format to " + << querySMT2LogPath.c_str() << "\n"; } return solver; 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 #include +#include #include #include #include @@ -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 >::iterator it = commonConstraints.begin(), - ie = commonConstraints.end(); it != ie; ++it) - std::cerr << *it << ", "; - std::cerr << "]\n"; - std::cerr << "\tA suffix: ["; - for (std::set< ref >::iterator it = aSuffix.begin(), - ie = aSuffix.end(); it != ie; ++it) - std::cerr << *it << ", "; - std::cerr << "]\n"; - std::cerr << "\tB suffix: ["; - for (std::set< ref >::iterator it = bSuffix.begin(), - ie = bSuffix.end(); it != ie; ++it) - std::cerr << *it << ", "; - std::cerr << "]\n"; + llvm::errs() << "\tconstraint prefix: ["; + for (std::set >::iterator it = commonConstraints.begin(), + ie = commonConstraints.end(); + it != ie; ++it) + llvm::errs() << *it << ", "; + llvm::errs() << "]\n"; + llvm::errs() << "\tA suffix: ["; + for (std::set >::iterator it = aSuffix.begin(), + ie = aSuffix.end(); + it != ie; ++it) + llvm::errs() << *it << ", "; + llvm::errs() << "]\n"; + llvm::errs() << "\tB suffix: ["; + for (std::set >::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 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 #include -#include #include +#include #include #include #include @@ -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::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 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(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 Executor::replaceReadWithSymbolic(ExecutionState &state, Expr::getMinBytesForWidth(e->getWidth())); ref res = Expr::createTempRead(array, e->getWidth()); ref 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::const_iterator it = states.begin(), diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 0d828ec4..79d1707e 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -62,7 +62,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..bbe1c42e 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -92,7 +92,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..f20259fb 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -246,7 +246,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref e, } else { if (it!=found.end()) { ref 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..7f5d024e 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -585,23 +585,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; inext) { - 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..a435cd5e 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -51,7 +51,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..2ac688bd 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -34,7 +34,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 >::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::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::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::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()); pausedStates.clear(); } diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 3944d4b4..3c077636 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -22,6 +22,7 @@ namespace llvm { class BasicBlock; class Function; class Instruction; + class raw_ostream; } namespace klee { @@ -43,7 +44,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 << "\n"; } @@ -90,7 +91,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty() { return states.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; } }; @@ -104,7 +105,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty() { return states.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "BFSSearcher\n"; } }; @@ -118,7 +119,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty() { return states.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "RandomSearcher\n"; } }; @@ -150,7 +151,7 @@ namespace klee { const std::set &addedStates, const std::set &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 +177,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty(); - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "RandomPathSearcher\n"; } }; @@ -199,7 +200,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "MergingSearcher\n"; } }; @@ -222,7 +223,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "BumpMergingSearcher\n"; } }; @@ -247,7 +248,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty() { return baseSearcher->empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << " timeBudget: " << timeBudget << ", instructionBudget: " << instructionBudget << ", baseSearcher:\n"; @@ -270,7 +271,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty() { return baseSearcher->empty() && pausedStates.empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << "IterativeDeepeningTimeSearcher\n"; } }; @@ -290,7 +291,7 @@ namespace klee { const std::set &addedStates, const std::set &removedStates); bool empty() { return searchers[0]->empty(); } - void printName(std::ostream &os) { + void printName(llvm::raw_ostream &os) { os << " 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..dcba5436 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -251,7 +251,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 +279,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", 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 +293,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 +309,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 +327,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 +445,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 +467,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, void SpecialFunctionHandler::handleStackTrace(ExecutionState &state, KInstruction *target, std::vector > &arguments) { - state.dumpStack(std::cout); + state.dumpStack(outs()); } void SpecialFunctionHandler::handleWarning(ExecutionState &state, @@ -497,7 +498,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(arguments[1])) { // FIXME: Pull into a unique value method? ref value; @@ -509,15 +510,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, ref > 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..4f4552e7 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -432,11 +432,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 +565,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; iprintName(os); diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 82c60205..14737e8c 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -14,6 +14,7 @@ #include "llvm/ADT/Hashing.h" #endif #include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" // FIXME: We shouldn't need this once fast constant support moves into // Core. If we need to do arithmetic, we probably want to use APInt. #include "klee/Internal/Support/IntEvaluation.h" @@ -116,7 +117,7 @@ int Expr::compare(const Expr &b, ExprEquivSet &equivs) const { return 0; } -void Expr::printKind(std::ostream &os, Kind k) { +void Expr::printKind(llvm::raw_ostream &os, Kind k) { switch(k) { #define X(C) case C: os << #C; break X(Constant); @@ -286,7 +287,7 @@ ref Expr::createFromKind(Kind k, std::vector args) { } -void Expr::printWidth(std::ostream &os, Width width) { +void Expr::printWidth(llvm::raw_ostream &os, Width width) { switch(width) { case Expr::Bool: os << "Expr::Bool"; break; case Expr::Int8: os << "Expr::Int8"; break; @@ -306,13 +307,13 @@ ref Expr::createIsZero(ref e) { return EqExpr::create(e, ConstantExpr::create(0, e->getWidth())); } -void Expr::print(std::ostream &os) const { +void Expr::print(llvm::raw_ostream &os) const { ExprPPrinter::printSingleExpr(os, const_cast(this)); } void Expr::dump() const { - this->print(std::cerr); - std::cerr << std::endl; + this->print(errs()); + errs() << "\n"; } /***/ diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index d58358b5..a7ad5ddc 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -13,6 +13,7 @@ #include "klee/Constraints.h" #include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" #include #include @@ -47,7 +48,7 @@ private: std::map updateBindings; std::set< ref > couldPrint, shouldPrint; std::set couldPrintUpdates, shouldPrintUpdates; - std::ostream &os; + llvm::raw_ostream &os; unsigned counter; unsigned updateCounter; bool hasScan; @@ -300,7 +301,7 @@ private: } public: - PPrinter(std::ostream &_os) : os(_os), newline("\n") { + PPrinter(llvm::raw_ostream &_os) : os(_os), newline("\n") { reset(); } @@ -426,11 +427,11 @@ public: } }; -ExprPPrinter *klee::ExprPPrinter::create(std::ostream &os) { +ExprPPrinter *klee::ExprPPrinter::create(llvm::raw_ostream &os) { return new PPrinter(os); } -void ExprPPrinter::printOne(std::ostream &os, +void ExprPPrinter::printOne(llvm::raw_ostream &os, const char *message, const ref &e) { PPrinter p(os); @@ -444,7 +445,7 @@ void ExprPPrinter::printOne(std::ostream &os, PC.breakLine(); } -void ExprPPrinter::printSingleExpr(std::ostream &os, const ref &e) { +void ExprPPrinter::printSingleExpr(llvm::raw_ostream &os, const ref &e) { PPrinter p(os); p.scan(e); @@ -454,13 +455,13 @@ void ExprPPrinter::printSingleExpr(std::ostream &os, const ref &e) { p.print(e, PC); } -void ExprPPrinter::printConstraints(std::ostream &os, +void ExprPPrinter::printConstraints(llvm::raw_ostream &os, const ConstraintManager &constraints) { printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool)); } -void ExprPPrinter::printQuery(std::ostream &os, +void ExprPPrinter::printQuery(llvm::raw_ostream &os, const ConstraintManager &constraints, const ref &q, const ref *evalExprsBegin, diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp index 6a88ab5d..2ea5c4e0 100644 --- a/lib/Expr/ExprSMTLIBLetPrinter.cpp +++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp @@ -31,7 +31,7 @@ ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter() void ExprSMTLIBLetPrinter::generateOutput() { if (p == NULL || query == NULL || o == NULL) { - std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl; + llvm::errs() << "Can't print SMTLIBv2. Output or query bad!\n"; return; } diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index cff5abfe..2dbf3634 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -53,7 +53,7 @@ ExprSMTLIBPrinter::~ExprSMTLIBPrinter() { delete p; } -void ExprSMTLIBPrinter::setOutput(std::ostream &output) { +void ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output) { o = &output; if (p != NULL) delete p; @@ -146,8 +146,8 @@ void ExprSMTLIBPrinter::printConstant(const ref &e) { break; default: - std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant " - "display mode" << std::endl; + llvm::errs() << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant " + "display mode\n"; } } @@ -425,8 +425,8 @@ void ExprSMTLIBPrinter::scanAll() { void ExprSMTLIBPrinter::generateOutput() { if (p == NULL || query == NULL || o == NULL) { - std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. " - "Output or query bad!" << std::endl; + llvm::errs() << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. " + "Output or query bad!\n"; return; } @@ -451,7 +451,7 @@ void ExprSMTLIBPrinter::printSetLogic() { *o << "QF_AUFBV"; break; } - *o << " )" << std::endl; + *o << " )\n"; } namespace { @@ -467,7 +467,7 @@ struct ArrayPtrsByName { void ExprSMTLIBPrinter::printArrayDeclarations() { // Assume scan() has been called if (humanReadable) - *o << "; Array declarations" << endl; + *o << "; Array declarations\n"; // Declare arrays in a deterministic order. std::vector sortedArrays(usedArrays.begin(), usedArrays.end()); @@ -478,13 +478,13 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { "(Array (_ BitVec " << (*it)->getDomain() << ") " "(_ BitVec " << (*it)->getRange() << ") ) )" - << endl; + << "\n"; } // Set array values for constant values if (haveConstantArray) { if (humanReadable) - *o << "; Constant Array Definitions" << endl; + *o << "; Constant Array Definitions\n"; const Array *array; @@ -527,7 +527,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { void ExprSMTLIBPrinter::printConstraints() { if (humanReadable) - *o << "; Constraints" << endl; + *o << "; Constraints\n"; // Generate assert statements for each constraint for (ConstraintManager::const_iterator i = query->constraints.begin(); @@ -548,7 +548,7 @@ void ExprSMTLIBPrinter::printConstraints() { void ExprSMTLIBPrinter::printAction() { // Ask solver to check for satisfiability - *o << "(check-sat)" << endl; + *o << "(check-sat)\n"; /* If we has arrays to find the values of then we'll * ask the solver for the value of each bitvector in each array @@ -565,7 +565,7 @@ void ExprSMTLIBPrinter::printAction() { // Loop over the array indices for (unsigned int index = 0; index < theArray->size; ++index) { *o << "(get-value ( (select " << (**it).name << " (_ bv" << index << " " - << theArray->getDomain() << ") ) ) )" << endl; + << theArray->getDomain() << ") ) ) )\n"; } } } @@ -573,8 +573,8 @@ void ExprSMTLIBPrinter::printAction() { void ExprSMTLIBPrinter::scan(const ref &e) { if (e.isNull()) { - std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!" - << std::endl; + llvm::errs() << "ExprSMTLIBPrinter::scan() : Found NULL expression!" + << "\n"; return; } @@ -609,7 +609,7 @@ void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) { } } -void ExprSMTLIBPrinter::printExit() { *o << "(exit)" << endl; } +void ExprSMTLIBPrinter::printExit() { *o << "(exit)\n"; } bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l) { if (l > QF_AUFBV) @@ -627,7 +627,7 @@ void ExprSMTLIBPrinter::printSeperator() { } void ExprSMTLIBPrinter::printNotice() { - *o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl; + *o << "; This file conforms to SMTLIBv2 and was generated by KLEE\n"; } void ExprSMTLIBPrinter::setHumanReadable(bool hr) { humanReadable = hr; } @@ -638,7 +638,7 @@ void ExprSMTLIBPrinter::printOptions() { smtlibBoolOptions.begin(); i != smtlibBoolOptions.end(); i++) { *o << "(set-option :" << getSMTLIBOptionString(i->first) << " " - << ((i->second) ? "true" : "false") << ")" << endl; + << ((i->second) ? "true" : "false") << ")\n"; } } @@ -742,8 +742,9 @@ void ExprSMTLIBPrinter::printCastToSort(const ref &e, *p << ")"; if (bitWidth != Expr::Bool) - std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " - << bitWidth << ") to bool!" << std::endl; + llvm::errs() + << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " + << bitWidth << ") to bool!\n"; } break; default: diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 5b3e96b7..6b346648 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -1522,7 +1522,7 @@ void ParserImpl::Error(const char *Message, const Token &At) { if (MaxErrors && NumErrors >= MaxErrors) return; - std::cerr << Filename + llvm::errs() << Filename << ":" << At.line << ":" << At.column << ": error: " << Message << "\n"; @@ -1544,18 +1544,18 @@ void ParserImpl::Error(const char *Message, const Token &At) { ++LineEnd; // Show the line. - std::cerr << std::string(LineBegin, LineEnd) << "\n"; + llvm::errs() << std::string(LineBegin, LineEnd) << "\n"; // Show the caret or squiggly, making sure to print back spaces the // same. for (const char *S=LineBegin; S != At.start; ++S) - std::cerr << (isspace(*S) ? *S : ' '); + llvm::errs() << (isspace(*S) ? *S : ' '); if (At.length > 1) { for (unsigned i=0; iname + llvm::outs() << "array " << Root->name << "[" << Root->size << "]" << " : " << 'w' << Domain << " -> " << 'w' << Range << " = "; if (Root->isSymbolicArray()) { - std::cout << "symbolic\n"; + llvm::outs() << "symbolic\n"; } else { - std::cout << '['; + llvm::outs() << '['; for (unsigned i = 0, e = Root->size; i != e; ++i) { if (i) - std::cout << " "; - std::cout << Root->constantValues[i]; + llvm::outs() << " "; + llvm::outs() << Root->constantValues[i]; } - std::cout << "]\n"; + llvm::outs() << "]\n"; } } @@ -1592,7 +1592,7 @@ void QueryCommand::dump() { ObjectsBegin = &Objects[0]; ObjectsEnd = ObjectsBegin + Objects.size(); } - ExprPPrinter::printQuery(std::cout, ConstraintManager(Constraints), + ExprPPrinter::printQuery(llvm::outs(), ConstraintManager(Constraints), Query, ValuesBegin, ValuesEnd, ObjectsBegin, ObjectsEnd, false); diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index e06e722a..697b6ea9 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -430,15 +430,13 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, // around a kcachegrind parsing bug (it puts them on new lines), so // that source browsing works. if (OutputSource) { - std::ostream *os = ih->openOutputFile("assembly.ll"); - assert(os && os->good() && "unable to open source output"); - - llvm::raw_os_ostream *ros = new llvm::raw_os_ostream(*os); + llvm::raw_fd_ostream *os = ih->openOutputFile("assembly.ll"); + assert(os && !os->has_error() && "unable to open source output"); // We have an option for this in case the user wants a .ll they // can compile. if (NoTruncateSourceLines) { - *ros << *module; + *os << *module; } else { std::string string; llvm::raw_string_ostream rss(string); @@ -449,30 +447,26 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, for (;;) { const char *end = index(position, '\n'); if (!end) { - *ros << position; + *os << position; break; } else { unsigned count = (end - position) + 1; if (count<255) { - ros->write(position, count); + os->write(position, count); } else { - ros->write(position, 254); - *ros << "\n"; + os->write(position, 254); + *os << "\n"; } position = end+1; } } } - delete ros; - delete os; } if (OutputModule) { - std::ostream *f = ih->openOutputFile("final.bc"); - llvm::raw_os_ostream* rfs = new llvm::raw_os_ostream(*f); - WriteBitcodeToFile(module, *rfs); - delete rfs; + llvm::raw_fd_ostream *f = ih->openOutputFile("final.bc"); + WriteBitcodeToFile(module, *f); delete f; } diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 9c200bc8..6f060edd 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -272,7 +272,7 @@ void Optimize(Module* M) { if (Opt->getNormalCtor()) addPass(Passes, Opt->getNormalCtor()()); else - std::cerr << "llvm-ld: cannot create pass: " << Opt->getPassName() + llvm::errs() << "llvm-ld: cannot create pass: " << Opt->getPassName() << "\n"; } #endif diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index 22578f46..d16e1edb 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -103,9 +103,8 @@ bool SMTParser::Solve() { // XXX: give more info int SMTParser::Error(const string& msg) { - std::cerr << SMTParser::parserTemp->fileName << ":" - << SMTParser::parserTemp->lineNum - << ": " << msg << "\n"; + llvm::errs() << SMTParser::parserTemp->fileName << ":" + << SMTParser::parserTemp->lineNum << ": " << msg << "\n"; exit(1); return 0; } @@ -213,7 +212,7 @@ void SMTParser::AddVar(std::string name, ExprHandle val) { ExprHandle SMTParser::GetVar(std::string name) { VarEnv top = varEnvs.top(); if (top.find(name) == top.end()) { - std::cerr << "Cannot find variable ?" << name << "\n"; + llvm::errs() << "Cannot find variable ?" << name << "\n"; exit(1); } return top[name]; @@ -241,7 +240,7 @@ void SMTParser::AddFVar(std::string name, ExprHandle val) { ExprHandle SMTParser::GetFVar(std::string name) { FVarEnv top = fvarEnvs.top(); if (top.find(name) == top.end()) { - std::cerr << "Cannot find fvar $" << name << "\n"; + llvm::errs() << "Cannot find fvar $" << name << "\n"; exit(1); } return top[name]; diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y index 01d3539d..eb3b3890 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -254,7 +254,7 @@ bench_attribute: | COLON_TOK LOGIC_TOK logic_name { if (*$3 != "QF_BV" && *$3 != "QF_AUFBV" && *$3 != "QF_UFBV") { - std::cerr << "ERROR: Logic " << *$3 << " not supported."; + llvm::errs() << "ERROR: Logic " << *$3 << " not supported."; exit(1); } diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 6e52dc32..a488db2a 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -18,6 +18,7 @@ // FIXME: Use APInt. #include "klee/Internal/Support/IntEvaluation.h" +#include "llvm/Support/raw_ostream.h" #include #include #include @@ -109,7 +110,7 @@ public: ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {} ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {} - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { if (isFixed()) { os << m_min; } else { @@ -283,7 +284,8 @@ public: } }; -inline std::ostream &operator<<(std::ostream &os, const ValueRange &vr) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const ValueRange &vr) { vr.print(os); return os; } @@ -443,7 +445,7 @@ public: void propogatePossibleValues(ref e, CexValueData range) { #ifdef DEBUG - std::cerr << "propogate: " << range << " for\n" << e << "\n"; + llvm::errs() << "propogate: " << range << " for\n" << e << "\n"; #endif switch (e->getKind()) { @@ -938,27 +940,29 @@ public: } void dump() { - std::cerr << "-- propogated values --\n"; - for (std::map::iterator - it = objects.begin(), ie = objects.end(); it != ie; ++it) { + llvm::errs() << "-- propogated values --\n"; + for (std::map::iterator + it = objects.begin(), + ie = objects.end(); + it != ie; ++it) { const Array *A = it->first; CexObjectData *COD = it->second; - - std::cerr << A->name << "\n"; - std::cerr << "possible: ["; + + llvm::errs() << A->name << "\n"; + llvm::errs() << "possible: ["; for (unsigned i = 0; i < A->size; ++i) { if (i) - std::cerr << ", "; - std::cerr << COD->getPossibleValues(i); + llvm::errs() << ", "; + llvm::errs() << COD->getPossibleValues(i); } - std::cerr << "]\n"; - std::cerr << "exact : ["; + llvm::errs() << "]\n"; + llvm::errs() << "exact : ["; for (unsigned i = 0; i < A->size; ++i) { if (i) - std::cerr << ", "; - std::cerr << COD->getExactValues(i); + llvm::errs() << ", "; + llvm::errs() << COD->getExactValues(i); } - std::cerr << "]\n"; + llvm::errs() << "]\n"; } } }; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index d9fc77dc..3c0b9b26 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -15,6 +15,7 @@ #include "klee/util/ExprUtil.h" +#include "llvm/Support/raw_ostream.h" #include #include #include @@ -60,7 +61,7 @@ public: return false; } - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { bool first = true; os << "{"; for (typename set_ty::iterator it = s.begin(), ie = s.end(); @@ -76,8 +77,9 @@ public: } }; -template -inline std::ostream &operator<<(std::ostream &os, const ::DenseSet &dis) { +template +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const ::DenseSet &dis) { dis.print(os); return os; } @@ -124,7 +126,7 @@ public: return *this; } - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { os << "{"; bool first = true; for (std::set::iterator it = wholeObjects.begin(), @@ -214,7 +216,8 @@ public: } }; -inline std::ostream &operator<<(std::ostream &os, const IndependentElementSet &ies) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const IndependentElementSet &ies) { ies.print(os); return os; } @@ -247,20 +250,22 @@ IndependentElementSet getIndependentConstraints(const Query& query, worklist.swap(newWorklist); } while (!done); +#if 0 if (0) { std::set< ref > reqset(result.begin(), result.end()); - std::cerr << "--\n"; - std::cerr << "Q: " << query.expr << "\n"; - std::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n"; + errs() << "--\n"; + errs() << "Q: " << query.expr << "\n"; + errs() << "\telts: " << IndependentElementSet(query.expr) << "\n"; int i = 0; - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) { - std::cerr << "C" << i++ << ": " << *it; - std::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; - std::cerr << "\telts: " << IndependentElementSet(*it) << "\n"; + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); it != ie; ++it) { + errs() << "C" << i++ << ": " << *it; + errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; + errs() << "\telts: " << IndependentElementSet(*it) << "\n"; } - std::cerr << "elts closure: " << eltsClosure << "\n"; + errs() << "elts closure: " << eltsClosure << "\n"; } +#endif return eltsClosure; } diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index f1e55614..b5c99907 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -599,9 +599,9 @@ typename SolverContext::result_type MetaSMTBuilder::constructActu ++stats::queryConstructs; -// std::cerr << "Constructing expression "; -// ExprPPrinter::printSingleExpr(std::cerr, e); -// std::cerr << "\n"; +// llvm::errs() << "Constructing expression "; +// ExprPPrinter::printSingleExpr(llvm::errs(), e); +// llvm::errs() << "\n"; switch (e->getKind()) { diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index f2e38182..d5598d1d 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -18,9 +18,10 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, const std::string& commentSign, int queryTimeToLog) - : solver(_solver), - os(path.c_str(), std::ios::trunc), - logBuffer(""), + : solver(_solver), + os(path.c_str(), ErrorInfo), + BufferString(""), + logBuffer(BufferString), queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f), @@ -79,8 +80,7 @@ void QueryLoggingSolver::flushBuffer() { } // prepare the buffer for reuse - logBuffer.clear(); - logBuffer.str(""); + BufferString = ""; } bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 2c7d80e8..ad1722ca 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -12,6 +12,7 @@ #include "klee/Solver.h" #include "klee/SolverImpl.h" +#include "llvm/Support/raw_ostream.h" #include #include @@ -25,9 +26,12 @@ class QueryLoggingSolver : public SolverImpl { protected: Solver *solver; - std::ofstream os; - std::ostringstream logBuffer; // buffer to store logs before flushing to - // file + 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); diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp index 0e8b86dd..e95fc582 100644 --- a/lib/Support/TreeStream.cpp +++ b/lib/Support/TreeStream.cpp @@ -16,6 +16,8 @@ #include #include +#include "llvm/Support/Debug.h" +#include "llvm/Support/raw_ostream.h" #include using namespace klee; @@ -105,10 +107,9 @@ void TreeStreamWriter::readStream(TreeStreamID streamID, std::ifstream is(path.c_str(), std::ios::in | std::ios::binary); assert(is.good()); -#if 0 - std::cout << "finding chain for: " << streamID << "\n"; -#endif - + DEBUG_WITH_TYPE("TreeStreamWriter", + llvm::errs() << "finding chain for: " << streamID << "\n"); + std::map parents; std::vector roots; for (;;) { @@ -137,11 +138,11 @@ void TreeStreamWriter::readStream(TreeStreamID streamID, while (size--) is.get(); } } -#if 0 - std::cout << "roots: "; - std::copy(roots.begin(), roots.end(), std::ostream_iterator(std::cout, " ")); - std::cout << "\n"; -#endif + DEBUG(llvm::errs() << "roots: "; + for (size_t i = 0, e = roots.size(); i < e; ++i) { + llvm::errs() << roots[i] << " "; + } + llvm::errs() << "\n";); is.seekg(0, std::ios::beg); for (;;) { unsigned id; -- cgit 1.4.1