From d934d983692c8952cdb887cbcd59f2df0001b9c0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:15:59 +0200 Subject: Refactoring from std::ostream to llvm::raw_ostream According to LLVM: lightweight and simpler implementation of streams. --- lib/Solver/FastCexSolver.cpp | 36 ++++++++++++++++++++---------------- 1 file changed, 20 insertions(+), 16 deletions(-) (limited to 'lib/Solver/FastCexSolver.cpp') 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"; } } }; -- 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(-) (limited to 'lib/Solver/FastCexSolver.cpp') 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 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(-) (limited to 'lib/Solver/FastCexSolver.cpp') 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