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. 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/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 158dc54bfc1..d5d575dc2da 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,12 +44,23 @@ 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); } +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 101730072bb..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,14 @@ 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 &); + void build_error_trace( goto_tracet &, const namespacet &, 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/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; } 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(),