basic fault localization

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) \

src/cbmc/bmc.cpp

@@ -35,6 +35,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-symex/memory_model_pso.h>
 
 #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<bv_cbmct &>(prop_conv), equation, ns);
+    }
 
     report_failure();
     return UNSAFE;

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"

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:

src/cbmc/fault_localization.cpp

@@ -0,0 +1,255 @@
+/*******************************************************************\
+
+Module: Fault Localization
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#include <util/threeval.h>
+#include <util/expr_util.h>
+#include <util/arith_tools.h>
+#include <util/symbol.h>
+#include <util/std_expr.h>
+#include <util/message.h>
+
+#include <solvers/prop/minimize.h>
+#include <solvers/prop/literal_expr.h>
+
+#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; i<v.size(); ++i)
+  {
+    v[i]=tvt(tvt::tv_enumt::TV_TRUE);
+    if(!check(prop_conv, v))
+      update_scores(prop_conv, v);
+    v[i]=tvt(tvt::tv_enumt::TV_FALSE);
+    if(!check(prop_conv, v))
+      update_scores(prop_conv, v);
+    v[i]=tvt(tvt::tv_enumt::TV_UNKNOWN);
+  }
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::operator()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void fault_localizationt::operator()(
+  bv_cbmct &bv_cbmc,
+  const symex_target_equationt &equation,
+  const namespacet &ns)
+{
+  // find failed property
+  failed=get_failed_property(bv_cbmc, equation);
+
+  if(failed==equation.SSA_steps.end())
+    return;
+
+  // lock the failed assertion
+  bv_cbmc.set_to(literal_exprt(failed->cond_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.score<l_it->second.score)
+      max=l_it;
+  }
+  bv_cbmc.status() << "Most likely fault location: \n"
+                   << "  " << max->second.target->source_location
+                   << messaget::eom;
+}