From 06a464aeaa6d3dc5f68f8e62a99995d4722ae9be Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 19 Jul 2016 10:49:46 +0100 Subject: [PATCH 1/2] basic fault localization --- src/cbmc/Makefile | 3 +- src/cbmc/bmc.cpp | 11 ++ src/cbmc/cbmc_parse_options.cpp | 10 +- src/cbmc/cbmc_parse_options.h | 1 + src/cbmc/fault_localization.cpp | 255 ++++++++++++++++++++++++++++++++ src/cbmc/fault_localization.h | 80 ++++++++++ 6 files changed, 358 insertions(+), 2 deletions(-) create mode 100644 src/cbmc/fault_localization.cpp create mode 100644 src/cbmc/fault_localization.h diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index a09e849017e..edbd0b99a85 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -1,7 +1,8 @@ SRC = cbmc_main.cpp cbmc_parse_options.cpp bmc.cpp cbmc_dimacs.cpp \ cbmc_languages.cpp counterexample_beautification.cpp \ bv_cbmc.cpp symex_bmc.cpp show_vcc.cpp cbmc_solvers.cpp \ - xml_interface.cpp bmc_cover.cpp all_properties.cpp + xml_interface.cpp bmc_cover.cpp all_properties.cpp \ + fault_localization.cpp OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../linking/linking$(LIBEXT) \ diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index f144d69014b..f29cfaf43ee 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -35,6 +35,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "counterexample_beautification.h" +#include "fault_localization.h" #include "bmc.h" /*******************************************************************\ @@ -588,6 +589,11 @@ safety_checkert::resultt bmct::stop_on_fail( const goto_functionst &goto_functions, prop_convt &prop_conv) { + if(options.get_bool_option("localize-faults")) + { + //ENHANCE: currently, requires only freezing of guards + prop_conv.set_all_frozen(); + } switch(run_decision_procedure(prop_conv)) { case decision_proceduret::D_UNSATISFIABLE: @@ -603,6 +609,11 @@ safety_checkert::resultt bmct::stop_on_fail( error_trace(); } + if(options.get_bool_option("localize-faults")) + { + fault_localizationt fault_localization(options); + fault_localization(dynamic_cast(prop_conv), equation, ns); + } report_failure(); return UNSAFE; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 9b47a7b1891..c07adfb5b64 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -181,7 +181,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("stop-on-fail") || cmdline.isset("property") || cmdline.isset("dimacs") || - cmdline.isset("outfile")) + cmdline.isset("outfile") || + cmdline.isset("localize-faults")) options.set_option("stop-on-fail", true); else options.set_option("stop-on-fail", false); @@ -191,6 +192,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cmdline.isset("property")) options.set_option("trace", true); + 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")); @@ -1158,6 +1165,7 @@ void cbmc_parse_optionst::help() "Backend options:\n" " --dimacs generate CNF in DIMACS format\n" " --beautify beautify the counterexample (greedy heuristic)\n" + " --localize-faults localize faults (experimental)\n" " --smt1 use default SMT1 solver (obsolete)\n" " --smt2 use default SMT2 solver (Z3)\n" " --boolector use Boolector\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 6588a2067fb..730c9bbe440 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -53,6 +53,7 @@ class optionst; "(string-abstraction)(no-arch)(arch):" \ "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ "(graphml-cex):" \ + "(localize-faults)(localize-faults-method):" \ "(floatbv)(all-claims)(all-properties)(decide)" // legacy, and will eventually disappear class cbmc_parse_optionst: diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp new file mode 100644 index 00000000000..c5798be088c --- /dev/null +++ b/src/cbmc/fault_localization.cpp @@ -0,0 +1,255 @@ +/*******************************************************************\ + +Module: Fault Localization + +Author: Peter Schrammel + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include + +#include +#include + +#include "fault_localization.h" + +/*******************************************************************\ + +Function: fault_localizationt::collect_guards + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void fault_localizationt::collect_guards( + const symex_target_equationt &equation) +{ + 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::STATE) + { + if(!it->guard_literal.is_constant()) + { + lpoints[it->guard_literal].target=it->source.pc; + lpoints[it->guard_literal].score=0; + } + } + + // reached failed assertion? + if(it==failed) + break; + } +} + +/*******************************************************************\ + +Function: fault_localizationt::get_failed_property + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +symex_target_equationt::SSA_stepst::const_iterator +fault_localizationt::get_failed_property( + const prop_convt &prop_conv, + const symex_target_equationt &equation) +{ + 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; + + assert(false); + return equation.SSA_steps.end(); +} + +/*******************************************************************\ + +Function: fault_localizationt::check + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool fault_localizationt::check( + prop_convt &prop_conv, + const lpoints_valuet& value) +{ + assert(value.size()==lpoints.size()); + bvt assumptions; + lpointst::const_iterator l_it=lpoints.begin(); + lpoints_valuet::const_iterator v_it=value.begin(); + for(; l_it!=lpoints.end(); + ++l_it, ++v_it) + { + if(v_it->is_true()) + assumptions.push_back(l_it->first); + else if(v_it->is_false()) + assumptions.push_back(!l_it->first); + } + prop_conv.set_assumptions(assumptions); + + if(prop_conv()==decision_proceduret::D_SATISFIABLE) + return false; + + return true; +} + +/*******************************************************************\ + +Function: fault_localizationt::update_scores + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void fault_localizationt::update_scores( + const prop_convt &prop_conv, + const lpoints_valuet& value) +{ + for(lpointst::iterator l_it=lpoints.begin(); + l_it!=lpoints.end(); + ++l_it) + { + if(prop_conv.l_get(l_it->first).is_true()) + l_it->second.score++; + else if(prop_conv.l_get(l_it->first).is_false() && + l_it->second.score>0) + l_it->second.score--; + } +} + +/*******************************************************************\ + +Function: fault_localizationt::localize_linear + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void fault_localizationt::localize_linear( + prop_convt &prop_conv) +{ + lpoints_valuet v; + for(lpointst::const_iterator l_it=lpoints.begin(); + l_it!=lpoints.end(); + ++l_it) + v.push_back(tvt(tvt::tv_enumt::TV_UNKNOWN)); + for(size_t i=0; icond_literal), false); + + // collect lpoints + collect_guards(equation); + + if(lpoints.empty()) + return; + + bv_cbmc.status() << "Localizing fault" + << messaget::eom; + + // pick localization method + // if(options.get_option("localize-faults-method")=="TBD") + localize_linear(bv_cbmc); + + // print results + report(bv_cbmc); +} + +/*******************************************************************\ + +Function: fault_localizationt::report() + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void fault_localizationt::report( + bv_cbmct &bv_cbmc) + +{ + assert(!lpoints.empty()); + lpointst::const_iterator max=lpoints.begin(); + bv_cbmc.debug() << "Fault localization scores:" << messaget::eom; + for(lpointst::const_iterator l_it=lpoints.begin(); + l_it!=lpoints.end(); + ++l_it) + { + bv_cbmc.debug() << l_it->second.target->source_location + << "\n score: " << l_it->second.score << messaget::eom; + if(max->second.scoresecond.score) + max=l_it; + } + bv_cbmc.status() << "Most likely fault location: \n" + << " " << max->second.target->source_location + << messaget::eom; +} diff --git a/src/cbmc/fault_localization.h b/src/cbmc/fault_localization.h new file mode 100644 index 00000000000..d135b4e0fad --- /dev/null +++ b/src/cbmc/fault_localization.h @@ -0,0 +1,80 @@ +/*******************************************************************\ + +Module: Fault Localization + +Author: Peter Schrammel + +\*******************************************************************/ + +#ifndef CPROVER_CBMC_FAULT_LOCALIZATION_H +#define CPROVER_CBMC_FAULT_LOCALIZATION_H + +#include +#include +#include +#include + +#include + +#include "bv_cbmc.h" + +class fault_localizationt +{ +public: + fault_localizationt(const optionst &_options) + : options(_options) + { + } + + virtual ~fault_localizationt() + { + } + + void operator()( + bv_cbmct &bv_cbmc, + const symex_target_equationt &equation, + const namespacet &ns); + +protected: + const optionst &options; + + // the failed property + symex_target_equationt::SSA_stepst::const_iterator failed; + + // the list of localization points up to the failed property + struct lpointt { + goto_programt::const_targett target; + unsigned score; + }; + typedef std::map lpointst; + lpointst lpoints; + + // this collects the guards as lpoints + void collect_guards( + const symex_target_equationt &equation); + + // specify an lpoint combination to check + typedef std::vector lpoints_valuet; + bool check( + prop_convt &prop_conv, + const lpoints_valuet& value); + void update_scores( + const prop_convt &prop_conv, + const lpoints_valuet& value); + + // localization method: flip each point + void localize_linear( + prop_convt &prop_conv); + + // localization method: TBD + //void localize_TBD( + // prop_convt &prop_conv); + + symex_target_equationt::SSA_stepst::const_iterator get_failed_property( + const prop_convt &prop_conv, + const symex_target_equationt &equation); + + void report(bv_cbmct &bv_cbmc); +}; + +#endif From 06d9e51d09d6eb0bd37e6394d9e18be806d405e4 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 22 Aug 2016 00:12:15 +0100 Subject: [PATCH 2/2] fault localization now integrates with bmc_all_properties and stop_on_fail --- src/cbmc/all_properties.cpp | 170 ++++----------- src/cbmc/all_properties_class.h | 115 +++++++++++ src/cbmc/bmc.cpp | 17 +- src/cbmc/bmc.h | 1 + src/cbmc/cbmc_parse_options.cpp | 3 +- src/cbmc/fault_localization.cpp | 355 +++++++++++++++++++++++++------- src/cbmc/fault_localization.h | 71 ++++--- 7 files changed, 487 insertions(+), 245 deletions(-) create mode 100644 src/cbmc/all_properties_class.h diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index f4672d9f3bc..1776361576e 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -6,109 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include - -#include -#include -#include - -#include -#include -#include - -#include -#include -#include - -#include "bmc.h" -#include "bv_cbmc.h" - -/*******************************************************************\ - - Class: bmc_all_propertiest - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -class bmc_all_propertiest: - public cover_goalst::observert, - public messaget -{ -public: - bmc_all_propertiest( - const goto_functionst &_goto_functions, - prop_convt &_solver, - bmct &_bmc): - goto_functions(_goto_functions), solver(_solver), bmc(_bmc) - { - } - - safety_checkert::resultt operator()(); - - virtual void goal_covered(const cover_goalst::goalt &); - - struct goalt - { - // a property holds if all instances of it are true - typedef std::vector instancest; - instancest instances; - std::string description; - - // if failed, we compute a goto_trace for the first failing instance - enum statust { UNKNOWN, FAILURE, SUCCESS, ERROR } status; - goto_tracet goto_trace; - - std::string status_string() const - { - switch(status) - { - case UNKNOWN: return "UNKNOWN"; - case FAILURE: return "FAILURE"; - case SUCCESS: return "SUCCESS"; - case ERROR: return "ERROR"; - } - - // make some poor compilers happy - assert(false); - return ""; - } - - explicit goalt( - const goto_programt::instructiont &instruction): - status(statust::UNKNOWN) - { - description=id2string(instruction.source_location.get_comment()); - } - - goalt():status(statust::UNKNOWN) - { - } - - exprt as_expr() const - { - std::vector tmp; - for(instancest::const_iterator - it=instances.begin(); - it!=instances.end(); - it++) - tmp.push_back(literal_exprt((*it)->cond_literal)); - return conjunction(tmp); - } - }; - - typedef std::map goal_mapt; - goal_mapt goal_map; - -protected: - const goto_functionst &goto_functions; - prop_convt &solver; - bmct &bmc; -}; +#include "all_properties_class.h" /*******************************************************************\ @@ -124,30 +22,23 @@ Function: bmc_all_propertiest::goal_covered void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &) { - for(goal_mapt::iterator - g_it=goal_map.begin(); - g_it!=goal_map.end(); - g_it++) + for(auto &g : goal_map) { - goalt &g=g_it->second; - // failed already? - if(g.status==goalt::statust::FAILURE) continue; + if(g.second.status==goalt::statust::FAILURE) continue; // check whether failed - for(goalt::instancest::const_iterator - c_it=g.instances.begin(); - c_it!=g.instances.end(); - c_it++) + for(auto &c : g.second.instances) { - literalt cond=(*c_it)->cond_literal; + literalt cond=c->cond_literal; if(solver.l_get(cond).is_false()) { - g.status=goalt::statust::FAILURE; - symex_target_equationt::SSA_stepst::iterator next=*c_it; + g.second.status=goalt::statust::FAILURE; + symex_target_equationt::SSA_stepst::iterator next=c; next++; // include the assertion - build_goto_trace(bmc.equation, next, solver, bmc.ns, g.goto_trace); + build_goto_trace(bmc.equation, next, solver, bmc.ns, + g.second.goto_trace); break; } } @@ -212,6 +103,8 @@ safety_checkert::resultt bmc_all_propertiest::operator()() } } + do_before_solving(); + cover_goalst cover_goals(solver); cover_goals.set_message_handler(get_message_handler()); @@ -254,6 +147,35 @@ safety_checkert::resultt bmc_all_propertiest::operator()() } // report + report(cover_goals); + + if(error) + return safety_checkert::ERROR; + + bool safe=(cover_goals.number_covered()==0); + + if(safe) + bmc.report_success(); // legacy, might go away + else + bmc.report_failure(); // legacy, might go away + + return safe?safety_checkert::SAFE:safety_checkert::UNSAFE; +} + +/*******************************************************************\ + +Function: bmc_all_propertiest::report() + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void bmc_all_propertiest::report(const cover_goalst &cover_goals) +{ switch(bmc.ui) { case ui_message_handlert::PLAIN: @@ -321,18 +243,6 @@ safety_checkert::resultt bmc_all_propertiest::operator()() break; } - - if(error) - return safety_checkert::ERROR; - - bool safe=(cover_goals.number_covered()==0); - - if(safe) - bmc.report_success(); // legacy, might go away - else - bmc.report_failure(); // legacy, might go away - - return safe?safety_checkert::SAFE:safety_checkert::UNSAFE; } /*******************************************************************\ diff --git a/src/cbmc/all_properties_class.h b/src/cbmc/all_properties_class.h new file mode 100644 index 00000000000..449dd771e0a --- /dev/null +++ b/src/cbmc/all_properties_class.h @@ -0,0 +1,115 @@ +/*******************************************************************\ + +Module: Symbolic Execution of ANSI-C + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include + +#include +#include +#include + +#include +#include +#include + +#include +#include +#include + +#include "bmc.h" +#include "bv_cbmc.h" + +/*******************************************************************\ + + Class: bmc_all_propertiest + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +class bmc_all_propertiest: + public cover_goalst::observert, + public messaget +{ +public: + bmc_all_propertiest( + const goto_functionst &_goto_functions, + prop_convt &_solver, + bmct &_bmc): + goto_functions(_goto_functions), solver(_solver), bmc(_bmc) + { + } + + safety_checkert::resultt operator()(); + + virtual void goal_covered(const cover_goalst::goalt &); + + struct goalt + { + // a property holds if all instances of it are true + typedef std::vector instancest; + instancest instances; + std::string description; + + // if failed, we compute a goto_trace for the first failing instance + enum statust { UNKNOWN, FAILURE, SUCCESS, ERROR } status; + goto_tracet goto_trace; + + std::string status_string() const + { + switch(status) + { + case UNKNOWN: return "UNKNOWN"; + case FAILURE: return "FAILURE"; + case SUCCESS: return "SUCCESS"; + case ERROR: return "ERROR"; + } + + // make some poor compilers happy + assert(false); + return ""; + } + + explicit goalt( + const goto_programt::instructiont &instruction): + status(statust::UNKNOWN) + { + description=id2string(instruction.source_location.get_comment()); + } + + goalt():status(statust::UNKNOWN) + { + } + + exprt as_expr() const + { + std::vector tmp; + for(instancest::const_iterator + it=instances.begin(); + it!=instances.end(); + it++) + tmp.push_back(literal_exprt((*it)->cond_literal)); + return conjunction(tmp); + } + }; + + typedef std::map goal_mapt; + goal_mapt goal_map; + +protected: + const goto_functionst &goto_functions; + prop_convt &solver; + bmct &bmc; + + virtual void report(const cover_goalst &cover_goals); + virtual void do_before_solving() {} +}; + diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index f29cfaf43ee..4072452112f 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -513,6 +513,13 @@ safety_checkert::resultt bmct::run( safety_checkert::ERROR:safety_checkert::SAFE; } + if(options.get_option("localize-faults")!="") + { + fault_localizationt fault_localization( + goto_functions, *this, options); + return fault_localization(); + } + // any properties to check at all? if(!options.get_bool_option("program-only") && symex.remaining_vccs==0) @@ -589,11 +596,6 @@ safety_checkert::resultt bmct::stop_on_fail( const goto_functionst &goto_functions, prop_convt &prop_conv) { - if(options.get_bool_option("localize-faults")) - { - //ENHANCE: currently, requires only freezing of guards - prop_conv.set_all_frozen(); - } switch(run_decision_procedure(prop_conv)) { case decision_proceduret::D_UNSATISFIABLE: @@ -609,11 +611,6 @@ safety_checkert::resultt bmct::stop_on_fail( error_trace(); } - if(options.get_bool_option("localize-faults")) - { - fault_localizationt fault_localization(options); - fault_localization(dynamic_cast(prop_conv), equation, ns); - } report_failure(); return UNSAFE; diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 6fced8c362e..815eaa1654f 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -108,6 +108,7 @@ class bmct:public safety_checkert friend class bmc_all_propertiest; friend class bmc_covert; + friend class fault_localizationt; }; #endif diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a01b0bfcff9..731e82bda9c 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -181,8 +181,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("stop-on-fail") || cmdline.isset("property") || cmdline.isset("dimacs") || - cmdline.isset("outfile") || - cmdline.isset("localize-faults")) + cmdline.isset("outfile")) options.set_option("stop-on-fail", true); else options.set_option("stop-on-fail", false); diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index c5798be088c..94bf13a5a60 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -17,6 +17,31 @@ Author: Peter Schrammel #include #include "fault_localization.h" +#include "counterexample_beautification.h" + +/*******************************************************************\ + +Function: fault_localizationt::freeze_guards + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void fault_localizationt::freeze_guards() +{ + for(const auto &step : bmc.equation.SSA_steps) + { + if(!step.guard_literal.is_constant()) + bmc.prop_conv.set_frozen(step.guard_literal); + if(step.is_assert() && + !step.cond_literal.is_constant()) + bmc.prop_conv.set_frozen(step.cond_literal); + } +} /*******************************************************************\ @@ -30,15 +55,15 @@ Function: fault_localizationt::collect_guards \*******************************************************************/ -void fault_localizationt::collect_guards( - const symex_target_equationt &equation) +void fault_localizationt::collect_guards(lpointst &lpoints) { for(symex_target_equationt::SSA_stepst::const_iterator - it=equation.SSA_steps.begin(); - it!=equation.SSA_steps.end(); it++) + it=bmc.equation.SSA_steps.begin(); + it!=bmc.equation.SSA_steps.end(); it++) { if(it->is_assignment() && - it->assignment_type==symex_targett::STATE) + it->assignment_type==symex_targett::STATE && + !it->ignore) { if(!it->guard_literal.is_constant()) { @@ -66,20 +91,18 @@ Function: fault_localizationt::get_failed_property \*******************************************************************/ symex_target_equationt::SSA_stepst::const_iterator -fault_localizationt::get_failed_property( - const prop_convt &prop_conv, - const symex_target_equationt &equation) +fault_localizationt::get_failed_property() { for(symex_target_equationt::SSA_stepst::const_iterator - it=equation.SSA_steps.begin(); - it!=equation.SSA_steps.end(); it++) + it=bmc.equation.SSA_steps.begin(); + it!=bmc.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()) + bmc.prop_conv.l_get(it->guard_literal).is_true() && + bmc.prop_conv.l_get(it->cond_literal).is_false()) return it; assert(false); - return equation.SSA_steps.end(); + return bmc.equation.SSA_steps.end(); } /*******************************************************************\ @@ -94,25 +117,27 @@ Function: fault_localizationt::check \*******************************************************************/ -bool fault_localizationt::check( - prop_convt &prop_conv, - const lpoints_valuet& value) +bool fault_localizationt::check(const lpointst &lpoints, + const lpoints_valuet& value) { assert(value.size()==lpoints.size()); bvt assumptions; - lpointst::const_iterator l_it=lpoints.begin(); lpoints_valuet::const_iterator v_it=value.begin(); - for(; l_it!=lpoints.end(); - ++l_it, ++v_it) + for(const auto &l : lpoints) { if(v_it->is_true()) - assumptions.push_back(l_it->first); + assumptions.push_back(l.first); else if(v_it->is_false()) - assumptions.push_back(!l_it->first); + assumptions.push_back(!l.first); + ++v_it; } - prop_conv.set_assumptions(assumptions); - if(prop_conv()==decision_proceduret::D_SATISFIABLE) + // lock the failed assertion + assumptions.push_back(!failed->cond_literal); + + bmc.prop_conv.set_assumptions(assumptions); + + if(bmc.prop_conv()==decision_proceduret::D_SATISFIABLE) return false; return true; @@ -130,19 +155,20 @@ Function: fault_localizationt::update_scores \*******************************************************************/ -void fault_localizationt::update_scores( - const prop_convt &prop_conv, - const lpoints_valuet& value) +void fault_localizationt::update_scores(lpointst &lpoints, + const lpoints_valuet& value) { - for(lpointst::iterator l_it=lpoints.begin(); - l_it!=lpoints.end(); - ++l_it) + for(auto &l : lpoints) { - if(prop_conv.l_get(l_it->first).is_true()) - l_it->second.score++; - else if(prop_conv.l_get(l_it->first).is_false() && - l_it->second.score>0) - l_it->second.score--; + if(bmc.prop_conv.l_get(l.first).is_true()) + { + l.second.score++; + } + else if(bmc.prop_conv.l_get(l.first).is_false() && + l.second.score>0) + { + l.second.score--; + } } } @@ -158,29 +184,25 @@ Function: fault_localizationt::localize_linear \*******************************************************************/ -void fault_localizationt::localize_linear( - prop_convt &prop_conv) +void fault_localizationt::localize_linear(lpointst &lpoints) { lpoints_valuet v; - for(lpointst::const_iterator l_it=lpoints.begin(); - l_it!=lpoints.end(); - ++l_it) - v.push_back(tvt(tvt::tv_enumt::TV_UNKNOWN)); + v.resize(lpoints.size()); + for(size_t i=0; icond_literal), false); + if(goal_id==ID_nil) + goal_id=failed->source.pc->source_location.get_property_id(); + lpointst &lpoints = lpoints_map[goal_id]; // collect lpoints - collect_guards(equation); + collect_guards(lpoints); if(lpoints.empty()) return; - bv_cbmc.status() << "Localizing fault" - << messaget::eom; + status() << "Localizing fault" << eom; // pick localization method // if(options.get_option("localize-faults-method")=="TBD") - localize_linear(bv_cbmc); + localize_linear(lpoints); - // print results - report(bv_cbmc); + //clear assumptions + bvt assumptions; + bmc.prop_conv.set_assumptions(assumptions); } /*******************************************************************\ @@ -233,23 +251,206 @@ Function: fault_localizationt::report() \*******************************************************************/ -void fault_localizationt::report( - bv_cbmct &bv_cbmc) - +void fault_localizationt::report(irep_idt goal_id) { + if(goal_id==ID_nil) + goal_id=failed->source.pc->source_location.get_property_id(); + lpointst &lpoints = lpoints_map[goal_id]; assert(!lpoints.empty()); - lpointst::const_iterator max=lpoints.begin(); - bv_cbmc.debug() << "Fault localization scores:" << messaget::eom; - for(lpointst::const_iterator l_it=lpoints.begin(); - l_it!=lpoints.end(); - ++l_it) + debug() << "Fault localization scores:" << eom; + lpointt &max=lpoints.begin()->second; + for(auto &l : lpoints) { - bv_cbmc.debug() << l_it->second.target->source_location - << "\n score: " << l_it->second.score << messaget::eom; - if(max->second.scoresecond.score) - max=l_it; + debug() << l.second.target->source_location + << "\n score: " << l.second.score << eom; + if(max.scoresecond.target->source_location - << messaget::eom; + status() << "["+id2string(goal_id)+"]: \n" + << " " << max.target->source_location + << eom; } + +/*******************************************************************\ + +Function: fault_localizationt::operator() + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +safety_checkert::resultt fault_localizationt::operator()() +{ + if(options.get_bool_option("stop-on-fail")) + return stop_on_fail(); + else + return bmc_all_propertiest::operator()(); +} + +/*******************************************************************\ + +Function: fault_localizationt::run_decision_procedure + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +decision_proceduret::resultt +fault_localizationt::run_decision_procedure(prop_convt &prop_conv) +{ + status() << "Passing problem to " + << prop_conv.decision_procedure_text() << eom; + + prop_conv.set_message_handler(bmc.get_message_handler()); + + // stop the time + absolute_timet sat_start=current_time(); + + bmc.do_conversion(); + + freeze_guards(); + + status() << "Running " << prop_conv.decision_procedure_text() + << eom; + + decision_proceduret::resultt dec_result=prop_conv.dec_solve(); + // output runtime + + { + absolute_timet sat_stop=current_time(); + status() << "Runtime decision procedure: " + << (sat_stop-sat_start) << "s" << eom; + } + + return dec_result; +} + +/*******************************************************************\ + +Function: fault_localizationt::stop_on_fail + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +safety_checkert::resultt fault_localizationt::stop_on_fail() +{ + switch(run_decision_procedure(bmc.prop_conv)) + { + case decision_proceduret::D_UNSATISFIABLE: + bmc.report_success(); + return safety_checkert::SAFE; + + case decision_proceduret::D_SATISFIABLE: + if(options.get_bool_option("trace")) + { + if(options.get_bool_option("beautify")) + counterexample_beautificationt()( + dynamic_cast(bmc.prop_conv), bmc.equation, bmc.ns); + + bmc.error_trace(); + } + + //localize faults + run(ID_nil); + status() << "\n** Most likely fault location:" << eom; + report(ID_nil); + + bmc.report_failure(); + return safety_checkert::UNSAFE; + + default: + error() << "decision procedure failed" << eom; + + return safety_checkert::ERROR; + } +} + +/*******************************************************************\ + +Function: fault_localizationt::goal_covered + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void fault_localizationt::goal_covered( + const cover_goalst::goalt &) +{ + for(auto &g : goal_map) + { + // failed already? + if(g.second.status==goalt::statust::FAILURE) continue; + + // check whether failed + for(auto &c : g.second.instances) + { + literalt cond=c->cond_literal; + + if(solver.l_get(cond).is_false()) + { + g.second.status=goalt::statust::FAILURE; + symex_target_equationt::SSA_stepst::iterator next=c; + next++; // include the assertion + build_goto_trace(bmc.equation, next, solver, bmc.ns, + g.second.goto_trace); + + //localize faults + run(g.first); + + break; + } + } + } +} + +/*******************************************************************\ + +Function: fault_localizationt::report + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void fault_localizationt::report( + const cover_goalst &cover_goals) +{ + bmc_all_propertiest::report(cover_goals); + + switch(bmc.ui) + { + case ui_message_handlert::PLAIN: + status() << "\n** Most likely fault location:" << eom; + for(auto &g : goal_map) + { + if(g.second.status!=goalt::statust::FAILURE) continue; + report(g.first); + } + break; + case ui_message_handlert::XML_UI: + break; + case ui_message_handlert::JSON_UI: + break; + } +} + diff --git a/src/cbmc/fault_localization.h b/src/cbmc/fault_localization.h index d135b4e0fad..d57a8a493a1 100644 --- a/src/cbmc/fault_localization.h +++ b/src/cbmc/fault_localization.h @@ -16,26 +16,35 @@ Author: Peter Schrammel #include -#include "bv_cbmc.h" +#include "bmc.h" +#include "all_properties_class.h" -class fault_localizationt +class fault_localizationt: + public bmc_all_propertiest { public: - fault_localizationt(const optionst &_options) - : options(_options) + explicit fault_localizationt( + const goto_functionst &_goto_functions, + bmct &_bmc, + const optionst &_options) + : + bmc_all_propertiest(_goto_functions, _bmc.prop_conv, _bmc), + goto_functions(_goto_functions), + bmc(_bmc), + options(_options) { + set_message_handler(bmc.get_message_handler()); } - virtual ~fault_localizationt() - { - } + safety_checkert::resultt operator()(); + safety_checkert::resultt stop_on_fail(); - void operator()( - bv_cbmct &bv_cbmc, - const symex_target_equationt &equation, - const namespacet &ns); + //override bmc_all_propertiest + virtual void goal_covered(const cover_goalst::goalt &); protected: + const goto_functionst &goto_functions; + bmct &bmc; const optionst &options; // the failed property @@ -47,34 +56,44 @@ class fault_localizationt unsigned score; }; typedef std::map lpointst; - lpointst lpoints; + typedef std::map lpoints_mapt; + lpoints_mapt lpoints_map; + + // this does the actual work + void run(irep_idt goal_id); // this collects the guards as lpoints - void collect_guards( - const symex_target_equationt &equation); + void collect_guards(lpointst &lpoints); + void freeze_guards(); // specify an lpoint combination to check typedef std::vector lpoints_valuet; - bool check( - prop_convt &prop_conv, - const lpoints_valuet& value); - void update_scores( - const prop_convt &prop_conv, - const lpoints_valuet& value); + bool check(const lpointst &lpoints, const lpoints_valuet& value); + void update_scores(lpointst &lpoints, + const lpoints_valuet& value); // localization method: flip each point - void localize_linear( - prop_convt &prop_conv); + void localize_linear(lpointst &lpoints); // localization method: TBD //void localize_TBD( // prop_convt &prop_conv); - symex_target_equationt::SSA_stepst::const_iterator get_failed_property( - const prop_convt &prop_conv, - const symex_target_equationt &equation); + symex_target_equationt::SSA_stepst::const_iterator get_failed_property(); + + decision_proceduret::resultt + run_decision_procedure(prop_convt &prop_conv); - void report(bv_cbmct &bv_cbmc); + void report(irep_idt goal_id); + + //override bmc_all_propertiest + virtual void report(const cover_goalst &cover_goals); + + //override bmc_all_propertiest + virtual void do_before_solving() + { + freeze_guards(); + } }; #endif