diff options
author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2014-05-29 23:15:59 +0200 |
---|---|---|
committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2014-05-29 23:57:45 +0200 |
commit | d934d983692c8952cdb887cbcd59f2df0001b9c0 (patch) | |
tree | 9179a257bb053ba0a0da0e9dc4d2c030202c0f28 /lib/Solver | |
parent | c2dec441f3f89916962175f0307b5c33473fa616 (diff) | |
download | klee-d934d983692c8952cdb887cbcd59f2df0001b9c0.tar.gz |
Refactoring from std::ostream to llvm::raw_ostream
According to LLVM: lightweight and simpler implementation of streams.
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 36 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 33 | ||||
-rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 6 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 10 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 10 |
5 files changed, 54 insertions, 41 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 6e52dc32..a488db2a 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -18,6 +18,7 @@ // FIXME: Use APInt. #include "klee/Internal/Support/IntEvaluation.h" +#include "llvm/Support/raw_ostream.h" #include <iostream> #include <sstream> #include <cassert> @@ -109,7 +110,7 @@ public: ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {} ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {} - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { if (isFixed()) { os << m_min; } else { @@ -283,7 +284,8 @@ public: } }; -inline std::ostream &operator<<(std::ostream &os, const ValueRange &vr) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const ValueRange &vr) { vr.print(os); return os; } @@ -443,7 +445,7 @@ public: void propogatePossibleValues(ref<Expr> e, CexValueData range) { #ifdef DEBUG - std::cerr << "propogate: " << range << " for\n" << e << "\n"; + llvm::errs() << "propogate: " << range << " for\n" << e << "\n"; #endif switch (e->getKind()) { @@ -938,27 +940,29 @@ public: } void dump() { - std::cerr << "-- propogated values --\n"; - for (std::map<const Array*, CexObjectData*>::iterator - it = objects.begin(), ie = objects.end(); it != ie; ++it) { + llvm::errs() << "-- propogated values --\n"; + for (std::map<const Array *, CexObjectData *>::iterator + it = objects.begin(), + ie = objects.end(); + it != ie; ++it) { const Array *A = it->first; CexObjectData *COD = it->second; - - std::cerr << A->name << "\n"; - std::cerr << "possible: ["; + + llvm::errs() << A->name << "\n"; + llvm::errs() << "possible: ["; for (unsigned i = 0; i < A->size; ++i) { if (i) - std::cerr << ", "; - std::cerr << COD->getPossibleValues(i); + llvm::errs() << ", "; + llvm::errs() << COD->getPossibleValues(i); } - std::cerr << "]\n"; - std::cerr << "exact : ["; + llvm::errs() << "]\n"; + llvm::errs() << "exact : ["; for (unsigned i = 0; i < A->size; ++i) { if (i) - std::cerr << ", "; - std::cerr << COD->getExactValues(i); + llvm::errs() << ", "; + llvm::errs() << COD->getExactValues(i); } - std::cerr << "]\n"; + llvm::errs() << "]\n"; } } }; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index d9fc77dc..3c0b9b26 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -15,6 +15,7 @@ #include "klee/util/ExprUtil.h" +#include "llvm/Support/raw_ostream.h" #include <map> #include <vector> #include <ostream> @@ -60,7 +61,7 @@ public: return false; } - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { bool first = true; os << "{"; for (typename set_ty::iterator it = s.begin(), ie = s.end(); @@ -76,8 +77,9 @@ public: } }; -template<class T> -inline std::ostream &operator<<(std::ostream &os, const ::DenseSet<T> &dis) { +template <class T> +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const ::DenseSet<T> &dis) { dis.print(os); return os; } @@ -124,7 +126,7 @@ public: return *this; } - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { os << "{"; bool first = true; for (std::set<const Array*>::iterator it = wholeObjects.begin(), @@ -214,7 +216,8 @@ public: } }; -inline std::ostream &operator<<(std::ostream &os, const IndependentElementSet &ies) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const IndependentElementSet &ies) { ies.print(os); return os; } @@ -247,20 +250,22 @@ IndependentElementSet getIndependentConstraints(const Query& query, worklist.swap(newWorklist); } while (!done); +#if 0 if (0) { std::set< ref<Expr> > reqset(result.begin(), result.end()); - std::cerr << "--\n"; - std::cerr << "Q: " << query.expr << "\n"; - std::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n"; + errs() << "--\n"; + errs() << "Q: " << query.expr << "\n"; + errs() << "\telts: " << IndependentElementSet(query.expr) << "\n"; int i = 0; - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) { - std::cerr << "C" << i++ << ": " << *it; - std::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; - std::cerr << "\telts: " << IndependentElementSet(*it) << "\n"; + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); it != ie; ++it) { + errs() << "C" << i++ << ": " << *it; + errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; + errs() << "\telts: " << IndependentElementSet(*it) << "\n"; } - std::cerr << "elts closure: " << eltsClosure << "\n"; + errs() << "elts closure: " << eltsClosure << "\n"; } +#endif return eltsClosure; } diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index f1e55614..b5c99907 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -599,9 +599,9 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu ++stats::queryConstructs; -// std::cerr << "Constructing expression "; -// ExprPPrinter::printSingleExpr(std::cerr, e); -// std::cerr << "\n"; +// llvm::errs() << "Constructing expression "; +// ExprPPrinter::printSingleExpr(llvm::errs(), e); +// llvm::errs() << "\n"; switch (e->getKind()) { diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index f2e38182..d5598d1d 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -18,9 +18,10 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, const std::string& commentSign, int queryTimeToLog) - : solver(_solver), - os(path.c_str(), std::ios::trunc), - logBuffer(""), + : solver(_solver), + os(path.c_str(), ErrorInfo), + BufferString(""), + logBuffer(BufferString), queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f), @@ -79,8 +80,7 @@ void QueryLoggingSolver::flushBuffer() { } // prepare the buffer for reuse - logBuffer.clear(); - logBuffer.str(""); + BufferString = ""; } bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 2c7d80e8..ad1722ca 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -12,6 +12,7 @@ #include "klee/Solver.h" #include "klee/SolverImpl.h" +#include "llvm/Support/raw_ostream.h" #include <fstream> #include <sstream> @@ -25,9 +26,12 @@ class QueryLoggingSolver : public SolverImpl { protected: Solver *solver; - std::ofstream os; - std::ostringstream logBuffer; // buffer to store logs before flushing to - // file + std::string ErrorInfo; + llvm::raw_fd_ostream os; + // @brief Buffer used by logBuffer + std::string BufferString; + // @brief buffer to store logs before flushing to file + llvm::raw_string_ostream logBuffer; unsigned queryCount; int minQueryTimeToLog; // we log to file only those queries // which take longer than the specified time (ms); |