From cc1a90e4b825d0969b9e423feb1a7e91fc488ccd Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 21:13:52 +0000 Subject: [PATCH 1/3] Add count_properties with given result To count how many properties have a certain status. This will be used in property reporting. --- src/goto-checker/properties.cpp | 12 ++++++++++++ src/goto-checker/properties.h | 3 +++ 2 files changed, 15 insertions(+) diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 704891a1720..3d6be4b36fa 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -88,3 +88,15 @@ propertiest initialize_properties(const abstract_goto_modelt &goto_model) } return properties; } + +std::size_t +count_properties(const propertiest &properties, property_statust status) +{ + std::size_t count = 0; + for(const auto &property_pair : properties) + { + if(property_pair.second.status == status) + ++count; + } + return count; +} diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index 11050f24d8e..e96e1903de7 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -73,4 +73,7 @@ typedef std::unordered_map propertiest; /// Returns the properties in the goto model propertiest initialize_properties(const abstract_goto_modelt &); +/// Return the number of properties with given \p status +std::size_t count_properties(const propertiest &, property_statust); + #endif // CPROVER_GOTO_CHECKER_PROPERTIES_H From 4da669d4e8aa2c652fb4e9c03cce42ce7e11ee02 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 21:13:36 +0000 Subject: [PATCH 2/3] Add property output functions Plain text, XML and JSON output for property results. --- src/goto-checker/properties.cpp | 27 +++++++++++++++++++++++++++ src/goto-checker/properties.h | 11 +++++++++++ 2 files changed, 38 insertions(+) diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 3d6be4b36fa..321e3d465cf 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -12,6 +12,8 @@ Author: Daniel Kroening, Peter Schrammel #include "properties.h" #include +#include +#include std::string as_string(resultt result) { @@ -89,6 +91,31 @@ propertiest initialize_properties(const abstract_goto_modelt &goto_model) return properties; } +std::string +as_string(const irep_idt &property_id, const property_infot &property_info) +{ + return "[" + id2string(property_id) + "] " + property_info.description + + ": " + as_string(property_info.status); +} + +xmlt xml(const irep_idt &property_id, const property_infot &property_info) +{ + xmlt xml_result("result"); + xml_result.set_attribute("property", id2string(property_id)); + xml_result.set_attribute("status", as_string(property_info.status)); + return xml_result; +} + +json_objectt +json(const irep_idt &property_id, const property_infot &property_info) +{ + json_objectt result; + result["property"] = json_stringt(property_id); + result["description"] = json_stringt(property_info.description); + result["status"] = json_stringt(as_string(property_info.status)); + return result; +} + std::size_t count_properties(const propertiest &properties, property_statust status) { diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index e96e1903de7..134257396ef 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -16,6 +16,9 @@ Author: Daniel Kroening, Peter Schrammel #include +class json_objectt; +class xmlt; + /// The status of a property enum class property_statust { @@ -73,6 +76,14 @@ typedef std::unordered_map propertiest; /// Returns the properties in the goto model propertiest initialize_properties(const abstract_goto_modelt &); +std::string +as_string(const irep_idt &property_id, const property_infot &property_info); + +xmlt xml(const irep_idt &property_id, const property_infot &property_info); + +json_objectt +json(const irep_idt &property_id, const property_infot &property_info); + /// Return the number of properties with given \p status std::size_t count_properties(const propertiest &, property_statust); From 519fb989a3ab2dcedbf63616490a130f3c8ed02d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 18:41:28 +0000 Subject: [PATCH 3/3] Add report_util for outputting verification results Prints the property report in plain text, JSON or XML. --- src/goto-checker/Makefile | 1 + src/goto-checker/report_util.cpp | 130 +++++++++++++++++++++++++++++++ src/goto-checker/report_util.h | 23 ++++++ 3 files changed, 154 insertions(+) create mode 100644 src/goto-checker/report_util.cpp create mode 100644 src/goto-checker/report_util.h diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index eeb45de1516..650944f72db 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -2,6 +2,7 @@ SRC = bmc_util.cpp \ incremental_goto_checker.cpp \ goto_verifier.cpp \ properties.cpp \ + report_util.cpp \ solver_factory.cpp \ symex_coverage.cpp \ symex_bmc.cpp \ diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp new file mode 100644 index 00000000000..2e92e33d6d2 --- /dev/null +++ b/src/goto-checker/report_util.cpp @@ -0,0 +1,130 @@ +/*******************************************************************\ + +Module: Bounded Model Checking Utilities + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Bounded Model Checking Utilities + +#include "report_util.h" + +#include + +#include +#include +#include + +void output_properties( + const propertiest &properties, + ui_message_handlert &ui_message_handler) +{ + messaget log(ui_message_handler); + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + { + log.result() << "\n** Results:" << messaget::eom; + // collect properties in a vector + std::vector sorted_properties; + for(auto p_it = properties.begin(); p_it != properties.end(); p_it++) + sorted_properties.push_back(p_it); + // now determine an ordering for those goals: + // 1. alphabetical ordering of file name + // 2. numerical ordering of line number + // 3. alphabetical ordering of goal ID + std::sort( + sorted_properties.begin(), + sorted_properties.end(), + [](propertiest::const_iterator pit1, propertiest::const_iterator pit2) { + const auto &p1 = pit1->second.pc->source_location; + const auto &p2 = pit2->second.pc->source_location; + if(p1.get_file() != p2.get_file()) + return id2string(p1.get_file()) < id2string(p2.get_file()); + else if(!p1.get_line().empty() && !p2.get_line().empty()) + return std::stoul(id2string(p1.get_line())) < + std::stoul(id2string(p2.get_line())); + else + return id2string(pit1->first) < id2string(pit2->first); + }); + // now show in the order we have determined + irep_idt previous_function; + irep_idt current_file; + for(const auto &p : sorted_properties) + { + const auto &l = p->second.pc->source_location; + if(l.get_function() != previous_function) + { + if(!previous_function.empty()) + log.result() << '\n'; + previous_function = l.get_function(); + if(!previous_function.empty()) + { + current_file = l.get_file(); + if(!current_file.empty()) + log.result() << current_file << ' '; + if(!l.get_function().empty()) + log.result() << "function " << l.get_function(); + log.result() << messaget::eom; + } + } + log.result() << messaget::faint << '[' << p->first << "] " + << messaget::reset; + if(l.get_file() != current_file) + log.result() << "file " << l.get_file() << ' '; + if(!l.get_line().empty()) + log.result() << "line " << l.get_line() << ' '; + log.result() << p->second.description << ": "; + switch(p->second.status) + { + case property_statust::NOT_CHECKED: + log.result() << messaget::magenta; + break; + case property_statust::UNKNOWN: + log.result() << messaget::yellow; + break; + case property_statust::NOT_REACHABLE: + log.result() << messaget::bright_green; + break; + case property_statust::PASS: + log.result() << messaget::green; + break; + case property_statust::FAIL: + log.result() << messaget::red; + break; + case property_statust::ERROR: + log.result() << messaget::bright_red; + break; + } + log.result() << as_string(p->second.status) << messaget::reset + << messaget::eom; + } + log.status() << "\n** " + << count_properties(properties, property_statust::FAIL) + << " of " << properties.size() << " failed" << messaget::eom; + break; + } + case ui_message_handlert::uit::XML_UI: + { + for(const auto &property_pair : properties) + { + log.result() << xml(property_pair.first, property_pair.second); + } + break; + } + case ui_message_handlert::uit::JSON_UI: + { + json_stream_objectt &json_result = + ui_message_handler.get_json_stream().push_back_stream_object(); + json_stream_arrayt &result_array = + json_result.push_back_stream_array("result"); + for(const auto &property_pair : properties) + { + result_array.push_back(json(property_pair.first, property_pair.second)); + } + break; + } + } +} diff --git a/src/goto-checker/report_util.h b/src/goto-checker/report_util.h new file mode 100644 index 00000000000..b15de8a617e --- /dev/null +++ b/src/goto-checker/report_util.h @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Bounded Model Checking Utilities + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Bounded Model Checking Utilities + +#ifndef CPROVER_GOTO_CHECKER_REPORT_UTIL_H +#define CPROVER_GOTO_CHECKER_REPORT_UTIL_H + +#include "properties.h" + +class ui_message_handlert; + +void output_properties( + const propertiest &properties, + ui_message_handlert &ui_message_handler); + +#endif // CPROVER_GOTO_CHECKER_REPORT_UTIL_H