cprover
message.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_MESSAGE_H
11 #define CPROVER_UTIL_MESSAGE_H
12 
13 #include <functional>
14 #include <iosfwd>
15 #include <sstream>
16 #include <string>
17 
18 #include "invariant.h"
19 #include "json.h"
20 #include "source_location.h"
21 #include "xml.h"
22 
23 class json_stream_arrayt;
24 
26 {
27 public:
29  {
30  }
31 
32  virtual void print(unsigned level, const std::string &message)=0;
33 
34  virtual void print(unsigned level, const xmlt &xml)
35  {
36  // no-op by default
37  }
38 
41  {
43  }
44 
45  virtual void print(unsigned level, const jsont &json)
46  {
47  // no-op by default
48  }
49 
50  virtual void print(
51  unsigned level,
52  const std::string &message,
53  int sequence_number,
54  const source_locationt &location);
55 
56  virtual void flush(unsigned level)
57  {
58  // no-op by default
59  }
60 
62  {
63  }
64 
65  void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; }
66  unsigned get_verbosity() const { return verbosity; }
67 
68  unsigned get_message_count(unsigned level) const
69  {
70  if(level>=message_count.size())
71  return 0;
72 
73  return message_count[level];
74  }
75 
76 protected:
77  unsigned verbosity;
78  std::vector<unsigned> message_count;
79 };
80 
82 {
83 public:
84  virtual void print(unsigned level, const std::string &message)
85  {
86  message_handlert::print(level, message);
87  }
88 
89  virtual void print(
90  unsigned level,
91  const std::string &message,
92  int sequence_number,
93  const source_locationt &location)
94  {
95  print(level, message);
96  }
97 };
98 
100 {
101 public:
102  explicit stream_message_handlert(std::ostream &_out):out(_out)
103  {
104  }
105 
106  virtual void print(unsigned level, const std::string &message)
107  {
108  message_handlert::print(level, message);
109 
110  if(verbosity>=level)
111  out << message << '\n';
112  }
113 
114  virtual void flush(unsigned level)
115  {
116  out << std::flush;
117  }
118 
119 protected:
120  std::ostream &out;
121 };
122 
123 class messaget
124 {
125 public:
126  // Standard message levels:
127  //
128  // 0 none
129  // 1 only errors
130  // 2 + warnings
131  // 4 + results
132  // 6 + status/phase information
133  // 8 + statistical information
134  // 9 + progress information
135  // 10 + debug info
136 
138  {
141  };
142 
143  static unsigned eval_verbosity(
144  const std::string &user_input,
145  const message_levelt default_verbosity,
146  message_handlert &dest);
147 
148  virtual void set_message_handler(message_handlert &_message_handler)
149  {
150  message_handler=&_message_handler;
151  }
152 
154  {
155  INVARIANT(
156  message_handler!=nullptr,
157  "message handler should be set before calling get_message_handler");
158  return *message_handler;
159  }
160 
161  // constructors, destructor
162 
164  message_handler(nullptr),
165  mstream(M_DEBUG, *this)
166  {
167  }
168 
169  messaget(const messaget &other):
171  mstream(other.mstream, *this)
172  {
173  }
174 
175  messaget &operator=(const messaget &other)
176  {
178  mstream.assign_from(other.mstream);
179  return *this;
180  }
181 
182  explicit messaget(message_handlert &_message_handler):
183  message_handler(&_message_handler),
184  mstream(M_DEBUG, *this)
185  {
186  }
187 
188  virtual ~messaget();
189 
190  class mstreamt:public std::ostringstream
191  {
192  public:
194  unsigned _message_level,
195  messaget &_message):
196  message_level(_message_level),
197  message(_message)
198  {
199  }
200 
201  mstreamt(const mstreamt &other)=delete;
202 
203  mstreamt(const mstreamt &other, messaget &_message):
205  message(_message),
207  {
208  }
209 
210  mstreamt &operator=(const mstreamt &other)=delete;
211 
212  unsigned message_level;
215 
217  {
218  if(this->tellp() > 0)
219  *this << eom; // force end of previous message
221  {
223  }
224  return *this;
225  }
226 
228  {
229  if(this->tellp() > 0)
230  *this << eom; // force end of previous message
232  {
234  }
235  return *this;
236  }
237 
238  template <class T>
239  mstreamt &operator << (const T &x)
240  {
241  static_cast<std::ostream &>(*this) << x;
242  return *this;
243  }
244 
245  // for feeding in manipulator functions such as eom
247  {
248  return func(*this);
249  }
250 
253  {
254  if(this->tellp() > 0)
255  *this << eom; // force end of previous message
257  }
258 
259  private:
260  void assign_from(const mstreamt &other)
261  {
264  // message, the pointer to my enclosing messaget, remains unaltered.
265  }
266 
267  friend class messaget;
268  };
269 
270  // Feeding 'eom' into the stream triggers
271  // the printing of the message
272  static mstreamt &eom(mstreamt &m)
273  {
275  {
277  m.message_level,
278  m.str(),
279  -1,
280  m.source_location);
282  }
283  m.clear(); // clears error bits
284  m.str(std::string()); // clears the string
286  return m;
287  }
288 
289  // in lieu of std::endl
290  static mstreamt &endl(mstreamt &m)
291  {
292  static_cast<std::ostream &>(m) << std::endl;
293  return m;
294  }
295 
296  mstreamt &get_mstream(unsigned message_level) const
297  {
298  mstream.message_level=message_level;
299  return mstream;
300  }
301 
302  mstreamt &error() const
303  {
304  return get_mstream(M_ERROR);
305  }
306 
307  mstreamt &warning() const
308  {
309  return get_mstream(M_WARNING);
310  }
311 
312  mstreamt &result() const
313  {
314  return get_mstream(M_RESULT);
315  }
316 
317  mstreamt &status() const
318  {
319  return get_mstream(M_STATUS);
320  }
321 
323  {
324  return get_mstream(M_STATISTICS);
325  }
326 
328  {
329  return get_mstream(M_PROGRESS);
330  }
331 
332  mstreamt &debug() const
333  {
334  return get_mstream(M_DEBUG);
335  }
336 
337  void conditional_output(
338  mstreamt &mstream,
339  const std::function<void(mstreamt &)> &output_generator) const;
340 
341 protected:
343  mutable mstreamt mstream;
344 };
345 
346 #endif // CPROVER_UTIL_MESSAGE_H
mstreamt & progress() const
Definition: message.h:327
virtual ~messaget()
Definition: message.cpp:68
stream_message_handlert(std::ostream &_out)
Definition: message.h:102
Definition: json.h:23
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest...
Definition: message.cpp:78
mstreamt & operator<<(const xmlt &data)
Definition: message.h:216
unsigned verbosity
Definition: message.h:77
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
virtual void print(unsigned level, const std::string &message)
Definition: message.h:106
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
unsigned get_verbosity() const
Definition: message.h:66
mstreamt & warning() const
Definition: message.h:307
messaget(const messaget &other)
Definition: message.h:169
std::ostream & out
Definition: message.h:120
source_locationt source_location
Definition: message.h:214
messaget & message
Definition: message.h:213
mstreamt & get_mstream(unsigned message_level) const
Definition: message.h:296
messaget()
Definition: message.h:163
virtual void print(unsigned level, const std::string &message, int sequence_number, const source_locationt &location)
Definition: message.h:89
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
messaget & operator=(const messaget &other)
Definition: message.h:175
mstreamt & error() const
Definition: message.h:302
static mstreamt & endl(mstreamt &m)
Definition: message.h:290
Definition: xml.h:18
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
virtual void print(unsigned level, const xmlt &xml)
Definition: message.h:34
message_levelt
Definition: message.h:137
virtual void print(unsigned level, const std::string &message)
Definition: message.h:84
virtual void flush(unsigned level)
Definition: message.h:56
mstreamt & operator=(const mstreamt &other)=delete
virtual void print(unsigned level, const jsont &json)
Definition: message.h:45
messaget(message_handlert &_message_handler)
Definition: message.h:182
message_handlert & get_message_handler()
Definition: message.h:153
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
std::vector< unsigned > message_count
Definition: message.h:78
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to mstream using output_generator if the configured verbosity is at least as high as ...
Definition: message.cpp:113
#define UNREACHABLE
Definition: invariant.h:250
void clear()
Definition: irep.h:241
mstreamt(unsigned _message_level, messaget &_message)
Definition: message.h:193
virtual json_stream_arrayt & get_json_stream()
Return the underlying JSON stream.
Definition: message.h:40
void assign_from(const mstreamt &other)
Definition: message.h:260
void set_verbosity(unsigned _verbosity)
Definition: message.h:65
virtual ~message_handlert()
Definition: message.h:61
virtual void flush(unsigned level)
Definition: message.h:114
mstreamt & debug() const
Definition: message.h:332
json_stream_arrayt & json_stream()
Returns a reference to the top-level JSON array stream.
Definition: message.h:252
mstreamt mstream
Definition: message.h:343
message_handlert * message_handler
Definition: message.h:342
unsigned message_level
Definition: message.h:212
mstreamt(const mstreamt &other, messaget &_message)
Definition: message.h:203
mstreamt & statistics() const
Definition: message.h:322
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83
Definition: kdev_t.h:24
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:59
unsigned get_message_count(unsigned level) const
Definition: message.h:68