From 99018178a9296432ca46ba851c45198f2ab78402 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 22:08:15 +0000 Subject: [PATCH 1/6] Add stop-on-fail verifier Stops verification when the first property violation is found. --- src/goto-checker/stop_on_fail_verifier.h | 79 ++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 src/goto-checker/stop_on_fail_verifier.h diff --git a/src/goto-checker/stop_on_fail_verifier.h b/src/goto-checker/stop_on_fail_verifier.h new file mode 100644 index 00000000000..6c3d760d347 --- /dev/null +++ b/src/goto-checker/stop_on_fail_verifier.h @@ -0,0 +1,79 @@ +/*******************************************************************\ + +Module: Goto Verifier for stopping at the first failing property + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Verifier for stopping at the first failing property + +#ifndef CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H +#define CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H + +#include "bmc_util.h" +#include "goto_verifier.h" + +/// Stops when the first failing property is found. +/// Requires an incremental goto checker that is a +/// `goto_trace_providert` and `witness_providert`. +template +class stop_on_fail_verifiert : public goto_verifiert +{ +public: + stop_on_fail_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 = std::move(initialize_properties(goto_model)); + } + + resultt operator()() override + { + (void)incremental_goto_checker(properties); + return determine_result(properties); + } + + void report() override + { + switch(determine_result(properties)) + { + case resultt::PASS: + report_success(ui_message_handler); + incremental_goto_checker.output_proof(); + break; + + case resultt::FAIL: + { + goto_tracet goto_trace = incremental_goto_checker.build_trace(); + output_error_trace( + goto_trace, + incremental_goto_checker.get_namespace(), + trace_optionst(options), + ui_message_handler); + report_failure(ui_message_handler); + incremental_goto_checker.output_error_witness(goto_trace); + break; + } + + case resultt::UNKNOWN: + report_inconclusive(ui_message_handler); + break; + + case resultt::ERROR: + report_error(ui_message_handler); + break; + } + } + +protected: + abstract_goto_modelt &goto_model; + incremental_goto_checkerT incremental_goto_checker; +}; + +#endif // CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H From 2e84e22abe6b9d1ece3566ecfdfe0ff51076ca28 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 22:09:05 +0000 Subject: [PATCH 2/6] Use goto verifier for stop-on-fail in CBMC This was previously one of the bmct modes. Now it is a separate goto verifier. --- src/cbmc/cbmc_parse_options.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 7dbca0d1164..e121b89c4aa 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -38,6 +39,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -568,7 +570,13 @@ int cbmc_parse_optionst::doit() if(!options.get_bool_option("paths") && !options.is_set("cover")) { - if(!options.get_bool_option("stop-on-fail")) + if(options.get_bool_option("stop-on-fail")) + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } + else { verifier = util_make_unique< all_properties_verifier_with_trace_storaget>( From dc6a46c2c1c771513f287d68ced4ab3fd09fb42e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 22:09:48 +0000 Subject: [PATCH 3/6] Use goto verifier for stop-on-fail in JBMC This used to be one of the bmct modes; now it is a separate goto verifier. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 58c2214b10c..087e9ad06fb 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -19,9 +19,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include -#include #include +#include #include @@ -29,6 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -570,7 +572,13 @@ int jbmc_parse_optionst::doit() if(!options.get_bool_option("paths") && !options.is_set("cover")) { - if(!options.get_bool_option("stop-on-fail")) + if(options.get_bool_option("stop-on-fail")) + { + verifier = util_make_unique< + stop_on_fail_verifiert>( + options, ui_message_handler, goto_model); + } + else { verifier = util_make_unique>( From 9ad2f6c956d187ead18694bad0a15138c670f1a8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 22:53:13 +0000 Subject: [PATCH 4/6] Use goto verifier for dimacs and SMT2 outfile in CBMC These were special bmct modes. These modes call prop_convts that don't call an actual solver but just output the formula. This behaviour is only supported with --stop-on-fail; hence, we use the stop-on-fail verifier now. --- src/cbmc/cbmc_parse_options.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e121b89c4aa..1557a727fde 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -566,9 +566,23 @@ int cbmc_parse_optionst::doit() } } + if( + options.get_bool_option("dimacs") || !options.get_option("outfile").empty()) + { + if(!options.get_bool_option("paths")) + { + stop_on_fail_verifiert verifier( + options, ui_message_handler, goto_model); + (void)verifier(); + return CPROVER_EXIT_SUCCESS; + } + } + std::unique_ptr verifier = nullptr; - if(!options.get_bool_option("paths") && !options.is_set("cover")) + if( + !options.get_bool_option("paths") && !options.is_set("cover") && + !options.get_bool_option("dimacs") && options.get_option("outfile").empty()) { if(options.get_bool_option("stop-on-fail")) { From 1e0323e8f0962c823264a8e4b290cdd9a0b5c0d3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 22:54:47 +0000 Subject: [PATCH 5/6] Use goto verifier for dimacs and SMT2 outfile in JBMC These were special bmct modes. These modes call prop_convts that don't call an actual solver but just output the formula. This behaviour is only supported with --stop-on-fail; hence, we use the stop-on-fail verifier now. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 087e9ad06fb..28c0ab81a9c 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -568,9 +568,25 @@ int jbmc_parse_optionst::doit() } } + if( + options.get_bool_option("dimacs") || + !options.get_option("outfile").empty()) + { + if(!options.get_bool_option("paths")) + { + stop_on_fail_verifiert verifier( + options, ui_message_handler, goto_model); + (void)verifier(); + return CPROVER_EXIT_SUCCESS; + } + } + std::unique_ptr verifier = nullptr; - if(!options.get_bool_option("paths") && !options.is_set("cover")) + if( + !options.get_bool_option("paths") && !options.is_set("cover") && + !options.get_bool_option("dimacs") && + options.get_option("outfile").empty()) { if(options.get_bool_option("stop-on-fail")) { From 3b71199efa9d5be8f3e7daefc54e64aaf8631f71 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 31 Jan 2019 21:12:20 +0000 Subject: [PATCH 6/6] Amend goto-checker docs w.r.t. stop-on-fail goto verifier --- src/goto-checker/README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/goto-checker/README.md b/src/goto-checker/README.md index 13ef62e2ad7..1f4f062d184 100644 --- a/src/goto-checker/README.md +++ b/src/goto-checker/README.md @@ -51,6 +51,9 @@ The combination of these three concepts enables: without impacting others. There are the following variants of goto verifiers at the moment: +* \ref stop_on_fail_verifiert : Checks all properties, but terminates + as soon as the first violated property is found and reports this violation. + A trace ends at a violated property. * \ref all_properties_verifier_with_trace_storaget : Determines the status of all properties and outputs results when the verification algorithm has terminated. A trace ends at a violated property.