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