cprover
cover_goals_report_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Cover Goals Reporting Utilities
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <iomanip>
15 
16 #include <util/json.h>
17 #include <util/json_irep.h>
18 #include <util/json_stream.h>
19 #include <util/ui_message.h>
20 #include <util/xml.h>
21 #include <util/xml_irep.h>
22 
24  const propertiest &properties,
25  unsigned iterations,
26  messaget &log)
27 {
28  const std::size_t goals_covered =
29  count_properties(properties, property_statust::FAIL);
30  log.status() << "** " << goals_covered << " of " << properties.size()
31  << " covered (" << std::fixed << std::setw(1)
32  << std::setprecision(1)
33  << (properties.empty()
34  ? 100.0
35  : 100.0 * goals_covered / properties.size())
36  << "%)" << messaget::eom;
37  log.statistics() << "** Used " << iterations << " iteration"
38  << (iterations == 1 ? "" : "s") << messaget::eom;
39 }
40 
41 static void output_goals_plain(const propertiest &properties, messaget &log)
42 {
43  log.result() << "\n** coverage results:" << messaget::eom;
44 
45  for(const auto &property_pair : properties)
46  {
47  log.result() << "[" << property_pair.first << "]";
48 
49  if(property_pair.second.pc->source_location.is_not_nil())
50  log.result() << ' ' << property_pair.second.pc->source_location;
51 
52  if(!property_pair.second.description.empty())
53  log.result() << ' ' << property_pair.second.description;
54 
55  log.result() << ": "
56  << (property_pair.second.status == property_statust::FAIL
57  ? "SATISFIED"
58  : "FAILED")
59  << '\n';
60  }
61 
62  log.result() << messaget::eom;
63 }
64 
65 static void output_goals_xml(const propertiest &properties, messaget &log)
66 {
67  for(const auto &property_pair : properties)
68  {
69  xmlt xml_result(
70  "goal",
71  {{"id", id2string(property_pair.first)},
72  {"description", property_pair.second.description},
73  {"status",
74  property_pair.second.status == property_statust::FAIL ? "SATISFIED"
75  : "FAILED"}},
76  {});
77 
78  if(property_pair.second.pc->source_location.is_not_nil())
79  xml_result.new_element() = xml(property_pair.second.pc->source_location);
80 
81  log.result() << xml_result;
82  }
83 }
84 
85 static void output_goals_json(
86  const propertiest &properties,
87  messaget &log,
88  ui_message_handlert &ui_message_handler)
89 {
90  if(log.status().tellp() > 0)
91  log.status() << messaget::eom; // force end of previous message
92  json_stream_objectt &json_result =
93  ui_message_handler.get_json_stream().push_back_stream_object();
94  json_stream_arrayt &goals_array = json_result.push_back_stream_array("goals");
95  for(const auto &property_pair : properties)
96  {
97  const property_infot &property_info = property_pair.second;
98 
99  json_objectt json_goal;
100  json_goal["status"] = json_stringt(
101  property_info.status == property_statust::FAIL ? "satisfied" : "failed");
102  json_goal["goal"] = json_stringt(property_pair.first);
103  json_goal["description"] = json_stringt(property_info.description);
104 
105  if(property_info.pc->source_location.is_not_nil())
106  json_goal["sourceLocation"] = json(property_info.pc->source_location);
107 
108  goals_array.push_back(std::move(json_goal));
109  }
110  const std::size_t goals_covered =
111  count_properties(properties, property_statust::FAIL);
112  json_result.push_back(
113  "goalsCovered", json_numbert(std::to_string(goals_covered)));
114  json_result.push_back(
115  "totalGoals", json_numbert(std::to_string(properties.size())));
116 }
117 
119  const propertiest &properties,
120  unsigned iterations,
121  ui_message_handlert &ui_message_handler)
122 {
123  messaget log(ui_message_handler);
124  switch(ui_message_handler.get_ui())
125  {
127  {
128  output_goals_plain(properties, log);
129  break;
130  }
132  {
133  output_goals_xml(properties, log);
134  break;
135  }
137  {
138  output_goals_json(properties, log, ui_message_handler);
139  break;
140  }
141  }
142  output_goals_iterations(properties, iterations, log);
143 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
json_numbert
Definition: json.h:291
ui_message_handlert
Definition: ui_message.h:22
ui_message_handlert::uit::XML_UI
@ XML_UI
messaget::status
mstreamt & status() const
Definition: message.h:414
json_stream.h
output_goals_json
static void output_goals_json(const propertiest &properties, messaget &log, ui_message_handlert &ui_message_handler)
Definition: cover_goals_report_util.cpp:85
output_goals_iterations
static void output_goals_iterations(const propertiest &properties, unsigned iterations, messaget &log)
Definition: cover_goals_report_util.cpp:23
xml_irep.h
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
messaget::eom
static eomt eom
Definition: message.h:297
output_goals_xml
static void output_goals_xml(const propertiest &properties, messaget &log)
Definition: cover_goals_report_util.cpp:65
xml.h
json_irep.h
Util.
property_infot::description
std::string description
A description (usually derived from the assertion's comment)
Definition: properties.h:69
output_goals
void output_goals(const propertiest &properties, unsigned iterations, ui_message_handlert &ui_message_handler)
Outputs the properties interpreted as 'coverage goals' and the number of goto verifier iterations tha...
Definition: cover_goals_report_util.cpp:118
json_objectt
Definition: json.h:300
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:33
json_stream_objectt::push_back_stream_array
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
Definition: json_stream.cpp:120
ui_message_handlert::get_json_stream
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:40
property_infot::status
property_statust status
The status of the property.
Definition: properties.h:72
cover_goals_report_util.h
Cover Goals Reporting Utilities.
messaget::result
mstreamt & result() const
Definition: message.h:409
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:107
ui_message_handlert::uit::JSON_UI
@ JSON_UI
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:116
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
count_properties
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:159
xmlt
Definition: xml.h:21
json_stream_arrayt::push_back_stream_object
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
property_infot
Definition: properties.h:59
ui_message_handlert::uit::PLAIN
@ PLAIN
json.h
json_stream_arrayt::push_back
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
Definition: json_stream.h:106
output_goals_plain
static void output_goals_plain(const propertiest &properties, messaget &log)
Definition: cover_goals_report_util.cpp:41
property_infot::pc
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition: properties.h:66
json_stream_objectt::push_back
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
Definition: json_stream.h:178
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
json_stringt
Definition: json.h:270
ui_message.h