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_irep.h"
17 #include "json_stream.h"
18 #include "make_unique.h"
19 #include "xml.h"
20 #include "xml_irep.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") || cmdline.isset("xml-interface")
71  ? uit::XML_UI
72  : cmdline.isset("json-ui") || cmdline.isset("json-interface")
73  ? uit::JSON_UI
74  : uit::PLAIN,
75  program,
76  cmdline.isset("flush"),
77  cmdline.isset("timestamp") ? cmdline.get_value("timestamp") == "monotonic"
78  ? timestampert::clockt::MONOTONIC
79  : cmdline.get_value("timestamp") == "wall"
80  ? timestampert::clockt::WALL_CLOCK
81  : timestampert::clockt::NONE
82  : timestampert::clockt::NONE)
83 {
84  if(get_ui() == uit::PLAIN)
85  {
87  util_make_unique<console_message_handlert>(always_flush);
89  }
90 }
91 
94  &message_handler, uit::PLAIN, "", false, timestampert::clockt::NONE)
95 {
96 }
97 
99 {
100  switch(get_ui())
101  {
102  case uit::XML_UI:
103 
104  out << "</cprover>"
105  << "\n";
106  break;
107 
108  case uit::JSON_UI:
109  INVARIANT(json_stream, "JSON stream must be initialized before use");
110  json_stream->close();
111  out << '\n';
112  break;
113 
114  case uit::PLAIN:
115  break;
116  }
117 }
118 
119 const char *ui_message_handlert::level_string(unsigned level)
120 {
121  if(level==1)
122  return "ERROR";
123  else if(level==2)
124  return "WARNING";
125  else
126  return "STATUS-MESSAGE";
127 }
128 
130  unsigned level,
131  const std::string &message)
132 {
133  if(verbosity>=level)
134  {
135  switch(get_ui())
136  {
137  case uit::PLAIN:
138  {
139  std::stringstream ss;
140  const std::string timestamp = time->stamp();
141  ss << timestamp << (timestamp.empty() ? "" : " ") << message;
142  message_handler->print(level, ss.str());
143  if(always_flush)
144  message_handler->flush(level);
145  }
146  break;
147 
148  case uit::XML_UI:
149  case uit::JSON_UI:
150  {
151  source_locationt location;
152  location.make_nil();
153  print(level, message, location);
154  if(always_flush)
155  flush(level);
156  }
157  break;
158  }
159  }
160 }
161 
163  unsigned level,
164  const xmlt &data)
165 {
166  if(verbosity>=level)
167  {
168  switch(get_ui())
169  {
170  case uit::PLAIN:
171  INVARIANT(false, "Cannot print xml data on PLAIN UI");
172  break;
173  case uit::XML_UI:
174  out << data << '\n';
175  flush(level);
176  break;
177  case uit::JSON_UI:
178  INVARIANT(false, "Cannot print xml data on JSON UI");
179  break;
180  }
181  }
182 }
183 
185  unsigned level,
186  const jsont &data)
187 {
188  if(verbosity>=level)
189  {
190  switch(get_ui())
191  {
192  case uit::PLAIN:
193  INVARIANT(false, "Cannot print json data on PLAIN UI");
194  break;
195  case uit::XML_UI:
196  INVARIANT(false, "Cannot print json data on XML UI");
197  break;
198  case uit::JSON_UI:
199  INVARIANT(json_stream, "JSON stream must be initialized before use");
200  json_stream->push_back(data);
201  flush(level);
202  break;
203  }
204  }
205 }
206 
208  unsigned level,
209  const std::string &message,
210  const source_locationt &location)
211 {
213 
214  if(verbosity>=level)
215  {
216  switch(get_ui())
217  {
218  case uit::PLAIN:
220  level, message, location);
221  break;
222 
223  case uit::XML_UI:
224  case uit::JSON_UI:
225  {
226  std::string tmp_message(message);
227 
228  if(!tmp_message.empty() && *tmp_message.rbegin()=='\n')
229  tmp_message.resize(tmp_message.size()-1);
230 
231  const char *type=level_string(level);
232 
233  ui_msg(type, tmp_message, location);
234  }
235  break;
236  }
237  }
238 }
239 
241  const std::string &type,
242  const std::string &msg,
243  const source_locationt &location)
244 {
245  switch(get_ui())
246  {
247  case uit::PLAIN:
248  break;
249 
250  case uit::XML_UI:
251  xml_ui_msg(type, msg, location);
252  break;
253 
254  case uit::JSON_UI:
255  json_ui_msg(type, msg, location);
256  break;
257  }
258 }
259 
261  const std::string &type,
262  const std::string &msg1,
263  const source_locationt &location)
264 {
265  xmlt result;
266  result.name="message";
267 
268  if(location.is_not_nil() &&
269  !location.get_file().empty())
270  result.new_element(xml(location));
271 
272  result.new_element("text").data=msg1;
273  result.set_attribute("type", type);
274  const std::string timestamp = time->stamp();
275  if(!timestamp.empty())
276  result.set_attribute("timestamp", timestamp);
277 
278  out << result;
279  out << '\n';
280 }
281 
283  const std::string &type,
284  const std::string &msg1,
285  const source_locationt &location)
286 {
287  INVARIANT(json_stream, "JSON stream must be initialized before use");
288  json_objectt &result = json_stream->push_back().make_object();
289 
290  if(location.is_not_nil() &&
291  !location.get_file().empty())
292  result["sourceLocation"] = json(location);
293 
294  result["messageType"] = json_stringt(type);
295  result["messageText"] = json_stringt(msg1);
296  const std::string timestamp = time->stamp();
297  if(!timestamp.empty())
298  result["timestamp"] = json_stringt(timestamp);
299 }
300 
301 void ui_message_handlert::flush(unsigned level)
302 {
303  switch(get_ui())
304  {
305  case uit::PLAIN:
306  message_handler->flush(level);
307  break;
308 
309  case uit::XML_UI:
310  case uit::JSON_UI:
311  out << std::flush;
312  break;
313  }
314 }
316 {
317  switch(get_ui())
318  {
319  case uit::PLAIN:
320  print(level, to_pretty(data));
321  break;
322  case uit::XML_UI:
323  print(level, to_xml(data));
324  break;
325  case uit::JSON_UI:
326  print(level, to_json(data));
327  break;
328  }
329 }
to_pretty
std::string to_pretty(const structured_datat &data)
Convert the structured_data into plain text.
Definition: structured_data.cpp:149
complexity_violationt::NONE
@ NONE
ui_message_handlert
Definition: ui_message.h:20
ui_message_handlert::always_flush
const bool always_flush
Definition: ui_message.h:49
to_json
jsont to_json(const structured_datat &data)
Convert the structured_datat into an json object.
Definition: json.cpp:225
ui_message_handlert::uit::XML_UI
@ XML_UI
ui_message_handlert::_ui
uit _ui
Definition: ui_message.h:48
ui_message_handlert::ui_msg
virtual void ui_msg(const std::string &type, const std::string &msg, const source_locationt &location)
Definition: ui_message.cpp:240
irept::make_nil
void make_nil()
Definition: irep.h:475
timestampert::clockt
clockt
Derived types of timestampert.
Definition: timestamper.h:46
json_stream.h
data
Definition: kdev_t.h:24
ui_message_handlert::~ui_message_handlert
virtual ~ui_message_handlert()
Definition: ui_message.cpp:98
xml_irep.h
message_handlert::verbosity
unsigned verbosity
Definition: message.h:72
to_xml
xmlt to_xml(const structured_datat &data)
Convert the structured_datat into an xml object.
Definition: xml.cpp:280
jsont
Definition: json.h:27
xml.h
json_irep.h
Util.
message_handlert::print
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:59
json_objectt
Definition: json.h:300
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
ui_message_handlert::uit
uit
Definition: ui_message.h:22
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
cmdlinet
Definition: cmdline.h:21
ui_message_handlert::json_stream
std::unique_ptr< json_stream_arrayt > json_stream
Definition: ui_message.h:52
make_unique.h
ui_message_handlert::json_ui_msg
virtual void json_ui_msg(const std::string &type, const std::string &msg, const source_locationt &location)
Definition: ui_message.cpp:282
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
ui_message_handlert::time
std::unique_ptr< const timestampert > time
Definition: ui_message.h:50
ui_message_handlert::uit::JSON_UI
@ JSON_UI
xmlt::name
std::string name
Definition: xml.h:39
ui_message_handlert::out
std::ostream & out
Definition: ui_message.h:51
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
message_handlert
Definition: message.h:28
dstringt::empty
bool empty() const
Definition: dstring.h:88
xmlt
Definition: xml.h:21
structured_datat
A way of representing nested key/value data.
Definition: structured_data.h:74
ui_message_handlert::console_message_handler
std::unique_ptr< console_message_handlert > console_message_handler
Definition: ui_message.h:46
source_locationt
Definition: source_location.h:20
ui_message_handlert::uit::PLAIN
@ PLAIN
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
cmdline.h
ui_message_handlert::level_string
const char * level_string(unsigned level)
Definition: ui_message.cpp:119
json.h
ui_message_handlert::xml_ui_msg
virtual void xml_ui_msg(const std::string &type, const std::string &msg, const source_locationt &location)
Definition: ui_message.cpp:260
ui_message_handlert::flush
virtual void flush(unsigned level) override
Definition: ui_message.cpp:301
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
message_handlert::flush
virtual void flush(unsigned)=0
ui_message_handlert::ui_message_handlert
ui_message_handlert(const class cmdlinet &, const std::string &program)
Definition: ui_message.cpp:65
timestampert
Timestamp class hierarchy.
Definition: timestamper.h:42
xmlt::data
std::string data
Definition: xml.h:39
ui_message_handlert::print
void print(unsigned level, const structured_datat &data) override
Definition: ui_message.cpp:315
ui_message_handlert::message_handler
message_handlert * message_handler
Definition: ui_message.h:47
validation_modet::INVARIANT
@ INVARIANT
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
json_stringt
Definition: json.h:270
ui_message.h