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/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/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/properties.cpp b/src/goto-checker/properties.cpp index 704891a1720..7996102a15e 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -11,7 +11,10 @@ Author: Daniel Kroening, Peter Schrammel #include "properties.h" +#include #include +#include +#include std::string as_string(resultt result) { @@ -88,3 +91,56 @@ 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; +} + +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) +{ + 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..6bc5b49a81f 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,4 +76,17 @@ 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); + +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); + #endif // CPROVER_GOTO_CHECKER_PROPERTIES_H diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp new file mode 100644 index 00000000000..6123f7907b1 --- /dev/null +++ b/src/goto-checker/report_util.cpp @@ -0,0 +1,263 @@ +/*******************************************************************\ + +Module: Bounded Model Checking Utilities + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Bounded Model Checking Utilities + +#include "report_util.h" + +#include + +#include +#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 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) +{ + 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; + } + } +} + +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 new file mode 100644 index 00000000000..df3dbd97c2b --- /dev/null +++ b/src/goto-checker/report_util.h @@ -0,0 +1,32 @@ +/*******************************************************************\ + +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 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, + 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