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 <util/threeval.h>
15 #include <util/arith_tools.h>
16 #include <util/symbol.h>
17 #include <util/std_expr.h>
18 #include <util/message.h>
19 #include <util/time_stopping.h>
20 
21 #include <solvers/prop/minimize.h>
23 
25 
27 
29 {
30  for(const auto &step : bmc.equation.SSA_steps)
31  {
32  if(!step.guard_literal.is_constant())
33  bmc.prop_conv.set_frozen(step.guard_literal);
34  if(step.is_assert() &&
35  !step.cond_literal.is_constant())
36  bmc.prop_conv.set_frozen(step.cond_literal);
37  }
38 }
39 
41 {
42  for(symex_target_equationt::SSA_stepst::const_iterator
43  it=bmc.equation.SSA_steps.begin();
44  it!=bmc.equation.SSA_steps.end(); it++)
45  {
46  if(it->is_assignment() &&
47  it->assignment_type==symex_targett::assignment_typet::STATE &&
48  !it->ignore)
49  {
50  if(!it->guard_literal.is_constant())
51  {
52  lpoints[it->guard_literal].target=it->source.pc;
53  lpoints[it->guard_literal].score=0;
54  }
55  }
56 
57  // reached failed assertion?
58  if(it==failed)
59  break;
60  }
61 }
62 
63 symex_target_equationt::SSA_stepst::const_iterator
65 {
66  for(symex_target_equationt::SSA_stepst::const_iterator
67  it=bmc.equation.SSA_steps.begin();
68  it!=bmc.equation.SSA_steps.end(); it++)
69  if(it->is_assert() &&
70  bmc.prop_conv.l_get(it->guard_literal).is_true() &&
71  bmc.prop_conv.l_get(it->cond_literal).is_false())
72  return it;
73 
74  assert(false);
75  return bmc.equation.SSA_steps.end();
76 }
77 
79  const lpoints_valuet &value)
80 {
81  assert(value.size()==lpoints.size());
82  bvt assumptions;
83  lpoints_valuet::const_iterator v_it=value.begin();
84  for(const auto &l : lpoints)
85  {
86  if(v_it->is_true())
87  assumptions.push_back(l.first);
88  else if(v_it->is_false())
89  assumptions.push_back(!l.first);
90  ++v_it;
91  }
92 
93  // lock the failed assertion
94  assumptions.push_back(!failed->cond_literal);
95 
96  bmc.prop_conv.set_assumptions(assumptions);
97 
99  return false;
100 
101  return true;
102 }
103 
105  const lpoints_valuet &value)
106 {
107  for(auto &l : lpoints)
108  {
109  if(bmc.prop_conv.l_get(l.first).is_true())
110  {
111  l.second.score++;
112  }
113  else if(bmc.prop_conv.l_get(l.first).is_false() &&
114  l.second.score>0)
115  {
116  l.second.score--;
117  }
118  }
119 }
120 
122 {
123  lpoints_valuet v;
124  v.resize(lpoints.size());
125  for(size_t i=0; i<lpoints.size(); ++i)
127  for(size_t i=0; i<v.size(); ++i)
128  {
130  if(!check(lpoints, v))
131  update_scores(lpoints, v);
133  if(!check(lpoints, v))
134  update_scores(lpoints, v);
136  }
137 }
138 
140 {
141  // find failed property
143  assert(failed!=bmc.equation.SSA_steps.end());
144 
145  if(goal_id==ID_nil)
146  goal_id=failed->source.pc->source_location.get_property_id();
147  lpointst &lpoints = lpoints_map[goal_id];
148 
149  // collect lpoints
150  collect_guards(lpoints);
151 
152  if(lpoints.empty())
153  return;
154 
155  status() << "Localizing fault" << eom;
156 
157  // pick localization method
158  // if(options.get_option("localize-faults-method")=="TBD")
159  localize_linear(lpoints);
160 
161  // clear assumptions
162  bvt assumptions;
163  bmc.prop_conv.set_assumptions(assumptions);
164 }
165 
167 {
168  if(goal_id==ID_nil)
169  goal_id=failed->source.pc->source_location.get_property_id();
170 
171  lpointst &lpoints = lpoints_map[goal_id];
172 
173  if(lpoints.empty())
174  {
175  status() << "["+id2string(goal_id)+"]: \n"
176  << " unable to localize fault"
177  << eom;
178  return;
179  }
180 
181  debug() << "Fault localization scores:" << eom;
182  lpointt &max=lpoints.begin()->second;
183  for(auto &l : lpoints)
184  {
185  debug() << l.second.target->source_location
186  << "\n score: " << l.second.score << eom;
187  if(max.score<l.second.score)
188  max=l.second;
189  }
190  status() << "["+id2string(goal_id)+"]: \n"
191  << " " << max.target->source_location
192  << eom;
193 }
194 
196 {
197  if(options.get_bool_option("stop-on-fail"))
198  return stop_on_fail();
199  else
201 }
202 
205 {
206  status() << "Passing problem to "
207  << prop_conv.decision_procedure_text() << eom;
208 
210 
211  // stop the time
212  absolute_timet sat_start=current_time();
213 
214  bmc.do_conversion();
215 
216  freeze_guards();
217 
218  status() << "Running " << prop_conv.decision_procedure_text()
219  << eom;
220 
221  decision_proceduret::resultt dec_result=prop_conv.dec_solve();
222  // output runtime
223 
224  {
225  absolute_timet sat_stop=current_time();
226  status() << "Runtime decision procedure: "
227  << (sat_stop-sat_start) << "s" << eom;
228  }
229 
230  return dec_result;
231 }
232 
234 {
236  {
240 
242  if(options.get_bool_option("trace"))
243  {
244  if(options.get_bool_option("beautify"))
246  dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation, bmc.ns);
247 
248  bmc.error_trace();
249  }
250 
251  // localize faults
252  run(ID_nil);
253  status() << "\n** Most likely fault location:" << eom;
254  report(ID_nil);
255 
258 
259  default:
260  error() << "decision procedure failed" << eom;
261 
263  }
264 }
265 
267  const cover_goalst::goalt &)
268 {
269  for(auto &g : goal_map)
270  {
271  // failed already?
272  if(g.second.status==goalt::statust::FAILURE)
273  continue;
274 
275  // check whether failed
276  for(auto &c : g.second.instances)
277  {
278  literalt cond=c->cond_literal;
279 
280  if(solver.l_get(cond).is_false())
281  {
282  g.second.status=goalt::statust::FAILURE;
283  symex_target_equationt::SSA_stepst::iterator next=c;
284  next++; // include the assertion
286  g.second.goto_trace);
287 
288  // localize faults
289  run(g.first);
290 
291  break;
292  }
293  }
294  }
295 }
296 
298  const cover_goalst &cover_goals)
299 {
300  bmc_all_propertiest::report(cover_goals);
301 
302  switch(bmc.ui)
303  {
305  if(cover_goals.number_covered()>0)
306  {
307  status() << "\n** Most likely fault location:" << eom;
308  for(auto &g : goal_map)
309  {
310  if(g.second.status!=goalt::statust::FAILURE)
311  continue;
312  report(g.first);
313  }
314  }
315  break;
317  break;
319  break;
320  }
321 }
bool is_false() const
Definition: threeval.h:26
safety_checkert::resultt stop_on_fail()
Fault Localization.
void do_conversion()
Definition: bmc.cpp:118
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)
mstreamt & status()
Definition: message.h:238
const optionst & options
virtual void report_failure()
Definition: bmc.cpp:193
SAT Minimizer.
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void report(irep_idt goal_id)
namespacet ns
Definition: bmc.h:71
virtual void error_trace()
Definition: bmc.cpp:51
virtual resultt dec_solve()=0
source_locationt source_location
Definition: message.h:175
prop_convt & prop_conv
Definition: bmc.h:74
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
std::vector< tvt > lpoints_valuet
virtual void goal_covered(const cover_goalst::goalt &)
Time Stopping.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
std::size_t number_covered() const
Definition: cover_goals.h:51
void run(irep_idt goal_id)
std::map< literalt, lpointt > lpointst
symex_target_equationt::SSA_stepst::const_iterator failed
language_uit::uit ui
Definition: bmc.h:77
bool is_true() const
Definition: threeval.h:25
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
mstreamt & debug()
Definition: message.h:253
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
Definition: message.h:127
absolute_timet current_time()
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
virtual void report(const cover_goalst &cover_goals)
Traces of GOTO Programs.
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
mstreamt & error()
Definition: message.h:223
symex_target_equationt equation
Definition: bmc.h:72
virtual void set_frozen(literalt a)
Definition: prop_conv.cpp:34
virtual void report_success()
Definition: bmc.cpp:165
void collect_guards(lpointst &lpoints)
void update_scores(lpointst &lpoints, const lpoints_valuet &value)
std::vector< literalt > bvt
Definition: literal.h:197
void localize_linear(lpointst &lpoints)
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)
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop_conv.cpp:29
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0