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