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 
22 class xmlt;
23 
25 {
26 public:
28  {
29  }
30 
31  virtual void print(unsigned level, const std::string &message)=0;
32 
33  virtual void print(unsigned level, const xmlt &xml) = 0;
34 
35  virtual void print(unsigned level, const jsont &json) = 0;
36 
37  virtual void print(
38  unsigned level,
39  const std::string &message,
40  const source_locationt &location);
41 
42  virtual void flush(unsigned) = 0;
43 
45  {
46  }
47 
48  void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; }
49  unsigned get_verbosity() const { return verbosity; }
50 
51  std::size_t get_message_count(unsigned level) const
52  {
53  if(level>=message_count.size())
54  return 0;
55 
56  return message_count[level];
57  }
58 
61  virtual std::string command(unsigned) const
62  {
63  return std::string();
64  }
65 
66 protected:
67  unsigned verbosity;
68  std::vector<std::size_t> message_count;
69 };
70 
72 {
73 public:
74  void print(unsigned level, const std::string &message) override
75  {
76  message_handlert::print(level, message);
77  }
78 
79  void print(unsigned, const xmlt &) override
80  {
81  }
82 
83  void print(unsigned, const jsont &) override
84  {
85  }
86 
87  void print(
88  unsigned level,
89  const std::string &message,
90  const source_locationt &) override
91  {
92  print(level, message);
93  }
94 
95  void flush(unsigned) override
96  {
97  }
98 };
99 
101 {
102 public:
103  explicit stream_message_handlert(std::ostream &_out):out(_out)
104  {
105  }
106 
107  void print(unsigned level, const std::string &message) override
108  {
109  message_handlert::print(level, message);
110 
111  if(verbosity>=level)
112  out << message << '\n';
113  }
114 
115  void print(unsigned, const xmlt &) override
116  {
117  }
118 
119  void print(unsigned, const jsont &) override
120  {
121  }
122 
123  void flush(unsigned) override
124  {
125  out << std::flush;
126  }
127 
128 protected:
129  std::ostream &out;
130 };
131 
140 // new instance of `mstreamt` set with the appropriate level.
144 class messaget
145 {
146 public:
147  // Standard message levels:
148  //
149  // 0 none
150  // 1 only errors
151  // 2 + warnings
152  // 4 + results
153  // 6 + status/phase information
154  // 8 + statistical information
155  // 9 + progress information
156  // 10 + debug info
157 
159  {
162  };
163 
164  static unsigned eval_verbosity(
165  const std::string &user_input,
166  const message_levelt default_verbosity,
167  message_handlert &dest);
168 
169  virtual void set_message_handler(message_handlert &_message_handler)
170  {
171  message_handler=&_message_handler;
172  }
173 
175  {
176  INVARIANT(
177  message_handler!=nullptr,
178  "message handler should be set before calling get_message_handler");
179  return *message_handler;
180  }
181 
182  // constructors, destructor
183 
185  message_handler(nullptr),
186  mstream(M_DEBUG, *this)
187  {
188  }
189 
190  messaget(const messaget &other):
192  mstream(other.mstream, *this)
193  {
194  }
195 
196  messaget &operator=(const messaget &other)
197  {
199  mstream.assign_from(other.mstream);
200  return *this;
201  }
202 
203  explicit messaget(message_handlert &_message_handler):
204  message_handler(&_message_handler),
205  mstream(M_DEBUG, *this)
206  {
207  }
208 
209  virtual ~messaget();
210 
211  // \brief Class that stores an individual 'message' with a verbosity 'level'.
212  class mstreamt:public std::ostringstream
213  {
214  public:
216  unsigned _message_level,
217  messaget &_message):
218  message_level(_message_level),
219  message(_message)
220  {
221  }
222 
223  mstreamt(const mstreamt &other)=delete;
224 
225  mstreamt(const mstreamt &other, messaget &_message):
227  message(_message),
229  {
230  }
231 
232  mstreamt &operator=(const mstreamt &other)=delete;
233 
234  unsigned message_level;
237 
239  {
240  if(this->tellp() > 0)
241  *this << eom; // force end of previous message
243  {
245  }
246  return *this;
247  }
248 
250  {
251  if(this->tellp() > 0)
252  *this << eom; // force end of previous message
254  {
256  }
257  return *this;
258  }
259 
260  template <class T>
261  mstreamt &operator << (const T &x)
262  {
263  static_cast<std::ostream &>(*this) << x;
264  return *this;
265  }
266 
267  private:
268  void assign_from(const mstreamt &other)
269  {
272  // message, the pointer to my enclosing messaget, remains unaltered.
273  }
274 
275  friend class messaget;
276  };
277 
278  // Feeding 'eom' into the stream triggers the printing of the message
279  // This is implemented as an I/O manipulator (compare to STL's endl).
280  class eomt
281  {
282  };
283 
284  static eomt eom;
285 
287  {
289  {
291  m.message_level,
292  m.str(),
293  m.source_location);
295  }
296  m.clear(); // clears error bits
297  m.str(std::string()); // clears the string
299  return m;
300  }
301 
302  // This is an I/O manipulator (compare to STL's set_precision).
303  class commandt
304  {
305  public:
306  explicit commandt(unsigned _command) : command(_command)
307  {
308  }
309 
310  unsigned command;
311  };
312 
314  friend mstreamt &operator<<(mstreamt &m, const commandt &c)
315  {
317  return m << m.message.message_handler->command(c.command);
318  else
319  return m;
320  }
321 
323  static commandt command(unsigned c)
324  {
325  return commandt(c);
326  }
327 
330  static const commandt reset;
331 
333  static const commandt red;
334 
336  static const commandt green;
337 
339  static const commandt yellow;
340 
342  static const commandt blue;
343 
345  static const commandt magenta;
346 
348  static const commandt cyan;
349 
351  static const commandt bright_red;
352 
354  static const commandt bright_green;
355 
357  static const commandt bright_yellow;
358 
360  static const commandt bright_blue;
361 
363  static const commandt bright_magenta;
364 
366  static const commandt bright_cyan;
367 
369  static const commandt bold;
370 
372  static const commandt faint;
373 
375  static const commandt italic;
376 
378  static const commandt underline;
379 
380  mstreamt &get_mstream(unsigned message_level) const
381  {
382  mstream.message_level=message_level;
383  return mstream;
384  }
385 
386  mstreamt &error() const
387  {
388  return get_mstream(M_ERROR);
389  }
390 
391  mstreamt &warning() const
392  {
393  return get_mstream(M_WARNING);
394  }
395 
396  mstreamt &result() const
397  {
398  return get_mstream(M_RESULT);
399  }
400 
401  mstreamt &status() const
402  {
403  return get_mstream(M_STATUS);
404  }
405 
407  {
408  return get_mstream(M_STATISTICS);
409  }
410 
412  {
413  return get_mstream(M_PROGRESS);
414  }
415 
416  mstreamt &debug() const
417  {
418  return get_mstream(M_DEBUG);
419  }
420 
421  void conditional_output(
422  mstreamt &mstream,
423  const std::function<void(mstreamt &)> &output_generator) const;
424 
425 protected:
427  mutable mstreamt mstream;
428 };
429 
430 #endif // CPROVER_UTIL_MESSAGE_H
static const commandt bright_magenta
render text with bright magenta foreground color
Definition: message.h:363
static const commandt bright_yellow
render text with bright yellow foreground color
Definition: message.h:357
void print(unsigned, const xmlt &) override
Definition: message.h:79
void print(unsigned, const xmlt &) override
Definition: message.h:115
static const commandt bold
render text with bold font
Definition: message.h:369
mstreamt & progress() const
Definition: message.h:411
void flush(unsigned) override
Definition: message.h:123
void print(unsigned level, const std::string &message) override
Definition: message.h:107
virtual ~messaget()
Definition: message.cpp:67
static const commandt blue
render text with blue foreground color
Definition: message.h:342
stream_message_handlert(std::ostream &_out)
Definition: message.h:103
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:98
static const commandt bright_red
render text with bright red foreground color
Definition: message.h:351
mstreamt & operator<<(const xmlt &data)
Definition: message.h:238
static const commandt bright_blue
render text with bright blue foreground color
Definition: message.h:360
friend mstreamt & operator<<(mstreamt &m, eomt)
Definition: message.h:286
unsigned verbosity
Definition: message.h:67
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
unsigned get_verbosity() const
Definition: message.h:49
mstreamt & warning() const
Definition: message.h:391
messaget(const messaget &other)
Definition: message.h:190
static const commandt underline
render underlined text
Definition: message.h:378
static const commandt magenta
render text with magenta foreground color
Definition: message.h:345
virtual std::string command(unsigned) const
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition: message.h:61
void print(unsigned, const jsont &) override
Definition: message.h:83
std::ostream & out
Definition: message.h:129
friend mstreamt & operator<<(mstreamt &m, const commandt &c)
feed a command into an mstreamt
Definition: message.h:314
source_locationt source_location
Definition: message.h:236
messaget & message
Definition: message.h:235
mstreamt & get_mstream(unsigned message_level) const
Definition: message.h:380
messaget()
Definition: message.h:184
messaget & operator=(const messaget &other)
Definition: message.h:196
static const commandt red
render text with red foreground color
Definition: message.h:333
mstreamt & error() const
Definition: message.h:386
Definition: xml.h:18
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
void print(unsigned, const jsont &) override
Definition: message.h:119
message_levelt
Definition: message.h:158
static const commandt bright_cyan
render text with bright cyan foreground color
Definition: message.h:366
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
static const commandt bright_green
render text with bright green foreground color
Definition: message.h:354
mstreamt & operator=(const mstreamt &other)=delete
void print(unsigned level, const std::string &message, const source_locationt &) override
Definition: message.h:87
static const commandt faint
render text with faint font
Definition: message.h:372
static eomt eom
Definition: message.h:284
commandt(unsigned _command)
Definition: message.h:306
messaget(message_handlert &_message_handler)
Definition: message.h:203
message_handlert & get_message_handler()
Definition: message.h:174
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
unsigned command
Definition: message.h:310
void flush(unsigned) override
Definition: message.h:95
std::vector< std::size_t > message_count
Definition: message.h:68
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:132
std::size_t get_message_count(unsigned level) const
Definition: message.h:51
void clear()
Definition: irep.h:313
mstreamt(unsigned _message_level, messaget &_message)
Definition: message.h:215
static commandt command(unsigned c)
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition: message.h:323
void assign_from(const mstreamt &other)
Definition: message.h:268
void set_verbosity(unsigned _verbosity)
Definition: message.h:48
virtual ~message_handlert()
Definition: message.h:44
mstreamt & debug() const
Definition: message.h:416
static const commandt green
render text with green foreground color
Definition: message.h:336
mstreamt mstream
Definition: message.h:427
static const commandt cyan
render text with cyan foreground color
Definition: message.h:348
message_handlert * message_handler
Definition: message.h:426
virtual void flush(unsigned)=0
unsigned message_level
Definition: message.h:234
static const commandt yellow
render text with yellow foreground color
Definition: message.h:339
mstreamt(const mstreamt &other, messaget &_message)
Definition: message.h:225
mstreamt & statistics() const
Definition: message.h:406
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
static const commandt italic
render italic text
Definition: message.h:375
Definition: kdev_t.h:24
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:58
void print(unsigned level, const std::string &message) override
Definition: message.h:74