diff --git a/jbmc/src/java_bytecode/java_multi_path_symex_checker.h b/jbmc/src/java_bytecode/java_multi_path_symex_checker.h new file mode 100644 index 00000000000..c36a89065c8 --- /dev/null +++ b/jbmc/src/java_bytecode/java_multi_path_symex_checker.h @@ -0,0 +1,32 @@ +/*******************************************************************\ + +Module: Goto Checker using Bounded Model Checking for Java + +Author: Daniel Kroening, Peter Schrammel + + \*******************************************************************/ + +/// \file +/// Goto Checker using Bounded Model Checking for Java + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H +#define CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H + +#include + +#include "java_bmc_util.h" + +class java_multi_path_symex_checkert : public multi_path_symex_checkert +{ +public: + java_multi_path_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : multi_path_symex_checkert(options, ui_message_handler, goto_model) + { + java_setup_symex(options, goto_model, symex); + } +}; + +#endif // CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index 0e85a394f16..166b21616cf 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -41,7 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \ - ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \ # Empty last line diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index e9ee849d176..58c2214b10c 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -61,6 +62,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -564,13 +566,30 @@ int jbmc_parse_optionst::doit() } } - // The `configure_bmc` callback passed will enable enum-unwind-static if - // applicable. - return bmct::do_language_agnostic_bmc( - options, - goto_model, - ui_message_handler, - configure_bmc); + std::unique_ptr verifier = nullptr; + + if(!options.get_bool_option("paths") && !options.is_set("cover")) + { + if(!options.get_bool_option("stop-on-fail")) + { + verifier = util_make_unique>( + options, ui_message_handler, goto_model); + } + } + + // fall back until everything has been ported to goto-checker + if(verifier == nullptr) + { + // The `configure_bmc` callback passed will enable enum-unwind-static if + // applicable. + return bmct::do_language_agnostic_bmc( + options, goto_model, ui_message_handler, configure_bmc); + } + + resultt result = (*verifier)(); + verifier->report(); + return result_to_exit_code(result); } else { diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index b060ca349d3..3c4e5bd57de 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -86,7 +86,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \ - $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \ $(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \ @@ -131,6 +130,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \ $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ $(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \ + $(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \ $(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \ $(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \ $(BMC_DEPS) \ diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc index 050f2fd2d15..6a638d1e767 100644 --- a/regression/cbmc/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc @@ -3,8 +3,8 @@ main.c --unwind 3 --no-unwinding-assertions ^EXIT=10$ ^SIGNAL=0$ -^\[main\.assertion\.1\] .* : SUCCESS$ -^\[main\.assertion\.2\] .* : FAILURE$ +^\[main\.assertion\.1\] .*: SUCCESS$ +^\[main\.assertion\.2\] .*: FAILURE$ ^\*\* 1 of 2 failed -- ^warning: ignoring diff --git a/regression/cbmc/goto4/test.desc b/regression/cbmc/goto4/test.desc index 961ee72a83b..a38a3191f53 100644 --- a/regression/cbmc/goto4/test.desc +++ b/regression/cbmc/goto4/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[.*] line 5 assertion g == 0: SUCCESS$ -^\[.*] unwinding assertion loop 0: FAILURE$ +^\[.*] line 14 unwinding assertion loop 0: FAILURE$ -- ^warning: ignoring diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc index 20a7e46f099..908ec83b393 100644 --- a/regression/contracts/function_check_04/test.desc +++ b/regression/contracts/function_check_04/test.desc @@ -2,7 +2,7 @@ CORE main.c --apply-code-contracts ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$ -^\[foo.1\] line 9 : FAILURE$ +^\[foo.1\] line 9 .*: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 4ce2be97bab..17b0f86b0ef 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -4,7 +4,6 @@ SRC = all_properties.cpp \ cbmc_languages.cpp \ cbmc_main.cpp \ cbmc_parse_options.cpp \ - counterexample_beautification.cpp \ fault_localization.cpp \ xml_interface.cpp \ # Empty last line diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 11cdc1e468d..8794b1d6aa5 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -25,10 +25,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include -#include "counterexample_beautification.h" #include "fault_localization.h" /// Hook used by CEGIS to selectively freeze variables diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 26ff8e7f573..7dbca0d1164 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -33,7 +33,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include +#include #include #include @@ -562,8 +564,28 @@ int cbmc_parse_optionst::doit() } } - return bmct::do_language_agnostic_bmc( - options, goto_model, ui_message_handler); + std::unique_ptr verifier = nullptr; + + if(!options.get_bool_option("paths") && !options.is_set("cover")) + { + if(!options.get_bool_option("stop-on-fail")) + { + verifier = util_make_unique< + all_properties_verifier_with_trace_storaget>( + options, ui_message_handler, goto_model); + } + } + + // fall back until everything has been ported to goto-checker + if(verifier == nullptr) + { + return bmct::do_language_agnostic_bmc( + options, goto_model, ui_message_handler); + } + + resultt result = (*verifier)(); + verifier->report(); + return result_to_exit_code(result); } bool cbmc_parse_optionst::set_properties() diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index 56a7dcc241f..b5ffd603490 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -24,12 +24,13 @@ Author: Peter Schrammel #include #include + #include #include +#include #include -#include "counterexample_beautification.h" void fault_localizationt::freeze_guards() { diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index cc295d54732..da5ce406e31 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -1,6 +1,9 @@ SRC = bmc_util.cpp \ + counterexample_beautification.cpp \ incremental_goto_checker.cpp \ + goto_trace_storage.cpp \ goto_verifier.cpp \ + multi_path_symex_checker.cpp \ multi_path_symex_only_checker.cpp \ properties.cpp \ report_util.cpp \ diff --git a/src/goto-checker/README.md b/src/goto-checker/README.md new file mode 100644 index 00000000000..13ef62e2ad7 --- /dev/null +++ b/src/goto-checker/README.md @@ -0,0 +1,74 @@ +\ingroup module_hidden +\defgroup goto-checker goto-checker + +# Folder goto-checker + +\author Peter Schrammel + +The \ref goto-checker directory contains interfaces for the verification of +goto-programs. + +There are three main concepts: +* Property +* Goto Verifier +* Incremental Goto Checker + +A property has a `property_id` and identifies an assertion that is either +part of the goto model or generated in the course of executing the verification +algorithm. A verification algorithm determines the `status` of a property, +i.e. whether the property has passed verification, failed, is yet to be +analyzed, etc. See \ref property_infot. + +A goto verifier aims at determining and reporting +the status of all or some of the properties, _independently_ of the +actual verification algorithm (e.g. path-merging symbolic execution, +path-wise symbolic execution, abstract interpretation). +See \ref goto_verifiert. + +An incremental goto checker is used by a goto verifier to execute the +verification algorithm. Incremental goto checkers keep the state of the +analysis and can be queried by the goto verifier repeatedly to return +their results incrementally. A query to an incremental goto checker +either returns when a violated property has been found or the +verification algorithm has terminated. If a violated property has been +found then additional information (e.g. a trace) can be retrieved +from the incremental goto checker (if it supports that). +See \ref incremental_goto_checkert. + +The combination of these three concepts enables: +* _Verification algorithms can be used interchangeably._ + There is a single, small interface for our verification engines. +* _Verification results reporting is uniform across all engines._ + Downstream tools can use the reporting output without knowing + which verification algorithm was at work. +* _Building variants of verification engines becomes easy._ + Goto verifier and incremental goto checker implementations are built from + small building blocks. It should therefore be easy to build variants + by implementing these interfaces instead of hooking into a monolithic engine. +* _The code becomes easier to maintain._ + There are N things that do one thing each rather than one thing that does + N things. New variants of verification algorithms can be added and removed + without impacting others. + +There are the following variants of goto verifiers at the moment: +* \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. +* \ref all_properties_verifiert : Determines the status of all properties and + outputs verification results incrementally. In contrast to + \ref all_properties_verifier_with_trace_storaget, + \ref all_properties_verifiert does not require to store any traces. + A trace ends at a violated property. + +There are the following variants of incremental goto checkers at the moment: +* \ref multi_path_symex_checkert : The default mode of goto-symex. It explores + all paths and applies aggressive path merging to generate a formula + (aka 'equation') that is passed to the SAT/SMT solver. It supports + determining the status of all properties, but not adding new properties + after the first invocation. +* \ref multi_path_symex_only_checkert : Same as \ref multi_path_symex_checkert, + but does not call the SAT/SMT solver. It can only decide the status of + properties by the simplifications that goto-symex performs. +* There are variants for Java that perform a Java-specific preprocessing: + \ref java_multi_path_symex_checkert, + \ref java_multi_path_symex_only_checkert diff --git a/src/goto-checker/all_properties_verifier.h b/src/goto-checker/all_properties_verifier.h index 4c65fe3b2ad..8462a845d0e 100644 --- a/src/goto-checker/all_properties_verifier.h +++ b/src/goto-checker/all_properties_verifier.h @@ -43,19 +43,21 @@ class all_properties_verifiert : public goto_verifiert incremental_goto_checkert::resultt::progresst::DONE) { // loop until we are done + ++iterations; } return determine_result(properties); } void report() override { - output_properties(properties, ui_message_handler); + output_properties(properties, iterations, ui_message_handler); output_overall_result(determine_result(properties), ui_message_handler); } protected: abstract_goto_modelt &goto_model; incremental_goto_checkerT incremental_goto_checker; + std::size_t iterations = 1; }; #endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H diff --git a/src/goto-checker/all_properties_verifier_with_trace_storage.h b/src/goto-checker/all_properties_verifier_with_trace_storage.h new file mode 100644 index 00000000000..30c0f8e9d0c --- /dev/null +++ b/src/goto-checker/all_properties_verifier_with_trace_storage.h @@ -0,0 +1,82 @@ +/*******************************************************************\ + +Module: Goto Verifier for Verifying all Properties that stores Traces + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto verifier for verifying all properties that stores traces + +#ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H +#define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H + +#include "goto_verifier.h" + +#include "goto_trace_storage.h" +#include "incremental_goto_checker.h" +#include "properties.h" +#include "report_util.h" + +template +class all_properties_verifier_with_trace_storaget : public goto_verifiert +{ +public: + all_properties_verifier_with_trace_storaget( + 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), + traces(incremental_goto_checker.get_namespace()) + { + properties = initialize_properties(goto_model); + } + + resultt operator()() override + { + while(incremental_goto_checker(properties).progress != + incremental_goto_checkert::resultt::progresst::DONE) + { + // we've got an error trace; store it and link it to the failed properties + (void)traces.insert(incremental_goto_checker.build_trace()); + + ++iterations; + } + + return determine_result(properties); + } + + void report() override + { + if( + options.get_bool_option("trace") || + // currently --trace only affects plain text output + ui_message_handler.get_ui() != ui_message_handlert::uit::PLAIN) + { + const trace_optionst trace_options(options); + output_properties_with_traces( + properties, traces, trace_options, iterations, ui_message_handler); + } + else + { + output_properties(properties, iterations, ui_message_handler); + } + output_overall_result(determine_result(properties), ui_message_handler); + } + + const goto_trace_storaget &get_traces() const + { + return traces; + } + +protected: + abstract_goto_modelt &goto_model; + incremental_goto_checkerT incremental_goto_checker; + std::size_t iterations = 1; + goto_trace_storaget traces; +}; + +#endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index fc0fcb2f2d6..3389f086505 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -218,23 +218,21 @@ void slice( << " remaining after simplification" << messaget::eom; } -std::vector update_properties_status_from_symex_target_equation( +void update_properties_status_from_symex_target_equation( propertiest &properties, + std::unordered_set &updated_properties, const symex_target_equationt &equation) { - std::vector updated_properties; - for(const auto &step : equation.SSA_steps) { if(!step.is_assert()) continue; irep_idt property_id = step.get_property_id(); + CHECK_RETURN(!property_id.empty()); - if(property_id.empty()) - continue; - - // Don't set false properties; we wouldn't have traces for them. + // Don't update status of properties that are constant 'false'; + // we wouldn't have traces for them. const auto status = step.cond_expr.is_true() ? property_statust::PASS : property_statust::UNKNOWN; auto emplace_result = properties.emplace( @@ -242,7 +240,7 @@ std::vector update_properties_status_from_symex_target_equation( if(emplace_result.second) { - updated_properties.push_back(property_id); + updated_properties.insert(property_id); } else { @@ -251,10 +249,15 @@ std::vector update_properties_status_from_symex_target_equation( property_info.status |= status; if(property_info.status != old_status) - updated_properties.push_back(property_id); + updated_properties.insert(property_id); } } +} +void update_status_of_not_checked_properties( + propertiest &properties, + std::unordered_set &updated_properties) +{ for(auto &property_pair : properties) { if(property_pair.second.status == property_statust::NOT_CHECKED) @@ -262,9 +265,7 @@ std::vector update_properties_status_from_symex_target_equation( // This could be a NOT_CHECKED, NOT_REACHABLE or PASS, // but the equation doesn't give us precise information. property_pair.second.status = property_statust::PASS; - updated_properties.push_back(property_pair.first); + updated_properties.insert(property_pair.first); } } - - return updated_properties; } diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index b8e85a6effb..abe0a6b9e17 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -70,12 +70,26 @@ void slice( ui_message_handlert &); /// Sets property status to PASS for properties whose -/// conditions are constant true. -/// \return IDs of updated properties -std::vector update_properties_status_from_symex_target_equation( +/// conditions are constant true in the \p equation. +/// \param [inout] properties: The status is updated in this data structure +/// \param [inout] updated_properties: The set of property IDs of +/// updated properties +/// \param equation: A equation generated by goto-symex +void update_properties_status_from_symex_target_equation( propertiest &properties, + std::unordered_set &updated_properties, const symex_target_equationt &equation); +/// Sets the property status of NOT_CHECKED properties to PASS. +/// \param [inout] properties: The status is updated in this data structure +/// \param [inout] updated_properties: The IDs of updated properties are +/// added here +/// Note: this should inspect the equation, but the equation doesn't have +/// any useful information at the moment. +void update_status_of_not_checked_properties( + propertiest &properties, + std::unordered_set &updated_properties); + // clang-format off #define OPT_BMC \ "(program-only)" \ diff --git a/src/cbmc/counterexample_beautification.cpp b/src/goto-checker/counterexample_beautification.cpp similarity index 68% rename from src/cbmc/counterexample_beautification.cpp rename to src/goto-checker/counterexample_beautification.cpp index b532512985f..d434a688bf5 100644 --- a/src/cbmc/counterexample_beautification.cpp +++ b/src/goto-checker/counterexample_beautification.cpp @@ -11,13 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com #include "counterexample_beautification.h" -#include #include -#include #include +#include +#include -#include #include +#include void counterexample_beautificationt::get_minimization_list( prop_convt &prop_conv, @@ -26,23 +26,25 @@ void counterexample_beautificationt::get_minimization_list( { // ignore the ones that are assigned under false guards - for(symex_target_equationt::SSA_stepst::const_iterator - it=equation.SSA_steps.begin(); - it!=equation.SSA_steps.end(); it++) + for(symex_target_equationt::SSA_stepst::const_iterator it = + equation.SSA_steps.begin(); + it != equation.SSA_steps.end(); + it++) { - if(it->is_assignment() && - it->assignment_type==symex_targett::assignment_typet::STATE) + if( + it->is_assignment() && + it->assignment_type == symex_targett::assignment_typet::STATE) { if(!prop_conv.l_get(it->guard_literal).is_false()) { - const typet &type=it->ssa_lhs.type(); + const typet &type = it->ssa_lhs.type(); - if(type!=bool_typet()) + if(type != bool_typet()) { // we minimize the absolute value, if applicable - if(type.id()==ID_signedbv || - type.id()==ID_fixedbv || - type.id()==ID_floatbv) + if( + type.id() == ID_signedbv || type.id() == ID_fixedbv || + type.id() == ID_floatbv) { abs_exprt abs_expr(it->ssa_lhs); minimization_list.insert(abs_expr); @@ -54,7 +56,7 @@ void counterexample_beautificationt::get_minimization_list( } // reached failed assertion? - if(it==failed) + if(it == failed) break; } } @@ -66,12 +68,13 @@ counterexample_beautificationt::get_failed_property( { // find failed property - for(symex_target_equationt::SSA_stepst::const_iterator - it=equation.SSA_steps.begin(); - it!=equation.SSA_steps.end(); it++) - if(it->is_assert() && - prop_conv.l_get(it->guard_literal).is_true() && - prop_conv.l_get(it->cond_literal).is_false()) + for(symex_target_equationt::SSA_stepst::const_iterator it = + equation.SSA_steps.begin(); + it != equation.SSA_steps.end(); + it++) + if( + it->is_assert() && prop_conv.l_get(it->guard_literal).is_true() && + prop_conv.l_get(it->cond_literal).is_false()) return it; UNREACHABLE; @@ -89,26 +92,27 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation) boolbv.set_to(literal_exprt(failed->cond_literal), false); { - boolbv.status() << "Beautifying counterexample (guards)" - << messaget::eom; + boolbv.status() << "Beautifying counterexample (guards)" << messaget::eom; // compute weights for guards typedef std::map guard_countt; guard_countt guard_count; - for(symex_target_equationt::SSA_stepst::const_iterator - it=equation.SSA_steps.begin(); - it!=equation.SSA_steps.end(); it++) + for(symex_target_equationt::SSA_stepst::const_iterator it = + equation.SSA_steps.begin(); + it != equation.SSA_steps.end(); + it++) { - if(it->is_assignment() && - it->assignment_type!=symex_targett::assignment_typet::HIDDEN) + if( + it->is_assignment() && + it->assignment_type != symex_targett::assignment_typet::HIDDEN) { if(!it->guard_literal.is_constant()) guard_count[it->guard_literal]++; } // reached failed assertion? - if(it==failed) + if(it == failed) break; } @@ -124,8 +128,7 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation) } { - boolbv.status() << "Beautifying counterexample (values)" - << messaget::eom; + boolbv.status() << "Beautifying counterexample (values)" << messaget::eom; // get symbols we care about minimization_listt minimization_list; diff --git a/src/cbmc/counterexample_beautification.h b/src/goto-checker/counterexample_beautification.h similarity index 72% rename from src/cbmc/counterexample_beautification.h rename to src/goto-checker/counterexample_beautification.h index 9cc96aaf016..5ff4fd25d12 100644 --- a/src/cbmc/counterexample_beautification.h +++ b/src/goto-checker/counterexample_beautification.h @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Counterexample Beautification -#ifndef CPROVER_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H -#define CPROVER_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H +#ifndef CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H +#define CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H #include @@ -25,8 +25,7 @@ class counterexample_beautificationt { } - void - operator()(boolbvt &boolbv, const symex_target_equationt &equation); + void operator()(boolbvt &boolbv, const symex_target_equationt &equation); protected: void get_minimization_list( @@ -34,9 +33,7 @@ class counterexample_beautificationt const symex_target_equationt &equation, minimization_listt &minimization_list); - void minimize( - const exprt &expr, - class prop_minimizet &prop_minimize); + void minimize(const exprt &expr, class prop_minimizet &prop_minimize); symex_target_equationt::SSA_stepst::const_iterator get_failed_property( const prop_convt &prop_conv, @@ -46,4 +43,4 @@ class counterexample_beautificationt symex_target_equationt::SSA_stepst::const_iterator failed; }; -#endif // CPROVER_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H +#endif // CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H diff --git a/src/goto-checker/goto_trace_storage.cpp b/src/goto-checker/goto_trace_storage.cpp new file mode 100644 index 00000000000..7febf158afb --- /dev/null +++ b/src/goto-checker/goto_trace_storage.cpp @@ -0,0 +1,45 @@ +/*******************************************************************\ + +Module: Goto Trace Storage + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Trace Storage + +#include "goto_trace_storage.h" + +goto_trace_storaget::goto_trace_storaget(const namespacet &ns) : ns(ns) +{ +} + +const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace) +{ + traces.push_back(trace); + const auto &last_step = traces.back().get_last_step(); + DATA_INVARIANT( + last_step.is_assert(), "last goto trace step expected to be assertion"); + property_id_to_trace_index.emplace(last_step.property_id, traces.size() - 1); + return traces.back(); +} + +const std::vector &goto_trace_storaget::all() const +{ + return traces; +} + +const goto_tracet &goto_trace_storaget:: +operator[](const irep_idt &property_id) const +{ + const auto trace_found = property_id_to_trace_index.find(property_id); + PRECONDITION(trace_found != property_id_to_trace_index.end()); + + return traces.at(trace_found->second); +} + +const namespacet &goto_trace_storaget::get_namespace() const +{ + return ns; +} diff --git a/src/goto-checker/goto_trace_storage.h b/src/goto-checker/goto_trace_storage.h new file mode 100644 index 00000000000..e8ff75126e0 --- /dev/null +++ b/src/goto-checker/goto_trace_storage.h @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Goto Trace Storage + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Trace Storage + +#ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H +#define CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H + +#include + +class goto_trace_storaget +{ +public: + explicit goto_trace_storaget(const namespacet &); + goto_trace_storaget(const goto_trace_storaget &) = delete; + + const goto_tracet &insert(goto_tracet &&); + + const std::vector &all() const; + const goto_tracet &operator[](const irep_idt &property_id) const; + + const namespacet &get_namespace() const; + +protected: + /// the namespace related to the traces + const namespacet &ns; + + /// stores the traces + std::vector traces; + + // maps property ID to index in traces + std::unordered_map property_id_to_trace_index; +}; + +#endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H diff --git a/src/goto-checker/incremental_goto_checker.cpp b/src/goto-checker/incremental_goto_checker.cpp index 01c17fb7d18..d3ec2c4f021 100644 --- a/src/goto-checker/incremental_goto_checker.cpp +++ b/src/goto-checker/incremental_goto_checker.cpp @@ -20,9 +20,7 @@ incremental_goto_checkert::incremental_goto_checkert( { } -incremental_goto_checkert::resultt::resultt( - progresst progress, - const std::vector &updated_properties) - : progress(progress), updated_properties(updated_properties) +incremental_goto_checkert::resultt::resultt(resultt::progresst progress) + : progress(progress) { } diff --git a/src/goto-checker/incremental_goto_checker.h b/src/goto-checker/incremental_goto_checker.h index 134c1d55a05..ba764f5fbd4 100644 --- a/src/goto-checker/incremental_goto_checker.h +++ b/src/goto-checker/incremental_goto_checker.h @@ -49,20 +49,18 @@ class incremental_goto_checkert DONE }; - progresst progress = progresst::DONE; + progresst progress; + + resultt() = delete; + explicit resultt(progresst); /// Changed properties since the last call to /// `incremental_goto_checkert::operator()` - std::vector updated_properties; - - resultt() = default; - resultt( - progresst progress, - const std::vector &updated_properties); + std::unordered_set updated_properties; }; /// Check whether the given properties with status NOT_CHECKED, UNKNOWN or - /// properties newly discovered by `goto_checkert` hold. + /// properties newly discovered by `incremental_goto_checkert` hold. /// \param [out] properties: Properties updated to whether their status /// have been determined. Newly discovered properties are added. /// \return whether the goto checker found a violated property (FOUND_FAIL) or @@ -73,7 +71,7 @@ class incremental_goto_checkert /// If there is a property with status FAIL then its counterexample /// can be retrieved by calling `build_error_trace` before any /// subsequent call to operator(). - /// `goto_checkert` derivatives shall be implemented in a way such + /// `incremental_goto_checkert` derivatives shall be implemented in a way such /// that repeated calls to operator() shall return when the next FAILed /// property has been found until eventually it does not find any /// failing properties any more. diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp new file mode 100644 index 00000000000..3b8b4073197 --- /dev/null +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -0,0 +1,248 @@ +/*******************************************************************\ + +Module: Goto Checker using Bounded Model Checking + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using Bounded Model Checking + +#include "multi_path_symex_checker.h" + +#include + +#include "bmc_util.h" +#include "counterexample_beautification.h" + +multi_path_symex_checkert::multi_path_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : multi_path_symex_only_checkert(options, ui_message_handler, goto_model), + equation_generated(false) +{ + solver_factoryt solvers( + options, + ns, + ui_message_handler, + ui_message_handler.get_ui() == ui_message_handlert::uit::XML_UI); + solver = solvers.get_solver(); + solver->prop_conv().set_message_handler(ui_message_handler); +} + +incremental_goto_checkert::resultt multi_path_symex_checkert:: +operator()(propertiest &properties) +{ + resultt result(resultt::progresst::DONE); + + // When the equation has been generated, we know all the properties. + // Have we got anything to check? Otherwise we return DONE. + if(equation_generated && !has_properties_to_check(properties)) + return result; + + prop_convt &prop_conv = solver->prop_conv(); + std::chrono::duration solver_runtime(0); + + // we haven't got an equation yet + if(!equation_generated) + { + perform_symex(); + output_coverage_report(); + // This might add new properties such as unwinding assertions, for instance. + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, equation); + // Since we will not symex any further we can decide the status + // of all properties that do not occur in the equation now. + // The current behavior is PASS. + update_status_of_not_checked_properties( + properties, result.updated_properties); + + // Have we got anything to check? Otherwise we return DONE. + if(!has_properties_to_check(properties)) + return result; + + log.status() << "Passing problem to " << prop_conv.decision_procedure_text() + << messaget::eom; + + const auto solver_start = std::chrono::steady_clock::now(); + + convert_symex_target_equation(equation, prop_conv, ui_message_handler); + update_properties_goals_from_symex_target_equation(properties); + convert_goals(); + freeze_goal_variables(); + + const auto solver_stop = std::chrono::steady_clock::now(); + solver_runtime += std::chrono::duration(solver_stop - solver_start); + + log.status() << "Running " << prop_conv.decision_procedure_text() + << messaget::eom; + equation_generated = true; + } + + const auto solver_start = std::chrono::steady_clock::now(); + + add_constraint_from_goals(properties); + + decision_proceduret::resultt dec_result = prop_conv.dec_solve(); + + update_properties_status_from_goals( + properties, result.updated_properties, dec_result); + + const auto solver_stop = std::chrono::steady_clock::now(); + solver_runtime += std::chrono::duration(solver_stop - solver_start); + log.status() << "Runtime decision procedure: " << solver_runtime.count() + << "s" << messaget::eom; + + result.progress = dec_result == decision_proceduret::resultt::D_SATISFIABLE + ? resultt::progresst::FOUND_FAIL + : resultt::progresst::DONE; + return result; +} + +goto_tracet multi_path_symex_checkert::build_trace() const +{ + if(options.get_bool_option("beautify")) + { + counterexample_beautificationt()( + dynamic_cast(solver->prop_conv()), equation); + } + goto_tracet goto_trace; + ::build_error_trace( + goto_trace, ns, equation, solver->prop_conv(), ui_message_handler); + return goto_trace; +} + +const namespacet &multi_path_symex_checkert::get_namespace() const +{ + return ns; +} + +void multi_path_symex_checkert::output_proof() +{ + output_graphml(equation, ns, options); +} + +void multi_path_symex_checkert::output_error_witness( + const goto_tracet &error_trace) +{ + output_graphml(error_trace, ns, options); +} + +exprt multi_path_symex_checkert::goalt::as_expr() const +{ + std::vector tmp; + tmp.reserve(instances.size()); + for(const auto &inst : instances) + tmp.push_back(literal_exprt(inst->cond_literal)); + return conjunction(tmp); +} + +void multi_path_symex_checkert:: + update_properties_goals_from_symex_target_equation(propertiest &properties) +{ + for(symex_target_equationt::SSA_stepst::iterator it = + equation.SSA_steps.begin(); + it != equation.SSA_steps.end(); + ++it) + { + if(it->is_assert()) + { + irep_idt property_id = it->get_property_id(); + CHECK_RETURN(!property_id.empty()); + + // consider goal instance if it is in the given properties + auto property_pair_it = properties.find(property_id); + if( + property_pair_it != properties.end() && + is_property_to_check(property_pair_it->second.status)) + { + // it's going to be checked, but we don't know the status yet + property_pair_it->second.status |= property_statust::UNKNOWN; + goal_map[property_id].instances.push_back(it); + } + } + } +} + +void multi_path_symex_checkert::convert_goals() +{ + for(auto &goal_pair : goal_map) + { + // Our goal is to falsify a property, i.e., we will + // add the negation of the property as goal. + goal_pair.second.condition = + !solver->prop_conv().convert(goal_pair.second.as_expr()); + } +} + +void multi_path_symex_checkert::freeze_goal_variables() +{ + for(const auto &goal_pair : goal_map) + { + if(!goal_pair.second.condition.is_constant()) + solver->prop_conv().set_frozen(goal_pair.second.condition); + } +} + +void multi_path_symex_checkert::add_constraint_from_goals( + const propertiest &properties) +{ + exprt::operandst disjuncts; + + // cover at least one unknown goal + + for(const auto &goal_pair : goal_map) + { + if( + is_property_to_check(properties.at(goal_pair.first).status) && + !goal_pair.second.condition.is_false()) + { + disjuncts.push_back(literal_exprt(goal_pair.second.condition)); + } + } + + // this is 'false' if there are no disjuncts + solver->prop_conv().set_to_true(disjunction(disjuncts)); +} + +void multi_path_symex_checkert::update_properties_status_from_goals( + propertiest &properties, + std::unordered_set &updated_properties, + decision_proceduret::resultt dec_result) +{ + switch(dec_result) + { + case decision_proceduret::resultt::D_SATISFIABLE: + for(auto &goal_pair : goal_map) + { + if(solver->prop_conv().l_get(goal_pair.second.condition).is_true()) + { + properties.at(goal_pair.first).status |= property_statust::FAIL; + updated_properties.insert(goal_pair.first); + } + } + break; + case decision_proceduret::resultt::D_UNSATISFIABLE: + for(auto &property_pair : properties) + { + if(property_pair.second.status == property_statust::UNKNOWN) + { + property_pair.second.status |= property_statust::PASS; + updated_properties.insert(property_pair.first); + } + } + break; + case decision_proceduret::resultt::D_ERROR: + for(auto &property_pair : properties) + { + if(property_pair.second.status == property_statust::UNKNOWN) + { + property_pair.second.status |= property_statust::ERROR; + updated_properties.insert(property_pair.first); + } + } + break; + } +} diff --git a/src/goto-checker/multi_path_symex_checker.h b/src/goto-checker/multi_path_symex_checker.h new file mode 100644 index 00000000000..82675a47554 --- /dev/null +++ b/src/goto-checker/multi_path_symex_checker.h @@ -0,0 +1,95 @@ +/*******************************************************************\ + +Module: Goto Checker using Multi-Path Symbolic Execution + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using Multi-Path Symbolic Execution + +#ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H +#define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H + +#include "goto_trace_provider.h" +#include "multi_path_symex_only_checker.h" +#include "solver_factory.h" +#include "witness_provider.h" + +/// Performs a multi-path symbolic execution using goto-symex +/// and calls a SAT/SMT solver to check the status of the properties. +class multi_path_symex_checkert : public multi_path_symex_only_checkert, + public goto_trace_providert, + public witness_providert +{ +public: + multi_path_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model); + + /// \copydoc incremental_goto_checkert::operator()(propertiest &properties) + /// + /// Note: Repeated invocations of this operator with properties P_1, P_2, ... + /// must satisfy the condition 'P_i contains P_i+1'. + /// I.e. after checking properties P_i the caller may decide to check + /// only a subset of properties P_i+1 in the following invocation, + /// but the caller may not add properties to P_i+1 that have not been + /// in P_i. Such additional properties will be ignored. + resultt operator()(propertiest &) override; + + goto_tracet build_trace() const override; + const namespacet &get_namespace() const override; + + void output_error_witness(const goto_tracet &) override; + void output_proof() override; + +protected: + std::unique_ptr solver; + + struct goalt + { + /// A property holds if all instances of it are true + std::vector instances; + + /// The goal variable + literalt condition; + + exprt as_expr() const; + }; + + /// Maintains the relation between a property ID and + /// the corresponding goal variable that encodes + /// the negation of the conjunction of the instances of the property + std::map goal_map; + + bool equation_generated; + + /// Get the conditions for the properties from the equation + /// and collect all 'instances' of the properties in the `goal_map` + void + update_properties_goals_from_symex_target_equation(propertiest &properties); + + /// Convert the instances of a property into a goal variable + void convert_goals(); + + /// Prevent the solver to optimize-away the goal variables + /// (necessary for incremental solving) + void freeze_goal_variables(); + + /// Add disjunction of negated properties to the equation + void add_constraint_from_goals(const propertiest &properties); + + /// Update the property status from the truth value of the goal variable + /// \param [inout] properties: The status is updated in this data structure + /// \param [inout] updated_properties: The set of property IDs of + /// updated properties + /// \param dec_result: The result returned by the solver + void update_properties_status_from_goals( + propertiest &properties, + std::unordered_set &updated_properties, + decision_proceduret::resultt dec_result); +}; + +#endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index bea03d22eda..89477c97529 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, Peter Schrammel #include -#include +#include #include #include @@ -53,9 +53,15 @@ operator()(propertiest &properties) show_program(ns, equation); } - return resultt( - resultt::progresst::DONE, - update_properties_status_from_symex_target_equation(properties, equation)); + resultt result(resultt::progresst::DONE); + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, equation); + // Since we will not symex any further we can decide the status + // of all properties that do not occur in the equation now. + // The current behavior is PASS. + update_status_of_not_checked_properties( + properties, result.updated_properties); + return result; } void multi_path_symex_only_checkert::perform_symex() diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 26126526b3a..c88a2f91846 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include +#include #include std::string as_string(resultt result) @@ -44,9 +45,9 @@ std::string as_string(property_statust status) case property_statust::NOT_REACHABLE: return "UNREACHABLE"; case property_statust::PASS: - return "PASS"; + return "SUCCESS"; case property_statust::FAIL: - return "FAIL"; + return "FAILURE"; case property_statust::ERROR: return "ERROR"; } @@ -103,16 +104,33 @@ xmlt xml(const irep_idt &property_id, const property_infot &property_info) return xml_result; } -json_objectt -json(const irep_idt &property_id, const property_infot &property_info) +template +static void json( + json_objectT &result, + 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)); +} + +json_objectt +json(const irep_idt &property_id, const property_infot &property_info) +{ + json_objectt result; + json(result, property_id, property_info); return result; } +void json( + json_stream_objectt &result, + const irep_idt &property_id, + const property_infot &property_info) +{ + json(result, property_id, property_info); +} + int result_to_exit_code(resultt result) { switch(result) diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index 8fb4ecd1287..a4ee9cf7303 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, Peter Schrammel #include class json_objectt; +class json_stream_objectt; class xmlt; /// The status of a property @@ -84,6 +85,9 @@ 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); +/// Write the property info into the given JSON stream object +void json(json_stream_objectt &, const irep_idt &, const property_infot &); + int result_to_exit_code(resultt result); /// Return the number of properties with given \p status diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index 6123f7907b1..b5e7424455b 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -17,6 +17,13 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include + +#include +#include + +#include "goto_trace_storage.h" + void report_success(ui_message_handlert &ui_message_handler) { messaget msg(ui_message_handler); @@ -129,8 +136,116 @@ void report_error(ui_message_handlert &ui_message_handler) } } +static void output_single_property_plain( + const irep_idt &property_id, + const property_infot &property_info, + messaget &log, + irep_idt current_file = irep_idt()) +{ + const auto &l = property_info.pc->source_location; + log.result() << messaget::faint << '[' << property_id << "] " + << 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() << property_info.description << ": "; + switch(property_info.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(property_info.status) << messaget::reset + << messaget::eom; +} + +static void +output_properties_plain(const propertiest &properties, messaget &log) +{ + if(properties.empty()) + return; + + 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; + } + } + output_single_property_plain(p->first, p->second, log, current_file); + } +} + +static void output_iterations( + const propertiest &properties, + std::size_t iterations, + messaget &log) +{ + if(properties.empty()) + return; + + log.status() << "\n** " + << count_properties(properties, property_statust::FAIL) << " of " + << properties.size() << " failed (" << iterations + << " iterations)" << messaget::eom; +} + void output_properties( const propertiest &properties, + std::size_t iterations, ui_message_handlert &ui_message_handler) { messaget log(ui_message_handler); @@ -138,91 +253,77 @@ void output_properties( { 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) + output_properties_plain(properties, log); + output_iterations(properties, iterations, log); + break; + } + case ui_message_handlert::uit::XML_UI: + { + for(const auto &property_pair : 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) + 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_properties_with_traces( + const propertiest &properties, + const goto_trace_storaget &traces, + const trace_optionst &trace_options, + std::size_t iterations, + ui_message_handlert &ui_message_handler) +{ + messaget log(ui_message_handler); + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + { + output_properties_plain(properties, log); + for(const auto &property_pair : properties) + { + if(property_pair.second.status == property_statust::FAIL) { - 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() << "\n" + << "Trace for " << property_pair.first << ":" + << "\n"; + show_goto_trace( + log.result(), + traces.get_namespace(), + traces[property_pair.first], + trace_options); + log.result() << messaget::eom; } - 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; + output_iterations(properties, iterations, log); break; } case ui_message_handlert::uit::XML_UI: { for(const auto &property_pair : properties) { - log.result() << xml(property_pair.first, property_pair.second); + xmlt xml_result = xml(property_pair.first, property_pair.second); + if(property_pair.second.status == property_statust::FAIL) + { + convert( + traces.get_namespace(), + traces[property_pair.first], + xml_result.new_element()); + } + log.result() << xml_result; } break; } @@ -234,7 +335,19 @@ void output_properties( json_result.push_back_stream_array("result"); for(const auto &property_pair : properties) { - result_array.push_back(json(property_pair.first, property_pair.second)); + json_stream_objectt &json_property = + result_array.push_back_stream_object(); + json(json_property, property_pair.first, property_pair.second); + if(property_pair.second.status == property_statust::FAIL) + { + json_stream_arrayt &json_trace = + json_property.push_back_stream_array("trace"); + convert( + traces.get_namespace(), + traces[property_pair.first], + json_trace, + trace_options); + } } break; } diff --git a/src/goto-checker/report_util.h b/src/goto-checker/report_util.h index df3dbd97c2b..931ca6da147 100644 --- a/src/goto-checker/report_util.h +++ b/src/goto-checker/report_util.h @@ -14,6 +14,9 @@ Author: Daniel Kroening, Peter Schrammel #include "properties.h" +class goto_trace_storaget; +class goto_tracet; +struct trace_optionst; class ui_message_handlert; void report_success(ui_message_handlert &); @@ -23,6 +26,14 @@ void report_error(ui_message_handlert &); void output_properties( const propertiest &properties, + std::size_t iterations, + ui_message_handlert &ui_message_handler); + +void output_properties_with_traces( + const propertiest &properties, + const goto_trace_storaget &traces, + const trace_optionst &trace_options, + std::size_t iterations, ui_message_handlert &ui_message_handler); void output_overall_result( diff --git a/unit/Makefile b/unit/Makefile index 9da939db1f6..e1c778b5974 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -67,7 +67,7 @@ SRC += analyses/ai/ai.cpp \ util/simplify_expr.cpp \ util/small_map.cpp \ util/small_shared_two_way_ptr.cpp \ - util/std_expr.cpp \ + util/std_expr.cpp \ util/string_utils/split_string.cpp \ util/string_utils/strip_string.cpp \ util/symbol_table.cpp \ @@ -95,7 +95,6 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ ../src/cbmc/bmc_cover$(OBJEXT) \ ../src/cbmc/cbmc_languages$(OBJEXT) \ ../src/cbmc/cbmc_parse_options$(OBJEXT) \ - ../src/cbmc/counterexample_beautification$(OBJEXT) \ ../src/cbmc/fault_localization$(OBJEXT) \ ../src/cbmc/xml_interface$(OBJEXT) \ ../src/goto-instrument/cover$(OBJEXT) \