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 
40  using assertion_factoryt = std::function<
42  static_assert(
43  std::is_same<
45  std::function<decltype(goto_programt::make_assertion)>>::value,
46  "`assertion_factoryt` is expected to have the same type as "
47  "`goto_programt::make_assertion`.");
48 
55  void operator()(
56  const irep_idt &function_id,
57  goto_programt &goto_program,
58  const cover_blocks_baset &basic_blocks,
59  const assertion_factoryt &make_assertion) const
60  {
61  Forall_goto_program_instructions(i_it, goto_program)
62  {
63  instrument(function_id, goto_program, i_it, basic_blocks, make_assertion);
64  }
65  }
66 
67  const irep_idt property_class = "coverage";
69 
70 protected:
71  const namespacet ns;
73 
75  virtual void instrument(
76  const irep_idt &function_id,
77  goto_programt &,
79  const cover_blocks_baset &,
80  const assertion_factoryt &) const = 0;
81 
84  const std::string &comment,
85  const irep_idt &function_id) const
86  {
87  t->source_location.set_comment(comment);
88  t->source_location.set(ID_coverage_criterion, coverage_criterion);
89  t->source_location.set_property_class(property_class);
90  t->source_location.set_function(function_id);
91  }
92 
94  {
95  return t->is_assert() &&
96  t->source_location.get_property_class() != property_class;
97  }
98 };
99 
102 {
103 public:
104  void add_from_criterion(
106  const symbol_tablet &,
107  const goal_filterst &);
108 
116  const irep_idt &function_id,
117  goto_programt &goto_program,
118  const cover_blocks_baset &basic_blocks,
119  const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
120  {
121  for(const auto &instrumenter : instrumenters)
122  (*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
123  }
124 
125 private:
126  std::vector<std::unique_ptr<cover_instrumenter_baset>> instrumenters;
127 };
128 
131 {
132 public:
134  const symbol_tablet &_symbol_table,
135  const goal_filterst &_goal_filters)
136  : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
137  {
138  }
139 
140 protected:
141  void instrument(
142  const irep_idt &function_id,
143  goto_programt &,
145  const cover_blocks_baset &,
146  const assertion_factoryt &) const override;
147 };
148 
151 {
152 public:
154  const symbol_tablet &_symbol_table,
155  const goal_filterst &_goal_filters)
156  : cover_instrumenter_baset(_symbol_table, _goal_filters, "branch")
157  {
158  }
159 
160 protected:
161  void instrument(
162  const irep_idt &function_id,
163  goto_programt &,
165  const cover_blocks_baset &,
166  const assertion_factoryt &) 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, "condition")
177  {
178  }
179 
180 protected:
181  void instrument(
182  const irep_idt &function_id,
183  goto_programt &,
185  const cover_blocks_baset &,
186  const assertion_factoryt &) const override;
187 };
188 
191 {
192 public:
194  const symbol_tablet &_symbol_table,
195  const goal_filterst &_goal_filters)
196  : cover_instrumenter_baset(_symbol_table, _goal_filters, "decision")
197  {
198  }
199 
200 protected:
201  void instrument(
202  const irep_idt &function_id,
203  goto_programt &,
205  const cover_blocks_baset &,
206  const assertion_factoryt &) const override;
207 };
208 
211 {
212 public:
214  const symbol_tablet &_symbol_table,
215  const goal_filterst &_goal_filters)
216  : cover_instrumenter_baset(_symbol_table, _goal_filters, "MC/DC")
217  {
218  }
219 
220 protected:
221  void instrument(
222  const irep_idt &function_id,
223  goto_programt &,
225  const cover_blocks_baset &,
226  const assertion_factoryt &) const override;
227 };
228 
231 {
232 public:
234  const symbol_tablet &_symbol_table,
235  const goal_filterst &_goal_filters)
236  : cover_instrumenter_baset(_symbol_table, _goal_filters, "path")
237  {
238  }
239 
240 protected:
241  void instrument(
242  const irep_idt &function_id,
243  goto_programt &,
245  const cover_blocks_baset &,
246  const assertion_factoryt &) const override;
247 };
248 
251 {
252 public:
254  const symbol_tablet &_symbol_table,
255  const goal_filterst &_goal_filters)
256  : cover_instrumenter_baset(_symbol_table, _goal_filters, "assertion")
257  {
258  }
259 
260 protected:
261  void instrument(
262  const irep_idt &function_id,
263  goto_programt &,
265  const cover_blocks_baset &,
266  const assertion_factoryt &) const override;
267 };
268 
271 {
272 public:
274  const symbol_tablet &_symbol_table,
275  const goal_filterst &_goal_filters)
276  : cover_instrumenter_baset(_symbol_table, _goal_filters, "cover")
277  {
278  }
279 
280 protected:
281  void instrument(
282  const irep_idt &function_id,
283  goto_programt &,
285  const cover_blocks_baset &,
286  const assertion_factoryt &) const override;
287 };
288 
290  const irep_idt &function_id,
291  goto_programt &goto_program,
293 
294 #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)
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:102
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:74
instructionst::iterator targett
Definition: goto_program.h:550
instructionst::const_iterator const_targett
Definition: goto_program.h:551
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:864
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The symbol table.
Definition: symbol_table.h:20
coverage_criteriont
Definition: cover.h:41
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &)
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109