From b5a482fd97db99cda51025178194ac678cf6a556 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 11 Feb 2019 22:00:08 +0000 Subject: [PATCH 1/5] Helper for building error trace message Produce message in a single place. --- src/goto-checker/bmc_util.cpp | 9 +++++++-- src/goto-checker/bmc_util.h | 3 +++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 158dc54bfc1..4b75157081f 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -32,6 +32,11 @@ Author: Daniel Kroening, Peter Schrammel #include "symex_bmc.h" +void message_building_error_trace(messaget &log) +{ + log.status() << "Building error trace" << messaget::eom; +} + void build_error_trace( goto_tracet &goto_trace, const namespacet &ns, @@ -39,8 +44,8 @@ void build_error_trace( const prop_convt &prop_conv, ui_message_handlert &ui_message_handler) { - messaget msg(ui_message_handler); - msg.status() << "Building error trace" << messaget::eom; + messaget log(ui_message_handler); + message_building_error_trace(log); build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace); } diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 101730072bb..bcc1cb22ebc 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -35,6 +35,9 @@ void convert_symex_target_equation( prop_convt &, message_handlert &); +/// Outputs a message that an error trace is being built +void message_building_error_trace(messaget &); + void build_error_trace( goto_tracet &, const namespacet &, From 21ea8fc074572580d3d007c4886e3a9927c0efb6 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 11 Feb 2019 21:55:51 +0000 Subject: [PATCH 2/5] Function for matching SSA step with property ID to be used in build_goto_trace to truncate traces. --- src/goto-checker/bmc_util.cpp | 11 +++++++++++ src/goto-checker/bmc_util.h | 6 ++++++ 2 files changed, 17 insertions(+) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 4b75157081f..d5d575dc2da 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -50,6 +50,17 @@ void build_error_trace( build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace); } +ssa_step_predicatet +ssa_step_matches_failing_property(const irep_idt &property_id) +{ + return [property_id]( + symex_target_equationt::SSA_stepst::const_iterator step, + const prop_convt &prop_conv) { + return step->is_assert() && step->get_property_id() == property_id && + prop_conv.l_get(step->cond_literal).is_false(); + }; +} + void output_error_trace( const goto_tracet &goto_trace, const namespacet &ns, diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index bcc1cb22ebc..df36406fdf4 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include #include #include "properties.h" @@ -35,6 +36,11 @@ void convert_symex_target_equation( prop_convt &, message_handlert &); +/// Returns a function that checks whether an SSA step is an assertion +/// with \p property_id. Usually used for `build_goto_trace`. +ssa_step_predicatet +ssa_step_matches_failing_property(const irep_idt &property_id); + /// Outputs a message that an error trace is being built void message_building_error_trace(messaget &); From 5929aee5b5637a82982f20b7e52629b104ff85de Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 11 Feb 2019 21:55:07 +0000 Subject: [PATCH 3/5] Extend goto_trace_provider interface to support - full trace for whole SSA - trace for a specific property - trace for the "first" failing property (behavior of stop-on-fail) --- ...l_properties_verifier_with_trace_storage.h | 21 ++++++++--- .../cover_goals_verifier_with_trace_storage.h | 4 ++- src/goto-checker/goto_trace_provider.h | 13 +++++-- src/goto-checker/multi_path_symex_checker.cpp | 34 +++++++++++++++--- src/goto-checker/multi_path_symex_checker.h | 4 ++- .../single_path_symex_checker.cpp | 36 ++++++++++++++++--- src/goto-checker/single_path_symex_checker.h | 4 ++- src/goto-checker/stop_on_fail_verifier.h | 3 +- 8 files changed, 100 insertions(+), 19 deletions(-) diff --git a/src/goto-checker/all_properties_verifier_with_trace_storage.h b/src/goto-checker/all_properties_verifier_with_trace_storage.h index 30c0f8e9d0c..cf83b15cd60 100644 --- a/src/goto-checker/all_properties_verifier_with_trace_storage.h +++ b/src/goto-checker/all_properties_verifier_with_trace_storage.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel #include "goto_verifier.h" +#include "bmc_util.h" #include "goto_trace_storage.h" #include "incremental_goto_checker.h" #include "properties.h" @@ -37,11 +38,23 @@ class all_properties_verifier_with_trace_storaget : public goto_verifiert resultt operator()() override { - while(incremental_goto_checker(properties).progress != - incremental_goto_checkert::resultt::progresst::DONE) + while(true) { - // we've got an error trace; store it and link it to the failed properties - (void)traces.insert(incremental_goto_checker.build_trace()); + const auto result = incremental_goto_checker(properties); + if(result.progress == incremental_goto_checkert::resultt::progresst::DONE) + break; + + // we've got an error trace + message_building_error_trace(log); + for(const auto &property_id : result.updated_properties) + { + if(properties.at(property_id).status == property_statust::FAIL) + { + // get correctly truncated error trace for property and store it + (void)traces.insert( + incremental_goto_checker.build_trace(property_id)); + } + } ++iterations; } diff --git a/src/goto-checker/cover_goals_verifier_with_trace_storage.h b/src/goto-checker/cover_goals_verifier_with_trace_storage.h index 95d058c009b..771b18812be 100644 --- a/src/goto-checker/cover_goals_verifier_with_trace_storage.h +++ b/src/goto-checker/cover_goals_verifier_with_trace_storage.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel #include "goto_verifier.h" +#include "bmc_util.h" #include "cover_goals_report_util.h" #include "goto_trace_storage.h" #include "incremental_goto_checker.h" @@ -41,7 +42,8 @@ class cover_goals_verifier_with_trace_storaget : public goto_verifiert incremental_goto_checkert::resultt::progresst::DONE) { // we've got a trace; store it and link it to the covered goals - (void)traces.insert_all(incremental_goto_checker.build_trace()); + message_building_error_trace(log); + (void)traces.insert_all(incremental_goto_checker.build_full_trace()); ++iterations; } diff --git a/src/goto-checker/goto_trace_provider.h b/src/goto-checker/goto_trace_provider.h index 27f56c60c72..cab2138e4bd 100644 --- a/src/goto-checker/goto_trace_provider.h +++ b/src/goto-checker/goto_trace_provider.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H #define CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H +#include + class goto_tracet; class namespacet; @@ -20,8 +22,15 @@ class namespacet; class goto_trace_providert { public: - /// Builds and returns a trace - virtual goto_tracet build_trace() const = 0; + /// Builds and returns the complete trace + virtual goto_tracet build_full_trace() const = 0; + + /// Builds and returns the trace up to the first failed property + virtual goto_tracet build_shortest_trace() const = 0; + + /// Builds and returns the trace for the FAILed property + /// with the given \p property_id + virtual goto_tracet build_trace(const irep_idt &property_id) const = 0; /// Returns the namespace associated with the traces virtual const namespacet &get_namespace() const = 0; diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index 64872c2c827..9dfd2ba6d80 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -109,20 +109,44 @@ operator()(propertiest &properties) return result; } -goto_tracet multi_path_symex_checkert::build_trace() const +goto_tracet multi_path_symex_checkert::build_full_trace() const +{ + goto_tracet goto_trace; + build_goto_trace( + equation, + equation.SSA_steps.end(), + property_decider.get_solver(), + ns, + goto_trace); + + return goto_trace; +} + +goto_tracet multi_path_symex_checkert::build_shortest_trace() const { if(options.get_bool_option("beautify")) { counterexample_beautificationt()( dynamic_cast(property_decider.get_solver()), equation); } + goto_tracet goto_trace; - ::build_error_trace( - goto_trace, - ns, + build_goto_trace(equation, property_decider.get_solver(), ns, goto_trace); + + return goto_trace; +} + +goto_tracet +multi_path_symex_checkert::build_trace(const irep_idt &property_id) const +{ + goto_tracet goto_trace; + build_goto_trace( equation, + ssa_step_matches_failing_property(property_id), property_decider.get_solver(), - ui_message_handler); + ns, + goto_trace); + return goto_trace; } diff --git a/src/goto-checker/multi_path_symex_checker.h b/src/goto-checker/multi_path_symex_checker.h index 9e2b443a97e..14541ff5861 100644 --- a/src/goto-checker/multi_path_symex_checker.h +++ b/src/goto-checker/multi_path_symex_checker.h @@ -39,7 +39,9 @@ class multi_path_symex_checkert : public multi_path_symex_only_checkert, /// in P_i. Such additional properties will be ignored. resultt operator()(propertiest &) override; - goto_tracet build_trace() const override; + goto_tracet build_full_trace() const override; + goto_tracet build_shortest_trace() const override; + goto_tracet build_trace(const irep_idt &) const override; const namespacet &get_namespace() const override; void output_error_witness(const goto_tracet &) override; diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index 372c7fea75e..298cf3d53dc 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -110,7 +110,20 @@ operator()(propertiest &properties) return result; } -goto_tracet single_path_symex_checkert::build_trace() const +goto_tracet single_path_symex_checkert::build_full_trace() const +{ + goto_tracet goto_trace; + build_goto_trace( + property_decider->get_equation(), + property_decider->get_equation().SSA_steps.end(), + property_decider->get_solver(), + ns, + goto_trace); + + return goto_trace; +} + +goto_tracet single_path_symex_checkert::build_shortest_trace() const { if(options.get_bool_option("beautify")) { @@ -118,13 +131,28 @@ goto_tracet single_path_symex_checkert::build_trace() const dynamic_cast(property_decider->get_solver()), property_decider->get_equation()); } + goto_tracet goto_trace; - ::build_error_trace( - goto_trace, + build_goto_trace( + property_decider->get_equation(), + property_decider->get_solver(), ns, + goto_trace); + + return goto_trace; +} + +goto_tracet +single_path_symex_checkert::build_trace(const irep_idt &property_id) const +{ + goto_tracet goto_trace; + build_goto_trace( property_decider->get_equation(), + ssa_step_matches_failing_property(property_id), property_decider->get_solver(), - ui_message_handler); + ns, + goto_trace); + return goto_trace; } diff --git a/src/goto-checker/single_path_symex_checker.h b/src/goto-checker/single_path_symex_checker.h index c7c74359a70..2178d107501 100644 --- a/src/goto-checker/single_path_symex_checker.h +++ b/src/goto-checker/single_path_symex_checker.h @@ -34,7 +34,9 @@ class single_path_symex_checkert : public single_path_symex_only_checkert, resultt operator()(propertiest &) override; - goto_tracet build_trace() const override; + goto_tracet build_full_trace() const override; + goto_tracet build_shortest_trace() const override; + goto_tracet build_trace(const irep_idt &) const override; const namespacet &get_namespace() const override; void output_error_witness(const goto_tracet &) override; diff --git a/src/goto-checker/stop_on_fail_verifier.h b/src/goto-checker/stop_on_fail_verifier.h index 6c3d760d347..ffc0ac87390 100644 --- a/src/goto-checker/stop_on_fail_verifier.h +++ b/src/goto-checker/stop_on_fail_verifier.h @@ -50,7 +50,8 @@ class stop_on_fail_verifiert : public goto_verifiert case resultt::FAIL: { - goto_tracet goto_trace = incremental_goto_checker.build_trace(); + message_building_error_trace(log); + goto_tracet goto_trace = incremental_goto_checker.build_shortest_trace(); output_error_trace( goto_trace, incremental_goto_checker.get_namespace(), From a6c65e63091840ee27522e183ed641287b7cca17 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 11 Feb 2019 23:25:20 +0000 Subject: [PATCH 4/5] Output traces in same order as properties which is more readable. --- src/goto-checker/report_util.cpp | 34 ++++++++++++++++++++------------ 1 file changed, 21 insertions(+), 13 deletions(-) diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index b5e7424455b..bc12782b81b 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -175,14 +175,9 @@ static void output_single_property_plain( << messaget::eom; } -static void -output_properties_plain(const propertiest &properties, messaget &log) +static std::vector +get_sorted_properties(const propertiest &properties) { - 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); @@ -204,6 +199,17 @@ output_properties_plain(const propertiest &properties, messaget &log) else return id2string(pit1->first) < id2string(pit2->first); }); + return sorted_properties; +} + +static void output_properties_plain( + const std::vector &sorted_properties, + messaget &log) +{ + if(sorted_properties.empty()) + return; + + log.result() << "\n** Results:" << messaget::eom; // now show in the order we have determined irep_idt previous_function; irep_idt current_file; @@ -253,7 +259,8 @@ void output_properties( { case ui_message_handlert::uit::PLAIN: { - output_properties_plain(properties, log); + const auto sorted_properties = get_sorted_properties(properties); + output_properties_plain(sorted_properties, log); output_iterations(properties, iterations, log); break; } @@ -292,18 +299,19 @@ void output_properties_with_traces( { case ui_message_handlert::uit::PLAIN: { - output_properties_plain(properties, log); - for(const auto &property_pair : properties) + const auto sorted_properties = get_sorted_properties(properties); + output_properties_plain(sorted_properties, log); + for(const auto &property_it : sorted_properties) { - if(property_pair.second.status == property_statust::FAIL) + if(property_it->second.status == property_statust::FAIL) { log.result() << "\n" - << "Trace for " << property_pair.first << ":" + << "Trace for " << property_it->first << ":" << "\n"; show_goto_trace( log.result(), traces.get_namespace(), - traces[property_pair.first], + traces[property_it->first], trace_options); log.result() << messaget::eom; } From cbd61b2ab8987ba64bc2b934aa2f86a176e71d53 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 11 Feb 2019 23:58:43 +0000 Subject: [PATCH 5/5] Test for printing multiple goto traces from one counterexample The traces need to be correctly truncated so that the failing property comes last. The traces are printed in the same order as the properties are listed in the result report. --- regression/cbmc/multiple-goto-traces/main.c | 14 ++++++++++++++ regression/cbmc/multiple-goto-traces/test.desc | 14 ++++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 regression/cbmc/multiple-goto-traces/main.c create mode 100644 regression/cbmc/multiple-goto-traces/test.desc diff --git a/regression/cbmc/multiple-goto-traces/main.c b/regression/cbmc/multiple-goto-traces/main.c new file mode 100644 index 00000000000..065af0009bf --- /dev/null +++ b/regression/cbmc/multiple-goto-traces/main.c @@ -0,0 +1,14 @@ +#include + +int main(int argc, char **argv) +{ + assert(4 != argc); + argc++; + argc--; + assert(argc >= 1); + assert(argc != 4); + argc++; + argc--; + assert(argc + 1 != 5); + return 0; +} diff --git a/regression/cbmc/multiple-goto-traces/test.desc b/regression/cbmc/multiple-goto-traces/test.desc new file mode 100644 index 00000000000..799bc993644 --- /dev/null +++ b/regression/cbmc/multiple-goto-traces/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--trace +activate-multi-line-match +EXIT=10 +SIGNAL=0 +VERIFICATION FAILED +Trace for main\.assertion\.1:(\n.*){16} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){30} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){44} assertion argc \+ 1 != 5 +\*\* 3 of 4 failed +-- +^warning: ignoring +-- +We have one counterexample violating multiple properties. +Make sure the traces are correctly truncated.