cprover
cover_instrument.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
13 #define CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
14 
15 #include <memory>
16 
18 #include <util/message.h>
19 
20 enum class coverage_criteriont;
21 class cover_blocks_baset;
22 class goal_filterst;
23 
26 {
27 public:
28  virtual ~cover_instrumenter_baset() = default;
30  const symbol_tablet &_symbol_table,
31  const goal_filterst &_goal_filters,
32  const irep_idt &_coverage_criterion)
33  : coverage_criterion(_coverage_criterion),
34  ns(_symbol_table),
35  goal_filters(_goal_filters)
36  {
37  }
38 
43  virtual void operator()(
44  const irep_idt &function_id,
45  goto_programt &goto_program,
46  const cover_blocks_baset &basic_blocks) const
47  {
48  Forall_goto_program_instructions(i_it, goto_program)
49  {
50  instrument(function_id, goto_program, i_it, basic_blocks);
51  }
52  }
53 
54  const irep_idt property_class = "coverage";
56 
57 protected:
58  const namespacet ns;
60 
62  virtual void instrument(
63  const irep_idt &function_id,
64  goto_programt &,
66  const cover_blocks_baset &) const = 0;
67 
70  const std::string &comment,
71  const irep_idt &function_id) const
72  {
73  t->source_location.set_comment(comment);
74  t->source_location.set(ID_coverage_criterion, coverage_criterion);
75  t->source_location.set_property_class(property_class);
76  t->source_location.set_function(function_id);
77  }
78 
80  {
81  return t->is_assert() &&
82  t->source_location.get_property_class() != property_class;
83  }
84 };
85 
88 {
89 public:
90  void add_from_criterion(
92  const symbol_tablet &,
93  const goal_filterst &);
94 
99  void operator()(
100  const irep_idt &function_id,
101  goto_programt &goto_program,
102  const cover_blocks_baset &basic_blocks) const
103  {
104  for(const auto &instrumenter : instrumenters)
105  (*instrumenter)(function_id, goto_program, basic_blocks);
106  }
107 
108 private:
109  std::vector<std::unique_ptr<cover_instrumenter_baset>> instrumenters;
110 };
111 
114 {
115 public:
117  const symbol_tablet &_symbol_table,
118  const goal_filterst &_goal_filters)
119  : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
120  {
121  }
122 
123 protected:
124  void instrument(
125  const irep_idt &function_id,
126  goto_programt &,
128  const cover_blocks_baset &) const override;
129 };
130 
133 {
134 public:
136  const symbol_tablet &_symbol_table,
137  const goal_filterst &_goal_filters)
138  : cover_instrumenter_baset(_symbol_table, _goal_filters, "branch")
139  {
140  }
141 
142 protected:
143  void instrument(
144  const irep_idt &function_id,
145  goto_programt &,
147  const cover_blocks_baset &) const override;
148 };
149 
152 {
153 public:
155  const symbol_tablet &_symbol_table,
156  const goal_filterst &_goal_filters)
157  : cover_instrumenter_baset(_symbol_table, _goal_filters, "condition")
158  {
159  }
160 
161 protected:
162  void instrument(
163  const irep_idt &function_id,
164  goto_programt &,
166  const cover_blocks_baset &) const override;
167 };
168 
171 {
172 public:
174  const symbol_tablet &_symbol_table,
175  const goal_filterst &_goal_filters)
176  : cover_instrumenter_baset(_symbol_table, _goal_filters, "decision")
177  {
178  }
179 
180 protected:
181  void instrument(
182  const irep_idt &function_id,
183  goto_programt &,
185  const cover_blocks_baset &) const override;
186 };
187 
190 {
191 public:
193  const symbol_tablet &_symbol_table,
194  const goal_filterst &_goal_filters)
195  : cover_instrumenter_baset(_symbol_table, _goal_filters, "MC/DC")
196  {
197  }
198 
199 protected:
200  void instrument(
201  const irep_idt &function_id,
202  goto_programt &,
204  const cover_blocks_baset &) const override;
205 };
206 
209 {
210 public:
212  const symbol_tablet &_symbol_table,
213  const goal_filterst &_goal_filters)
214  : cover_instrumenter_baset(_symbol_table, _goal_filters, "path")
215  {
216  }
217 
218 protected:
219  void instrument(
220  const irep_idt &function_id,
221  goto_programt &,
223  const cover_blocks_baset &) const override;
224 };
225 
228 {
229 public:
231  const symbol_tablet &_symbol_table,
232  const goal_filterst &_goal_filters)
233  : cover_instrumenter_baset(_symbol_table, _goal_filters, "assertion")
234  {
235  }
236 
237 protected:
238  void instrument(
239  const irep_idt &function_id,
240  goto_programt &,
242  const cover_blocks_baset &) const override;
243 };
244 
247 {
248 public:
250  const symbol_tablet &_symbol_table,
251  const goal_filterst &_goal_filters)
252  : cover_instrumenter_baset(_symbol_table, _goal_filters, "cover")
253  {
254  }
255 
256 protected:
257  void instrument(
258  const irep_idt &function_id,
259  goto_programt &,
261  const cover_blocks_baset &) const override;
262 };
263 
265  const irep_idt &function_id,
266  goto_programt &goto_program);
267 
268 #endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1177
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
cover_instrumenter_baset::is_non_cover_assertion
bool is_non_cover_assertion(goto_programt::const_targett t) const
Definition: cover_instrument.h:79
cover_instrumenter_baset::initialize_source_location
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
Definition: cover_instrument.h:68
cover_condition_instrumentert
Condition coverage instrumenter.
Definition: cover_instrument.h:152
cover_branch_instrumentert::cover_branch_instrumentert
cover_branch_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:135
cover_instrumenter_baset::ns
const namespacet ns
Definition: cover_instrument.h:58
goto_model.h
cover_instrumenterst::add_from_criterion
void add_from_criterion(coverage_criteriont, const symbol_tablet &, const goal_filterst &)
Create and add an instrumenter based on the given criterion.
Definition: cover.cpp:55
cover_instrumenter_baset::goal_filters
const goal_filterst & goal_filters
Definition: cover_instrument.h:59
cover_instrumenter_baset
Base class for goto program coverage instrumenters.
Definition: cover_instrument.h:26
cover_path_instrumentert::cover_path_instrumentert
cover_path_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:211
cover_condition_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_condition.cpp:19
cover_location_instrumentert
Basic block coverage instrumenter.
Definition: cover_instrument.h:114
coverage_criteriont
coverage_criteriont
Definition: cover.h:26
cover_decision_instrumentert::cover_decision_instrumentert
cover_decision_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:173
cover_decision_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_decision.cpp:18
cover_cover_instrumentert::cover_cover_instrumentert
cover_cover_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:249
cover_instrumenter_baset::operator()
virtual void operator()(const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks) const
Instruments a goto program.
Definition: cover_instrument.h:43
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
cover_instrumenterst::instrumenters
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
Definition: cover_instrument.h:109
cover_mcdc_instrumentert::cover_mcdc_instrumentert
cover_mcdc_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:192
cover_instrumenter_baset::~cover_instrumenter_baset
virtual ~cover_instrumenter_baset()=default
cover_cover_instrumentert
__CPROVER_cover coverage instrumenter
Definition: cover_instrument.h:247
cover_path_instrumentert
Path coverage instrumenter.
Definition: cover_instrument.h:209
cover_assertion_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_other.cpp:30
cover_blocks_baset
Definition: cover_basic_blocks.h:24
cover_decision_instrumentert
Decision coverage instrumenter.
Definition: cover_instrument.h:171
cover_mcdc_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_mcdc.cpp:622
goal_filterst
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:113
cover_instrument_end_of_function
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program)
Definition: cover_instrument_other.cpp:74
cover_branch_instrumentert
Branch coverage instrumenter.
Definition: cover_instrument.h:133
cover_location_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_location.cpp:17
cover_condition_instrumentert::cover_condition_instrumentert
cover_condition_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:154
cover_instrumenterst::operator()
void operator()(const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks) const
Applies all instrumenters to the given goto program.
Definition: cover_instrument.h:99
cover_instrumenter_baset::coverage_criterion
const irep_idt coverage_criterion
Definition: cover_instrument.h:55
cover_instrumenter_baset::property_class
const irep_idt property_class
Definition: cover_instrument.h:54
cover_cover_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_other.cpp:45
cover_assertion_instrumentert::cover_assertion_instrumentert
cover_assertion_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:230
cover_location_instrumentert::cover_location_instrumentert
cover_location_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:116
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
cover_instrumenter_baset::instrument
virtual void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const =0
Override this method to implement an instrumenter.
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
cover_path_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_other.cpp:18
cover_branch_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_branch.cpp:16
message.h
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
cover_mcdc_instrumentert
MC/DC coverage instrumenter.
Definition: cover_instrument.h:190
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
cover_assertion_instrumentert
Assertion coverage instrumenter.
Definition: cover_instrument.h:228
cover_instrumenterst
A collection of instrumenters to be run.
Definition: cover_instrument.h:88
cover_instrumenter_baset::cover_instrumenter_baset
cover_instrumenter_baset(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters, const irep_idt &_coverage_criterion)
Definition: cover_instrument.h:29