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/all_properties_verifier.h b/src/goto-checker/all_properties_verifier.h new file mode 100644 index 00000000000..391da10d977 --- /dev/null +++ b/src/goto-checker/all_properties_verifier.h @@ -0,0 +1,61 @@ +/*******************************************************************\ + +Module: Goto Verifier for Verifying all Properties + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Verifier for Verifying all Properties + +#ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H +#define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H + +#include "goto_verifier.h" + +#include "incremental_goto_checker.h" +#include "properties.h" +#include "report_util.h" + +template +class all_properties_verifiert : public goto_verifiert +{ +public: + all_properties_verifiert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : goto_verifiert(options, ui_message_handler), + goto_model(goto_model), + incremental_goto_checker(options, ui_message_handler, goto_model) + { + properties = initialize_properties(goto_model); + } + + resultt operator()() override + { + // have we got anything to check? otherwise we return PASS + if(!has_properties_to_check(properties)) + return resultt::PASS; + + while(incremental_goto_checker(properties) != + incremental_goto_checkert::resultt::DONE) + { + // loop until we are done + } + return determine_result(properties); + } + + void report() override + { + output_properties(properties, ui_message_handler); + output_overall_result(determine_result(properties), ui_message_handler); + } + +protected: + abstract_goto_modelt &goto_model; + incremental_goto_checkerT incremental_goto_checker; +}; + +#endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_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/properties.cpp b/src/goto-checker/properties.cpp index 704891a1720..58de8528ba1 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,169 @@ 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; +} + +bool is_property_to_check(property_statust status) +{ + return status == property_statust::NOT_CHECKED || + status == property_statust::UNKNOWN; +} + +bool has_properties_to_check(const propertiest &properties) +{ + for(const auto &property_pair : properties) + { + if(is_property_to_check(property_pair.second.status)) + return true; + } + return false; +} + +/// Update with the preference order +/// 1. old non-UNKNOWN/non-NOT_CHECKED status +/// 2. new non-UNKNOWN/non-NOT_CHECKED status +/// 3. UNKNOWN +/// 4. NOT_CHECKED +/// Suitable for updating property status +property_statust &operator|=(property_statust &a, property_statust const &b) +{ + // non-monotonic use is likely a bug + PRECONDITION( + a == property_statust::NOT_CHECKED || + (a == property_statust::UNKNOWN && b != property_statust::NOT_CHECKED) || + a == b); + switch(a) + { + case property_statust::NOT_CHECKED: + case property_statust::UNKNOWN: + a = b; + return a; + case property_statust::ERROR: + case property_statust::PASS: + case property_statust::NOT_REACHABLE: + case property_statust::FAIL: + return a; + } + UNREACHABLE; +} + +/// Update with the preference order +/// 1. ERROR +/// 2. FAIL +/// 3. UNKNOWN +/// 4. NOT_CHECKED +/// 5. NOT_REACHABLE +/// 6. PASS +/// Suitable for computing overall results +property_statust &operator&=(property_statust &a, property_statust const &b) +{ + switch(a) + { + case property_statust::ERROR: + a = b; + return a; + case property_statust::FAIL: + a = (b == property_statust::ERROR ? b : a); + return a; + case property_statust::UNKNOWN: + a = (b == property_statust::ERROR || b == property_statust::FAIL ? b : a); + return a; + case property_statust::NOT_CHECKED: + a = + (b != property_statust::PASS && b != property_statust::NOT_REACHABLE ? b + : a); + return a; + case property_statust::NOT_REACHABLE: + a = (b != property_statust::PASS ? b : a); + return a; + case property_statust::PASS: + a = (b == property_statust::PASS ? a : b); + return a; + } + UNREACHABLE; +} + +/// Determines the overall result corresponding from the given properties +/// That is PASS if all properties are PASS or NOT_CHECKED, +/// FAIL if at least one property is FAIL and no property is ERROR, +/// UNKNOWN if no property is FAIL or ERROR and +/// at least one property is UNKNOWN, +/// ERROR if at least one property is error. +resultt determine_result(const propertiest &properties) +{ + property_statust status = property_statust::PASS; + for(const auto &property_pair : properties) + { + status &= property_pair.second.status; + } + switch(status) + { + case property_statust::NOT_CHECKED: + // If we have unchecked properties then we don't know. + return resultt::UNKNOWN; + case property_statust::UNKNOWN: + return resultt::UNKNOWN; + case property_statust::NOT_REACHABLE: + // If a property is not reachable then overall it's still a PASS. + return resultt::PASS; + case property_statust::PASS: + return resultt::PASS; + case property_statust::FAIL: + return resultt::FAIL; + case property_statust::ERROR: + return resultt::ERROR; + } + UNREACHABLE; +} diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index 11050f24d8e..8fb4ecd1287 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,27 @@ 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); + +/// Return true if the status is NOT_CHECKED or UNKNOWN +bool is_property_to_check(property_statust); + +/// Return true if there as a property with NOT_CHECKED or UNKNOWN status +bool has_properties_to_check(const propertiest &properties); + +property_statust &operator|=(property_statust &, property_statust const &); +property_statust &operator&=(property_statust &, property_statust const &); +resultt determine_result(const propertiest &properties); + #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