diff options
41 files changed, 456 insertions, 389 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index 720488cc..824fbed5 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -32,7 +32,7 @@ namespace klee { class PTreeNode; struct InstructionInfo; -std::ostream &operator<<(std::ostream &os, const MemoryMap &mm); +llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); struct StackFrame { KInstIterator caller; @@ -137,7 +137,7 @@ public: } bool merge(const ExecutionState &b); - void dumpStack(std::ostream &out) const; + void dumpStack(llvm::raw_ostream &out) const; }; } diff --git a/include/klee/Expr.h b/include/klee/Expr.h index a302591a..ae5bfd2b 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -17,13 +17,15 @@ #include "llvm/ADT/APFloat.h" #include "llvm/ADT/DenseSet.h" #include "llvm/ADT/SmallVector.h" +#include "llvm/Support/raw_ostream.h" +#include <sstream> #include <set> #include <vector> -#include <iosfwd> // FIXME: Remove this!!! namespace llvm { class Type; + class raw_ostream; } namespace klee { @@ -181,7 +183,7 @@ public: virtual unsigned getNumKids() const = 0; virtual ref<Expr> getKid(unsigned i) const = 0; - virtual void print(std::ostream &os) const; + virtual void print(llvm::raw_ostream &os) const; /// dump - Print the expression to stderr. void dump() const; @@ -221,8 +223,8 @@ public: /* Static utility methods */ - static void printKind(std::ostream &os, Kind k); - static void printWidth(std::ostream &os, Expr::Width w); + static void printKind(llvm::raw_ostream &os, Kind k); + static void printWidth(llvm::raw_ostream &os, Expr::Width w); /// returns the smallest number of bytes in which the given width fits static inline unsigned getMinBytesForWidth(Width w) { @@ -291,16 +293,32 @@ inline bool operator>=(const Expr &lhs, const Expr &rhs) { // Printing operators -inline std::ostream &operator<<(std::ostream &os, const Expr &e) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr &e) { e.print(os); return os; } -inline std::ostream &operator<<(std::ostream &os, const Expr::Kind kind) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr::Kind kind) { Expr::printKind(os, kind); return os; } +inline std::stringstream &operator<<(std::stringstream &os, const Expr &e) { + std::string str; + llvm::raw_string_ostream TmpStr(str); + e.print(TmpStr); + os << TmpStr.str(); + return os; +} + +inline std::stringstream &operator<<(std::stringstream &os, const Expr::Kind kind) { + std::string str; + llvm::raw_string_ostream TmpStr(str); + Expr::printKind(TmpStr, kind); + os << TmpStr.str(); + return os; +} + // Terminal Exprs class ConstantExpr : public Expr { diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index e93284d6..abd454b1 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -19,6 +19,8 @@ struct KTest; namespace llvm { class Function; class Module; +class raw_ostream; +class raw_fd_ostream; } namespace klee { @@ -31,10 +33,10 @@ public: InterpreterHandler() {} virtual ~InterpreterHandler() {} - virtual std::ostream &getInfoStream() const = 0; + virtual llvm::raw_ostream &getInfoStream() const = 0; virtual std::string getOutputFilename(const std::string &filename) = 0; - virtual std::ostream *openOutputFile(const std::string &filename) = 0; + virtual llvm::raw_fd_ostream *openOutputFile(const std::string &filename) = 0; virtual void incPathsExplored() = 0; diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h index cf4ebb18..622b0e80 100644 --- a/include/klee/util/ExprPPrinter.h +++ b/include/klee/util/ExprPPrinter.h @@ -12,6 +12,9 @@ #include "klee/Expr.h" +namespace llvm { + class raw_ostream; +} namespace klee { class ConstraintManager; @@ -20,7 +23,7 @@ namespace klee { ExprPPrinter() {} public: - static ExprPPrinter *create(std::ostream &os); + static ExprPPrinter *create(llvm::raw_ostream &os); virtual ~ExprPPrinter() {} @@ -45,7 +48,7 @@ namespace klee { /// printOne - Pretty print a single expression prefixed by a /// message and followed by a line break. - static void printOne(std::ostream &os, const char *message, + static void printOne(llvm::raw_ostream &os, const char *message, const ref<Expr> &e); /// printSingleExpr - Pretty print a single expression. @@ -55,12 +58,12 @@ namespace klee { /// Note that if the output stream is not positioned at the /// beginning of a line then printing will not resume at the /// correct position following any output line breaks. - static void printSingleExpr(std::ostream &os, const ref<Expr> &e); + static void printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e); - static void printConstraints(std::ostream &os, + static void printConstraints(llvm::raw_ostream &os, const ConstraintManager &constraints); - static void printQuery(std::ostream &os, + static void printQuery(llvm::raw_ostream &os, const ConstraintManager &constraints, const ref<Expr> &q, const ref<Expr> *evalExprsBegin = 0, diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index 42f38007..8b072242 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -11,7 +11,6 @@ #ifndef KLEE_EXPRSMTLIBPRINTER_H #define KLEE_EXPRSMTLIBPRINTER_H -#include <ostream> #include <string> #include <set> #include <map> @@ -20,6 +19,10 @@ #include <klee/util/PrintContext.h> #include <klee/Solver.h> +namespace llvm { +class raw_ostream; +} + namespace klee { /// Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic. @@ -121,7 +124,7 @@ public: /// Set the output stream that will be printed to. /// This call is persistent across queries. - void setOutput(std::ostream &output); + void setOutput(llvm::raw_ostream &output); /// Set the query to print. This will setArrayValuesToGet() /// to none (i.e. no array values will be requested using @@ -130,7 +133,7 @@ public: virtual ~ExprSMTLIBPrinter(); - /// Print the query to the std::ostream + /// Print the query to the llvm::raw_ostream /// setOutput() and setQuery() must be called before calling this. /// /// All options should be set before calling this. @@ -202,7 +205,7 @@ protected: std::set<const Array *> usedArrays; /// Output stream to write to - std::ostream *o; + llvm::raw_ostream *o; /// The query to print const Query *query; diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h index a9e91925..6b1ef77a 100644 --- a/include/klee/util/PrintContext.h +++ b/include/klee/util/PrintContext.h @@ -1,14 +1,14 @@ #ifndef PRINTCONTEXT_H_ #define PRINTCONTEXT_H_ -#include <ostream> +#include "klee/Expr.h" +#include "llvm/Support/raw_ostream.h" #include <sstream> #include <string> #include <stack> -#include <iomanip> /// PrintContext - Helper class for pretty printing. -/// It provides a basic wrapper around std::ostream that keeps track of +/// It provides a basic wrapper around llvm::raw_ostream that keeps track of /// how many characters have been used on the current line. /// /// It also provides an optional way keeping track of the various levels of indentation @@ -16,8 +16,7 @@ /// \sa breakLineI() , \sa pushIndent(), \sa popIndent() class PrintContext { private: - std::ostream &os; - std::stringstream ss; + llvm::raw_ostream &os; std::string newline; ///This is used to keep track of the stack of indentations used by @@ -30,7 +29,7 @@ public: /// Number of characters on the current line. unsigned pos; - PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos() + PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos() { indentStack.push(pos); } @@ -42,7 +41,7 @@ public: void breakLine(unsigned indent=0) { os << newline; if (indent) - os << std::setw(indent) << ' '; + os.indent(indent) << ' '; pos = indent; } @@ -79,7 +78,8 @@ public: template <typename T> PrintContext &operator<<(T elt) { - ss.str(""); + std::string str; + llvm::raw_string_ostream ss(str); ss << elt; write(ss.str()); return *this; diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h index d14de471..c77149aa 100644 --- a/include/klee/util/Ref.h +++ b/include/klee/util/Ref.h @@ -20,6 +20,10 @@ using llvm::dyn_cast_or_null; #include <assert.h> #include <iosfwd> // FIXME: Remove this!!! +namespace llvm { + class raw_ostream; +} + namespace klee { template<class T> @@ -107,7 +111,13 @@ public: }; template<class T> -inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const ref<T> &e) { + os << *e; + return os; +} + +template<class T> +inline std::stringstream &operator<<(std::stringstream &os, const ref<T> &e) { os << *e; return os; } 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 <iostream> #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 <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..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<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..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; 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..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<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..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 << "<unnamed searcher>\n"; } @@ -90,7 +91,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 +105,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 +119,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 +151,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 +177,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 +200,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 +223,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 +248,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 +271,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 +291,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..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<ref<Expr> > &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<ConstantExpr>(arguments[1])) { // FIXME: Pull into a unique value method? ref<ConstantExpr> 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<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..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; i<istatsSize; ++i) of << '\n'; diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h index 8f3a01a2..f06decdc 100644 --- a/lib/Core/StatsTracker.h +++ b/lib/Core/StatsTracker.h @@ -19,6 +19,7 @@ namespace llvm { class BranchInst; class Function; class Instruction; + class raw_fd_ostream; } namespace klee { @@ -36,7 +37,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); 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> Expr::createFromKind(Kind k, std::vector<CreateArg> 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> Expr::createIsZero(ref<Expr> 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<Expr*>(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 <map> #include <vector> @@ -47,7 +48,7 @@ private: std::map<const UpdateNode*, unsigned> updateBindings; std::set< ref<Expr> > couldPrint, shouldPrint; std::set<const UpdateNode*> 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<Expr> &e) { PPrinter p(os); @@ -444,7 +445,7 @@ void ExprPPrinter::printOne(std::ostream &os, PC.breakLine(); } -void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &e) { +void ExprPPrinter::printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e) { PPrinter p(os); p.scan(e); @@ -454,13 +455,13 @@ void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &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<Expr> &q, const ref<Expr> *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<ConstantExpr> &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<const Array *> 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<Expr> &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<Expr> &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; i<At.length; ++i) - std::cerr << '~'; + llvm::errs() << '~'; } else - std::cerr << '^'; - std::cerr << '\n'; + llvm::errs() << '^'; + llvm::errs() << '\n'; } // AST API @@ -1564,20 +1564,20 @@ void ParserImpl::Error(const char *Message, const Token &At) { Decl::Decl(DeclKind _Kind) : Kind(_Kind) {} void ArrayDecl::dump() { - std::cout << "array " << Root->name + 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 <iostream> #include <sstream> #include <cassert> @@ -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<Expr> 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<const Array*, CexObjectData*>::iterator - it = objects.begin(), ie = objects.end(); it != ie; ++it) { + llvm::errs() << "-- propogated values --\n"; + for (std::map<const Array *, CexObjectData *>::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 <map> #include <vector> #include <ostream> @@ -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<class T> -inline std::ostream &operator<<(std::ostream &os, const ::DenseSet<T> &dis) { +template <class T> +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const ::DenseSet<T> &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<const Array*>::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<Expr> > 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<SolverContext>::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 <fstream> #include <sstream> @@ -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 <iterator> #include <map> +#include "llvm/Support/Debug.h" +#include "llvm/Support/raw_ostream.h" #include <string.h> 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<unsigned,unsigned> parents; std::vector<unsigned> 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<unsigned>(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; diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index abc37d4b..e31140e8 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -124,9 +124,11 @@ static std::string getQueryLogPath(const char filename[]) struct stat s; if( !(stat(directoryToWriteQueryLogs.c_str(),&s) == 0 && S_ISDIR(s.st_mode)) ) { - std::cerr << "Directory to log queries \"" << directoryToWriteQueryLogs << "\" does not exist!" << std::endl; - exit(1); - } + llvm::errs() << "Directory to log queries \"" + << directoryToWriteQueryLogs << "\" does not exist!" + << "\n"; + exit(1); + } //check permissions okay if( !( (s.st_mode & S_IWUSR) && getuid() == s.st_uid) && @@ -134,9 +136,11 @@ static std::string getQueryLogPath(const char filename[]) !( s.st_mode & S_IWOTH) ) { - std::cerr << "Directory to log queries \"" << directoryToWriteQueryLogs << "\" is not writable!" << std::endl; - exit(1); - } + llvm::errs() << "Directory to log queries \"" + << directoryToWriteQueryLogs << "\" is not writable!" + << "\n"; + exit(1); + } std::string path=directoryToWriteQueryLogs; path+="/"; @@ -167,10 +171,9 @@ static void PrintInputTokens(const MemoryBuffer *MB) { Token T; do { L.Lex(T); - std::cout << "(Token \"" << T.getKindName() << "\" " - << "\"" << escapedString(T.start, T.length) << "\" " - << T.length << " " - << T.line << " " << T.column << ")\n"; + llvm::outs() << "(Token \"" << T.getKindName() << "\" " + << "\"" << escapedString(T.start, T.length) << "\" " + << T.length << " " << T.line << " " << T.column << ")\n"; } while (T.kind != Token::EndOfFile); } @@ -185,7 +188,7 @@ static bool PrintInputAST(const char *Filename, while (Decl *D = P->ParseTopLevelDecl()) { if (!P->GetNumErrors()) { if (isa<QueryCommand>(D)) - std::cout << "# Query " << ++NumQueries << "\n"; + llvm::outs() << "# Query " << ++NumQueries << "\n"; D->dump(); } @@ -194,8 +197,7 @@ static bool PrintInputAST(const char *Filename, bool success = true; if (unsigned N = P->GetNumErrors()) { - std::cerr << Filename << ": parse failure: " - << N << " errors.\n"; + llvm::errs() << Filename << ": parse failure: " << N << " errors.\n"; success = false; } @@ -220,8 +222,7 @@ static bool EvaluateInputAST(const char *Filename, bool success = true; if (unsigned N = P->GetNumErrors()) { - std::cerr << Filename << ": parse failure: " - << N << " errors.\n"; + llvm::errs() << Filename << ": parse failure: " << N << " errors.\n"; success = false; } @@ -253,7 +254,7 @@ static bool EvaluateInputAST(const char *Filename, assert(false); break; }; - std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; } else { coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); @@ -280,16 +281,16 @@ static bool EvaluateInputAST(const char *Filename, ie = Decls.end(); it != ie; ++it) { Decl *D = *it; if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) { - std::cout << "Query " << Index << ":\t"; + llvm::outs() << "Query " << Index << ":\t"; assert("FIXME: Support counterexample query commands!"); if (QC->Values.empty() && QC->Objects.empty()) { bool result; if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query), result)) { - std::cout << (result ? "VALID" : "INVALID"); + llvm::outs() << (result ? "VALID" : "INVALID"); } else { - std::cout << "FAIL (reason: " + llvm::outs() << "FAIL (reason: " << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) << ")"; } @@ -304,10 +305,10 @@ static bool EvaluateInputAST(const char *Filename, if (S->getValue(Query(ConstraintManager(QC->Constraints), QC->Values[0]), result)) { - std::cout << "INVALID\n"; - std::cout << "\tExpr 0:\t" << result; + llvm::outs() << "INVALID\n"; + llvm::outs() << "\tExpr 0:\t" << result; } else { - std::cout << "FAIL (reason: " + llvm::outs() << "FAIL (reason: " << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) << ")"; } @@ -317,35 +318,35 @@ static bool EvaluateInputAST(const char *Filename, if (S->getInitialValues(Query(ConstraintManager(QC->Constraints), QC->Query), QC->Objects, result)) { - std::cout << "INVALID\n"; + llvm::outs() << "INVALID\n"; for (unsigned i = 0, e = result.size(); i != e; ++i) { - std::cout << "\tArray " << i << ":\t" + llvm::outs() << "\tArray " << i << ":\t" << QC->Objects[i]->name << "["; for (unsigned j = 0; j != QC->Objects[i]->size; ++j) { - std::cout << (unsigned) result[i][j]; + llvm::outs() << (unsigned) result[i][j]; if (j + 1 != QC->Objects[i]->size) - std::cout << ", "; + llvm::outs() << ", "; } - std::cout << "]"; + llvm::outs() << "]"; if (i + 1 != e) - std::cout << "\n"; + llvm::outs() << "\n"; } } else { SolverImpl::SolverRunStatus retCode = S->impl->getOperationStatusCode(); if (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT == retCode) { - std::cout << " FAIL (reason: " + llvm::outs() << " FAIL (reason: " << SolverImpl::getOperationStatusString(retCode) << ")"; } else { - std::cout << "VALID (counterexample request ignored)"; + llvm::outs() << "VALID (counterexample request ignored)"; } } } - std::cout << "\n"; + llvm::outs() << "\n"; ++Index; } } @@ -358,7 +359,7 @@ static bool EvaluateInputAST(const char *Filename, delete S; if (uint64_t queries = *theStatisticManager->getStatisticByName("Queries")) { - std::cout + llvm::outs() << "--\n" << "total queries = " << queries << "\n" << "total queries constructs = " @@ -390,7 +391,7 @@ static bool printInputAsSMTLIBv2(const char *Filename, bool success = true; if (unsigned N = P->GetNumErrors()) { - std::cerr << Filename << ": parse failure: " + llvm::errs() << Filename << ": parse failure: " << N << " errors.\n"; success = false; } @@ -399,7 +400,7 @@ static bool printInputAsSMTLIBv2(const char *Filename, return false; ExprSMTLIBPrinter* printer = createSMTLIBPrinter(); - printer->setOutput(std::cout); + printer->setOutput(llvm::outs()); unsigned int queryNumber = 0; //Loop over the declarations @@ -409,10 +410,10 @@ static bool printInputAsSMTLIBv2(const char *Filename, if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) { //print line break to separate from previous query - if(queryNumber!=0) std::cout << std::endl; + if(queryNumber!=0) llvm::outs() << "\n"; //Output header for this query as a SMT-LIBv2 comment - std::cout << ";SMTLIBv2 Query " << queryNumber << std::endl; + llvm::outs() << ";SMTLIBv2 Query " << queryNumber << "\n"; /* Can't pass ConstraintManager constructor directly * as argument to Query object. Like... @@ -458,7 +459,7 @@ int main(int argc, char **argv) { OwningPtr<MemoryBuffer> MB; error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), MB); if (ec) { - std::cerr << argv[0] << ": error: " << ec.message() << "\n"; + llvm::errs() << argv[0] << ": error: " << ec.message() << "\n"; return 1; } @@ -494,7 +495,7 @@ int main(int argc, char **argv) { success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB.get(),Builder); break; default: - std::cerr << argv[0] << ": error: Unknown program action!\n"; + llvm::errs() << argv[0] << ": error: Unknown program action!\n"; } delete Builder; diff --git a/tools/klee/Debug.cpp b/tools/klee/Debug.cpp index 3d46de03..ad264045 100644 --- a/tools/klee/Debug.cpp +++ b/tools/klee/Debug.cpp @@ -2,11 +2,11 @@ #include <iostream> void kdb_printExpr(klee::Expr *e) { - std::cerr << "expr: " << e << " -- "; + llvm::errs() << "expr: " << e << " -- "; if (e) { - std::cerr << *e; + llvm::errs() << *e; } else { - std::cerr << "(null)"; + llvm::errs() << "(null)"; } - std::cerr << "\n"; + llvm::errs() << "\n"; } diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 07c33f2a..6abb1569 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -221,7 +221,7 @@ class KleeHandler : public InterpreterHandler { private: Interpreter *m_interpreter; TreeStreamWriter *m_pathWriter, *m_symPathWriter; - std::ostream *m_infoFile; + llvm::raw_ostream *m_infoFile; SmallString<128> m_outputDirectory; @@ -236,7 +236,7 @@ public: KleeHandler(int argc, char **argv); ~KleeHandler(); - std::ostream &getInfoStream() const { return *m_infoFile; } + llvm::raw_ostream &getInfoStream() const { return *m_infoFile; } unsigned getNumTestCases() { return m_testIndex; } unsigned getNumPathsExplored() { return m_pathsExplored; } void incPathsExplored() { m_pathsExplored++; } @@ -248,9 +248,9 @@ public: const char *errorSuffix); std::string getOutputFilename(const std::string &filename); - std::ostream *openOutputFile(const std::string &filename); + llvm::raw_fd_ostream *openOutputFile(const std::string &filename); std::string getTestFilename(const std::string &suffix, unsigned id); - std::ostream *openTestFile(const std::string &suffix, unsigned id); + llvm::raw_fd_ostream *openTestFile(const std::string &suffix, unsigned id); // load a .out file static void loadOutFile(std::string name, @@ -370,16 +370,20 @@ std::string KleeHandler::getOutputFilename(const std::string &filename) { return path.str(); } -std::ostream *KleeHandler::openOutputFile(const std::string &filename) { - std::ios::openmode io_mode = std::ios::out | std::ios::trunc - | std::ios::binary; - std::ostream *f; +llvm::raw_fd_ostream *KleeHandler::openOutputFile(const std::string &filename) { + llvm::raw_fd_ostream *f; + std::string Error; std::string path = getOutputFilename(filename); - f = new std::ofstream(path.c_str(), io_mode); - if (!f) { - klee_error("error opening file \"%s\" (out of memory)", filename.c_str()); - } else if (!f->good()) { - klee_error("error opening file \"%s\". KLEE may have run out of file descriptors: try to increase the maximum number of open file descriptors by using ulimit.", filename.c_str()); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3,0) + f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::sys::fs::F_Binary); +#else + f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::raw_fd_ostream::F_Binary); +#endif + if (!Error.empty()) { + klee_error("error opening file \"%s\". KLEE may have run out of file " + "descriptors: try to increase the maximum number of open file " + "descriptors by using ulimit (%s).", + filename.c_str(), Error.c_str()); delete f; f = NULL; } @@ -393,7 +397,8 @@ std::string KleeHandler::getTestFilename(const std::string &suffix, unsigned id) return filename.str(); } -std::ostream *KleeHandler::openTestFile(const std::string &suffix, unsigned id) { +llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix, + unsigned id) { return openOutputFile(getTestFilename(suffix, id)); } @@ -403,7 +408,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, const char *errorMessage, const char *errorSuffix) { if (errorMessage && ExitOnError) { - std::cerr << "EXITING ON ERROR:\n" << errorMessage << "\n"; + llvm::errs() << "EXITING ON ERROR:\n" << errorMessage << "\n"; exit(1); } @@ -446,7 +451,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, } if (errorMessage) { - std::ostream *f = openTestFile(errorSuffix, id); + llvm::raw_ostream *f = openTestFile(errorSuffix, id); *f << errorMessage; delete f; } @@ -455,16 +460,19 @@ void KleeHandler::processTestCase(const ExecutionState &state, std::vector<unsigned char> concreteBranches; m_pathWriter->readStream(m_interpreter->getPathStreamID(state), concreteBranches); - std::ostream *f = openTestFile("path", id); - std::copy(concreteBranches.begin(), concreteBranches.end(), - std::ostream_iterator<unsigned char>(*f, "\n")); + llvm::raw_fd_ostream *f = openTestFile("path", id); + for (std::vector<unsigned char>::iterator I = concreteBranches.begin(), + E = concreteBranches.end(); + I != E; ++I) { + *f << *I << "\n"; + } delete f; } if (errorMessage || WritePCs) { std::string constraints; m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY); - std::ostream *f = openTestFile("pc", id); + llvm::raw_ostream *f = openTestFile("pc", id); *f << constraints; delete f; } @@ -472,7 +480,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, if (WriteCVCs) { std::string constraints; m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); - std::ostream *f = openTestFile("cvc", id); + llvm::raw_ostream *f = openTestFile("cvc", id); *f << constraints; delete f; } @@ -480,7 +488,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, if(WriteSMT2s) { std::string constraints; m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); - std::ostream *f = openTestFile("smt2", id); + llvm::raw_ostream *f = openTestFile("smt2", id); *f << constraints; delete f; } @@ -489,16 +497,17 @@ void KleeHandler::processTestCase(const ExecutionState &state, std::vector<unsigned char> symbolicBranches; m_symPathWriter->readStream(m_interpreter->getSymbolicPathStreamID(state), symbolicBranches); - std::ostream *f = openTestFile("sym.path", id); - std::copy(symbolicBranches.begin(), symbolicBranches.end(), - std::ostream_iterator<unsigned char>(*f, "\n")); + llvm::raw_fd_ostream *f = openTestFile("sym.path", id); + for (std::vector<unsigned char>::iterator I = symbolicBranches.begin(), E = symbolicBranches.end(); I!=E; ++I) { + *f << *I << "\n"; + } delete f; } if (WriteCov) { std::map<const std::string*, std::set<unsigned> > cov; m_interpreter->getCoveredLines(state, cov); - std::ostream *f = openTestFile("cov", id); + llvm::raw_ostream *f = openTestFile("cov", id); for (std::map<const std::string*, std::set<unsigned> >::iterator it = cov.begin(), ie = cov.end(); it != ie; ++it) { @@ -515,7 +524,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, if (WriteTestInfo) { double elapsed_time = util::getWallTime() - start_time; - std::ostream *f = openTestFile("info", id); + llvm::raw_ostream *f = openTestFile("info", id); *f << "Time to generate test case: " << elapsed_time << "s\n"; delete f; @@ -550,8 +559,8 @@ void KleeHandler::getOutFiles(std::string path, } if (ec) { - std::cerr << "ERROR: unable to read output directory: " << path - << ": " << ec.message() << "\n"; + llvm::errs() << "ERROR: unable to read output directory: " << path << ": " + << ec.message() << "\n"; exit(1); } } @@ -954,11 +963,11 @@ void stop_forking() { static void interrupt_handle() { if (!interrupted && theInterpreter) { - std::cerr << "KLEE: ctrl-c detected, requesting interpreter to halt.\n"; + llvm::errs() << "KLEE: ctrl-c detected, requesting interpreter to halt.\n"; halt_execution(); sys::SetInterruptFunction(interrupt_handle); } else { - std::cerr << "KLEE: ctrl-c detected, exiting.\n"; + llvm::errs() << "KLEE: ctrl-c detected, exiting.\n"; exit(1); } interrupted = true; @@ -1292,7 +1301,7 @@ int main(int argc, char **argv, char **envp) { // locale and other data and then calls main. Function *mainFn = mainModule->getFunction("main"); if (!mainFn) { - std::cerr << "'main' function not found in module.\n"; + llvm::errs() << "'main' function not found in module.\n"; return -1; } @@ -1347,8 +1356,8 @@ int main(int argc, char **argv, char **envp) { Interpreter *interpreter = theInterpreter = Interpreter::create(IOpts, handler); handler->setInterpreter(interpreter); - - std::ostream &infoFile = handler->getInfoStream(); + + llvm::raw_ostream &infoFile = handler->getInfoStream(); for (int i=0; i<argc; i++) { infoFile << argv[i] << (i+1<argc ? " ":"\n"); } @@ -1386,7 +1395,7 @@ int main(int argc, char **argv, char **envp) { if (out) { kTests.push_back(out); } else { - std::cerr << "KLEE: unable to open: " << *it << "\n"; + llvm::errs() << "KLEE: unable to open: " << *it << "\n"; } } @@ -1403,8 +1412,9 @@ int main(int argc, char **argv, char **envp) { it != ie; ++it) { KTest *out = *it; interpreter->setReplayOut(out); - std::cerr << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) << " bytes)" - << " (" << ++i << "/" << outFiles.size() << ")\n"; + llvm::errs() << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) + << " bytes)" + << " (" << ++i << "/" << outFiles.size() << ")\n"; // XXX should put envp in .ktest ? interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp); if (interrupted) break; @@ -1421,7 +1431,7 @@ int main(int argc, char **argv, char **envp) { it != ie; ++it) { KTest *out = kTest_fromFile(it->c_str()); if (!out) { - std::cerr << "KLEE: unable to open: " << *it << "\n"; + llvm::errs() << "KLEE: unable to open: " << *it << "\n"; exit(1); } seeds.push_back(out); @@ -1436,19 +1446,19 @@ int main(int argc, char **argv, char **envp) { it2 != ie; ++it2) { KTest *out = kTest_fromFile(it2->c_str()); if (!out) { - std::cerr << "KLEE: unable to open: " << *it2 << "\n"; + llvm::errs() << "KLEE: unable to open: " << *it2 << "\n"; exit(1); } seeds.push_back(out); } if (outFiles.empty()) { - std::cerr << "KLEE: seeds directory is empty: " << *it << "\n"; + llvm::errs() << "KLEE: seeds directory is empty: " << *it << "\n"; exit(1); } } if (!seeds.empty()) { - std::cerr << "KLEE: using " << seeds.size() << " seeds\n"; + llvm::errs() << "KLEE: using " << seeds.size() << " seeds\n"; interpreter->useSeeds(&seeds); } if (RunInDir != "") { @@ -1518,7 +1528,7 @@ int main(int argc, char **argv, char **envp) { << handler->getNumPathsExplored() << "\n"; stats << "KLEE: done: generated tests = " << handler->getNumTestCases() << "\n"; - std::cerr << stats.str(); + llvm::errs() << stats.str(); handler->getInfoStream() << stats.str(); BufferPtr.take(); |