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 "xml.h"
15 #include "json.h"
16 #include "xml_expr.h"
17 #include "json_expr.h"
18 #include "json_stream.h"
19 #include "cout_message.h"
20 #include "cmdline.h"
21 
23  : _ui(uit::PLAIN),
24  always_flush(false),
25  time(timestampert::make(timestampert::clockt::NONE)),
26  out(std::cout),
27  json_stream(nullptr)
28 {
29 }
30 
32  uit __ui,
33  const std::string &program,
34  bool always_flush,
35  timestampert::clockt clock_type)
36  : _ui(__ui),
37  always_flush(always_flush),
38  time(timestampert::make(clock_type)),
39  out(std::cout),
40  json_stream(nullptr)
41 {
42  switch(_ui)
43  {
44  case uit::PLAIN:
45  break;
46 
47  case uit::XML_UI:
48  out << "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
49  << "\n";
50  out << "<cprover>"
51  << "\n";
52 
53  {
54  xmlt program_xml;
55  program_xml.name="program";
56  program_xml.data=program;
57 
58  out << program_xml;
59  }
60  break;
61 
62  case uit::JSON_UI:
63  {
64  if(!json_stream)
65  {
66  json_stream =
67  std::unique_ptr<json_stream_arrayt>(new json_stream_arrayt(out));
68  }
69 
70  INVARIANT(json_stream, "JSON stream must be initialized before use");
71  json_stream->push_back().make_object()["program"] = json_stringt(program);
72  }
73  break;
74  }
75 }
76 
78  const class cmdlinet &cmdline,
79  const std::string &program)
81  cmdline.isset("xml-ui") ? uit::XML_UI : cmdline.isset("json-ui")
82  ? uit::JSON_UI
83  : uit::PLAIN,
84  program,
85  cmdline.isset("flush"),
86  cmdline.isset("timestamp")
87  ? cmdline.get_value("timestamp") == "monotonic"
88  ? timestampert::clockt::MONOTONIC
89  : cmdline.get_value("timestamp") == "wall"
90  ? timestampert::clockt::WALL_CLOCK
91  : timestampert::clockt::NONE
92  : 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  console_message_handlert console_message_handler(always_flush);
138  std::stringstream ss;
139  const std::string timestamp = time->stamp();
140  ss << timestamp << (timestamp.empty() ? "" : " ") << message;
141  console_message_handler.print(level, ss.str());
142  if(always_flush)
143  console_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, -1, 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  int sequence_number,
210  const source_locationt &location)
211 {
212  message_handlert::print(level, message);
213 
214  if(verbosity>=level)
215  {
216  switch(get_ui())
217  {
218  case uit::PLAIN:
220  level, message, sequence_number, 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  std::string sequence_number_str=
234  sequence_number>=0?std::to_string(sequence_number):"";
235 
236  ui_msg(type, tmp_message, sequence_number_str, location);
237  }
238  break;
239  }
240  }
241 }
242 
244  const std::string &type,
245  const std::string &msg1,
246  const std::string &msg2,
247  const source_locationt &location)
248 {
249  switch(get_ui())
250  {
251  case uit::PLAIN:
252  break;
253 
254  case uit::XML_UI:
255  xml_ui_msg(type, msg1, msg2, location);
256  break;
257 
258  case uit::JSON_UI:
259  json_ui_msg(type, msg1, msg2, location);
260  break;
261  }
262 }
263 
265  const std::string &type,
266  const std::string &msg1,
267  const std::string &,
268  const source_locationt &location)
269 {
270  xmlt result;
271  result.name="message";
272 
273  if(location.is_not_nil() &&
274  !location.get_file().empty())
275  result.new_element(xml(location));
276 
277  result.new_element("text").data=msg1;
278  result.set_attribute("type", type);
279  const std::string timestamp = time->stamp();
280  if(!timestamp.empty())
281  result.set_attribute("timestamp", timestamp);
282 
283  out << result;
284  out << '\n';
285 }
286 
288  const std::string &type,
289  const std::string &msg1,
290  const std::string &,
291  const source_locationt &location)
292 {
293  INVARIANT(json_stream, "JSON stream must be initialized before use");
294  json_objectt &result = json_stream->push_back().make_object();
295 
296  if(location.is_not_nil() &&
297  !location.get_file().empty())
298  result["sourceLocation"] = json(location);
299 
300  result["messageType"] = json_stringt(type);
301  result["messageText"] = json_stringt(msg1);
302  const std::string timestamp = time->stamp();
303  if(!timestamp.empty())
304  result["timestamp"] = json_stringt(timestamp);
305 }
306 
307 void ui_message_handlert::flush(unsigned level)
308 {
309  switch(get_ui())
310  {
311  case uit::PLAIN:
312  {
313  console_message_handlert console_message_handler(always_flush);
314  console_message_handler.flush(level);
315  }
316  break;
317 
318  case uit::XML_UI:
319  case uit::JSON_UI:
320  {
321  out << std::flush;
322  }
323  break;
324  }
325 }
std::ostream & out
Definition: ui_message.h:64
bool is_not_nil() const
Definition: irep.h:173
uit get_ui() const
Definition: ui_message.h:37
Definition: json.h:23
std::string name
Definition: xml.h:30
STL namespace.
const char * level_string(unsigned level)
Definition: ui_message.cpp:117
unsigned verbosity
Definition: message.h:77
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
ui_message_handlert()
Default constructor; implementation is in .cpp file.
Definition: ui_message.cpp:22
virtual void json_ui_msg(const std::string &type, const std::string &msg1, const std::string &msg2, const source_locationt &location)
Definition: ui_message.cpp:287
virtual void print(unsigned level, const std::string &message) override
Definition: ui_message.cpp:127
Timestamp class hierarchy.
Definition: timestamper.h:41
Expressions in JSON.
virtual void flush(unsigned level) override
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
virtual void xml_ui_msg(const std::string &type, const std::string &msg1, const std::string &msg2, const source_locationt &location)
Definition: ui_message.cpp:264
Definition: xml.h:18
std::string data
Definition: xml.h:30
clockt
Derived types of timestampert.
Definition: timestamper.h:45
virtual void ui_msg(const std::string &type, const std::string &msg1, const std::string &msg2, const source_locationt &location)
Definition: ui_message.cpp:243
xmlt & new_element(const std::string &name)
Definition: xml.h:86
const bool always_flush
Definition: ui_message.h:62
const irep_idt & get_file() const
std::unique_ptr< json_stream_arrayt > json_stream
Definition: ui_message.h:65
virtual ~ui_message_handlert()
Definition: ui_message.cpp:96
std::string to_string(const string_constraintt &expr)
Used for debug printing.
void make_nil()
Definition: irep.h:315
virtual void print(unsigned level, const std::string &message) override
std::unique_ptr< const timestampert > time
Definition: ui_message.h:63
bool empty() const
Definition: dstring.h:73
virtual void flush(unsigned level) override
Definition: ui_message.cpp:307
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83
Definition: kdev_t.h:24
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:59