cprover
Loading...
Searching...
No Matches
goto_symex_fault_localizer.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Fault Localization for Goto Symex
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
13
14#include <util/ui_message.h>
15
17
19
31
33operator()(const irep_idt &failed_property_id)
34{
35 fault_location_infot fault_location;
36 localization_pointst localization_points;
37 const auto &failed_step =
38 collect_guards(failed_property_id, localization_points, fault_location);
39
40 if(!localization_points.empty())
41 {
43 log.status() << "Localizing fault" << messaget::eom;
44
45 // pick localization method
46 // if(options.get_option("localize-faults-method")=="TBD")
47 localize_linear(failed_step, localization_points);
48 }
49
50 return fault_location;
51}
52
54 const irep_idt &failed_property_id,
55 localization_pointst &localization_points,
56 fault_location_infot &fault_location)
57{
58 for(const auto &step : equation.SSA_steps)
59 {
60 if(
61 step.is_assignment() &&
62 step.assignment_type == symex_targett::assignment_typet::STATE &&
63 !step.ignore)
64 {
65 exprt l = solver.handle(step.guard_handle);
66 if(!l.is_constant())
67 {
68 auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
69 localization_points.emplace(l, emplace_result.first);
70 }
71 }
72 else if(step.is_assert() && step.property_id == failed_property_id)
73 {
74 return step;
75 }
76 }
78}
79
81 const SSA_stept &failed_step,
82 const localization_pointst &localization_points,
83 const localization_points_valuet &value)
84{
85 PRECONDITION(value.size() == localization_points.size());
86 std::vector<exprt> assumptions;
87 localization_points_valuet::const_iterator v_it = value.begin();
88 for(const auto &l : localization_points)
89 {
90 if(v_it->is_true())
91 assumptions.push_back(l.first);
92 else if(v_it->is_false())
93 assumptions.push_back(solver.handle(not_exprt(l.first)));
94 ++v_it;
95 }
96
97 // lock the failed assertion
98 assumptions.push_back(not_exprt(failed_step.cond_handle));
99
100 solver.push(assumptions);
101
103}
104
106 const localization_pointst &localization_points)
107{
108 for(auto &l : localization_points)
109 {
110 auto &score = l.second->second;
111 if(solver.get(l.first).is_true())
112 {
113 score++;
114 }
115 else if(solver.get(l.first).is_false() && score > 0)
116 {
117 score--;
118 }
119 }
120}
121
123 const SSA_stept &failed_step,
124 const localization_pointst &localization_points)
125{
126 localization_points_valuet v(localization_points.size(), tvt::unknown());
127
128 for(std::size_t i = 0; i < v.size(); ++i)
129 {
131 if(!check(failed_step, localization_points, v))
132 update_scores(localization_points);
133
135 if(!check(failed_step, localization_points, v))
136 update_scores(localization_points);
137
138 v[i] = tvt::unknown();
139 }
140
141 // clear assumptions
142 solver.pop();
143}
Single SSA step in the equation.
Definition ssa_step.h:47
exprt cond_handle
Definition ssa_step.h:146
Base class for all expressions.
Definition expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
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:154
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
Boolean negation.
Definition std_expr.h:2454
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.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Decision procedure with incremental solving with contexts and assumptions.
Generate Equation using Symbolic Execution.
dstringt irep_idt