diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 94a34f48000..03d24c1ae65 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -29,8 +29,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include +#include #include #include @@ -161,12 +163,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("localize-faults")) options.set_option("localize-faults", true); - if(cmdline.isset("localize-faults-method")) - { - options.set_option( - "localize-faults-method", - cmdline.get_value("localize-faults-method")); - } if(cmdline.isset("unwind")) options.set_option("unwind", cmdline.get_value("unwind")); @@ -613,9 +609,19 @@ int jbmc_parse_optionst::doit() } else { - verifier = util_make_unique< - stop_on_fail_verifiert>( - options, ui_message_handler, goto_model); + if(options.get_bool_option("localize-faults")) + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } + else + { + verifier = util_make_unique< + stop_on_fail_verifiert>( + options, ui_message_handler, goto_model); + } } } else @@ -629,10 +635,20 @@ int jbmc_parse_optionst::doit() } else { - verifier = - util_make_unique>( - options, ui_message_handler, goto_model); + if(options.get_bool_option("localize-faults")) + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } + else + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } } } } diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index e502cd6d953..99600de88dd 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -77,7 +77,7 @@ class optionst; OPT_FLUSH \ JAVA_BYTECODE_LANGUAGE_OPTIONS \ "(java-unwind-enum-static)" \ - "(localize-faults)(localize-faults-method):" \ + "(localize-faults)" \ "(java-threading)" \ OPT_GOTO_TRACE \ OPT_VALIDATE \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index bf53e05ec51..43b24793e1f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -43,6 +44,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -230,12 +232,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("localize-faults")) options.set_option("localize-faults", true); - if(cmdline.isset("localize-faults-method")) - { - options.set_option( - "localize-faults-method", - cmdline.get_value("localize-faults-method")); - } if(cmdline.isset("unwind")) options.set_option("unwind", cmdline.get_value("unwind")); @@ -625,9 +621,19 @@ int cbmc_parse_optionst::doit() } else { - verifier = - util_make_unique>( - options, ui_message_handler, goto_model); + if(options.get_bool_option("localize-faults")) + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } + else + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } } } else @@ -639,8 +645,20 @@ int cbmc_parse_optionst::doit() } else { - verifier = util_make_unique>(options, ui_message_handler, goto_model); + if(options.get_bool_option("localize-faults")) + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } + else + { + verifier = + util_make_unique>( + options, ui_message_handler, goto_model); + } } } } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 1b26e83ab7e..f3d63499913 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -76,7 +76,7 @@ class optionst; "(string-abstraction)(no-arch)(arch):" \ "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ OPT_FLUSH \ - "(localize-faults)(localize-faults-method):" \ + "(localize-faults)" \ OPT_GOTO_TRACE \ OPT_VALIDATE \ OPT_ANSI_C_LANGUAGE \ diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index c6bba2e1a9e..c96f85066e3 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -2,6 +2,7 @@ SRC = bmc_util.cpp \ counterexample_beautification.cpp \ cover_goals_report_util.cpp \ incremental_goto_checker.cpp \ + goto_symex_fault_localizer.cpp \ goto_symex_property_decider.cpp \ goto_trace_storage.cpp \ goto_verifier.cpp \ diff --git a/src/goto-checker/all_properties_verifier_with_fault_localization.h b/src/goto-checker/all_properties_verifier_with_fault_localization.h new file mode 100644 index 00000000000..ff001c644d6 --- /dev/null +++ b/src/goto-checker/all_properties_verifier_with_fault_localization.h @@ -0,0 +1,109 @@ +/*******************************************************************\ + +Module: Goto Verifier for Verifying all Properties and Localizing Faults + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto verifier for verifying all properties that stores traces +/// and localizes faults + +#ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_FAULT_LOCALIZATION_H +#define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_FAULT_LOCALIZATION_H + +#include "goto_verifier.h" + +#include "fault_localization_provider.h" +#include "goto_trace_storage.h" +#include "incremental_goto_checker.h" +#include "properties.h" +#include "report_util.h" + +/// Requires an incremental goto checker that is a +/// `goto_trace_providert` and `fault_localization_providert`. +template +class all_properties_verifier_with_fault_localizationt : public goto_verifiert +{ +public: + all_properties_verifier_with_fault_localizationt( + 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(true) + { + 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)); + + fault_locations.insert( + {property_id, + incremental_goto_checker.localize_fault(property_id)}); + } + } + + ++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_and_fault_localization( + properties, + traces, + trace_options, + fault_locations, + iterations, + ui_message_handler); + } + else + { + output_properties_with_fault_localization( + properties, fault_locations, 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; + std::unordered_map fault_locations; +}; + +#endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_FAULT_LOCALIZATION_H diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index d5d575dc2da..335a831e015 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -102,6 +102,19 @@ void output_error_trace( } } +void freeze_guards( + const symex_target_equationt &equation, + prop_convt &prop_conv) +{ + for(const auto &step : equation.SSA_steps) + { + if(!step.guard_literal.is_constant()) + prop_conv.set_frozen(step.guard_literal); + if(step.is_assert() && !step.cond_literal.is_constant()) + prop_conv.set_frozen(step.cond_literal); + } +} + /// outputs an error witness in graphml format void output_graphml( const goto_tracet &goto_trace, diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index df36406fdf4..ac0e9af788f 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -57,6 +57,8 @@ void output_error_trace( const trace_optionst &, ui_message_handlert &); +void freeze_guards(const symex_target_equationt &, prop_convt &); + void output_graphml(const goto_tracet &, const namespacet &, const optionst &); void output_graphml( const symex_target_equationt &, diff --git a/src/goto-checker/fault_localization_provider.h b/src/goto-checker/fault_localization_provider.h new file mode 100644 index 00000000000..2c74b1ecbc3 --- /dev/null +++ b/src/goto-checker/fault_localization_provider.h @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Interface for Goto Checkers to provide Fault Localization + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Interface for Goto Checkers to provide Fault Localization + +#ifndef CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H +#define CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H + +#include + +#include + +class goto_tracet; +class namespacet; + +struct fault_location_infot +{ + typedef std::map score_mapt; + score_mapt scores; +}; + +/// An implementation of `incremental_goto_checkert` +/// may implement this interface to provide fault localization information. +class fault_localization_providert +{ +public: + /// Returns the most likely fault locations + /// for the given FAILed \p property_id + virtual fault_location_infot + localize_fault(const irep_idt &property_id) const = 0; + + virtual ~fault_localization_providert() = default; +}; + +#endif // CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp new file mode 100644 index 00000000000..4bb0b4c113c --- /dev/null +++ b/src/goto-checker/goto_symex_fault_localizer.cpp @@ -0,0 +1,140 @@ +/*******************************************************************\ + +Module: Fault Localization for Goto Symex + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Fault Localization for Goto Symex + +#include "goto_symex_fault_localizer.h" + +#include + +goto_symex_fault_localizert::goto_symex_fault_localizert( + const optionst &options, + ui_message_handlert &ui_message_handler, + const symex_target_equationt &equation, + prop_convt &solver) + : options(options), + ui_message_handler(ui_message_handler), + equation(equation), + solver(solver) +{ +} + +fault_location_infot goto_symex_fault_localizert:: +operator()(const irep_idt &failed_property_id) +{ + fault_location_infot fault_location; + localization_pointst localization_points; + const auto &failed_step = + collect_guards(failed_property_id, localization_points, fault_location); + + if(!localization_points.empty()) + { + messaget log(ui_message_handler); + log.status() << "Localizing fault" << messaget::eom; + + // pick localization method + // if(options.get_option("localize-faults-method")=="TBD") + localize_linear(failed_step, localization_points); + } + + return fault_location; +} + +const symex_target_equationt::SSA_stept & +goto_symex_fault_localizert::collect_guards( + const irep_idt &failed_property_id, + localization_pointst &localization_points, + fault_location_infot &fault_location) +{ + for(const auto &step : equation.SSA_steps) + { + if( + step.is_assignment() && + step.assignment_type == symex_targett::assignment_typet::STATE && + !step.ignore) + { + if(!step.guard_literal.is_constant()) + { + auto emplace_result = fault_location.scores.emplace(step.source.pc, 0); + localization_points.emplace(step.guard_literal, emplace_result.first); + } + } + + // reached failed assertion? + if(step.is_assert() && step.get_property_id() == failed_property_id) + return step; + } + UNREACHABLE; +} + +bool goto_symex_fault_localizert::check( + const symex_target_equationt::SSA_stept &failed_step, + const localization_pointst &localization_points, + const localization_points_valuet &value) +{ + PRECONDITION(value.size() == localization_points.size()); + bvt assumptions; + localization_points_valuet::const_iterator v_it = value.begin(); + for(const auto &l : localization_points) + { + if(v_it->is_true()) + assumptions.push_back(l.first); + else if(v_it->is_false()) + assumptions.push_back(!l.first); + ++v_it; + } + + // lock the failed assertion + assumptions.push_back(!failed_step.cond_literal); + + solver.set_assumptions(assumptions); + + return solver() != decision_proceduret::resultt::D_SATISFIABLE; +} + +void goto_symex_fault_localizert::update_scores( + const localization_pointst &localization_points) +{ + for(auto &l : localization_points) + { + auto &score = l.second->second; + if(solver.l_get(l.first).is_true()) + { + score++; + } + else if(solver.l_get(l.first).is_false() && score > 0) + { + score--; + } + } +} + +void goto_symex_fault_localizert::localize_linear( + const symex_target_equationt::SSA_stept &failed_step, + const localization_pointst &localization_points) +{ + localization_points_valuet v(localization_points.size(), tvt::unknown()); + + for(std::size_t i = 0; i < v.size(); ++i) + { + v[i] = tvt(tvt::tv_enumt::TV_TRUE); + if(!check(failed_step, localization_points, v)) + update_scores(localization_points); + + v[i] = tvt(tvt::tv_enumt::TV_FALSE); + if(!check(failed_step, localization_points, v)) + update_scores(localization_points); + + v[i] = tvt::unknown(); + } + + // clear assumptions + bvt assumptions; + solver.set_assumptions(assumptions); +} diff --git a/src/goto-checker/goto_symex_fault_localizer.h b/src/goto-checker/goto_symex_fault_localizer.h new file mode 100644 index 00000000000..4a9e98b6165 --- /dev/null +++ b/src/goto-checker/goto_symex_fault_localizer.h @@ -0,0 +1,67 @@ +/*******************************************************************\ + +Module: Fault Localization for Goto Symex + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Fault Localization for Goto Symex + +#ifndef CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H +#define CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H + +#include +#include +#include + +#include + +#include "fault_localization_provider.h" + +class goto_symex_fault_localizert +{ +public: + goto_symex_fault_localizert( + const optionst &options, + ui_message_handlert &ui_message_handler, + const symex_target_equationt &equation, + prop_convt &solver); + + fault_location_infot operator()(const irep_idt &failed_property_id); + +protected: + const optionst &options; + ui_message_handlert &ui_message_handler; + const symex_target_equationt &equation; + prop_convt &solver; + + /// A localization point is a goto instruction that is potentially at fault + typedef std::map + localization_pointst; + + /// Collects the guards as \p localization_points up to \p failed_property_id + /// and initializes fault_location_info, and returns the SSA step of + /// the failed property + const symex_target_equationt::SSA_stept &collect_guards( + const irep_idt &failed_property_id, + localization_pointst &localization_points, + fault_location_infot &fault_location); + + // specify a localization point combination to check + typedef std::vector localization_points_valuet; + bool check( + const symex_target_equationt::SSA_stept &failed_step, + const localization_pointst &, + const localization_points_valuet &); + + void update_scores(const localization_pointst &); + + // localization method: flip each point + void localize_linear( + const symex_target_equationt::SSA_stept &failed_step, + const localization_pointst &); +}; + +#endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index d9093eedce2..b50f683195d 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -127,9 +127,12 @@ void goto_symex_property_decidert::update_properties_status_from_goals( case decision_proceduret::resultt::D_SATISFIABLE: for(auto &goal_pair : goal_map) { - if(solver->prop_conv().l_get(goal_pair.second.condition).is_true()) + auto &status = properties.at(goal_pair.first).status; + if( + solver->prop_conv().l_get(goal_pair.second.condition).is_true() && + status != property_statust::FAIL) { - properties.at(goal_pair.first).status |= property_statust::FAIL; + status |= property_statust::FAIL; updated_properties.insert(goal_pair.first); } } diff --git a/src/goto-checker/goto_trace_storage.cpp b/src/goto-checker/goto_trace_storage.cpp index 9a95ac82e6a..d59d29ea8e0 100644 --- a/src/goto-checker/goto_trace_storage.cpp +++ b/src/goto-checker/goto_trace_storage.cpp @@ -21,7 +21,12 @@ const goto_tracet &goto_trace_storaget::insert(goto_tracet &&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); + const auto emplace_result = property_id_to_trace_index.emplace( + last_step.property_id, traces.size() - 1); + INVARIANT( + emplace_result.second, + "cannot associate more than one error trace with property " + + id2string(last_step.property_id)); return traces.back(); } diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index 9dfd2ba6d80..f3b95cf0133 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, Peter Schrammel #include "bmc_util.h" #include "counterexample_beautification.h" +#include "goto_symex_fault_localizer.h" multi_path_symex_checkert::multi_path_symex_checkert( const optionst &options, @@ -77,6 +78,9 @@ operator()(propertiest &properties) property_decider.convert_goals(); property_decider.freeze_goal_variables(); + if(options.get_bool_option("localize-faults")) + freeze_guards(equation, property_decider.get_solver()); + const auto solver_stop = std::chrono::steady_clock::now(); solver_runtime += std::chrono::duration(solver_stop - solver_start); @@ -165,3 +169,12 @@ void multi_path_symex_checkert::output_error_witness( { output_graphml(error_trace, ns, options); } + +fault_location_infot +multi_path_symex_checkert::localize_fault(const irep_idt &property_id) const +{ + goto_symex_fault_localizert fault_localizer( + options, ui_message_handler, equation, property_decider.get_solver()); + + return fault_localizer(property_id); +} diff --git a/src/goto-checker/multi_path_symex_checker.h b/src/goto-checker/multi_path_symex_checker.h index 14541ff5861..9f9c6c0050f 100644 --- a/src/goto-checker/multi_path_symex_checker.h +++ b/src/goto-checker/multi_path_symex_checker.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H #define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H +#include "fault_localization_provider.h" #include "goto_symex_property_decider.h" #include "goto_trace_provider.h" #include "multi_path_symex_only_checker.h" @@ -21,7 +22,8 @@ Author: Daniel Kroening, Peter Schrammel /// 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 witness_providert, + public fault_localization_providert { public: multi_path_symex_checkert( @@ -47,6 +49,9 @@ class multi_path_symex_checkert : public multi_path_symex_only_checkert, void output_error_witness(const goto_tracet &) override; void output_proof() override; + fault_location_infot + localize_fault(const irep_idt &property_id) const override; + protected: bool equation_generated; goto_symex_property_decidert property_decider; diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index bc12782b81b..d082002a3de 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -14,16 +14,21 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include #include #include +#include #include #include #include +#include "fault_localization_provider.h" #include "goto_trace_storage.h" +#include "bmc_util.h" + void report_success(ui_message_handlert &ui_message_handler) { messaget msg(ui_message_handler); @@ -362,6 +367,261 @@ void output_properties_with_traces( } } +void output_fault_localization_scores( + const fault_location_infot &fault_location, + messaget &log) +{ + log.conditional_output( + log.debug(), [fault_location](messaget::mstreamt &out) { + out << "Fault localization scores:" << messaget::eom; + for(auto &score_pair : fault_location.scores) + { + out << score_pair.first->source_location + << "\n score: " << score_pair.second << messaget::eom; + } + }); +} + +static goto_programt::const_targett +max_fault_localization_score(const fault_location_infot &fault_location) +{ + PRECONDITION(!fault_location.scores.empty()); + + return std::max_element( + fault_location.scores.begin(), + fault_location.scores.end(), + []( + fault_location_infot::score_mapt::value_type score_pair1, + fault_location_infot::score_mapt::value_type score_pair2) { + return score_pair1.second < score_pair2.second; + }) + ->first; +} + +static void output_fault_localization_plain( + const irep_idt &property_id, + const fault_location_infot &fault_location, + messaget &log) +{ + if(fault_location.scores.empty()) + { + log.result() << "[" + id2string(property_id) + "]: \n" + << " unable to localize fault" << messaget::eom; + return; + } + + output_fault_localization_scores(fault_location, log); + log.result() << "[" + id2string(property_id) + "]: \n " + << max_fault_localization_score(fault_location)->source_location + << messaget::eom; +} + +static void output_fault_localization_plain( + const std::unordered_map &fault_locations, + messaget &log) +{ + log.result() << "\n** Most likely fault location:" << messaget::eom; + for(const auto fault_location_pair : fault_locations) + { + output_fault_localization_plain( + fault_location_pair.first, fault_location_pair.second, log); + } +} + +static xmlt xml( + const irep_idt &property_id, + const fault_location_infot &fault_location, + messaget &log) +{ + xmlt xml_diagnosis("diagnosis"); + + xml_diagnosis.set_attribute("property", id2string(property_id)); + + if(fault_location.scores.empty()) + { + xml_diagnosis.new_element("result").data = "unable to localize fault"; + return xml_diagnosis; + } + + output_fault_localization_scores(fault_location, log); + + xmlt xml_location = + xml(max_fault_localization_score(fault_location)->source_location); + xml_diagnosis.new_element("result").new_element().swap(xml_location); + + return xml_diagnosis; +} + +static void output_fault_localization_xml( + const std::unordered_map &fault_locations, + messaget &log) +{ + xmlt dest("fault-localization"); + for(const auto fault_location_pair : fault_locations) + { + xmlt xml_diagnosis = + xml(fault_location_pair.first, fault_location_pair.second, log); + dest.new_element().swap(xml_diagnosis); + } + log.result() << dest; +} + +static json_objectt json(const fault_location_infot &fault_location) +{ + json_objectt json_result; + if(fault_location.scores.empty()) + { + json_result["result"] = json_stringt("unable to localize fault"); + } + else + { + json_result["result"] = + json(max_fault_localization_score(fault_location)->source_location); + } + return json_result; +} + +void output_properties_with_fault_localization( + const propertiest &properties, + const std::unordered_map &fault_locations, + 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(properties, iterations, ui_message_handler); + output_fault_localization_plain(fault_locations, log); + 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) + { + 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_property.push_back( + "diagnosis", json(fault_locations.at(property_pair.first))); + } + } + break; + } + case ui_message_handlert::uit::XML_UI: + { + output_properties(properties, iterations, ui_message_handler); + output_fault_localization_xml(fault_locations, log); + break; + } + } +} + +void output_properties_with_traces_and_fault_localization( + const propertiest &properties, + const goto_trace_storaget &traces, + const trace_optionst &trace_options, + const std::unordered_map &fault_locations, + 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_with_traces( + properties, traces, trace_options, iterations, ui_message_handler); + output_fault_localization_plain(fault_locations, log); + 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) + { + 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); + json_property.push_back( + "diagnosis", json(fault_locations.at(property_pair.first))); + } + } + break; + } + case ui_message_handlert::uit::XML_UI: + { + output_properties_with_traces( + properties, traces, trace_options, iterations, ui_message_handler); + output_fault_localization_xml(fault_locations, log); + break; + } + } +} + +void output_error_trace_with_fault_localization( + const goto_tracet &goto_trace, + const namespacet &ns, + const trace_optionst &trace_options, + const fault_location_infot &fault_location_info, + ui_message_handlert &ui_message_handler) +{ + messaget log(ui_message_handler); + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + output_error_trace(goto_trace, ns, trace_options, ui_message_handler); + output_fault_localization_plain( + goto_trace.get_last_step().property_id, fault_location_info, log); + break; + + case ui_message_handlert::uit::JSON_UI: + { + json_stream_objectt &json_result = + ui_message_handler.get_json_stream().push_back_stream_object(); + const goto_trace_stept &step = goto_trace.get_last_step(); + json_result["property"] = json_stringt(step.property_id); + json_result["description"] = json_stringt(step.comment); + json_result["status"] = json_stringt("failed"); + json_stream_arrayt &json_trace = + json_result.push_back_stream_array("trace"); + convert(ns, goto_trace, json_trace, trace_options); + json_result.push_back("diagnosis", json(fault_location_info)); + break; + } + + case ui_message_handlert::uit::XML_UI: + { + output_error_trace(goto_trace, ns, trace_options, ui_message_handler); + xmlt dest( + "fault-localization", + {}, + {xml(goto_trace.get_last_step().property_id, fault_location_info, log)}); + log.result() << dest; + break; + } + } +} + void output_overall_result( resultt result, ui_message_handlert &ui_message_handler) diff --git a/src/goto-checker/report_util.h b/src/goto-checker/report_util.h index 931ca6da147..6976ea7de7e 100644 --- a/src/goto-checker/report_util.h +++ b/src/goto-checker/report_util.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel #include "properties.h" +struct fault_location_infot; class goto_trace_storaget; class goto_tracet; struct trace_optionst; @@ -36,6 +37,27 @@ void output_properties_with_traces( std::size_t iterations, ui_message_handlert &ui_message_handler); +void output_properties_with_fault_localization( + const propertiest &properties, + const std::unordered_map &, + std::size_t iterations, + ui_message_handlert &ui_message_handler); + +void output_properties_with_traces_and_fault_localization( + const propertiest &properties, + const goto_trace_storaget &traces, + const trace_optionst &trace_options, + const std::unordered_map &, + std::size_t iterations, + ui_message_handlert &ui_message_handler); + +void output_error_trace_with_fault_localization( + const goto_tracet &, + const namespacet &, + const trace_optionst &, + const fault_location_infot &, + ui_message_handlert &); + void output_overall_result( resultt result, ui_message_handlert &ui_message_handler); diff --git a/src/goto-checker/stop_on_fail_verifier_with_fault_localization.h b/src/goto-checker/stop_on_fail_verifier_with_fault_localization.h new file mode 100644 index 00000000000..154a9e7dcfe --- /dev/null +++ b/src/goto-checker/stop_on_fail_verifier_with_fault_localization.h @@ -0,0 +1,87 @@ +/*******************************************************************\ + +Module: Goto Verifier for stopping at the first failing property + and localizing the fault + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Verifier for stopping at the first failing property +/// and localizing the fault + +#ifndef CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_WITH_FAULT_LOCALIZATION_H +#define CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_WITH_FAULT_LOCALIZATION_H + +#include "bmc_util.h" +#include "fault_localization_provider.h" +#include "goto_verifier.h" + +/// Stops when the first failing property is found and localizes the fault +/// Requires an incremental goto checker that is a +/// `goto_trace_providert` and `fault_localization_providert`. +template +class stop_on_fail_verifier_with_fault_localizationt : public goto_verifiert +{ +public: + stop_on_fail_verifier_with_fault_localizationt( + 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); + break; + + case resultt::FAIL: + { + const goto_tracet goto_trace = + incremental_goto_checker.build_shortest_trace(); + const fault_location_infot fault_location = + incremental_goto_checker.localize_fault( + goto_trace.get_last_step().property_id); + + output_error_trace_with_fault_localization( + goto_trace, + incremental_goto_checker.get_namespace(), + trace_optionst(options), + fault_location, + ui_message_handler); + + report_failure(ui_message_handler); + 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_WITH_FAULT_LOCALIZATION_H diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 27a637ab4d7..99a43478109 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -201,6 +201,11 @@ class goto_tracet return steps.back(); } + const goto_trace_stept &get_last_step() const + { + return steps.back(); + } + /// Returns the property IDs of all assertions in the trace std::vector get_all_property_ids() const; };