Skip to content

Commit 034b072

Browse files
peterschrammelpeterschrammel
committed
Add reporting utils for covering goals
The output for --cover is quite different from verification. These functions should be moved into the prospective ccover tool.
1 parent 6ad4039 commit 034b072

File tree

3 files changed

+164
-0
lines changed

3 files changed

+164
-0
lines changed

‎src/goto-checker/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
SRC = bmc_util.cpp \
22
counterexample_beautification.cpp \
3+
cover_goals_report_util.cpp \
34
incremental_goto_checker.cpp \
45
goto_trace_storage.cpp \
56
goto_verifier.cpp \

‎src/goto-checker/cover_goals_report_util.cpp

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
/*******************************************************************\
2+
3+
Module: Cover Goals Reporting Utilities
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Cover Goals Reporting Utilities
11+
12+
#include "cover_goals_report_util.h"
13+
14+
#include <iomanip>
15+
16+
#include <util/json.h>
17+
#include <util/json_irep.h>
18+
#include <util/ui_message.h>
19+
#include <util/xml.h>
20+
#include <util/xml_irep.h>
21+
22+
static void output_goals_iterations(
23+
const propertiest &properties,
24+
unsigned iterations,
25+
messaget &log)
26+
{
27+
const std::size_t goals_covered =
28+
count_properties(properties, property_statust::FAIL);
29+
log.status() << "** " << goals_covered << " of " << properties.size()
30+
<< " covered (" << std::fixed << std::setw(1)
31+
<< std::setprecision(1)
32+
<< (properties.empty()
33+
? 100.0
34+
: 100.0 * goals_covered / properties.size())
35+
<< "%)" << messaget::eom;
36+
log.statistics() << "** Used " << iterations << " iteration"
37+
<< (iterations == 1 ? "" : "s") << messaget::eom;
38+
}
39+
40+
static void output_goals_plain(const propertiest &properties, messaget &log)
41+
{
42+
log.result() << "\n** coverage results:" << messaget::eom;
43+
44+
for(const auto &property_pair : properties)
45+
{
46+
log.result() << "[" << property_pair.first << "]";
47+
48+
if(property_pair.second.pc->source_location.is_not_nil())
49+
log.result() << ' ' << property_pair.second.pc->source_location;
50+
51+
if(!property_pair.second.description.empty())
52+
log.result() << ' ' << property_pair.second.description;
53+
54+
log.result() << ": "
55+
<< (property_pair.second.status == property_statust::FAIL
56+
? "SATISFIED"
57+
: "FAILED")
58+
<< '\n';
59+
}
60+
61+
log.result() << messaget::eom;
62+
}
63+
64+
static void output_goals_xml(const propertiest &properties, messaget &log)
65+
{
66+
for(const auto &property_pair : properties)
67+
{
68+
xmlt xml_result(
69+
"goal",
70+
{{"id", id2string(property_pair.first)},
71+
{"description", property_pair.second.description},
72+
{"status",
73+
property_pair.second.status == property_statust::FAIL ? "SATISFIED"
74+
: "FAILED"}},
75+
{});
76+
77+
if(property_pair.second.pc->source_location.is_not_nil())
78+
xml_result.new_element() = xml(property_pair.second.pc->source_location);
79+
80+
log.result() << xml_result;
81+
}
82+
}
83+
84+
static void output_goals_json(
85+
const propertiest &properties,
86+
messaget &log,
87+
ui_message_handlert &ui_message_handler)
88+
{
89+
if(log.status().tellp() > 0)
90+
log.status() << messaget::eom; // force end of previous message
91+
json_stream_objectt &json_result =
92+
ui_message_handler.get_json_stream().push_back_stream_object();
93+
for(const auto &property_pair : properties)
94+
{
95+
const property_infot &property_info = property_pair.second;
96+
97+
json_result["status"] = json_stringt(
98+
property_info.status == property_statust::FAIL ? "satisfied" : "failed");
99+
json_result["goal"] = json_stringt(property_pair.first);
100+
json_result["description"] = json_stringt(property_info.description);
101+
102+
if(property_info.pc->source_location.is_not_nil())
103+
json_result["sourceLocation"] = json(property_info.pc->source_location);
104+
}
105+
json_result["totalGoals"] = json_numbert(std::to_string(properties.size()));
106+
const std::size_t goals_covered =
107+
count_properties(properties, property_statust::FAIL);
108+
json_result["goalsCovered"] = json_numbert(std::to_string(goals_covered));
109+
}
110+
111+
void output_goals(
112+
const propertiest &properties,
113+
unsigned iterations,
114+
ui_message_handlert &ui_message_handler)
115+
{
116+
messaget log(ui_message_handler);
117+
switch(ui_message_handler.get_ui())
118+
{
119+
case ui_message_handlert::uit::PLAIN:
120+
{
121+
output_goals_plain(properties, log);
122+
break;
123+
}
124+
case ui_message_handlert::uit::XML_UI:
125+
{
126+
output_goals_xml(properties, log);
127+
break;
128+
}
129+
case ui_message_handlert::uit::JSON_UI:
130+
{
131+
output_goals_json(properties, log, ui_message_handler);
132+
break;
133+
}
134+
}
135+
output_goals_iterations(properties, iterations, log);
136+
}

‎src/goto-checker/cover_goals_report_util.h

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
/*******************************************************************\
2+
3+
Module: Cover Goals Reporting Utilities
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Cover Goals Reporting Utilities
11+
12+
#ifndef CPROVER_GOTO_CHECKER_COVER_GOALS_REPORT_UTIL_H
13+
#define CPROVER_GOTO_CHECKER_COVER_GOALS_REPORT_UTIL_H
14+
15+
#include "properties.h"
16+
17+
class ui_message_handlert;
18+
19+
/// Outputs the \p properties interpreted as 'coverage goals'
20+
/// and the number of goto verifier \p iterations that
21+
/// were required to compute the properties' status
22+
void output_goals(
23+
const propertiest &properties,
24+
unsigned iterations,
25+
ui_message_handlert &ui_message_handler);
26+
27+
#endif // CPROVER_GOTO_CHECKER_COVER_GOALS_REPORT_UTIL_H

0 commit comments

Comments
 (0)