From cc1a90e4b825d0969b9e423feb1a7e91fc488ccd Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 21:13:52 +0000 Subject: [PATCH 1/7] 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/7] 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/7] 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 From 0ba2e84e2e303f39837f94bb8eb33492e3dbb64f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 18:47:03 +0000 Subject: [PATCH 4/7] Move reporting functions to report_util --- src/cbmc/all_properties.cpp | 1 + src/cbmc/bmc.cpp | 1 + src/cbmc/fault_localization.cpp | 1 + src/goto-checker/bmc_util.cpp | 55 ------------------------------- src/goto-checker/bmc_util.h | 3 -- src/goto-checker/report_util.cpp | 56 ++++++++++++++++++++++++++++++++ src/goto-checker/report_util.h | 3 ++ 7 files changed, 62 insertions(+), 58 deletions(-) diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index a9e5b346f4c..2fc125f10fa 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 51c015adc86..282c749c90a 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include "counterexample_beautification.h" diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index 603b4025d85..56a7dcc241f 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -27,6 +27,7 @@ Author: Peter Schrammel #include #include +#include #include "counterexample_beautification.h" diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 5974a7538b8..b8b2279ed87 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -225,58 +225,3 @@ void slice( << " remaining after simplification" << messaget::eom; } -void report_success(ui_message_handlert &ui_message_handler) -{ - messaget msg(ui_message_handler); - msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom; - - switch(ui_message_handler.get_ui()) - { - case ui_message_handlert::uit::PLAIN: - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml("cprover-status"); - xml.data = "SUCCESS"; - msg.result() << xml; - } - break; - - case ui_message_handlert::uit::JSON_UI: - { - json_objectt json_result; - json_result["cProverStatus"] = json_stringt("success"); - msg.result() << json_result; - } - break; - } -} - -void report_failure(ui_message_handlert &ui_message_handler) -{ - messaget msg(ui_message_handler); - msg.result() << "VERIFICATION FAILED" << messaget::eom; - - switch(ui_message_handler.get_ui()) - { - case ui_message_handlert::uit::PLAIN: - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml("cprover-status"); - xml.data = "FAILURE"; - msg.result() << xml; - } - break; - - case ui_message_handlert::uit::JSON_UI: - { - json_objectt json_result; - json_result["cProverStatus"] = json_stringt("failure"); - msg.result() << json_result; - } - break; - } -} diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 8d73ced8fc2..8ccb81e7df7 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -32,9 +32,6 @@ void convert_symex_target_equation( prop_convt &, message_handlert &); -void report_failure(ui_message_handlert &); -void report_success(ui_message_handlert &); - void build_error_trace( goto_tracet &, const namespacet &, diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index 2e92e33d6d2..880db5ebe78 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -17,6 +17,62 @@ Author: Daniel Kroening, Peter Schrammel #include #include +void report_success(ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom; + + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + break; + + case ui_message_handlert::uit::XML_UI: + { + xmlt xml("cprover-status"); + xml.data = "SUCCESS"; + msg.result() << xml; + } + break; + + case ui_message_handlert::uit::JSON_UI: + { + json_objectt json_result; + json_result["cProverStatus"] = json_stringt("success"); + msg.result() << json_result; + } + break; + } +} + +void report_failure(ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + msg.result() << "VERIFICATION FAILED" << messaget::eom; + + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + break; + + case ui_message_handlert::uit::XML_UI: + { + xmlt xml("cprover-status"); + xml.data = "FAILURE"; + msg.result() << xml; + } + break; + + case ui_message_handlert::uit::JSON_UI: + { + json_objectt json_result; + json_result["cProverStatus"] = json_stringt("failure"); + msg.result() << json_result; + } + break; + } +} + void output_properties( const propertiest &properties, ui_message_handlert &ui_message_handler) diff --git a/src/goto-checker/report_util.h b/src/goto-checker/report_util.h index b15de8a617e..16b39580015 100644 --- a/src/goto-checker/report_util.h +++ b/src/goto-checker/report_util.h @@ -16,6 +16,9 @@ Author: Daniel Kroening, Peter Schrammel class ui_message_handlert; +void report_success(ui_message_handlert &); +void report_failure(ui_message_handlert &); + void output_properties( const propertiest &properties, ui_message_handlert &ui_message_handler); From 0ba08336605b62ed170a208d672270863080b07f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 21:10:50 +0000 Subject: [PATCH 5/7] Add report_error and report_inconclusive to report_util --- src/goto-checker/report_util.cpp | 56 ++++++++++++++++++++++++++++++++ src/goto-checker/report_util.h | 2 ++ 2 files changed, 58 insertions(+) diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index 880db5ebe78..1b325f4684c 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -73,6 +73,62 @@ void report_failure(ui_message_handlert &ui_message_handler) } } +void report_inconclusive(ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + msg.result() << "VERIFICATION INCONCLUSIVE" << messaget::eom; + + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + break; + + case ui_message_handlert::uit::XML_UI: + { + xmlt xml("cprover-status"); + xml.data = "INCONCLUSIVE"; + msg.result() << xml; + } + break; + + case ui_message_handlert::uit::JSON_UI: + { + json_objectt json_result; + json_result["cProverStatus"] = json_stringt("inconclusive"); + msg.result() << json_result; + } + break; + } +} + +void report_error(ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + msg.result() << "VERIFICATION ERROR" << messaget::eom; + + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + break; + + case ui_message_handlert::uit::XML_UI: + { + xmlt xml("cprover-status"); + xml.data = "ERROR"; + msg.result() << xml; + } + break; + + case ui_message_handlert::uit::JSON_UI: + { + json_objectt json_result; + json_result["cProverStatus"] = json_stringt("error"); + msg.result() << json_result; + } + break; + } +} + void output_properties( const propertiest &properties, ui_message_handlert &ui_message_handler) diff --git a/src/goto-checker/report_util.h b/src/goto-checker/report_util.h index 16b39580015..1083446f7ed 100644 --- a/src/goto-checker/report_util.h +++ b/src/goto-checker/report_util.h @@ -18,6 +18,8 @@ class ui_message_handlert; void report_success(ui_message_handlert &); void report_failure(ui_message_handlert &); +void report_inconclusive(ui_message_handlert &); +void report_error(ui_message_handlert &); void output_properties( const propertiest &properties, From 02bc6905e3e09bced715e219e4b1f9fc08b6e5ab Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 21:05:21 +0000 Subject: [PATCH 6/7] Add result_to_exit_code Enable consistent result-dependent exit codes across all driver programs. --- src/goto-checker/properties.cpp | 17 +++++++++++++++++ src/goto-checker/properties.h | 2 ++ 2 files changed, 19 insertions(+) diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 321e3d465cf..7996102a15e 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel #include "properties.h" +#include #include #include #include @@ -116,6 +117,22 @@ json(const irep_idt &property_id, const property_infot &property_info) return result; } +int result_to_exit_code(resultt result) +{ + switch(result) + { + case resultt::PASS: + return CPROVER_EXIT_VERIFICATION_SAFE; + case resultt::FAIL: + return CPROVER_EXIT_VERIFICATION_UNSAFE; + case resultt::ERROR: + return CPROVER_EXIT_INTERNAL_ERROR; + case resultt::UNKNOWN: + return CPROVER_EXIT_VERIFICATION_INCONCLUSIVE; + } + UNREACHABLE; +} + 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 134257396ef..6bc5b49a81f 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -84,6 +84,8 @@ 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); +int result_to_exit_code(resultt result); + /// Return the number of properties with given \p status std::size_t count_properties(const propertiest &, property_statust); From b1587fa769a761eb8844eb4acec15825b6bc0de9 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 18:44:57 +0000 Subject: [PATCH 7/7] Utility for printing overall result Enable consistent overall status reporting across all driver programs. --- src/goto-checker/report_util.cpp | 21 +++++++++++++++++++++ src/goto-checker/report_util.h | 4 ++++ 2 files changed, 25 insertions(+) diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index 1b325f4684c..6123f7907b1 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -240,3 +240,24 @@ void output_properties( } } } + +void output_overall_result( + resultt result, + ui_message_handlert &ui_message_handler) +{ + switch(result) + { + case resultt::PASS: + report_success(ui_message_handler); + break; + case resultt::FAIL: + report_failure(ui_message_handler); + break; + case resultt::UNKNOWN: + report_inconclusive(ui_message_handler); + break; + case resultt::ERROR: + report_error(ui_message_handler); + break; + } +} diff --git a/src/goto-checker/report_util.h b/src/goto-checker/report_util.h index 1083446f7ed..df3dbd97c2b 100644 --- a/src/goto-checker/report_util.h +++ b/src/goto-checker/report_util.h @@ -25,4 +25,8 @@ void output_properties( const propertiest &properties, ui_message_handlert &ui_message_handler); +void output_overall_result( + resultt result, + ui_message_handlert &ui_message_handler); + #endif // CPROVER_GOTO_CHECKER_REPORT_UTIL_H