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  assert(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
145  assert(failed!=bmc.equation.SSA_steps.end());
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<bv_cbmct &>(bmc.prop_conv), bmc.equation);
284 
285  bmc.error_trace();
286  }
287 
288  // localize faults
289  run(ID_nil);
290 
291  switch(bmc.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)
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 }
bool is_false() const
Definition: threeval.h:26
safety_checkert::resultt stop_on_fail()
Fault Localization.
void do_conversion()
Definition: bmc.cpp:112
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)
goto_programt::const_targett target
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
safety_checkert::resultt operator()()
bool check(const lpointst &lpoints, const lpoints_valuet &value)
const optionst & options
virtual void report_failure()
Definition: bmc.cpp:176
SAT Minimizer.
xmlt report_xml(irep_idt goal_id)
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
void report(irep_idt goal_id)
namespacet ns
Definition: bmc.h:182
virtual void error_trace()
Definition: bmc.cpp:47
virtual resultt dec_solve()=0
Some safety properties were violated.
ui_message_handlert::uit ui
Definition: bmc.h:189
void update_scores(lpointst &lpoints)
source_locationt source_location
Definition: message.h:214
void swap(xmlt &xml)
Definition: xml.cpp:23
prop_convt & prop_conv
Definition: bmc.h:186
Safety is unknown due to an error during safety checking.
safety_checkert::resultt operator()()
API to expression classes.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
Definition: threeval.h:19
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
mstreamt & error() const
Definition: message.h:302
std::vector< tvt > lpoints_valuet
virtual void goal_covered(const cover_goalst::goalt &)
Definition: xml.h:18
Traces of GOTO Programs.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
std::size_t number_covered() const
Definition: cover_goals.h:53
void run(irep_idt goal_id)
std::map< literalt, lpointt > lpointst
std::string data
Definition: xml.h:30
symex_target_equationt::SSA_stepst::const_iterator failed
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
No safety properties were violated.
xmlt & new_element(const std::string &name)
Definition: xml.h:86
bool is_true() const
Definition: threeval.h:25
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
Definition: message.h:153
mstreamt & status() const
Definition: message.h:317
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
virtual void report(const cover_goalst &cover_goals)
#define UNREACHABLE
Definition: invariant.h:271
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
symex_target_equationt equation
Definition: bmc.h:183
virtual void set_frozen(literalt a)
Definition: prop_conv.cpp:24
virtual void report_success()
Definition: bmc.cpp:149
mstreamt & debug() const
Definition: message.h:332
void collect_guards(lpointst &lpoints)
std::vector< literalt > bvt
Definition: literal.h:200
Traces of GOTO Programs.
void localize_linear(lpointst &lpoints)
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop_conv.cpp:19
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0