CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
report_util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Bounded Model Checking Utilities
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "report_util.h"
13
14#include <algorithm>
15
16#include <util/json.h>
17#include <util/json_irep.h>
18#include <util/json_stream.h>
19#include <util/string2int.h>
20#include <util/ui_message.h>
21#include <util/xml.h>
22#include <util/xml_irep.h>
23
26
28#include "goto_trace_storage.h"
29
30#include "bmc_util.h"
31
32void report_success(ui_message_handlert &ui_message_handler)
33{
34 messaget msg(ui_message_handler);
35 msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom;
36
37 switch(ui_message_handler.get_ui())
38 {
40 break;
41
43 {
44 xmlt xml("cprover-status");
45 xml.data = "SUCCESS";
46 msg.result() << xml;
47 }
48 break;
49
51 {
53 json_result["cProverStatus"] = json_stringt("success");
54 msg.result() << json_result;
55 }
56 break;
57 }
58}
59
60void report_failure(ui_message_handlert &ui_message_handler)
61{
62 messaget msg(ui_message_handler);
63 msg.result() << "VERIFICATION FAILED" << messaget::eom;
64
65 switch(ui_message_handler.get_ui())
66 {
68 break;
69
71 {
72 xmlt xml("cprover-status");
73 xml.data = "FAILURE";
74 msg.result() << xml;
75 }
76 break;
77
79 {
81 json_result["cProverStatus"] = json_stringt("failure");
82 msg.result() << json_result;
83 }
84 break;
85 }
86}
87
89{
90 messaget msg(ui_message_handler);
91 msg.result() << "VERIFICATION INCONCLUSIVE" << messaget::eom;
92
93 switch(ui_message_handler.get_ui())
94 {
96 break;
97
99 {
100 xmlt xml("cprover-status");
101 xml.data = "INCONCLUSIVE";
102 msg.result() << xml;
103 }
104 break;
105
107 {
109 json_result["cProverStatus"] = json_stringt("inconclusive");
110 msg.result() << json_result;
111 }
112 break;
113 }
114}
115
116void report_error(ui_message_handlert &ui_message_handler)
117{
118 messaget msg(ui_message_handler);
119 msg.result() << "VERIFICATION ERROR" << messaget::eom;
120
121 switch(ui_message_handler.get_ui())
122 {
124 break;
125
127 {
128 xmlt xml("cprover-status");
129 xml.data = "ERROR";
130 msg.result() << xml;
131 }
132 break;
133
135 {
137 json_result["cProverStatus"] = json_stringt("error");
138 msg.result() << json_result;
139 }
140 break;
141 }
142}
143
145 const irep_idt &property_id,
147 messaget &log,
149{
150 const auto &l = property_info.pc->source_location();
151 log.result() << messaget::faint << '[' << property_id << "] "
153 if(l.get_file() != current_file)
154 log.result() << "file " << l.get_file() << ' ';
155 if(!l.get_line().empty())
156 log.result() << "line " << l.get_line() << ' ';
157 log.result() << property_info.description << ": ";
158 switch(property_info.status)
159 {
161 log.result() << messaget::magenta;
162 break;
164 log.result() << messaget::yellow;
165 break;
167 log.result() << messaget::bright_green;
168 break;
170 log.result() << messaget::green;
171 break;
173 log.result() << messaget::red;
174 break;
176 log.result() << messaget::bright_red;
177 break;
178 }
179 log.result() << as_string(property_info.status) << messaget::reset
180 << messaget::eom;
181}
182
183using propertyt = std::pair<irep_idt, property_infot>;
193static bool
195{
196 const auto &p1 = property1.second.pc->source_location();
197 const auto &p2 = property2.second.pc->source_location();
198 if(p1.get_file() != p2.get_file())
199 return id2string(p1.get_file()) < id2string(p2.get_file());
200 if(p1.get_function() != p2.get_function())
201 return id2string(p1.get_function()) < id2string(p2.get_function());
202 else if(
203 !p1.get_line().empty() && !p2.get_line().empty() &&
204 p1.get_line() != p2.get_line())
205 return std::stoul(id2string(p1.get_line())) <
206 std::stoul(id2string(p2.get_line()));
207
208 const auto split_property_id =
209 [](const irep_idt &property_id) -> std::pair<std::string, std::size_t> {
210 const auto property_string = id2string(property_id);
211 const auto last_dot = property_string.rfind('.');
212 std::string property_name;
213 std::string property_number;
214 if(last_dot == std::string::npos)
215 {
216 property_name = "";
218 }
219 else
220 {
223 }
225 if(maybe_number.has_value())
226 return std::make_pair(property_name, *maybe_number);
227 else
228 return std::make_pair(property_name, 0);
229 };
230
231 const auto left_split = split_property_id(property1.first);
232 const auto left_id_name = left_split.first;
233 const auto left_id_number = left_split.second;
234
235 const auto right_split = split_property_id(property2.first);
236 const auto right_id_name = right_split.first;
237 const auto right_id_number = right_split.second;
238
241 else
243}
244
245static std::vector<propertiest::const_iterator>
247{
248 std::vector<propertiest::const_iterator> sorted_properties;
249 for(auto p_it = properties.begin(); p_it != properties.end(); p_it++)
250 sorted_properties.push_back(p_it);
251
252 std::sort(
253 sorted_properties.begin(),
254 sorted_properties.end(),
255 [](propertiest::const_iterator pit1, propertiest::const_iterator pit2) {
256 return is_property_less_than(*pit1, *pit2);
257 });
258 return sorted_properties;
259}
260
262 const std::vector<propertiest::const_iterator> &sorted_properties,
263 messaget &log)
264{
265 if(sorted_properties.empty())
266 return;
267
268 log.result() << "\n** Results:" << messaget::eom;
269 // now show in the order we have determined
272 for(const auto &p : sorted_properties)
273 {
274 const auto &l = p->second.pc->source_location();
275 if(l.get_function() != previous_function)
276 {
277 if(!previous_function.empty())
278 log.result() << '\n';
279 previous_function = l.get_function();
280 if(!previous_function.empty())
281 {
282 current_file = l.get_file();
283 if(!current_file.empty())
284 log.result() << current_file << ' ';
285 if(!l.get_function().empty())
286 log.result() << "function " << l.get_function();
287 log.result() << messaget::eom;
288 }
289 }
290 output_single_property_plain(p->first, p->second, log, current_file);
291 }
292}
293
295 const propertiest &properties,
296 std::size_t iterations,
297 messaget &log)
298{
299 if(properties.empty())
300 return;
301
302 log.status() << "\n** "
303 << count_properties(properties, property_statust::FAIL) << " of "
304 << properties.size() << " failed (" << iterations
305 << " iterations)" << messaget::eom;
306}
307
309 const propertiest &properties,
310 std::size_t iterations,
311 ui_message_handlert &ui_message_handler)
312{
313 messaget log(ui_message_handler);
314 switch(ui_message_handler.get_ui())
315 {
317 {
318 const auto sorted_properties = get_sorted_properties(properties);
320 output_iterations(properties, iterations, log);
321 break;
322 }
324 {
325 for(const auto &property_pair : properties)
326 {
327 log.result() << xml(property_pair.first, property_pair.second);
328 }
329 break;
330 }
332 {
334 ui_message_handler.get_json_stream().push_back_stream_object();
336 json_result.push_back_stream_array("result");
337 for(const auto &property_pair : properties)
338 {
339 result_array.push_back(json(property_pair.first, property_pair.second));
340 }
341 break;
342 }
343 }
344}
345
347 const propertiest &properties,
348 const goto_trace_storaget &traces,
350 std::size_t iterations,
351 ui_message_handlert &ui_message_handler)
352{
353 messaget log(ui_message_handler);
354 switch(ui_message_handler.get_ui())
355 {
357 {
358 const auto sorted_properties = get_sorted_properties(properties);
360 for(const auto &property_it : sorted_properties)
361 {
362 if(property_it->second.status == property_statust::FAIL)
363 {
364 log.result() << "\n"
365 << "Trace for " << property_it->first << ":"
366 << "\n";
368 log.result(),
369 traces.get_namespace(),
370 traces[property_it->first],
372 log.result() << messaget::eom;
373 }
374 }
375 output_iterations(properties, iterations, log);
376 break;
377 }
379 {
380 for(const auto &property_pair : properties)
381 {
383 if(property_pair.second.status == property_statust::FAIL)
384 {
385 convert(
386 traces.get_namespace(),
387 traces[property_pair.first],
388 xml_result.new_element());
389 }
390 log.result() << xml_result;
391 }
392 break;
393 }
395 {
397 ui_message_handler.get_json_stream().push_back_stream_object();
399 json_result.push_back_stream_array("result");
400 for(const auto &property_pair : properties)
401 {
403 result_array.push_back_stream_object();
405 if(property_pair.second.status == property_statust::FAIL)
406 {
408 json_property.push_back_stream_array("trace");
410 traces.get_namespace(),
411 traces[property_pair.first],
414 }
415 }
416 break;
417 }
418 }
419}
420
423 messaget &log)
424{
425 log.conditional_output(
426 log.debug(), [fault_location](messaget::mstreamt &out) {
427 out << "Fault localization scores:" << messaget::eom;
428 for(auto &score_pair : fault_location.scores)
429 {
430 out << score_pair.first->source_location()
431 << "\n score: " << score_pair.second << messaget::eom;
432 }
433 });
434}
435
438{
439 PRECONDITION(!fault_location.scores.empty());
440
441 return std::max_element(
442 fault_location.scores.begin(),
443 fault_location.scores.end(),
444 [](
445 fault_location_infot::score_mapt::value_type score_pair1,
446 fault_location_infot::score_mapt::value_type score_pair2) {
447 return score_pair1.second < score_pair2.second;
448 })
449 ->first;
450}
451
453 const irep_idt &property_id,
455 messaget &log)
456{
457 if(fault_location.scores.empty())
458 {
459 log.result() << "[" + id2string(property_id) + "]: \n"
460 << " unable to localize fault" << messaget::eom;
461 return;
462 }
463
465 log.result()
466 << "[" + id2string(property_id) + "]: \n "
467 << max_fault_localization_score(fault_location)->source_location()
468 << messaget::eom;
469}
470
472 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
473 messaget &log)
474{
475 log.result() << "\n** Most likely fault location:" << messaget::eom;
476 for(const auto &fault_location_pair : fault_locations)
477 {
480 }
481}
482
483static xmlt xml(
484 const irep_idt &property_id,
486 messaget &log)
487{
488 xmlt xml_diagnosis("diagnosis");
489
490 xml_diagnosis.set_attribute("property", id2string(property_id));
491
492 if(fault_location.scores.empty())
493 {
494 xml_diagnosis.new_element("result").data = "unable to localize fault";
495 return xml_diagnosis;
496 }
497
499
502 xml_diagnosis.new_element("result").new_element().swap(xml_location);
503
504 return xml_diagnosis;
505}
506
508 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
509 messaget &log)
510{
511 xmlt dest("fault-localization");
512 for(const auto &fault_location_pair : fault_locations)
513 {
517 }
518 log.result() << dest;
519}
520
522{
524 if(fault_location.scores.empty())
525 {
526 json_result["result"] = json_stringt("unable to localize fault");
527 }
528 else
529 {
530 json_result["result"] =
532 }
533 return json_result;
534}
535
537 const propertiest &properties,
538 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
539 std::size_t iterations,
540 ui_message_handlert &ui_message_handler)
541{
542 messaget log(ui_message_handler);
543 switch(ui_message_handler.get_ui())
544 {
546 {
547 output_properties(properties, iterations, ui_message_handler);
548 output_fault_localization_plain(fault_locations, log);
549 break;
550 }
552 {
554 ui_message_handler.get_json_stream().push_back_stream_object();
556 json_result.push_back_stream_array("result");
557 for(const auto &property_pair : properties)
558 {
560 result_array.push_back_stream_object();
562 if(property_pair.second.status == property_statust::FAIL)
563 {
564 json_property.push_back(
565 "diagnosis", json(fault_locations.at(property_pair.first)));
566 }
567 }
568 break;
569 }
571 {
572 output_properties(properties, iterations, ui_message_handler);
573 output_fault_localization_xml(fault_locations, log);
574 break;
575 }
576 }
577}
578
580 const propertiest &properties,
581 const goto_trace_storaget &traces,
583 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
584 std::size_t iterations,
585 ui_message_handlert &ui_message_handler)
586{
587 messaget log(ui_message_handler);
588 switch(ui_message_handler.get_ui())
589 {
591 {
593 properties, traces, trace_options, iterations, ui_message_handler);
594 output_fault_localization_plain(fault_locations, log);
595 break;
596 }
598 {
600 ui_message_handler.get_json_stream().push_back_stream_object();
602 json_result.push_back_stream_array("result");
603 for(const auto &property_pair : properties)
604 {
606 result_array.push_back_stream_object();
608 if(property_pair.second.status == property_statust::FAIL)
609 {
611 json_property.push_back_stream_array("trace");
613 traces.get_namespace(),
614 traces[property_pair.first],
617 json_property.push_back(
618 "diagnosis", json(fault_locations.at(property_pair.first)));
619 }
620 }
621 break;
622 }
624 {
626 properties, traces, trace_options, iterations, ui_message_handler);
627 output_fault_localization_xml(fault_locations, log);
628 break;
629 }
630 }
631}
632
634 const goto_tracet &goto_trace,
635 const namespacet &ns,
638 ui_message_handlert &ui_message_handler)
639{
640 messaget log(ui_message_handler);
641 switch(ui_message_handler.get_ui())
642 {
644 output_error_trace(goto_trace, ns, trace_options, ui_message_handler);
646 goto_trace.get_last_step().property_id, fault_location_info, log);
647 break;
648
650 {
652 ui_message_handler.get_json_stream().push_back_stream_object();
653 const goto_trace_stept &step = goto_trace.get_last_step();
654 json_result["property"] = json_stringt(step.property_id);
655 json_result["description"] = json_stringt(step.comment);
656 json_result["status"] = json_stringt("failed");
658 json_result.push_back_stream_array("trace");
660 json_result.push_back("diagnosis", json(fault_location_info));
661 break;
662 }
663
665 {
666 output_error_trace(goto_trace, ns, trace_options, ui_message_handler);
667 xmlt dest(
668 "fault-localization",
669 {},
670 {xml(goto_trace.get_last_step().property_id, fault_location_info, log)});
671 log.result() << dest;
672 break;
673 }
674 }
675}
676
678 resultt result,
679 ui_message_handlert &ui_message_handler)
680{
681 switch(result)
682 {
683 case resultt::PASS:
684 report_success(ui_message_handler);
685 break;
686 case resultt::FAIL:
687 report_failure(ui_message_handler);
688 break;
689 case resultt::UNKNOWN:
690 report_inconclusive(ui_message_handler);
691 break;
692 case resultt::ERROR:
693 report_error(ui_message_handler);
694 break;
695 }
696}
void output_error_trace(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, ui_message_handlert &ui_message_handler)
Definition bmc_util.cpp:64
Bounded Model Checking Utilities.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_table_baset &symbol_table, message_handlert &message_handler)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
instructionst::const_iterator const_targett
Step of the trace of a GOTO program.
Definition goto_trace.h:50
std::string comment
Definition goto_trace.h:124
irep_idt property_id
Definition goto_trace.h:123
const namespacet & get_namespace() const
Trace of a GOTO program.
Definition goto_trace.h:177
Provides methods for streaming JSON arrays.
Definition json_stream.h:93
Provides methods for streaming JSON objects.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static const commandt yellow
render text with yellow foreground color
Definition message.h:344
static const commandt magenta
render text with magenta foreground color
Definition message.h:350
static const commandt reset
return to default formatting, as defined by the terminal
Definition message.h:335
static const commandt green
render text with green foreground color
Definition message.h:341
static const commandt faint
render text with faint font
Definition message.h:377
static const commandt bright_red
render text with bright red foreground color
Definition message.h:356
static const commandt red
render text with red foreground color
Definition message.h:338
static eomt eom
Definition message.h:289
static const commandt bright_green
render text with bright green foreground color
Definition message.h:359
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
virtual uit get_ui() const
Definition ui_message.h:33
virtual json_stream_arrayt & get_json_stream()
Definition ui_message.h:40
Definition xml.h:21
xmlt & new_element(const std::string &key)
Definition xml.h:95
void swap(xmlt &xml)
Definition xml.cpp:25
Interface for Goto Checkers to provide Fault Localization.
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Output the trace on the given stream out.
Goto Trace Storage.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Traces of GOTO Programs.
double log(double x)
Definition math.c:2449
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
@ UNKNOWN
The checker was unable to determine the status of the property.
@ NOT_REACHABLE
The property was proven to be unreachable.
@ PASS
The property was not violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
The property was violated.
@ NOT_CHECKED
The property was not checked (also used for initialization)
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76
resultt
The result of goto verifying.
Definition properties.h:45
@ UNKNOWN
No property was violated, neither was there an error.
@ PASS
No properties were violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
Some properties were violated.
static std::vector< propertiest::const_iterator > get_sorted_properties(const propertiest &properties)
void output_properties(const propertiest &properties, std::size_t iterations, ui_message_handlert &ui_message_handler)
static void output_properties_plain(const std::vector< propertiest::const_iterator > &sorted_properties, messaget &log)
static goto_programt::const_targett max_fault_localization_score(const fault_location_infot &fault_location)
void output_properties_with_fault_localization(const propertiest &properties, const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, std::size_t iterations, ui_message_handlert &ui_message_handler)
void output_properties_with_traces_and_fault_localization(const propertiest &properties, const goto_trace_storaget &traces, const trace_optionst &trace_options, const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, std::size_t iterations, ui_message_handlert &ui_message_handler)
static json_objectt json(const fault_location_infot &fault_location)
static void output_fault_localization_plain(const irep_idt &property_id, const fault_location_infot &fault_location, messaget &log)
void report_success(ui_message_handlert &ui_message_handler)
static bool is_property_less_than(const propertyt &property1, const propertyt &property2)
Compare two properties according to the following sort:
static xmlt xml(const irep_idt &property_id, const fault_location_infot &fault_location, messaget &log)
void report_inconclusive(ui_message_handlert &ui_message_handler)
void output_overall_result(resultt result, ui_message_handlert &ui_message_handler)
void output_properties_with_traces(const propertiest &properties, const goto_trace_storaget &traces, const trace_optionst &trace_options, std::size_t iterations, ui_message_handlert &ui_message_handler)
void output_fault_localization_scores(const fault_location_infot &fault_location, messaget &log)
static void output_fault_localization_xml(const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, messaget &log)
void output_error_trace_with_fault_localization(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, const fault_location_infot &fault_location_info, ui_message_handlert &ui_message_handler)
static void output_iterations(const propertiest &properties, std::size_t iterations, messaget &log)
void report_error(ui_message_handlert &ui_message_handler)
void report_failure(ui_message_handlert &ui_message_handler)
static void output_single_property_plain(const irep_idt &property_id, const property_infot &property_info, messaget &log, irep_idt current_file=irep_idt())
Bounded Model Checking Utilities.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
std::optional< std::size_t > string2optional_size_t(const std::string &str, int base)
Convert string to size_t similar to the stoul or stoull functions, return nullopt when the conversion...
Options for printing the trace using show_goto_trace.
Definition goto_trace.h:221
dstringt irep_idt
Traces of GOTO Programs.