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 
17 #include <util/symbol_table.h>
18 
20 
21 enum class coverage_criteriont;
22 class cover_blocks_baset;
23 class goal_filterst;
24 
27 {
28 public:
29  virtual ~cover_instrumenter_baset() = default;
31  const symbol_tablet &_symbol_table,
32  const goal_filterst &_goal_filters,
33  const irep_idt &_coverage_criterion)
34  : coverage_criterion(_coverage_criterion),
35  ns(_symbol_table),
36  goal_filters(_goal_filters)
37  {
38  }
39 
41  using assertion_factoryt = std::function<
43  static_assert(
44  std::is_same<
46  std::function<decltype(goto_programt::make_assertion)>>::value,
47  "`assertion_factoryt` is expected to have the same type as "
48  "`goto_programt::make_assertion`.");
49 
56  void operator()(
57  const irep_idt &function_id,
58  goto_programt &goto_program,
59  const cover_blocks_baset &basic_blocks,
60  const assertion_factoryt &make_assertion) const
61  {
62  Forall_goto_program_instructions(i_it, goto_program)
63  {
64  instrument(function_id, goto_program, i_it, basic_blocks, make_assertion);
65  }
66  }
67 
68  const irep_idt property_class = "coverage";
70 
71 protected:
72  const namespacet ns;
74 
76  virtual void instrument(
77  const irep_idt &function_id,
78  goto_programt &,
80  const cover_blocks_baset &,
81  const assertion_factoryt &) const = 0;
82 
85  const std::string &comment,
86  const irep_idt &function_id) const
87  {
88  t->source_location_nonconst().set_comment(comment);
89  t->source_location_nonconst().set(
90  ID_coverage_criterion, coverage_criterion);
91  t->source_location_nonconst().set_property_class(property_class);
92  t->source_location_nonconst().set_function(function_id);
93  }
94 
96  {
97  return t->is_assert() &&
98  t->source_location().get_property_class() != property_class;
99  }
100 };
101 
104 {
105 public:
106  void add_from_criterion(
108  const symbol_tablet &,
109  const goal_filterst &);
110 
118  const irep_idt &function_id,
119  goto_programt &goto_program,
120  const cover_blocks_baset &basic_blocks,
121  const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
122  {
123  for(const auto &instrumenter : instrumenters)
124  (*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
125  }
126 
127 private:
128  std::vector<std::unique_ptr<cover_instrumenter_baset>> instrumenters;
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, "location")
139  {
140  }
141 
142 protected:
143  void instrument(
144  const irep_idt &function_id,
145  goto_programt &,
147  const cover_blocks_baset &,
148  const assertion_factoryt &) const override;
149 };
150 
153 {
154 public:
156  const symbol_tablet &_symbol_table,
157  const goal_filterst &_goal_filters)
158  : cover_instrumenter_baset(_symbol_table, _goal_filters, "branch")
159  {
160  }
161 
162 protected:
163  void instrument(
164  const irep_idt &function_id,
165  goto_programt &,
167  const cover_blocks_baset &,
168  const assertion_factoryt &) const override;
169 };
170 
173 {
174 public:
176  const symbol_tablet &_symbol_table,
177  const goal_filterst &_goal_filters)
178  : cover_instrumenter_baset(_symbol_table, _goal_filters, "condition")
179  {
180  }
181 
182 protected:
183  void instrument(
184  const irep_idt &function_id,
185  goto_programt &,
187  const cover_blocks_baset &,
188  const assertion_factoryt &) const override;
189 };
190 
193 {
194 public:
196  const symbol_tablet &_symbol_table,
197  const goal_filterst &_goal_filters)
198  : cover_instrumenter_baset(_symbol_table, _goal_filters, "decision")
199  {
200  }
201 
202 protected:
203  void instrument(
204  const irep_idt &function_id,
205  goto_programt &,
207  const cover_blocks_baset &,
208  const assertion_factoryt &) const override;
209 };
210 
213 {
214 public:
216  const symbol_tablet &_symbol_table,
217  const goal_filterst &_goal_filters)
218  : cover_instrumenter_baset(_symbol_table, _goal_filters, "MC/DC")
219  {
220  }
221 
222 protected:
223  void instrument(
224  const irep_idt &function_id,
225  goto_programt &,
227  const cover_blocks_baset &,
228  const assertion_factoryt &) const override;
229 };
230 
233 {
234 public:
236  const symbol_tablet &_symbol_table,
237  const goal_filterst &_goal_filters)
238  : cover_instrumenter_baset(_symbol_table, _goal_filters, "path")
239  {
240  }
241 
242 protected:
243  void instrument(
244  const irep_idt &function_id,
245  goto_programt &,
247  const cover_blocks_baset &,
248  const assertion_factoryt &) const override;
249 };
250 
253 {
254 public:
256  const symbol_tablet &_symbol_table,
257  const goal_filterst &_goal_filters)
258  : cover_instrumenter_baset(_symbol_table, _goal_filters, "assertion")
259  {
260  }
261 
262 protected:
263  void instrument(
264  const irep_idt &function_id,
265  goto_programt &,
267  const cover_blocks_baset &,
268  const assertion_factoryt &) const override;
269 };
270 
273 {
274 public:
276  const symbol_tablet &_symbol_table,
277  const goal_filterst &_goal_filters)
278  : cover_instrumenter_baset(_symbol_table, _goal_filters, "cover")
279  {
280  }
281 
282 protected:
283  void instrument(
284  const irep_idt &function_id,
285  goto_programt &,
287  const cover_blocks_baset &,
288  const assertion_factoryt &) const override;
289 };
290 
292  const irep_idt &function_id,
293  goto_programt &goto_program,
295 
296 // assume-instructions instrumenter.
298 {
299 public:
301  const symbol_tablet &_symbol_table,
302  const goal_filterst &_goal_filters)
303  : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
304  {
305  }
306 
307 protected:
308  void instrument(
309  const irep_idt &,
310  goto_programt &,
312  const cover_blocks_baset &,
313  const assertion_factoryt &) const override;
314 };
315 
316 #endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
Assertion coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_assertion_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
cover_assume_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
void instrument(const irep_idt &, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Instrument program to check coverage of assume statements.
Branch coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_branch_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Condition coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_condition_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
__CPROVER_cover coverage instrumenter
cover_cover_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
Decision coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_decision_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Base class for goto program coverage instrumenters.
cover_instrumenter_baset(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters, const irep_idt &_coverage_criterion)
const irep_idt property_class
virtual void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const =0
Override this method to implement an instrumenter.
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
void operator()(const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks, const assertion_factoryt &make_assertion) const
Instruments a goto program.
const goal_filterst & goal_filters
const irep_idt coverage_criterion
bool is_non_cover_assertion(goto_programt::const_targett t) const
virtual ~cover_instrumenter_baset()=default
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
A collection of instrumenters to be run.
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
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:60
void operator()(const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks, const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
Applies all instrumenters to the given goto program.
Basic block coverage instrumenter.
cover_location_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
MC/DC coverage instrumenter.
cover_mcdc_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
Path coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_path_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
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
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:99
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The symbol table.
Definition: symbol_table.h:14
coverage_criteriont
Definition: cover.h:43
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &)
Concrete Goto Program.
#define Forall_goto_program_instructions(it, program)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
Author: Diffblue Ltd.