Skip to content

Commit dd52eec

Browse files
tautschnigtautschnig
authored
Merge pull request #3583 from peterschrammel/property-reporting-utils
Property reporting utilities [blocks: 3584]
2 parents 4bd418a + 519fb98 commit dd52eec

File tree

5 files changed

+207
-0
lines changed

5 files changed

+207
-0
lines changed

‎src/goto-checker/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ SRC = bmc_util.cpp \
22
incremental_goto_checker.cpp \
33
goto_verifier.cpp \
44
properties.cpp \
5+
report_util.cpp \
56
solver_factory.cpp \
67
symex_coverage.cpp \
78
symex_bmc.cpp \

‎src/goto-checker/properties.cpp

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
1212
#include "properties.h"
1313

1414
#include <util/invariant.h>
15+
#include <util/json.h>
16+
#include <util/xml.h>
1517

1618
std::string as_string(resultt result)
1719
{
@@ -88,3 +90,40 @@ propertiest initialize_properties(const abstract_goto_modelt &goto_model)
8890
}
8991
return properties;
9092
}
93+
94+
std::string
95+
as_string(const irep_idt &property_id, const property_infot &property_info)
96+
{
97+
return "[" + id2string(property_id) + "] " + property_info.description +
98+
": " + as_string(property_info.status);
99+
}
100+
101+
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
102+
{
103+
xmlt xml_result("result");
104+
xml_result.set_attribute("property", id2string(property_id));
105+
xml_result.set_attribute("status", as_string(property_info.status));
106+
return xml_result;
107+
}
108+
109+
json_objectt
110+
json(const irep_idt &property_id, const property_infot &property_info)
111+
{
112+
json_objectt result;
113+
result["property"] = json_stringt(property_id);
114+
result["description"] = json_stringt(property_info.description);
115+
result["status"] = json_stringt(as_string(property_info.status));
116+
return result;
117+
}
118+
119+
std::size_t
120+
count_properties(const propertiest &properties, property_statust status)
121+
{
122+
std::size_t count = 0;
123+
for(const auto &property_pair : properties)
124+
{
125+
if(property_pair.second.status == status)
126+
++count;
127+
}
128+
return count;
129+
}

‎src/goto-checker/properties.h

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,9 @@ Author: Daniel Kroening, Peter Schrammel
1616

1717
#include <goto-programs/goto_model.h>
1818

19+
class json_objectt;
20+
class xmlt;
21+
1922
/// The status of a property
2023
enum class property_statust
2124
{
@@ -73,4 +76,15 @@ typedef std::unordered_map<irep_idt, property_infot> propertiest;
7376
/// Returns the properties in the goto model
7477
propertiest initialize_properties(const abstract_goto_modelt &);
7578

79+
std::string
80+
as_string(const irep_idt &property_id, const property_infot &property_info);
81+
82+
xmlt xml(const irep_idt &property_id, const property_infot &property_info);
83+
84+
json_objectt
85+
json(const irep_idt &property_id, const property_infot &property_info);
86+
87+
/// Return the number of properties with given \p status
88+
std::size_t count_properties(const propertiest &, property_statust);
89+
7690
#endif // CPROVER_GOTO_CHECKER_PROPERTIES_H

‎src/goto-checker/report_util.cpp

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
/*******************************************************************\
2+
3+
Module: Bounded Model Checking Utilities
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Bounded Model Checking Utilities
11+
12+
#include "report_util.h"
13+
14+
#include <algorithm>
15+
16+
#include <util/json.h>
17+
#include <util/ui_message.h>
18+
#include <util/xml.h>
19+
20+
void output_properties(
21+
const propertiest &properties,
22+
ui_message_handlert &ui_message_handler)
23+
{
24+
messaget log(ui_message_handler);
25+
switch(ui_message_handler.get_ui())
26+
{
27+
case ui_message_handlert::uit::PLAIN:
28+
{
29+
log.result() << "\n** Results:" << messaget::eom;
30+
// collect properties in a vector
31+
std::vector<propertiest::const_iterator> sorted_properties;
32+
for(auto p_it = properties.begin(); p_it != properties.end(); p_it++)
33+
sorted_properties.push_back(p_it);
34+
// now determine an ordering for those goals:
35+
// 1. alphabetical ordering of file name
36+
// 2. numerical ordering of line number
37+
// 3. alphabetical ordering of goal ID
38+
std::sort(
39+
sorted_properties.begin(),
40+
sorted_properties.end(),
41+
[](propertiest::const_iterator pit1, propertiest::const_iterator pit2) {
42+
const auto &p1 = pit1->second.pc->source_location;
43+
const auto &p2 = pit2->second.pc->source_location;
44+
if(p1.get_file() != p2.get_file())
45+
return id2string(p1.get_file()) < id2string(p2.get_file());
46+
else if(!p1.get_line().empty() && !p2.get_line().empty())
47+
return std::stoul(id2string(p1.get_line())) <
48+
std::stoul(id2string(p2.get_line()));
49+
else
50+
return id2string(pit1->first) < id2string(pit2->first);
51+
});
52+
// now show in the order we have determined
53+
irep_idt previous_function;
54+
irep_idt current_file;
55+
for(const auto &p : sorted_properties)
56+
{
57+
const auto &l = p->second.pc->source_location;
58+
if(l.get_function() != previous_function)
59+
{
60+
if(!previous_function.empty())
61+
log.result() << '\n';
62+
previous_function = l.get_function();
63+
if(!previous_function.empty())
64+
{
65+
current_file = l.get_file();
66+
if(!current_file.empty())
67+
log.result() << current_file << ' ';
68+
if(!l.get_function().empty())
69+
log.result() << "function " << l.get_function();
70+
log.result() << messaget::eom;
71+
}
72+
}
73+
log.result() << messaget::faint << '[' << p->first << "] "
74+
<< messaget::reset;
75+
if(l.get_file() != current_file)
76+
log.result() << "file " << l.get_file() << ' ';
77+
if(!l.get_line().empty())
78+
log.result() << "line " << l.get_line() << ' ';
79+
log.result() << p->second.description << ": ";
80+
switch(p->second.status)
81+
{
82+
case property_statust::NOT_CHECKED:
83+
log.result() << messaget::magenta;
84+
break;
85+
case property_statust::UNKNOWN:
86+
log.result() << messaget::yellow;
87+
break;
88+
case property_statust::NOT_REACHABLE:
89+
log.result() << messaget::bright_green;
90+
break;
91+
case property_statust::PASS:
92+
log.result() << messaget::green;
93+
break;
94+
case property_statust::FAIL:
95+
log.result() << messaget::red;
96+
break;
97+
case property_statust::ERROR:
98+
log.result() << messaget::bright_red;
99+
break;
100+
}
101+
log.result() << as_string(p->second.status) << messaget::reset
102+
<< messaget::eom;
103+
}
104+
log.status() << "\n** "
105+
<< count_properties(properties, property_statust::FAIL)
106+
<< " of " << properties.size() << " failed" << messaget::eom;
107+
break;
108+
}
109+
case ui_message_handlert::uit::XML_UI:
110+
{
111+
for(const auto &property_pair : properties)
112+
{
113+
log.result() << xml(property_pair.first, property_pair.second);
114+
}
115+
break;
116+
}
117+
case ui_message_handlert::uit::JSON_UI:
118+
{
119+
json_stream_objectt &json_result =
120+
ui_message_handler.get_json_stream().push_back_stream_object();
121+
json_stream_arrayt &result_array =
122+
json_result.push_back_stream_array("result");
123+
for(const auto &property_pair : properties)
124+
{
125+
result_array.push_back(json(property_pair.first, property_pair.second));
126+
}
127+
break;
128+
}
129+
}
130+
}

‎src/goto-checker/report_util.h

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
/*******************************************************************\
2+
3+
Module: Bounded Model Checking Utilities
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Bounded Model Checking Utilities
11+
12+
#ifndef CPROVER_GOTO_CHECKER_REPORT_UTIL_H
13+
#define CPROVER_GOTO_CHECKER_REPORT_UTIL_H
14+
15+
#include "properties.h"
16+
17+
class ui_message_handlert;
18+
19+
void output_properties(
20+
const propertiest &properties,
21+
ui_message_handlert &ui_message_handler);
22+
23+
#endif // CPROVER_GOTO_CHECKER_REPORT_UTIL_H

0 commit comments

Comments
 (0)