Refactoring from std::ostream to llvm::raw_ostream

According to LLVM: lightweight and simpler implementation of streams.

7 files changed, 64 insertions, 28 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 720488cc..824fbed5 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -32,7 +32,7 @@ namespace klee {
   class PTreeNode;
   struct InstructionInfo;
 
-std::ostream &operator<<(std::ostream &os, const MemoryMap &mm);
+llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
 
 struct StackFrame {
   KInstIterator caller;
@@ -137,7 +137,7 @@ public:
   }
 
   bool merge(const ExecutionState &b);
-  void dumpStack(std::ostream &out) const;
+  void dumpStack(llvm::raw_ostream &out) const;
 };
 
 }
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index a302591a..ae5bfd2b 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -17,13 +17,15 @@
 #include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/SmallVector.h"
+#include "llvm/Support/raw_ostream.h"
 
+#include <sstream>
 #include <set>
 #include <vector>
-#include <iosfwd> // FIXME: Remove this!!!
 
 namespace llvm {
   class Type;
+  class raw_ostream;
 }
 
 namespace klee {
@@ -181,7 +183,7 @@ public:
   virtual unsigned getNumKids() const = 0;
   virtual ref<Expr> getKid(unsigned i) const = 0;
     
-  virtual void print(std::ostream &os) const;
+  virtual void print(llvm::raw_ostream &os) const;
 
   /// dump - Print the expression to stderr.
   void dump() const;
@@ -221,8 +223,8 @@ public:
 
   /* Static utility methods */
 
-  static void printKind(std::ostream &os, Kind k);
-  static void printWidth(std::ostream &os, Expr::Width w);
+  static void printKind(llvm::raw_ostream &os, Kind k);
+  static void printWidth(llvm::raw_ostream &os, Expr::Width w);
 
   /// returns the smallest number of bytes in which the given width fits
   static inline unsigned getMinBytesForWidth(Width w) {
@@ -291,16 +293,32 @@ inline bool operator>=(const Expr &lhs, const Expr &rhs) {
 
 // Printing operators
 
-inline std::ostream &operator<<(std::ostream &os, const Expr &e) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr &e) {
   e.print(os);
   return os;
 }
 
-inline std::ostream &operator<<(std::ostream &os, const Expr::Kind kind) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr::Kind kind) {
   Expr::printKind(os, kind);
   return os;
 }
 
+inline std::stringstream &operator<<(std::stringstream &os, const Expr &e) {
+  std::string str;
+  llvm::raw_string_ostream TmpStr(str);
+  e.print(TmpStr);
+  os << TmpStr.str();
+  return os;
+}
+
+inline std::stringstream &operator<<(std::stringstream &os, const Expr::Kind kind) {
+  std::string str;
+  llvm::raw_string_ostream TmpStr(str);
+  Expr::printKind(TmpStr, kind);
+  os << TmpStr.str();
+  return os;
+}
+
 // Terminal Exprs
 
 class ConstantExpr : public Expr {
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index e93284d6..abd454b1 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -19,6 +19,8 @@ struct KTest;
 namespace llvm {
 class Function;
 class Module;
+class raw_ostream;
+class raw_fd_ostream;
 }
 
 namespace klee {
@@ -31,10 +33,10 @@ public:
   InterpreterHandler() {}
   virtual ~InterpreterHandler() {}
 
-  virtual std::ostream &getInfoStream() const = 0;
+  virtual llvm::raw_ostream &getInfoStream() const = 0;
 
   virtual std::string getOutputFilename(const std::string &filename) = 0;
-  virtual std::ostream *openOutputFile(const std::string &filename) = 0;
+  virtual llvm::raw_fd_ostream *openOutputFile(const std::string &filename) = 0;
 
   virtual void incPathsExplored() = 0;
 
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
index cf4ebb18..622b0e80 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/util/ExprPPrinter.h
@@ -12,6 +12,9 @@
 
 #include "klee/Expr.h"
 
+namespace llvm {
+  class raw_ostream;
+}
 namespace klee {
   class ConstraintManager;
 
@@ -20,7 +23,7 @@ namespace klee {
     ExprPPrinter() {}
     
   public:
-    static ExprPPrinter *create(std::ostream &os);
+    static ExprPPrinter *create(llvm::raw_ostream &os);
 
     virtual ~ExprPPrinter() {}
 
@@ -45,7 +48,7 @@ namespace klee {
 
     /// printOne - Pretty print a single expression prefixed by a
     /// message and followed by a line break.
-    static void printOne(std::ostream &os, const char *message, 
+    static void printOne(llvm::raw_ostream &os, const char *message,
                          const ref<Expr> &e);
 
     /// printSingleExpr - Pretty print a single expression.
@@ -55,12 +58,12 @@ namespace klee {
     /// Note that if the output stream is not positioned at the
     /// beginning of a line then printing will not resume at the
     /// correct position following any output line breaks.
-    static void printSingleExpr(std::ostream &os, const ref<Expr> &e);
+    static void printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e);
 
-    static void printConstraints(std::ostream &os,
+    static void printConstraints(llvm::raw_ostream &os,
                                  const ConstraintManager &constraints);
 
-    static void printQuery(std::ostream &os,
+    static void printQuery(llvm::raw_ostream &os,
                            const ConstraintManager &constraints,
                            const ref<Expr> &q,
                            const ref<Expr> *evalExprsBegin = 0,
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h
index 42f38007..8b072242 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/util/ExprSMTLIBPrinter.h
@@ -11,7 +11,6 @@
 #ifndef KLEE_EXPRSMTLIBPRINTER_H
 #define KLEE_EXPRSMTLIBPRINTER_H
 
-#include <ostream>
 #include <string>
 #include <set>
 #include <map>
@@ -20,6 +19,10 @@
 #include <klee/util/PrintContext.h>
 #include <klee/Solver.h>
 
+namespace llvm {
+class raw_ostream;
+}
+
 namespace klee {
 
 /// Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic.
@@ -121,7 +124,7 @@ public:
 
   /// Set the output stream that will be printed to.
   /// This call is persistent across queries.
-  void setOutput(std::ostream &output);
+  void setOutput(llvm::raw_ostream &output);
 
   /// Set the query to print. This will setArrayValuesToGet()
   /// to none (i.e. no array values will be requested using
@@ -130,7 +133,7 @@ public:
 
   virtual ~ExprSMTLIBPrinter();
 
-  /// Print the query to the std::ostream
+  /// Print the query to the llvm::raw_ostream
   /// setOutput() and setQuery() must be called before calling this.
   ///
   /// All options should be set before calling this.
@@ -202,7 +205,7 @@ protected:
   std::set<const Array *> usedArrays;
 
   /// Output stream to write to
-  std::ostream *o;
+  llvm::raw_ostream *o;
 
   /// The query to print
   const Query *query;
diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h
index a9e91925..6b1ef77a 100644
--- a/include/klee/util/PrintContext.h
+++ b/include/klee/util/PrintContext.h
@@ -1,14 +1,14 @@
 #ifndef PRINTCONTEXT_H_
 #define PRINTCONTEXT_H_
 
-#include <ostream>
+#include "klee/Expr.h"
+#include "llvm/Support/raw_ostream.h"
 #include <sstream>
 #include <string>
 #include <stack>
-#include <iomanip>
 
 /// PrintContext - Helper class for pretty printing.
-/// It provides a basic wrapper around std::ostream that keeps track of
+/// It provides a basic wrapper around llvm::raw_ostream that keeps track of
 /// how many characters have been used on the current line.
 ///
 /// It also provides an optional way keeping track of the various levels of indentation
@@ -16,8 +16,7 @@
 /// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
 class PrintContext {
 private:
-  std::ostream &os;
-  std::stringstream ss;
+  llvm::raw_ostream &os;
   std::string newline;
 
   ///This is used to keep track of the stack of indentations used by
@@ -30,7 +29,7 @@ public:
   /// Number of characters on the current line.
   unsigned pos;
 
-  PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
+  PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
   {
 	  indentStack.push(pos);
   }
@@ -42,7 +41,7 @@ public:
   void breakLine(unsigned indent=0) {
     os << newline;
     if (indent)
-      os << std::setw(indent) << ' ';
+      os.indent(indent) << ' ';
     pos = indent;
   }
 
@@ -79,7 +78,8 @@ public:
 
   template <typename T>
   PrintContext &operator<<(T elt) {
-    ss.str("");
+    std::string str;
+    llvm::raw_string_ostream ss(str);
     ss << elt;
     write(ss.str());
     return *this;
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index d14de471..c77149aa 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -20,6 +20,10 @@ using llvm::dyn_cast_or_null;
 #include <assert.h>
 #include <iosfwd> // FIXME: Remove this!!!
 
+namespace llvm {
+  class raw_ostream;
+}
+
 namespace klee {
 
 template<class T>
@@ -107,7 +111,13 @@ public:
 };
 
 template<class T>
-inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const ref<T> &e) {
+  os << *e;
+  return os;
+}
+
+template<class T>
+inline std::stringstream &operator<<(std::stringstream &os, const ref<T> &e) {
   os << *e;
   return os;
 }