From cc1a90e4b825d0969b9e423feb1a7e91fc488ccd Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 21:13:52 +0000 Subject: [PATCH 01/10] 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 02/10] 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 03/10] 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 04/10] 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 05/10] 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 06/10] 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 07/10] 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 From 3c2778e5654d5af74bda0826f587c581b7fa50d1 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 13 Jan 2019 20:25:53 +0000 Subject: [PATCH 08/10] Add functions to combine property results Used to update the properties map and to compute the overall result. --- src/goto-checker/properties.cpp | 97 +++++++++++++++++++++++++++++++++ src/goto-checker/properties.h | 4 ++ 2 files changed, 101 insertions(+) diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 7996102a15e..5da5e4b681e 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -144,3 +144,100 @@ count_properties(const propertiest &properties, property_statust status) } return count; } + +/// 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 6bc5b49a81f..f07f4749253 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -89,4 +89,8 @@ 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); +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 From 4b559625878126a49722182c0a966b0a9d9578b0 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 15:54:43 +0000 Subject: [PATCH 09/10] Add has_properties_to_check --- src/goto-checker/properties.cpp | 16 ++++++++++++++++ src/goto-checker/properties.h | 6 ++++++ 2 files changed, 22 insertions(+) diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 5da5e4b681e..58de8528ba1 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -145,6 +145,22 @@ count_properties(const propertiest &properties, property_statust status) 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 diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index f07f4749253..8fb4ecd1287 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -89,6 +89,12 @@ 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); From c61ca64c9a558eb892e59ffb04b60091153aac93 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 21:05:40 +0000 Subject: [PATCH 10/10] Add all_properties_verifier This will replace bmc_all_propertiest. --- src/goto-checker/all_properties_verifier.h | 61 ++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 src/goto-checker/all_properties_verifier.h 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