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 }
Single SSA step in the equation.
Definition: ssa_step.h:45
exprt cond_handle
Definition: ssa_step.h:148
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
ui_message_handlert & ui_message_handler
bool check(const SSA_stept &failed_step, const localization_pointst &, const localization_points_valuet &)
std::map< exprt, fault_location_infot::score_mapt::iterator > localization_pointst
A localization point is a goto instruction that is potentially at fault.
goto_symex_fault_localizert(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation, stack_decision_proceduret &solver)
fault_location_infot operator()(const irep_idt &failed_property_id)
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...
stack_decision_proceduret & solver
void update_scores(const localization_pointst &)
void localize_linear(const SSA_stept &failed_step, const localization_pointst &)
const symex_target_equationt & equation
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
Boolean negation.
Definition: std_expr.h:2042
virtual void pop()=0
Pop whatever is on top of the stack.
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.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: threeval.h:20
static tvt unknown()
Definition: threeval.h:33
Fault Localization for Goto Symex.
int solver(std::istream &in)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define PRECONDITION(CONDITION)
Definition: invariant.h:464