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 "deprecate.h"
19 #include "invariant.h"
20 #include "source_location.h"
21 
22 class json_objectt;
23 class jsont;
24 class xmlt;
25 
27 {
28 public:
30  {
31  }
32 
33  virtual void print(unsigned level, const std::string &message)=0;
34 
35  virtual void print(unsigned level, const xmlt &xml) = 0;
36 
37  virtual void print(unsigned level, const jsont &json) = 0;
38 
39  virtual void print(
40  unsigned level,
41  const std::string &message,
42  const source_locationt &location);
43 
44  virtual void flush(unsigned) = 0;
45 
47  {
48  }
49 
50  void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; }
51  unsigned get_verbosity() const { return verbosity; }
52 
53  std::size_t get_message_count(unsigned level) const
54  {
55  if(level>=message_count.size())
56  return 0;
57 
58  return message_count[level];
59  }
60 
63  virtual std::string command(unsigned) const
64  {
65  return std::string();
66  }
67 
68 protected:
69  unsigned verbosity;
70  std::vector<std::size_t> message_count;
71 };
72 
74 {
75 public:
77  {
78  verbosity = 0;
79  }
80 
81  void print(unsigned level, const std::string &message) override
82  {
84  }
85 
86  void print(unsigned, const xmlt &) override
87  {
88  }
89 
90  void print(unsigned, const jsont &) override
91  {
92  }
93 
94  void print(
95  unsigned level,
96  const std::string &message,
97  const source_locationt &) override
98  {
99  print(level, message);
100  }
101 
102  void flush(unsigned) override
103  {
104  }
105 };
106 
108 {
109 public:
110  explicit stream_message_handlert(std::ostream &_out):out(_out)
111  {
112  }
113 
114  void print(unsigned level, const std::string &message) override
115  {
117 
118  if(verbosity>=level)
119  out << message << '\n';
120  }
121 
122  void print(unsigned, const xmlt &) override
123  {
124  }
125 
126  void print(unsigned, const jsont &) override
127  {
128  }
129 
130  void flush(unsigned) override
131  {
132  out << std::flush;
133  }
134 
135 protected:
136  std::ostream &out;
137 };
138 
151 class messaget
152 {
153 public:
154  // Standard message levels:
155  //
156  // 0 none
157  // 1 only errors
158  // 2 + warnings
159  // 4 + results
160  // 6 + status/phase information
161  // 8 + statistical information
162  // 9 + progress information
163  // 10 + debug info
164 
166  {
169  };
170 
171  static unsigned eval_verbosity(
172  const std::string &user_input,
173  const message_levelt default_verbosity,
174  message_handlert &dest);
175 
176  virtual void set_message_handler(message_handlert &_message_handler)
177  {
178  message_handler=&_message_handler;
179  }
180 
182  {
183  INVARIANT(
184  message_handler!=nullptr,
185  "message handler should be set before calling get_message_handler");
186  return *message_handler;
187  }
188 
189  // constructors, destructor
190 
191  DEPRECATED(SINCE(2019, 1, 7, "use messaget(message_handler) instead"))
193  message_handler(nullptr),
194  mstream(M_DEBUG, *this)
195  {
196  }
197 
198  messaget(const messaget &other):
200  mstream(other.mstream, *this)
201  {
202  }
203 
204  messaget &operator=(const messaget &other)
205  {
207  mstream.assign_from(other.mstream);
208  return *this;
209  }
210 
211  explicit messaget(message_handlert &_message_handler):
212  message_handler(&_message_handler),
213  mstream(M_DEBUG, *this)
214  {
215  }
216 
217  virtual ~messaget();
218 
219  // \brief Class that stores an individual 'message' with a verbosity 'level'.
220  class mstreamt:public std::ostringstream
221  {
222  public:
224  unsigned _message_level,
225  messaget &_message):
226  message_level(_message_level),
227  message(_message)
228  {
229  }
230 
231  mstreamt(const mstreamt &other)=delete;
232 
233  mstreamt(const mstreamt &other, messaget &_message):
235  message(_message),
237  {
238  }
239 
240  mstreamt &operator=(const mstreamt &other)=delete;
241 
242  unsigned message_level;
245 
247  {
248  if(this->tellp() > 0)
249  *this << eom; // force end of previous message
251  {
253  }
254  return *this;
255  }
256 
258 
259  template <class T>
260  mstreamt &operator << (const T &x)
261  {
262  static_cast<std::ostream &>(*this) << x;
263  return *this;
264  }
265 
266  private:
267  void assign_from(const mstreamt &other)
268  {
271  // message, the pointer to my enclosing messaget, remains unaltered.
272  }
273 
274  friend class messaget;
275  };
276 
277  // Feeding 'eom' into the stream triggers the printing of the message
278  // This is implemented as an I/O manipulator (compare to STL's endl).
279  class eomt
280  {
281  };
282 
283  static eomt eom;
284 
286  {
288  {
290  m.message_level,
291  m.str(),
292  m.source_location);
294  }
295  m.clear(); // clears error bits
296  m.str(std::string()); // clears the string
298  return m;
299  }
300 
301  // This is an I/O manipulator (compare to STL's set_precision).
302  class commandt
303  {
304  public:
305  explicit commandt(unsigned _command) : command(_command)
306  {
307  }
308 
309  unsigned command;
310  };
311 
313  friend mstreamt &operator<<(mstreamt &m, const commandt &c)
314  {
316  return m << m.message.message_handler->command(c.command);
317  else
318  return m;
319  }
320 
322  static commandt command(unsigned c)
323  {
324  return commandt(c);
325  }
326 
329  static const commandt reset;
330 
332  static const commandt red;
333 
335  static const commandt green;
336 
338  static const commandt yellow;
339 
341  static const commandt blue;
342 
344  static const commandt magenta;
345 
347  static const commandt cyan;
348 
350  static const commandt bright_red;
351 
353  static const commandt bright_green;
354 
356  static const commandt bright_yellow;
357 
359  static const commandt bright_blue;
360 
362  static const commandt bright_magenta;
363 
365  static const commandt bright_cyan;
366 
368  static const commandt bold;
369 
371  static const commandt faint;
372 
374  static const commandt italic;
375 
377  static const commandt underline;
378 
379  mstreamt &get_mstream(unsigned message_level) const
380  {
381  mstream.message_level=message_level;
382  return mstream;
383  }
384 
385  mstreamt &error() const
386  {
387  return get_mstream(M_ERROR);
388  }
389 
390  mstreamt &warning() const
391  {
392  return get_mstream(M_WARNING);
393  }
394 
395  mstreamt &result() const
396  {
397  return get_mstream(M_RESULT);
398  }
399 
400  mstreamt &status() const
401  {
402  return get_mstream(M_STATUS);
403  }
404 
406  {
407  return get_mstream(M_STATISTICS);
408  }
409 
411  {
412  return get_mstream(M_PROGRESS);
413  }
414 
415  mstreamt &debug() const
416  {
417  return get_mstream(M_DEBUG);
418  }
419 
420  void conditional_output(
421  mstreamt &mstream,
422  const std::function<void(mstreamt &)> &output_generator) const;
423 
424 protected:
426  mutable mstreamt mstream;
427 };
428 
429 #endif // CPROVER_UTIL_MESSAGE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
messaget::commandt::command
unsigned command
Definition: message.h:309
messaget::M_RESULT
@ M_RESULT
Definition: message.h:167
message_handlert::command
virtual std::string command(unsigned) const
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition: message.h:63
stream_message_handlert::print
void print(unsigned level, const std::string &message) override
Definition: message.h:114
messaget::operator=
messaget & operator=(const messaget &other)
Definition: message.h:204
irept::clear
void clear()
Definition: irep.h:473
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:329
null_message_handlert::print
void print(unsigned, const xmlt &) override
Definition: message.h:86
message_handlert::print
virtual void print(unsigned level, const xmlt &xml)=0
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:168
messaget::status
mstreamt & status() const
Definition: message.h:400
null_message_handlert::print
void print(unsigned level, const std::string &message) override
Definition: message.h:81
message_handlert::get_verbosity
unsigned get_verbosity() const
Definition: message.h:51
data
Definition: kdev_t.h:24
message_handlert::message_handlert
message_handlert()
Definition: message.h:29
messaget::commandt::commandt
commandt(unsigned _command)
Definition: message.h:305
stream_message_handlert::stream_message_handlert
stream_message_handlert(std::ostream &_out)
Definition: message.h:110
messaget::bright_red
static const commandt bright_red
render text with bright red foreground color
Definition: message.h:350
null_message_handlert::print
void print(unsigned, const jsont &) override
Definition: message.h:90
messaget::eom
static eomt eom
Definition: message.h:283
messaget::italic
static const commandt italic
render italic text
Definition: message.h:374
stream_message_handlert::flush
void flush(unsigned) override
Definition: message.h:130
message_handlert::verbosity
unsigned verbosity
Definition: message.h:69
messaget::mstreamt::operator=
mstreamt & operator=(const mstreamt &other)=delete
stream_message_handlert::out
std::ostream & out
Definition: message.h:136
jsont
Definition: json.h:25
messaget::mstreamt::operator<<
mstreamt & operator<<(const xmlt &data)
Definition: message.h:246
message_handlert::print
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:59
json_objectt
Definition: json.h:298
messaget::mstreamt::mstreamt
mstreamt(const mstreamt &other, messaget &_message)
Definition: message.h:233
messaget::bright_magenta
static const commandt bright_magenta
render text with bright magenta foreground color
Definition: message.h:362
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
messaget::messaget
messaget(message_handlert &_message_handler)
Definition: message.h:211
messaget::bright_yellow
static const commandt bright_yellow
render text with bright yellow foreground color
Definition: message.h:356
messaget::messaget
messaget(const messaget &other)
Definition: message.h:198
messaget::green
static const commandt green
render text with green foreground color
Definition: message.h:335
messaget::result
mstreamt & result() const
Definition: message.h:395
messaget::error
mstreamt & error() const
Definition: message.h:385
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:371
messaget::bold
static const commandt bold
render text with bold font
Definition: message.h:368
messaget::yellow
static const commandt yellow
render text with yellow foreground color
Definition: message.h:338
deprecate.h
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:244
messaget::command
static commandt command(unsigned c)
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition: message.h:322
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
messaget::M_ERROR
@ M_ERROR
Definition: message.h:167
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:176
source_location.h
stream_message_handlert::print
void print(unsigned, const xmlt &) override
Definition: message.h:122
messaget::operator<<
friend mstreamt & operator<<(mstreamt &m, const commandt &c)
feed a command into an mstreamt
Definition: message.h:313
message_handlert
Definition: message.h:27
messaget::mstreamt::assign_from
void assign_from(const mstreamt &other)
Definition: message.h:267
messaget::eomt
Definition: message.h:280
null_message_handlert::flush
void flush(unsigned) override
Definition: message.h:102
stream_message_handlert::print
void print(unsigned, const jsont &) override
Definition: message.h:126
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
xmlt
Definition: xml.h:19
messaget::mstreamt::message
messaget & message
Definition: message.h:243
messaget::mstreamt::mstreamt
mstreamt(unsigned _message_level, messaget &_message)
Definition: message.h:223
source_locationt
Definition: source_location.h:20
null_message_handlert::print
void print(unsigned level, const std::string &message, const source_locationt &) override
Definition: message.h:94
null_message_handlert
Definition: message.h:74
message_handlert::set_verbosity
void set_verbosity(unsigned _verbosity)
Definition: message.h:50
message_handlert::message_count
std::vector< std::size_t > message_count
Definition: message.h:70
message_handlert::print
virtual void print(unsigned level, const jsont &json)=0
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:181
messaget::message_handler
message_handlert * message_handler
Definition: message.h:425
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
messaget::M_WARNING
@ M_WARNING
Definition: message.h:167
messaget::red
static const commandt red
render text with red foreground color
Definition: message.h:332
null_message_handlert::null_message_handlert
null_message_handlert()
Definition: message.h:76
messaget::message_levelt
message_levelt
Definition: message.h:166
invariant.h
messaget::conditional_output
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:133
messaget::get_mstream
mstreamt & get_mstream(unsigned message_level) const
Definition: message.h:379
messaget::M_PROGRESS
@ M_PROGRESS
Definition: message.h:168
messaget::M_STATUS
@ M_STATUS
Definition: message.h:167
messaget::~messaget
virtual ~messaget()
Definition: message.cpp:68
message_handlert::flush
virtual void flush(unsigned)=0
messaget::underline
static const commandt underline
render underlined text
Definition: message.h:377
messaget::mstreamt
Definition: message.h:221
messaget::mstreamt::mstreamt
mstreamt(const mstreamt &other)=delete
messaget::cyan
static const commandt cyan
render text with cyan foreground color
Definition: message.h:347
messaget::debug
mstreamt & debug() const
Definition: message.h:415
messaget::M_DEBUG
@ M_DEBUG
Definition: message.h:168
messaget::progress
mstreamt & progress() const
Definition: message.h:410
messaget::mstream
mstreamt mstream
Definition: message.h:426
messaget::bright_green
static const commandt bright_green
render text with bright green foreground color
Definition: message.h:353
messaget::eval_verbosity
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:99
messaget::operator<<
friend mstreamt & operator<<(mstreamt &m, eomt)
Definition: message.h:285
message_handlert::~message_handlert
virtual ~message_handlert()
Definition: message.h:46
messaget::warning
mstreamt & warning() const
Definition: message.h:390
messaget::mstreamt::message_level
unsigned message_level
Definition: message.h:242
messaget::magenta
static const commandt magenta
render text with magenta foreground color
Definition: message.h:344
messaget::bright_cyan
static const commandt bright_cyan
render text with bright cyan foreground color
Definition: message.h:365
messaget::bright_blue
static const commandt bright_blue
render text with bright blue foreground color
Definition: message.h:359
messaget::commandt
Definition: message.h:303
messaget::blue
static const commandt blue
render text with blue foreground color
Definition: message.h:341
validation_modet::INVARIANT
@ INVARIANT
message_handlert::get_message_count
std::size_t get_message_count(unsigned level) const
Definition: message.h:53
messaget::statistics
mstreamt & statistics() const
Definition: message.h:405
stream_message_handlert
Definition: message.h:108