cprover
goto_symex_fault_localizer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fault Localization for Goto Symex
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
15  const optionst &options,
16  ui_message_handlert &ui_message_handler,
17  const symex_target_equationt &equation,
19  : options(options),
20  ui_message_handler(ui_message_handler),
21  equation(equation),
22  solver(solver)
23 {
24 }
25 
27 operator()(const irep_idt &failed_property_id)
28 {
29  fault_location_infot fault_location;
30  localization_pointst localization_points;
31  const auto &failed_step =
32  collect_guards(failed_property_id, localization_points, fault_location);
33 
34  if(!localization_points.empty())
35  {
37  log.status() << "Localizing fault" << messaget::eom;
38 
39  // pick localization method
40  // if(options.get_option("localize-faults-method")=="TBD")
41  localize_linear(failed_step, localization_points);
42  }
43 
44  return fault_location;
45 }
46 
48  const irep_idt &failed_property_id,
49  localization_pointst &localization_points,
50  fault_location_infot &fault_location)
51 {
52  for(const auto &step : equation.SSA_steps)
53  {
54  if(
55  step.is_assignment() &&
56  step.assignment_type == symex_targett::assignment_typet::STATE &&
57  !step.ignore)
58  {
59  exprt l = solver.handle(step.guard_handle);
60  if(!l.is_constant())
61  {
62  auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
63  localization_points.emplace(l, emplace_result.first);
64  }
65  }
66 
67  // reached failed assertion?
68  if(step.is_assert() && step.get_property_id() == failed_property_id)
69  return step;
70  }
72 }
73 
75  const SSA_stept &failed_step,
76  const localization_pointst &localization_points,
77  const localization_points_valuet &value)
78 {
79  PRECONDITION(value.size() == localization_points.size());
80  std::vector<exprt> assumptions;
81  localization_points_valuet::const_iterator v_it = value.begin();
82  for(const auto &l : localization_points)
83  {
84  if(v_it->is_true())
85  assumptions.push_back(l.first);
86  else if(v_it->is_false())
87  assumptions.push_back(solver.handle(not_exprt(l.first)));
88  ++v_it;
89  }
90 
91  // lock the failed assertion
92  assumptions.push_back(solver.handle(not_exprt(failed_step.cond_handle)));
93 
94  solver.push(assumptions);
95 
97 }
98 
100  const localization_pointst &localization_points)
101 {
102  for(auto &l : localization_points)
103  {
104  auto &score = l.second->second;
105  if(solver.get(l.first).is_true())
106  {
107  score++;
108  }
109  else if(solver.get(l.first).is_false() && score > 0)
110  {
111  score--;
112  }
113  }
114 }
115 
117  const SSA_stept &failed_step,
118  const localization_pointst &localization_points)
119 {
120  localization_points_valuet v(localization_points.size(), tvt::unknown());
121 
122  for(std::size_t i = 0; i < v.size(); ++i)
123  {
124  v[i] = tvt(tvt::tv_enumt::TV_TRUE);
125  if(!check(failed_step, localization_points, v))
126  update_scores(localization_points);
127 
129  if(!check(failed_step, localization_points, v))
130  update_scores(localization_points);
131 
132  v[i] = tvt::unknown();
133  }
134 
135  // clear assumptions
136  solver.pop();
137 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
decision_proceduret::get
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_symex_fault_localizert::collect_guards
const SSA_stept & collect_guards(const irep_idt &failed_property_id, localization_pointst &localization_points, fault_location_infot &fault_location)
Collects the guards as localization_points up to failed_property_id and initializes fault_location_in...
Definition: goto_symex_fault_localizer.cpp:47
goto_symex_fault_localizert::update_scores
void update_scores(const localization_pointst &)
Definition: goto_symex_fault_localizer.cpp:99
SSA_stept::cond_handle
exprt cond_handle
Definition: ssa_step.h:148
ui_message_handlert
Definition: ui_message.h:20
optionst
Definition: options.h:23
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
stack_decision_proceduret::push
virtual void push(const std::vector< exprt > &assumptions)=0
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
messaget::status
mstreamt & status() const
Definition: message.h:414
goto_symex_fault_localizert::localization_pointst
std::map< exprt, fault_location_infot::score_mapt::iterator > localization_pointst
A localization point is a goto instruction that is potentially at fault.
Definition: goto_symex_fault_localizer.h:44
exprt
Base class for all expressions.
Definition: expr.h:53
fault_location_infot
Definition: fault_localization_provider.h:23
goto_symex_fault_localizert::localization_points_valuet
std::vector< tvt > localization_points_valuet
Definition: goto_symex_fault_localizer.h:55
messaget::eom
static eomt eom
Definition: message.h:297
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
stack_decision_proceduret
Definition: stack_decision_procedure.h:58
goto_symex_fault_localizert::equation
const symex_target_equationt & equation
Definition: goto_symex_fault_localizer.h:39
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
symex_targett::assignment_typet::STATE
@ STATE
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
tvt::tv_enumt::TV_TRUE
@ TV_TRUE
goto_symex_fault_localizert::operator()
fault_location_infot operator()(const irep_idt &failed_property_id)
Definition: goto_symex_fault_localizer.cpp:27
fault_location_infot::scores
score_mapt scores
Definition: fault_localization_provider.h:25
goto_symex_fault_localizert::check
bool check(const SSA_stept &failed_step, const localization_pointst &, const localization_points_valuet &)
Definition: goto_symex_fault_localizer.cpp:74
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
goto_symex_fault_localizert::solver
stack_decision_proceduret & solver
Definition: goto_symex_fault_localizer.h:40
goto_symex_fault_localizert::localize_linear
void localize_linear(const SSA_stept &failed_step, const localization_pointst &)
Definition: goto_symex_fault_localizer.cpp:116
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
decision_proceduret::handle
virtual exprt handle(const exprt &expr)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
tvt
Definition: threeval.h:20
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:364
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
goto_symex_fault_localizer.h
Fault Localization for Goto Symex.
stack_decision_proceduret::pop
virtual void pop()=0
Pop whatever is on top of the stack.
tvt::tv_enumt::TV_FALSE
@ TV_FALSE
goto_symex_fault_localizert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: goto_symex_fault_localizer.h:38
goto_symex_fault_localizert::goto_symex_fault_localizert
goto_symex_fault_localizert(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation, stack_decision_proceduret &solver)
Definition: goto_symex_fault_localizer.cpp:14
not_exprt
Boolean negation.
Definition: std_expr.h:2843