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