1 //===-- PrintContext.h ------------------------------------------*- C++ -*-===//
2 //
3 //                     The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_PRINTCONTEXT_H
11 #define KLEE_PRINTCONTEXT_H
12 
13 #include "klee/Expr/Expr.h"
14 
15 #include "llvm/Support/raw_ostream.h"
16 
17 #include <sstream>
18 #include <string>
19 #include <stack>
20 
21 /// PrintContext - Helper class for pretty printing.
22 /// It provides a basic wrapper around llvm::raw_ostream that keeps track of
23 /// how many characters have been used on the current line.
24 ///
25 /// It also provides an optional way keeping track of the various levels of indentation
26 /// by using a stack.
27 /// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
28 class PrintContext {
29 private:
30   llvm::raw_ostream &os;
31   std::string newline;
32 
33   ///This is used to keep track of the stack of indentations used by
34   /// \sa breakLineI()
35   /// \sa pushIndent()
36   /// \sa popIndent()
37   std::stack<unsigned int> indentStack;
38 
39 public:
40   /// Number of characters on the current line.
41   unsigned pos;
42 
PrintContext(llvm::raw_ostream & _os)43   PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
44   {
45 	  indentStack.push(pos);
46   }
47 
setNewline(const std::string & _newline)48   void setNewline(const std::string &_newline) {
49     newline = _newline;
50   }
51 
52   void breakLine(unsigned indent=0) {
53     os << newline;
54     if (indent)
55       os.indent(indent) << ' ';
56     pos = indent;
57   }
58 
59   ///Break line using the indent on the top of the indent stack
60   /// \return The PrintContext object so the method is chainable
breakLineI()61   PrintContext& breakLineI()
62   {
63 	  breakLine(indentStack.top());
64 	  return *this;
65   }
66 
67   ///Add the current position on the line to the top of the indent stack
68   /// \return The PrintContext object so the method is chainable
pushIndent()69   PrintContext& pushIndent()
70   {
71 	  indentStack.push(pos);
72 	  return *this;
73   }
74 
75   ///Pop the top off the indent stack
76   /// \return The PrintContext object so the method is chainable
popIndent()77   PrintContext& popIndent()
78   {
79 	  indentStack.pop();
80 	  return *this;
81   }
82 
83   /// write - Output a string to the stream and update the
84   /// position. The stream should not have any newlines.
write(const std::string & s)85   void write(const std::string &s) {
86     os << s;
87     pos += s.length();
88   }
89 
90   template <typename T>
91   PrintContext &operator<<(T elt) {
92     std::string str;
93     llvm::raw_string_ostream ss(str);
94     ss << elt;
95     write(ss.str());
96     return *this;
97   }
98 
99 };
100 
101 
102 #endif /* KLEE_PRINTCONTEXT_H */
103