cprover
fault_localization.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fault Localization
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "fault_localization.h"
13 
14 #include <chrono>
15 
16 #include <util/threeval.h>
17 #include <util/arith_tools.h>
18 #include <util/symbol.h>
19 #include <util/std_expr.h>
20 #include <util/message.h>
21 #include <util/xml_expr.h>
22 
23 #include <solvers/prop/minimize.h>
25 
28 
30 
32 {
33  for(const auto &step : bmc.equation.SSA_steps)
34  {
35  if(!step.guard_literal.is_constant())
36  bmc.prop_conv.set_frozen(step.guard_literal);
37  if(step.is_assert() &&
38  !step.cond_literal.is_constant())
39  bmc.prop_conv.set_frozen(step.cond_literal);
40  }
41 }
42 
44 {
45  for(symex_target_equationt::SSA_stepst::const_iterator
46  it=bmc.equation.SSA_steps.begin();
47  it!=bmc.equation.SSA_steps.end(); it++)
48  {
49  if(it->is_assignment() &&
50  it->assignment_type==symex_targett::assignment_typet::STATE &&
51  !it->ignore)
52  {
53  if(!it->guard_literal.is_constant())
54  {
55  lpoints[it->guard_literal].target=it->source.pc;
56  lpoints[it->guard_literal].score=0;
57  }
58  }
59 
60  // reached failed assertion?
61  if(it==failed)
62  break;
63  }
64 }
65 
66 symex_target_equationt::SSA_stepst::const_iterator
68 {
69  for(symex_target_equationt::SSA_stepst::const_iterator
70  it=bmc.equation.SSA_steps.begin();
71  it!=bmc.equation.SSA_steps.end(); it++)
72  if(it->is_assert() &&
73  bmc.prop_conv.l_get(it->guard_literal).is_true() &&
74  bmc.prop_conv.l_get(it->cond_literal).is_false())
75  return it;
76 
78  return bmc.equation.SSA_steps.end();
79 }
80 
82  const lpoints_valuet &value)
83 {
84  PRECONDITION(value.size() == lpoints.size());
85  bvt assumptions;
86  lpoints_valuet::const_iterator v_it=value.begin();
87  for(const auto &l : lpoints)
88  {
89  if(v_it->is_true())
90  assumptions.push_back(l.first);
91  else if(v_it->is_false())
92  assumptions.push_back(!l.first);
93  ++v_it;
94  }
95 
96  // lock the failed assertion
97  assumptions.push_back(!failed->cond_literal);
98 
99  bmc.prop_conv.set_assumptions(assumptions);
100 
102  return false;
103 
104  return true;
105 }
106 
108 {
109  for(auto &l : lpoints)
110  {
111  if(bmc.prop_conv.l_get(l.first).is_true())
112  {
113  l.second.score++;
114  }
115  else if(bmc.prop_conv.l_get(l.first).is_false() &&
116  l.second.score>0)
117  {
118  l.second.score--;
119  }
120  }
121 }
122 
124 {
125  lpoints_valuet v;
126  v.resize(lpoints.size());
127  for(size_t i=0; i<lpoints.size(); ++i)
129  for(size_t i=0; i<v.size(); ++i)
130  {
132  if(!check(lpoints, v))
133  update_scores(lpoints);
135  if(!check(lpoints, v))
136  update_scores(lpoints);
138  }
139 }
140 
142 {
143  // find failed property
146 
147  if(goal_id==ID_nil)
148  goal_id=failed->source.pc->source_location.get_property_id();
149  lpointst &lpoints=lpoints_map[goal_id];
150 
151  // collect lpoints
152  collect_guards(lpoints);
153 
154  if(lpoints.empty())
155  return;
156 
157  status() << "Localizing fault" << eom;
158 
159  // pick localization method
160  // if(options.get_option("localize-faults-method")=="TBD")
161  localize_linear(lpoints);
162 
163  // clear assumptions
164  bvt assumptions;
165  bmc.prop_conv.set_assumptions(assumptions);
166 }
167 
169 {
170  if(goal_id==ID_nil)
171  goal_id=failed->source.pc->source_location.get_property_id();
172 
173  lpointst &lpoints=lpoints_map[goal_id];
174 
175  if(lpoints.empty())
176  {
177  status() << "["+id2string(goal_id)+"]: \n"
178  << " unable to localize fault"
179  << eom;
180  return;
181  }
182 
183  debug() << "Fault localization scores:" << eom;
184  lpointt &max=lpoints.begin()->second;
185  for(auto &l : lpoints)
186  {
187  debug() << l.second.target->source_location
188  << "\n score: " << l.second.score << eom;
189  if(max.score<l.second.score)
190  max=l.second;
191  }
192  status() << "["+id2string(goal_id)+"]: \n"
193  << " " << max.target->source_location
194  << eom;
195 }
196 
198 {
199  xmlt xml_diagnosis("diagnosis");
200  xml_diagnosis.new_element("method").data="linear fault localization";
201 
202  if(goal_id==ID_nil)
203  goal_id=failed->source.pc->source_location.get_property_id();
204 
205  xml_diagnosis.set_attribute("property", id2string(goal_id));
206 
207  const lpointst &lpoints=lpoints_map[goal_id];
208 
209  if(lpoints.empty())
210  {
211  xml_diagnosis.new_element("result").data="unable to localize fault";
212  return xml_diagnosis;
213  }
214 
215  debug() << "Fault localization scores:" << eom;
216  const lpointt *max=&lpoints.begin()->second;
217  for(const auto &pair : lpoints)
218  {
219  const auto &value=pair.second;
220  debug() << value.target->source_location
221  << "\n score: " << value.score << eom;
222  if(max->score<value.score)
223  max=&value;
224  }
225 
226  xmlt xml_location=xml(max->target->source_location);
227  xml_diagnosis.new_element("result").new_element().swap(xml_location);
228 
229  return xml_diagnosis;
230 }
231 
233 {
234  if(options.get_bool_option("stop-on-fail"))
235  return stop_on_fail();
236  else
238 }
239 
242 {
243  status() << "Passing problem to "
244  << prop_conv.decision_procedure_text() << eom;
245 
247 
248  auto solver_start=std::chrono::steady_clock::now();
249 
250  bmc.do_conversion();
251 
252  freeze_guards();
253 
254  status() << "Running " << prop_conv.decision_procedure_text()
255  << eom;
256 
257  decision_proceduret::resultt dec_result=prop_conv.dec_solve();
258  // output runtime
259 
260  {
261  auto solver_stop=std::chrono::steady_clock::now();
262  status() << "Runtime decision procedure: "
263  << std::chrono::duration<double>(solver_stop-solver_start).count()
264  << "s" << eom;
265  }
266 
267  return dec_result;
268 }
269 
271 {
273  {
277 
279  if(options.get_bool_option("trace"))
280  {
281  if(options.get_bool_option("beautify"))
283  dynamic_cast<boolbvt &>(bmc.prop_conv), bmc.equation);
284 
285  bmc.error_trace();
286  }
287 
288  // localize faults
289  run(ID_nil);
290 
291  switch(bmc.ui_message_handler.get_ui())
292  {
294  {
295  status() << "\n** Most likely fault location:" << eom;
296  report(ID_nil);
297  break;
298  }
300  {
301  xmlt dest("fault-localization");
302  xmlt xml_diagnosis=report_xml(ID_nil);
303  dest.new_element().swap(xml_diagnosis);
304  status() << dest;
305  break;
306  }
308  // not implemented
309  break;
310  }
311 
314 
315  default:
316  error() << "decision procedure failed" << eom;
317 
319  }
320 }
321 
323  const cover_goalst::goalt &)
324 {
325  for(auto &goal_pair : goal_map)
326  {
327  // failed already?
328  if(goal_pair.second.status==goalt::statust::FAILURE)
329  continue;
330 
331  // check whether failed
332  for(auto &inst : goal_pair.second.instances)
333  {
334  literalt cond=inst->cond_literal;
335 
336  if(solver.l_get(cond).is_false())
337  {
338  goal_pair.second.status=goalt::statust::FAILURE;
340  bmc.equation, inst, solver, bmc.ns, goal_pair.second.goto_trace);
341 
342  // localize faults
343  run(goal_pair.first);
344 
345  break;
346  }
347  }
348  }
349 }
350 
352  const cover_goalst &cover_goals)
353 {
354  bmc_all_propertiest::report(cover_goals);
355 
356  switch(bmc.ui_message_handler.get_ui())
357  {
359  if(cover_goals.number_covered()>0)
360  {
361  status() << "\n** Most likely fault location:" << eom;
362  for(auto &goal_pair : goal_map)
363  {
364  if(goal_pair.second.status!=goalt::statust::FAILURE)
365  continue;
366  report(goal_pair.first);
367  }
368  }
369  break;
371  {
372  xmlt dest("fault-localization");
373  for(auto &goal_pair : goal_map)
374  {
375  if(goal_pair.second.status!=goalt::statust::FAILURE)
376  continue;
377  xmlt xml_diagnosis=report_xml(goal_pair.first);
378  dest.new_element().swap(xml_diagnosis);
379  }
380  status() << dest;
381  }
382  break;
384  // not implemented
385  break;
386  }
387 }
fault_localizationt::lpoints_valuet
std::vector< tvt > lpoints_valuet
Definition: fault_localization.h:73
fault_localizationt::report_xml
xmlt report_xml(irep_idt goal_id)
Definition: fault_localization.cpp:197
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
fault_localization.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
prop_convt::set_assumptions
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop_conv.cpp:19
arith_tools.h
bmct::report_success
virtual void report_success()
Definition: bmc.cpp:155
build_goto_trace
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
Definition: build_goto_trace.cpp:166
ui_message_handlert::uit::XML_UI
@ XML_UI
fault_localizationt::report
void report(irep_idt goal_id)
Definition: fault_localization.cpp:168
prop_convt
Definition: prop_conv.h:27
bvt
std::vector< literalt > bvt
Definition: literal.h:200
bmc_all_propertiest::goal_map
goal_mapt goal_map
Definition: all_properties_class.h:87
threeval.h
messaget::status
mstreamt & status() const
Definition: message.h:401
safety_checkert::resultt::SAFE
@ SAFE
No safety properties were violated.
bmc_all_propertiest::report
virtual void report(const cover_goalst &cover_goals)
Definition: all_properties.cpp:154
fault_localizationt::run
void run(irep_idt goal_id)
Definition: fault_localization.cpp:141
xml
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
counterexample_beautificationt
Definition: counterexample_beautification.h:21
fault_localizationt::collect_guards
void collect_guards(lpointst &lpoints)
Definition: fault_localization.cpp:43
minimize.h
fault_localizationt::operator()
safety_checkert::resultt operator()()
Definition: fault_localization.cpp:232
fault_localizationt::lpointt
Definition: fault_localization.h:56
fault_localizationt::localize_linear
void localize_linear(lpointst &lpoints)
Definition: fault_localization.cpp:123
messaget::eom
static eomt eom
Definition: message.h:284
fault_localizationt::get_failed_property
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
Definition: fault_localization.cpp:67
cover_goalst
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
cover_goalst::number_covered
std::size_t number_covered() const
Definition: cover_goals.h:53
symex_targett::assignment_typet::STATE
@ STATE
bmct::error_trace
virtual void error_trace()
Definition: bmc.cpp:51
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
bmct::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: bmc.h:178
fault_localizationt::failed
symex_target_equationt::SSA_stepst::const_iterator failed
Definition: fault_localization.h:53
tvt::tv_enumt::TV_TRUE
@ TV_TRUE
messaget::error
mstreamt & error() const
Definition: message.h:386
fault_localizationt::lpointt::target
goto_programt::const_targett target
Definition: fault_localization.h:58
bmct::ns
namespacet ns
Definition: bmc.h:171
bmc_all_propertiest::operator()
safety_checkert::resultt operator()()
Definition: all_properties.cpp:50
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
ui_message_handlert::uit::JSON_UI
@ JSON_UI
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
xml_goto_trace.h
decision_proceduret::dec_solve
virtual resultt dec_solve()=0
bmct::prop_conv
prop_convt & prop_conv
Definition: bmc.h:175
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
fault_localizationt::lpointt::score
unsigned score
Definition: fault_localization.h:59
symbol.h
Symbol table entry.
fault_localizationt::bmc
bmct & bmc
Definition: fault_localization.h:49
tvt::is_false
bool is_false() const
Definition: threeval.h:26
safety_checkert::resultt::ERROR
@ ERROR
Safety is unknown due to an error during safety checking.
xmlt
Definition: xml.h:18
prop_convt::l_get
virtual tvt l_get(literalt a) const =0
fault_localizationt::goal_covered
virtual void goal_covered(const cover_goalst::goalt &)
Definition: fault_localization.cpp:322
safety_checkert::resultt::UNSAFE
@ UNSAFE
Some safety properties were violated.
tvt
Definition: threeval.h:19
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
decision_proceduret::decision_procedure_text
virtual std::string decision_procedure_text() const =0
ui_message_handlert::get_ui
uit get_ui() const
Definition: ui_message.h:30
safety_checkert::resultt
resultt
Definition: safety_checker.h:33
fault_localizationt::stop_on_fail
safety_checkert::resultt stop_on_fail()
Definition: fault_localization.cpp:270
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
prop_convt::set_frozen
virtual void set_frozen(literalt a)
Definition: prop_conv.cpp:24
bmc_all_propertiest::solver
prop_convt & solver
Definition: all_properties_class.h:91
fault_localizationt::freeze_guards
void freeze_guards()
Definition: fault_localization.cpp:31
ui_message_handlert::uit::PLAIN
@ PLAIN
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
bmct::equation
symex_target_equationt equation
Definition: bmc.h:172
build_goto_trace.h
literalt
Definition: literal.h:24
xmlt::swap
void swap(xmlt &xml)
Definition: xml.cpp:24
boolbvt
Definition: boolbv.h:32
counterexample_beautification.h
tvt::tv_enumt::TV_UNKNOWN
@ TV_UNKNOWN
bmct::report_failure
virtual void report_failure()
Definition: bmc.cpp:187
fault_localizationt::options
const optionst & options
Definition: fault_localization.h:50
messaget::debug
mstreamt & debug() const
Definition: message.h:416
cover_goalst::goalt
Definition: cover_goals.h:38
message.h
xmlt::data
std::string data
Definition: xml.h:30
fault_localizationt::lpointst
std::map< literalt, lpointt > lpointst
Definition: fault_localization.h:61
tvt::tv_enumt::TV_FALSE
@ TV_FALSE
std_expr.h
fault_localizationt::run_decision_procedure
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Definition: fault_localization.cpp:241
bmct::do_conversion
void do_conversion()
Definition: bmc.cpp:118
fault_localizationt::lpoints_map
lpoints_mapt lpoints_map
Definition: fault_localization.h:63
xml_expr.h
literal_expr.h
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:86
tvt::is_true
bool is_true() const
Definition: threeval.h:25
fault_localizationt::update_scores
void update_scores(lpointst &lpoints)
Definition: fault_localization.cpp:107
fault_localizationt::check
bool check(const lpointst &lpoints, const lpoints_valuet &value)
Definition: fault_localization.cpp:81