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. --- include/klee/ExecutionState.h | 4 +- include/klee/Expr.h | 30 +++++++-- include/klee/Interpreter.h | 6 +- include/klee/util/ExprPPrinter.h | 13 ++-- include/klee/util/ExprSMTLIBPrinter.h | 11 ++-- include/klee/util/PrintContext.h | 16 ++--- include/klee/util/Ref.h | 12 +++- 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 +++--- tools/kleaver/main.cpp | 77 +++++++++++----------- tools/klee/Debug.cpp | 8 +-- tools/klee/main.cpp | 94 +++++++++++++++------------ 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 #include #include -#include // FIXME: Remove this!!! namespace llvm { class Type; + class raw_ostream; } namespace klee { @@ -181,7 +183,7 @@ public: virtual unsigned getNumKids() const = 0; virtual ref 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 &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 &e); + static void printSingleExpr(llvm::raw_ostream &os, const ref &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 &q, const ref *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 #include #include #include @@ -20,6 +19,10 @@ #include #include +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 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 +#include "klee/Expr.h" +#include "llvm/Support/raw_ostream.h" #include #include #include -#include /// 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 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 #include // FIXME: Remove this!!! +namespace llvm { + class raw_ostream; +} + namespace klee { template @@ -107,7 +111,13 @@ public: }; template -inline std::ostream &operator<<(std::ostream &os, const ref &e) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const ref &e) { + os << *e; + return os; +} + +template +inline std::stringstream &operator<<(std::stringstream &os, const ref &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 #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; 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(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(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(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 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=="-"? "" : 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 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 concreteBranches; m_pathWriter->readStream(m_interpreter->getPathStreamID(state), concreteBranches); - std::ostream *f = openTestFile("path", id); - std::copy(concreteBranches.begin(), concreteBranches.end(), - std::ostream_iterator(*f, "\n")); + llvm::raw_fd_ostream *f = openTestFile("path", id); + for (std::vector::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 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(*f, "\n")); + llvm::raw_fd_ostream *f = openTestFile("sym.path", id); + for (std::vector::iterator I = symbolicBranches.begin(), E = symbolicBranches.end(); I!=E; ++I) { + *f << *I << "\n"; + } delete f; } if (WriteCov) { std::map > cov; m_interpreter->getCoveredLines(state, cov); - std::ostream *f = openTestFile("cov", id); + llvm::raw_ostream *f = openTestFile("cov", id); for (std::map >::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; isetReplayOut(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(); -- cgit 1.4.1 From 3b35ffed89405e7ba3059664dfbdc165b5d8625d Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:21:33 +0200 Subject: Remove #include to avoid static constructors iostream injects static constructor function into every compilation unit. Remove this to avoid it. --- include/klee/Internal/ADT/TreeStream.h | 1 - lib/Core/ExecutorUtil.cpp | 1 - lib/Core/ExternalDispatcher.cpp | 1 - lib/Core/ImpliedValue.cpp | 1 - lib/Core/Memory.cpp | 1 - lib/Core/PTree.cpp | 1 - lib/Core/PTree.h | 4 ---- lib/Core/Searcher.h | 4 +--- lib/Core/SpecialFunctionHandler.cpp | 5 +++-- lib/Core/StatsTracker.cpp | 2 -- lib/Core/StatsTracker.h | 1 - lib/Expr/Constraints.cpp | 1 - lib/Expr/Expr.cpp | 1 - lib/Expr/ExprPPrinter.cpp | 3 --- lib/Expr/ExprSMTLIBLetPrinter.cpp | 2 +- lib/Expr/ExprSMTLIBPrinter.cpp | 2 -- lib/Expr/Lexer.cpp | 1 - lib/Expr/Parser.cpp | 1 - lib/Module/Checks.cpp | 1 - lib/Module/ModuleUtil.cpp | 2 -- lib/Module/Optimize.cpp | 1 - lib/SMT/SMTParser.cpp | 1 - lib/SMT/SMTParser.h | 2 -- lib/SMT/main.cpp | 1 - lib/Solver/FastCexSolver.cpp | 1 - lib/Solver/IndependentSolver.cpp | 1 - lib/Solver/STPBuilder.cpp | 1 - lib/Solver/Solver.cpp | 1 - lib/Support/TreeStream.cpp | 1 - tools/kleaver/main.cpp | 2 -- tools/klee/Debug.cpp | 1 - tools/klee/main.cpp | 1 - 32 files changed, 5 insertions(+), 45 deletions(-) diff --git a/include/klee/Internal/ADT/TreeStream.h b/include/klee/Internal/ADT/TreeStream.h index 63e49dbb..1494aa76 100644 --- a/include/klee/Internal/ADT/TreeStream.h +++ b/include/klee/Internal/ADT/TreeStream.h @@ -11,7 +11,6 @@ #define __UTIL_TREESTREAM_H__ #include -#include #include namespace klee { diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 79d1707e..f6b3dd5e 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -41,7 +41,6 @@ #include "llvm/Support/CallSite.h" -#include #include using namespace klee; diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index bbe1c42e..4c1e2b86 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -42,7 +42,6 @@ #endif #include #include -#include using namespace llvm; using namespace klee; diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index f20259fb..c8342df1 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -18,7 +18,6 @@ #include "klee/util/ExprUtil.h" -#include #include #include diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 7f5d024e..b6f225d1 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -32,7 +32,6 @@ #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" -#include #include #include diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index a435cd5e..f0e7ab51 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -13,7 +13,6 @@ #include #include -#include using namespace klee; diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index 2ac688bd..11d3f48c 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -12,10 +12,6 @@ #include -#include -#include -#include - namespace klee { class ExecutionState; diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 3c077636..d866f521 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -10,14 +10,12 @@ #ifndef KLEE_SEARCHER_H #define KLEE_SEARCHER_H +#include "llvm/Support/raw_ostream.h" #include #include #include #include -// FIXME: Move out of header, use llvm streams. -#include - namespace llvm { class BasicBlock; class Function; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index dcba5436..a7a1b32e 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -27,6 +27,7 @@ #include "llvm/Module.h" #endif #include "llvm/ADT/Twine.h" +#include "llvm/Support/Debug.h" #include @@ -279,8 +280,8 @@ void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state, "invalid number of arguments to klee_alias_function"); std::string old_fn = readStringAtAddress(state, arguments[0]); std::string new_fn = readStringAtAddress(state, arguments[1]); - DEBUG_WITH_TYPE("alias_handling", errs() << "Replacing " << old_fn - << "() with " << new_fn << "()\n";); + DEBUG_WITH_TYPE("alias_handling", llvm::errs() << "Replacing " << old_fn + << "() with " << new_fn << "()\n"); if (old_fn == new_fn) state.removeFnAlias(old_fn); else state.addFnAlias(old_fn, new_fn); diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 4f4552e7..0946d2ba 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -46,12 +46,10 @@ #endif #include "llvm/Support/CommandLine.h" #include "llvm/Support/CFG.h" -#include "llvm/Support/raw_os_ostream.h" #include "llvm/Support/Process.h" #include "llvm/Support/Path.h" #include "llvm/Support/FileSystem.h" -#include #include #include diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h index f06decdc..629a723d 100644 --- a/lib/Core/StatsTracker.h +++ b/lib/Core/StatsTracker.h @@ -12,7 +12,6 @@ #include "CallPathManager.h" -#include #include namespace llvm { diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 90d9bcd4..ae4563f4 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -19,7 +19,6 @@ #include "llvm/Support/CommandLine.h" #include "klee/Internal/Module/KModule.h" -#include #include using namespace klee; diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 14737e8c..d54b8f4d 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -21,7 +21,6 @@ #include "klee/util/ExprPPrinter.h" -#include #include using namespace klee; diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index a7ad5ddc..ddcc57a1 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -17,9 +17,6 @@ #include #include -#include -#include -#include using namespace klee; diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp index 2ea5c4e0..bcdaab32 100644 --- a/lib/Expr/ExprSMTLIBLetPrinter.cpp +++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp @@ -8,7 +8,7 @@ // //===----------------------------------------------------------------------===// -#include +#include "llvm/Support/raw_ostream.h" #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBLetPrinter.h" diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index 2dbf3634..1cdab762 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -7,8 +7,6 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include - #include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBPrinter.h" diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp index 9859ff36..e250a968 100644 --- a/lib/Expr/Lexer.cpp +++ b/lib/Expr/Lexer.cpp @@ -13,7 +13,6 @@ #include "llvm/Support/raw_ostream.h" #include -#include #include using namespace llvm; diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 6b346648..aebce666 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -22,7 +22,6 @@ #include "llvm/Support/raw_ostream.h" #include -#include #include #include diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp index 80b6b245..e1076d43 100644 --- a/lib/Module/Checks.cpp +++ b/lib/Module/Checks.cpp @@ -46,7 +46,6 @@ #include "llvm/Transforms/Scalar.h" #include "llvm/Transforms/Utils/BasicBlockUtils.h" #include "llvm/Support/CallSite.h" -#include using namespace llvm; using namespace klee; diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 4f65d0e7..d00cf574 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -28,7 +28,6 @@ #include "llvm/Object/ObjectFile.h" #include "llvm/Object/Error.h" #include "llvm/Support/FileSystem.h" -#include "llvm/Support/raw_os_ostream.h" #include "llvm/IR/ValueSymbolTable.h" #include "llvm/Support/SourceMgr.h" #include "llvm/Support/DataStream.h" @@ -51,7 +50,6 @@ #include #include -#include #include #include #include diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 6f060edd..ed1e0e34 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -40,7 +40,6 @@ #include "llvm/Transforms/Scalar.h" #include "llvm/Support/PassNameParser.h" #include "llvm/Support/PluginLoader.h" -#include using namespace llvm; #if 0 diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index d16e1edb..5622f048 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -14,7 +14,6 @@ #include "klee/Constraints.h" #include "expr/Parser.h" -#include #include #include #include diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h index fd1ec044..ac84e74c 100644 --- a/lib/SMT/SMTParser.h +++ b/lib/SMT/SMTParser.h @@ -13,8 +13,6 @@ #include "expr/Parser.h" -#include -#include #include #include #include diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp index 034c4ce4..6b66e279 100644 --- a/lib/SMT/main.cpp +++ b/lib/SMT/main.cpp @@ -2,7 +2,6 @@ #include "klee/ExprBuilder.h" -#include using namespace std; using namespace klee; diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index a488db2a..5c0cf8d0 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -19,7 +19,6 @@ #include "klee/Internal/Support/IntEvaluation.h" #include "llvm/Support/raw_ostream.h" -#include #include #include #include diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 3c0b9b26..2cb4b2c6 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -19,7 +19,6 @@ #include #include #include -#include using namespace klee; using namespace llvm; diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index e4a21f74..34ce0ede 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -34,7 +34,6 @@ #include // max, min #include -#include #include #include #include diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 025c70f2..229fa234 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -771,7 +771,6 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, } } } -#include bool STPSolverImpl::computeInitialValues(const Query &query, const std::vector diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp index e95fc582..0d5e4568 100644 --- a/lib/Support/TreeStream.cpp +++ b/lib/Support/TreeStream.cpp @@ -10,7 +10,6 @@ #include "klee/Internal/ADT/TreeStream.h" #include -#include #include #include #include diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index e31140e8..b19e2ea6 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -1,5 +1,3 @@ -#include - #include "expr/Lexer.h" #include "expr/Parser.h" diff --git a/tools/klee/Debug.cpp b/tools/klee/Debug.cpp index ad264045..fbabed9d 100644 --- a/tools/klee/Debug.cpp +++ b/tools/klee/Debug.cpp @@ -1,5 +1,4 @@ #include -#include void kdb_printExpr(klee::Expr *e) { llvm::errs() << "expr: " << e << " -- "; diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 6abb1569..0292376c 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -62,7 +62,6 @@ #include #include #include -#include #include #include -- cgit 1.4.1 From 4290d38b1a8dbc5576c206a7d4f2db14d16362ca Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:22:43 +0200 Subject: Avoid non-explicit use of functions from std namespace in KLEE --- lib/Expr/ExprSMTLIBLetPrinter.cpp | 11 +++++------ lib/Expr/ExprSMTLIBPrinter.cpp | 9 ++++----- lib/SMT/SMTParser.cpp | 1 - lib/SMT/main.cpp | 2 -- 4 files changed, 9 insertions(+), 14 deletions(-) diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp index bcdaab32..d4243452 100644 --- a/lib/Expr/ExprSMTLIBLetPrinter.cpp +++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp @@ -12,8 +12,6 @@ #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBLetPrinter.h" -using namespace std; - namespace ExprSMTLIBOptions { llvm::cl::opt useLetExpressions("smtlib-use-let-expressions", @@ -85,7 +83,7 @@ void ExprSMTLIBLetPrinter::scan(const ref &e) { void ExprSMTLIBLetPrinter::generateBindings() { // Assign a number to each binding that will be used unsigned int counter = 0; - for (set >::const_iterator i = twoOrMoreEO.begin(); + for (std::set >::const_iterator i = twoOrMoreEO.begin(); i != twoOrMoreEO.end(); ++i) { bindings.insert(std::make_pair(*i, counter)); ++counter; @@ -94,7 +92,7 @@ void ExprSMTLIBLetPrinter::generateBindings() { void ExprSMTLIBLetPrinter::printExpression( const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) { - map, unsigned int>::const_iterator i = bindings.find(e); + std::map, unsigned int>::const_iterator i = bindings.find(e); if (disablePrintedAbbreviations || i == bindings.end()) { /*There is no abbreviation for this expression so print it normally. @@ -143,7 +141,7 @@ void ExprSMTLIBLetPrinter::printLetExpression() { p->pushIndent(); // Print each binding - for (map, unsigned int>::const_iterator i = + for (std::map, unsigned int>::const_iterator i = bindings.begin(); i != bindings.end(); ++i) { printSeperator(); @@ -173,7 +171,8 @@ void ExprSMTLIBLetPrinter::printLetExpression() { // print out Expressions with abbreviations. unsigned int numberOfItems = query->constraints.size() + 1; //+1 for query unsigned int itemsLeft = numberOfItems; - vector >::const_iterator constraint = query->constraints.begin(); + std::vector >::const_iterator constraint = + query->constraints.begin(); /* Produce nested (and () () statements. If the constraint set * is empty then we will only print the "queryAssert". diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index 1cdab762..e1a49afb 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -11,8 +11,6 @@ #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBPrinter.h" -using namespace std; - namespace ExprSMTLIBOptions { // Command line options llvm::cl::opt @@ -495,7 +493,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { /*loop over elements in the array and generate an assert statement for each one */ - for (vector >::const_iterator + for (std::vector >::const_iterator ce = array->constantValues.begin(); ce != array->constantValues.end(); ce++, byteIndex++) { *p << "(assert ("; @@ -556,7 +554,7 @@ void ExprSMTLIBPrinter::printAction() { const Array *theArray = 0; // loop over the array names - for (vector::const_iterator it = + for (std::vector::const_iterator it = arraysToCallGetValueOn->begin(); it != arraysToCallGetValueOn->end(); it++) { theArray = *it; @@ -882,7 +880,8 @@ ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector &a) { * that the solver knows what to do when we ask for the values of arrays * that don't feature in our query! */ - for (vector::const_iterator i = a.begin(); i != a.end(); ++i) { + for (std::vector::const_iterator i = a.begin(); i != a.end(); + ++i) { usedArrays.insert(*i); } } diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index 5622f048..03042fdd 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -22,7 +22,6 @@ //#define DEBUG -using namespace std; using namespace klee; using namespace klee::expr; diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp index 6b66e279..31fa311d 100644 --- a/lib/SMT/main.cpp +++ b/lib/SMT/main.cpp @@ -2,8 +2,6 @@ #include "klee/ExprBuilder.h" - -using namespace std; using namespace klee; int main(int argc, char** argv) { -- cgit 1.4.1 From d124e44cf09da646f88b61b1937efb39b98efc6d Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:22:59 +0200 Subject: Fix header --- lib/Expr/ExprSMTLIBPrinter.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index e1a49afb..bbb82d0d 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -1,5 +1,4 @@ -//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ -//-*-===// +//===-- ExprSMTLIBPrinter.cpp -----------------------------------*- C++ -*-===// // // The KLEE Symbolic Virtual Machine // -- cgit 1.4.1 From 48492cbfa729fe035b7b69b71b541cb67f8545df Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 22 May 2014 21:56:22 +0200 Subject: Use LLVM DEBUG macro instead of #if 0 or #if DEBUG --- lib/Solver/FastCexSolver.cpp | 14 ++++---------- lib/Solver/IndependentSolver.cpp | 9 +++++---- 2 files changed, 9 insertions(+), 14 deletions(-) diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 5c0cf8d0..57e44806 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -18,6 +18,8 @@ // FIXME: Use APInt. #include "klee/Internal/Support/IntEvaluation.h" +#define DEBUG_TYPE "cex-solver" +#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" #include #include @@ -406,10 +408,6 @@ public: : objects(_objects) {} }; -#if 0 -#define DEBUG -#endif - class CexData { public: std::map objects; @@ -443,9 +441,7 @@ public: } void propogatePossibleValues(ref e, CexValueData range) { - #ifdef DEBUG - llvm::errs() << "propogate: " << range << " for\n" << e << "\n"; - #endif + DEBUG(llvm::errs() << "propogate: " << range << " for\n" << e << "\n";); switch (e->getKind()) { case Expr::Constant: @@ -1012,9 +1008,7 @@ static bool propogateValues(const Query& query, CexData &cd, cd.propogateExactValue(query.expr, 0); } -#ifdef DEBUG - cd.dump(); -#endif + DEBUG(cd.dump();); // Check the result. bool hasSatisfyingAssignment = true; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 2cb4b2c6..46b4ee56 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -15,6 +15,8 @@ #include "klee/util/ExprUtil.h" +#define DEBUG_TYPE "independent-solver" +#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" #include #include @@ -249,8 +251,7 @@ IndependentElementSet getIndependentConstraints(const Query& query, worklist.swap(newWorklist); } while (!done); -#if 0 - if (0) { +DEBUG( std::set< ref > reqset(result.begin(), result.end()); errs() << "--\n"; errs() << "Q: " << query.expr << "\n"; @@ -263,8 +264,8 @@ IndependentElementSet getIndependentConstraints(const Query& query, errs() << "\telts: " << IndependentElementSet(*it) << "\n"; } errs() << "elts closure: " << eltsClosure << "\n"; - } -#endif + ); + return eltsClosure; } -- cgit 1.4.1 From eaac527a2821c41aa88c8767fd0305f9d610fb23 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 28 May 2014 22:35:45 +0200 Subject: Fix ExprTest under LLVM 2.9 --- include/klee/Expr.h | 3 +++ unittests/Expr/Makefile | 1 + 2 files changed, 4 insertions(+) diff --git a/include/klee/Expr.h b/include/klee/Expr.h index ae5bfd2b..c78cd690 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -298,10 +298,13 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr &e) { return os; } +// XXX the following macro is to work around the ExprTest unit test compile error +#ifndef LLVM_29_UNITTEST inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr::Kind kind) { Expr::printKind(os, kind); return os; } +#endif inline std::stringstream &operator<<(std::stringstream &os, const Expr &e) { std::string str; diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile index f1cd4ec4..a9bfeda1 100644 --- a/unittests/Expr/Makefile +++ b/unittests/Expr/Makefile @@ -9,4 +9,5 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest +CXXFLAGS += -DLLVM_29_UNITTEST LIBS += -lstp -- cgit 1.4.1