CBMC
ui_message.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "ui_message.h"
10 
11 #include "cmdline.h"
12 #include "cout_message.h"
13 #include "json.h"
14 #include "json_irep.h"
15 #include "json_stream.h"
16 #include "structured_data.h"
17 #include "xml.h"
18 #include "xml_irep.h"
19 
20 #include <fstream> // IWYU pragma: keep
21 #include <iostream>
22 
24  message_handlert *_message_handler,
25  uit __ui,
26  const std::string &program,
27  bool always_flush,
28  timestampert::clockt clock_type)
29  : message_handler(_message_handler),
30  _ui(__ui),
31  always_flush(always_flush),
32  time(timestampert::make(clock_type)),
33  out(std::cout),
34  json_stream(nullptr)
35 {
36  switch(_ui)
37  {
38  case uit::PLAIN:
39  break;
40 
41  case uit::XML_UI:
42  out << "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
43  << "\n";
44  out << "<cprover>"
45  << "\n";
46 
47  {
48  xmlt program_xml;
49  program_xml.name="program";
50  program_xml.data=program;
51 
52  out << program_xml;
53  }
54  break;
55 
56  case uit::JSON_UI:
57  {
58  json_stream =
59  std::unique_ptr<json_stream_arrayt>(new json_stream_arrayt(out));
60  json_stream->push_back().make_object()["program"] = json_stringt(program);
61  }
62  break;
63  }
64 }
65 
67  const class cmdlinet &cmdline,
68  const std::string &program)
70  nullptr,
71  cmdline.isset("xml-ui") || cmdline.isset("xml-interface")
72  ? uit::XML_UI
73  : cmdline.isset("json-ui") || cmdline.isset("json-interface")
74  ? uit::JSON_UI
75  : uit::PLAIN,
76  program,
77  cmdline.isset("flush"),
78  cmdline.isset("timestamp") ? cmdline.get_value("timestamp") == "monotonic"
79  ? timestampert::clockt::MONOTONIC
80  : cmdline.get_value("timestamp") == "wall"
81  ? timestampert::clockt::WALL_CLOCK
82  : timestampert::clockt::NONE
83  : timestampert::clockt::NONE)
84 {
85  if(get_ui() == uit::PLAIN)
86  {
88  std::make_unique<console_message_handlert>(always_flush);
90  }
91 }
92 
95  &message_handler, uit::PLAIN, "", false, timestampert::clockt::NONE)
96 {
97 }
98 
100 {
101  switch(get_ui())
102  {
103  case uit::XML_UI:
104 
105  out << "</cprover>"
106  << "\n";
107  break;
108 
109  case uit::JSON_UI:
110  INVARIANT(json_stream, "JSON stream must be initialized before use");
111  json_stream->close();
112  out << '\n';
113  break;
114 
115  case uit::PLAIN:
116  break;
117  }
118 }
119 
120 const char *ui_message_handlert::level_string(unsigned level)
121 {
122  if(level==1)
123  return "ERROR";
124  else if(level==2)
125  return "WARNING";
126  else
127  return "STATUS-MESSAGE";
128 }
129 
131  unsigned level,
132  const std::string &message)
133 {
134  if(verbosity>=level)
135  {
136  switch(get_ui())
137  {
138  case uit::PLAIN:
139  {
140  std::stringstream ss;
141  const std::string timestamp = time->stamp();
142  ss << timestamp << (timestamp.empty() ? "" : " ") << message;
143  message_handler->print(level, ss.str());
144  if(always_flush)
145  message_handler->flush(level);
146  }
147  break;
148 
149  case uit::XML_UI:
150  case uit::JSON_UI:
151  {
152  source_locationt location;
153  location.make_nil();
154  print(level, message, location);
155  if(always_flush)
156  flush(level);
157  }
158  break;
159  }
160  }
161 }
162 
164  unsigned level,
165  const xmlt &data)
166 {
167  if(verbosity>=level)
168  {
169  switch(get_ui())
170  {
171  case uit::PLAIN:
172  INVARIANT(false, "Cannot print xml data on PLAIN UI");
173  break;
174  case uit::XML_UI:
175  out << data << '\n';
176  flush(level);
177  break;
178  case uit::JSON_UI:
179  INVARIANT(false, "Cannot print xml data on JSON UI");
180  break;
181  }
182  }
183 }
184 
186  unsigned level,
187  const jsont &data)
188 {
189  if(verbosity>=level)
190  {
191  switch(get_ui())
192  {
193  case uit::PLAIN:
194  INVARIANT(false, "Cannot print json data on PLAIN UI");
195  break;
196  case uit::XML_UI:
197  INVARIANT(false, "Cannot print json data on XML UI");
198  break;
199  case uit::JSON_UI:
200  INVARIANT(json_stream, "JSON stream must be initialized before use");
201  json_stream->push_back(data);
202  flush(level);
203  break;
204  }
205  }
206 }
207 
209  unsigned level,
210  const std::string &message,
211  const source_locationt &location)
212 {
213  message_handlert::print(level, message);
214 
215  if(verbosity>=level)
216  {
217  switch(get_ui())
218  {
219  case uit::PLAIN:
221  level, message, location);
222  break;
223 
224  case uit::XML_UI:
225  case uit::JSON_UI:
226  {
227  std::string tmp_message(message);
228 
229  if(!tmp_message.empty() && *tmp_message.rbegin()=='\n')
230  tmp_message.resize(tmp_message.size()-1);
231 
232  const char *type=level_string(level);
233 
234  ui_msg(type, tmp_message, location);
235  }
236  break;
237  }
238  }
239 }
240 
242  const std::string &type,
243  const std::string &msg,
244  const source_locationt &location)
245 {
246  switch(get_ui())
247  {
248  case uit::PLAIN:
249  break;
250 
251  case uit::XML_UI:
252  xml_ui_msg(type, msg, location);
253  break;
254 
255  case uit::JSON_UI:
256  json_ui_msg(type, msg, location);
257  break;
258  }
259 }
260 
262  const std::string &type,
263  const std::string &msg1,
264  const source_locationt &location)
265 {
266  xmlt result;
267  result.name="message";
268 
269  if(location.is_not_nil() &&
270  !location.get_file().empty())
271  result.new_element(xml(location));
272 
273  result.new_element("text").data=msg1;
274  result.set_attribute("type", type);
275  const std::string timestamp = time->stamp();
276  if(!timestamp.empty())
277  result.set_attribute("timestamp", timestamp);
278 
279  out << result;
280  out << '\n';
281 }
282 
284  const std::string &type,
285  const std::string &msg1,
286  const source_locationt &location)
287 {
288  INVARIANT(json_stream, "JSON stream must be initialized before use");
289  json_objectt &result = json_stream->push_back().make_object();
290 
291  if(location.is_not_nil() &&
292  !location.get_file().empty())
293  result["sourceLocation"] = json(location);
294 
295  result["messageType"] = json_stringt(type);
296  result["messageText"] = json_stringt(msg1);
297  const std::string timestamp = time->stamp();
298  if(!timestamp.empty())
299  result["timestamp"] = json_stringt(timestamp);
300 }
301 
302 void ui_message_handlert::flush(unsigned level)
303 {
304  switch(get_ui())
305  {
306  case uit::PLAIN:
307  message_handler->flush(level);
308  break;
309 
310  case uit::XML_UI:
311  case uit::JSON_UI:
312  out << std::flush;
313  break;
314  }
315 }
316 void ui_message_handlert::print(unsigned level, const structured_datat &data)
317 {
318  switch(get_ui())
319  {
320  case uit::PLAIN:
321  print(level, to_pretty(data));
322  break;
323  case uit::XML_UI:
324  print(level, to_xml(data));
325  break;
326  case uit::JSON_UI:
327  print(level, to_json(data));
328  break;
329  }
330 }
bool empty() const
Definition: dstring.h:89
bool is_not_nil() const
Definition: irep.h:368
void make_nil()
Definition: irep.h:442
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
Definition: json.h:27
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:60
unsigned verbosity
Definition: message.h:72
virtual void flush(unsigned)=0
const irep_idt & get_file() const
A way of representing nested key/value data.
Timestamp class hierarchy.
Definition: timestamper.h:42
clockt
Derived types of timestampert.
Definition: timestamper.h:46
void print(unsigned level, const structured_datat &data) override
Definition: ui_message.cpp:316
virtual void json_ui_msg(const std::string &type, const std::string &msg, const source_locationt &location)
Definition: ui_message.cpp:283
const char * level_string(unsigned level)
Definition: ui_message.cpp:120
virtual uit get_ui() const
Definition: ui_message.h:33
std::ostream & out
Definition: ui_message.h:53
const bool always_flush
Definition: ui_message.h:51
message_handlert * message_handler
Definition: ui_message.h:49
std::unique_ptr< const timestampert > time
Definition: ui_message.h:52
virtual void flush(unsigned level) override
Definition: ui_message.cpp:302
virtual void xml_ui_msg(const std::string &type, const std::string &msg, const source_locationt &location)
Definition: ui_message.cpp:261
std::unique_ptr< json_stream_arrayt > json_stream
Definition: ui_message.h:54
virtual ~ui_message_handlert()
Definition: ui_message.cpp:99
ui_message_handlert(const class cmdlinet &, const std::string &program)
Definition: ui_message.cpp:66
virtual void ui_msg(const std::string &type, const std::string &msg, const source_locationt &location)
Definition: ui_message.cpp:241
std::unique_ptr< console_message_handlert > console_message_handler
Definition: ui_message.h:48
Definition: xml.h:21
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
xmlt & new_element(const std::string &key)
Definition: xml.h:95
std::string data
Definition: xml.h:39
std::string name
Definition: xml.h:39
@ NONE
Do not apply loop contracts.
jsont to_json(const structured_datat &data)
Convert the structured_datat into an json object.
Definition: json.cpp:225
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110
std::string to_pretty(const structured_datat &data)
Convert the structured_data into plain text.
time_t time(time_t *tloc)
Definition: time.c:12
xmlt to_xml(const structured_datat &data)
Convert the structured_datat into an xml object.
Definition: xml.cpp:303