cprover
fault_localization.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fault Localization
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_FAULT_LOCALIZATION_H
13 #define CPROVER_CBMC_FAULT_LOCALIZATION_H
14 
15 #include <util/namespace.h>
16 #include <util/options.h>
17 #include <util/threeval.h>
18 
20 
21 #include "bmc.h"
22 #include "all_properties_class.h"
23 
25  public bmc_all_propertiest
26 {
27 public:
29  const goto_functionst &_goto_functions,
30  bmct &_bmc,
31  const optionst &_options)
32  :
33  bmc_all_propertiest(_goto_functions, _bmc.prop_conv, _bmc),
34  goto_functions(_goto_functions),
35  bmc(_bmc),
36  options(_options)
37  {
39  }
40 
43 
44  // override bmc_all_propertiest
45  virtual void goal_covered(const cover_goalst::goalt &);
46 
47 protected:
50  const optionst &options;
51 
52  // the failed property
53  symex_target_equationt::SSA_stepst::const_iterator failed;
54 
55  // the list of localization points up to the failed property
56  struct lpointt
57  {
59  unsigned score;
60  };
61  typedef std::map<literalt, lpointt> lpointst;
62  typedef std::map<irep_idt, lpointst> lpoints_mapt;
64 
65  // this does the actual work
66  void run(irep_idt goal_id);
67 
68  // this collects the guards as lpoints
69  void collect_guards(lpointst &lpoints);
70  void freeze_guards();
71 
72  // specify an lpoint combination to check
73  typedef std::vector<tvt> lpoints_valuet;
74  bool check(const lpointst &lpoints, const lpoints_valuet &value);
75  void update_scores(lpointst &lpoints);
76 
77  // localization method: flip each point
78  void localize_linear(lpointst &lpoints);
79 
80  // localization method: TBD
81  // void localize_TBD(
82  // prop_convt &prop_conv);
83 
84  symex_target_equationt::SSA_stepst::const_iterator get_failed_property();
85 
88 
89  void report(irep_idt goal_id);
90 
91  xmlt report_xml(irep_idt goal_id);
92 
93  // override bmc_all_propertiest
94  virtual void report(const cover_goalst &cover_goals);
95 
96  // override bmc_all_propertiest
97  virtual void do_before_solving()
98  {
99  freeze_guards();
100  }
101 };
102 
103 #endif // CPROVER_CBMC_FAULT_LOCALIZATION_H
fault_localizationt::lpoints_valuet
std::vector< tvt > lpoints_valuet
Definition: fault_localization.h:73
fault_localizationt::report_xml
xmlt report_xml(irep_idt goal_id)
Definition: fault_localization.cpp:197
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_target_equation.h
bmct
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
optionst
Definition: options.h:22
fault_localizationt::report
void report(irep_idt goal_id)
Definition: fault_localization.cpp:168
prop_convt
Definition: prop_conv.h:27
threeval.h
fault_localizationt::run
void run(irep_idt goal_id)
Definition: fault_localization.cpp:141
fault_localizationt::collect_guards
void collect_guards(lpointst &lpoints)
Definition: fault_localization.cpp:43
fault_localizationt::operator()
safety_checkert::resultt operator()()
Definition: fault_localization.cpp:232
fault_localizationt::lpointt
Definition: fault_localization.h:56
fault_localizationt::localize_linear
void localize_linear(lpointst &lpoints)
Definition: fault_localization.cpp:123
options.h
namespace.h
fault_localizationt::get_failed_property
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
Definition: fault_localization.cpp:67
cover_goalst
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
fault_localizationt::failed
symex_target_equationt::SSA_stepst::const_iterator failed
Definition: fault_localization.h:53
fault_localizationt::goto_functions
const goto_functionst & goto_functions
Definition: fault_localization.h:48
fault_localizationt::lpoints_mapt
std::map< irep_idt, lpointst > lpoints_mapt
Definition: fault_localization.h:62
fault_localizationt::lpointt::target
goto_programt::const_targett target
Definition: fault_localization.h:58
fault_localizationt::do_before_solving
virtual void do_before_solving()
Definition: fault_localization.h:97
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
fault_localizationt::lpointt::score
unsigned score
Definition: fault_localization.h:59
fault_localizationt::bmc
bmct & bmc
Definition: fault_localization.h:49
bmc.h
xmlt
Definition: xml.h:18
fault_localizationt::goal_covered
virtual void goal_covered(const cover_goalst::goalt &)
Definition: fault_localization.cpp:322
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
safety_checkert::resultt
resultt
Definition: safety_checker.h:33
fault_localizationt::stop_on_fail
safety_checkert::resultt stop_on_fail()
Definition: fault_localization.cpp:270
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
fault_localizationt::freeze_guards
void freeze_guards()
Definition: fault_localization.cpp:31
fault_localizationt
Definition: fault_localization.h:24
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
fault_localizationt::options
const optionst & options
Definition: fault_localization.h:50
cover_goalst::goalt
Definition: cover_goals.h:38
fault_localizationt::fault_localizationt
fault_localizationt(const goto_functionst &_goto_functions, bmct &_bmc, const optionst &_options)
Definition: fault_localization.h:28
bmc_all_propertiest
Definition: all_properties_class.h:19
all_properties_class.h
fault_localizationt::lpointst
std::map< literalt, lpointt > lpointst
Definition: fault_localization.h:61
fault_localizationt::run_decision_procedure
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Definition: fault_localization.cpp:241
fault_localizationt::lpoints_map
lpoints_mapt lpoints_map
Definition: fault_localization.h:63
fault_localizationt::update_scores
void update_scores(lpointst &lpoints)
Definition: fault_localization.cpp:107
fault_localizationt::check
bool check(const lpointst &lpoints, const lpoints_valuet &value)
Definition: fault_localization.cpp:81