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  const lpoints_valuet &value)
109 {
110  for(auto &l : lpoints)
111  {
112  if(bmc.prop_conv.l_get(l.first).is_true())
113  {
114  l.second.score++;
115  }
116  else if(bmc.prop_conv.l_get(l.first).is_false() &&
117  l.second.score>0)
118  {
119  l.second.score--;
120  }
121  }
122 }
123 
125 {
126  lpoints_valuet v;
127  v.resize(lpoints.size());
128  for(size_t i=0; i<lpoints.size(); ++i)
130  for(size_t i=0; i<v.size(); ++i)
131  {
133  if(!check(lpoints, v))
134  update_scores(lpoints, v);
136  if(!check(lpoints, v))
137  update_scores(lpoints, v);
139  }
140 }
141 
143 {
144  // find failed property
146  assert(failed!=bmc.equation.SSA_steps.end());
147 
148  if(goal_id==ID_nil)
149  goal_id=failed->source.pc->source_location.get_property_id();
150  lpointst &lpoints=lpoints_map[goal_id];
151 
152  // collect lpoints
153  collect_guards(lpoints);
154 
155  if(lpoints.empty())
156  return;
157 
158  status() << "Localizing fault" << eom;
159 
160  // pick localization method
161  // if(options.get_option("localize-faults-method")=="TBD")
162  localize_linear(lpoints);
163 
164  // clear assumptions
165  bvt assumptions;
166  bmc.prop_conv.set_assumptions(assumptions);
167 }
168 
170 {
171  if(goal_id==ID_nil)
172  goal_id=failed->source.pc->source_location.get_property_id();
173 
174  lpointst &lpoints=lpoints_map[goal_id];
175 
176  if(lpoints.empty())
177  {
178  status() << "["+id2string(goal_id)+"]: \n"
179  << " unable to localize fault"
180  << eom;
181  return;
182  }
183 
184  debug() << "Fault localization scores:" << eom;
185  lpointt &max=lpoints.begin()->second;
186  for(auto &l : lpoints)
187  {
188  debug() << l.second.target->source_location
189  << "\n score: " << l.second.score << eom;
190  if(max.score<l.second.score)
191  max=l.second;
192  }
193  status() << "["+id2string(goal_id)+"]: \n"
194  << " " << max.target->source_location
195  << eom;
196 }
197 
199 {
200  xmlt xml_diagnosis("diagnosis");
201  xml_diagnosis.new_element("method").data="linear fault localization";
202 
203  if(goal_id==ID_nil)
204  goal_id=failed->source.pc->source_location.get_property_id();
205 
206  xml_diagnosis.set_attribute("property", id2string(goal_id));
207 
208  const lpointst &lpoints=lpoints_map[goal_id];
209 
210  if(lpoints.empty())
211  {
212  xml_diagnosis.new_element("result").data="unable to localize fault";
213  return xml_diagnosis;
214  }
215 
216  debug() << "Fault localization scores:" << eom;
217  const lpointt *max=&lpoints.begin()->second;
218  for(const auto &pair : lpoints)
219  {
220  const auto &value=pair.second;
221  debug() << value.target->source_location
222  << "\n score: " << value.score << eom;
223  if(max->score<value.score)
224  max=&value;
225  }
226 
227  xmlt xml_location=xml(max->target->source_location);
228  xml_diagnosis.new_element("result").new_element().swap(xml_location);
229 
230  return xml_diagnosis;
231 }
232 
234 {
235  if(options.get_bool_option("stop-on-fail"))
236  return stop_on_fail();
237  else
239 }
240 
243 {
244  status() << "Passing problem to "
245  << prop_conv.decision_procedure_text() << eom;
246 
248 
249  auto solver_start=std::chrono::steady_clock::now();
250 
251  bmc.do_conversion();
252 
253  freeze_guards();
254 
255  status() << "Running " << prop_conv.decision_procedure_text()
256  << eom;
257 
258  decision_proceduret::resultt dec_result=prop_conv.dec_solve();
259  // output runtime
260 
261  {
262  auto solver_stop=std::chrono::steady_clock::now();
263  status() << "Runtime decision procedure: "
264  << std::chrono::duration<double>(solver_stop-solver_start).count()
265  << "s" << eom;
266  }
267 
268  return dec_result;
269 }
270 
272 {
274  {
278 
280  if(options.get_bool_option("trace"))
281  {
282  if(options.get_bool_option("beautify"))
284  dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation, bmc.ns);
285 
286  bmc.error_trace();
287  }
288 
289  // localize faults
290  run(ID_nil);
291 
292  switch(bmc.ui)
293  {
295  {
296  status() << "\n** Most likely fault location:" << eom;
297  report(ID_nil);
298  break;
299  }
301  {
302  xmlt dest("fault-localization");
303  xmlt xml_diagnosis=report_xml(ID_nil);
304  dest.new_element().swap(xml_diagnosis);
305  status() << dest;
306  break;
307  }
309  // not implemented
310  break;
311  }
312 
315 
316  default:
317  error() << "decision procedure failed" << eom;
318 
320  }
321 }
322 
324  const cover_goalst::goalt &)
325 {
326  for(auto &goal_pair : goal_map)
327  {
328  // failed already?
329  if(goal_pair.second.status==goalt::statust::FAILURE)
330  continue;
331 
332  // check whether failed
333  for(auto &inst : goal_pair.second.instances)
334  {
335  literalt cond=inst->cond_literal;
336 
337  if(solver.l_get(cond).is_false())
338  {
339  goal_pair.second.status=goalt::statust::FAILURE;
340  symex_target_equationt::SSA_stepst::iterator next=inst;
341  next++; // include the assertion
343  bmc.equation, next, solver, bmc.ns, goal_pair.second.goto_trace);
344 
345  // localize faults
346  run(goal_pair.first);
347 
348  break;
349  }
350  }
351  }
352 }
353 
355  const cover_goalst &cover_goals)
356 {
357  bmc_all_propertiest::report(cover_goals);
358 
359  switch(bmc.ui)
360  {
362  if(cover_goals.number_covered()>0)
363  {
364  status() << "\n** Most likely fault location:" << eom;
365  for(auto &goal_pair : goal_map)
366  {
367  if(goal_pair.second.status!=goalt::statust::FAILURE)
368  continue;
369  report(goal_pair.first);
370  }
371  }
372  break;
374  {
375  xmlt dest("fault-localization");
376  for(auto &goal_pair : goal_map)
377  {
378  if(goal_pair.second.status!=goalt::statust::FAILURE)
379  continue;
380  xmlt xml_diagnosis=report_xml(goal_pair.first);
381  dest.new_element().swap(xml_diagnosis);
382  }
383  status() << dest;
384  }
385  break;
387  // not implemented
388  break;
389  }
390 }
bool is_false() const
Definition: threeval.h:26
safety_checkert::resultt stop_on_fail()
Fault Localization.
void do_conversion()
Definition: bmc.cpp:112
goto_programt::const_targett target
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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
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
No safety properties were violated.
xmlt & new_element(const std::string &name)
Definition: xml.h:86
bool is_true() const
Definition: threeval.h:25
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
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:250
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)
void update_scores(lpointst &lpoints, const lpoints_valuet &value)
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