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.set_comment(comment);
89  t->source_location.set(ID_coverage_criterion, coverage_criterion);
90  t->source_location.set_property_class(property_class);
91  t->source_location.set_function(function_id);
92  }
93 
95  {
96  return t->is_assert() &&
97  t->source_location.get_property_class() != property_class;
98  }
99 };
100 
103 {
104 public:
105  void add_from_criterion(
107  const symbol_tablet &,
108  const goal_filterst &);
109 
117  const irep_idt &function_id,
118  goto_programt &goto_program,
119  const cover_blocks_baset &basic_blocks,
120  const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
121  {
122  for(const auto &instrumenter : instrumenters)
123  (*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
124  }
125 
126 private:
127  std::vector<std::unique_ptr<cover_instrumenter_baset>> instrumenters;
128 };
129 
132 {
133 public:
135  const symbol_tablet &_symbol_table,
136  const goal_filterst &_goal_filters)
137  : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
138  {
139  }
140 
141 protected:
142  void instrument(
143  const irep_idt &function_id,
144  goto_programt &,
146  const cover_blocks_baset &,
147  const assertion_factoryt &) 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, "branch")
158  {
159  }
160 
161 protected:
162  void instrument(
163  const irep_idt &function_id,
164  goto_programt &,
166  const cover_blocks_baset &,
167  const assertion_factoryt &) const override;
168 };
169 
172 {
173 public:
175  const symbol_tablet &_symbol_table,
176  const goal_filterst &_goal_filters)
177  : cover_instrumenter_baset(_symbol_table, _goal_filters, "condition")
178  {
179  }
180 
181 protected:
182  void instrument(
183  const irep_idt &function_id,
184  goto_programt &,
186  const cover_blocks_baset &,
187  const assertion_factoryt &) const override;
188 };
189 
192 {
193 public:
195  const symbol_tablet &_symbol_table,
196  const goal_filterst &_goal_filters)
197  : cover_instrumenter_baset(_symbol_table, _goal_filters, "decision")
198  {
199  }
200 
201 protected:
202  void instrument(
203  const irep_idt &function_id,
204  goto_programt &,
206  const cover_blocks_baset &,
207  const assertion_factoryt &) const override;
208 };
209 
212 {
213 public:
215  const symbol_tablet &_symbol_table,
216  const goal_filterst &_goal_filters)
217  : cover_instrumenter_baset(_symbol_table, _goal_filters, "MC/DC")
218  {
219  }
220 
221 protected:
222  void instrument(
223  const irep_idt &function_id,
224  goto_programt &,
226  const cover_blocks_baset &,
227  const assertion_factoryt &) const override;
228 };
229 
232 {
233 public:
235  const symbol_tablet &_symbol_table,
236  const goal_filterst &_goal_filters)
237  : cover_instrumenter_baset(_symbol_table, _goal_filters, "path")
238  {
239  }
240 
241 protected:
242  void instrument(
243  const irep_idt &function_id,
244  goto_programt &,
246  const cover_blocks_baset &,
247  const assertion_factoryt &) const override;
248 };
249 
252 {
253 public:
255  const symbol_tablet &_symbol_table,
256  const goal_filterst &_goal_filters)
257  : cover_instrumenter_baset(_symbol_table, _goal_filters, "assertion")
258  {
259  }
260 
261 protected:
262  void instrument(
263  const irep_idt &function_id,
264  goto_programt &,
266  const cover_blocks_baset &,
267  const assertion_factoryt &) const override;
268 };
269 
272 {
273 public:
275  const symbol_tablet &_symbol_table,
276  const goal_filterst &_goal_filters)
277  : cover_instrumenter_baset(_symbol_table, _goal_filters, "cover")
278  {
279  }
280 
281 protected:
282  void instrument(
283  const irep_idt &function_id,
284  goto_programt &,
286  const cover_blocks_baset &,
287  const assertion_factoryt &) const override;
288 };
289 
291  const irep_idt &function_id,
292  goto_programt &goto_program,
294 
295 #endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1260
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:14
cover_instrumenter_baset::is_non_cover_assertion
bool is_non_cover_assertion(goto_programt::const_targett t) const
Definition: cover_instrument.h:94
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:83
cover_instrumenter_baset::operator()
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.
Definition: cover_instrument.h:56
cover_decision_instrumentert::instrument
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.
Definition: cover_instrument_decision.cpp:18
cover_instrument_end_of_function
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &)
Definition: cover_instrument_other.cpp:75
cover_condition_instrumentert
Condition coverage instrumenter.
Definition: cover_instrument.h:172
cover_instrumenterst::operator()
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.
Definition: cover_instrument.h:116
cover_branch_instrumentert::cover_branch_instrumentert
cover_branch_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:154
cover_instrumenter_baset::ns
const namespacet ns
Definition: cover_instrument.h:72
exprt
Base class for all expressions.
Definition: expr.h:54
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:60
cover_instrumenter_baset::goal_filters
const goal_filterst & goal_filters
Definition: cover_instrument.h:73
cover_instrumenter_baset
Base class for goto program coverage instrumenters.
Definition: cover_instrument.h:27
cover_path_instrumentert::cover_path_instrumentert
cover_path_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:234
cover_location_instrumentert
Basic block coverage instrumenter.
Definition: cover_instrument.h:132
coverage_criteriont
coverage_criteriont
Definition: cover.h:43
cover_decision_instrumentert::cover_decision_instrumentert
cover_decision_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:194
cover_cover_instrumentert::cover_cover_instrumentert
cover_cover_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:274
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
cover_instrumenterst::instrumenters
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
Definition: cover_instrument.h:127
cover_mcdc_instrumentert::cover_mcdc_instrumentert
cover_mcdc_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:214
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
cover_cover_instrumentert::instrument
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.
Definition: cover_instrument_other.cpp:49
cover_instrumenter_baset::~cover_instrumenter_baset
virtual ~cover_instrumenter_baset()=default
cover_assertion_instrumentert::instrument
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.
Definition: cover_instrument_other.cpp:33
cover_cover_instrumentert
__CPROVER_cover coverage instrumenter
Definition: cover_instrument.h:272
cover_path_instrumentert
Path coverage instrumenter.
Definition: cover_instrument.h:232
cover_blocks_baset
Definition: cover_basic_blocks.h:26
cover_decision_instrumentert
Decision coverage instrumenter.
Definition: cover_instrument.h:192
cover_branch_instrumentert::instrument
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.
Definition: cover_instrument_branch.cpp:16
goal_filterst
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:99
cover_instrumenter_baset::assertion_factoryt
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
Definition: cover_instrument.h:42
cover_branch_instrumentert
Branch coverage instrumenter.
Definition: cover_instrument.h:152
goto_program.h
Concrete Goto Program.
source_locationt
Definition: source_location.h:19
cover_condition_instrumentert::cover_condition_instrumentert
cover_condition_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:174
cover_instrumenter_baset::coverage_criterion
const irep_idt coverage_criterion
Definition: cover_instrument.h:69
cover_condition_instrumentert::instrument
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.
Definition: cover_instrument_condition.cpp:18
cover_instrumenter_baset::property_class
const irep_idt property_class
Definition: cover_instrument.h:68
cover_mcdc_instrumentert::instrument
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.
Definition: cover_instrument_mcdc.cpp:622
cover_assertion_instrumentert::cover_assertion_instrumentert
cover_assertion_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:254
cover_location_instrumentert::cover_location_instrumentert
cover_location_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:134
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
cover_path_instrumentert::instrument
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.
Definition: cover_instrument_other.cpp:20
cover_instrumenter_baset::instrument
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.
symbol_table.h
Author: Diffblue Ltd.
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
cover_mcdc_instrumentert
MC/DC coverage instrumenter.
Definition: cover_instrument.h:212
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
cover_assertion_instrumentert
Assertion coverage instrumenter.
Definition: cover_instrument.h:252
cover_location_instrumentert::instrument
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.
Definition: cover_instrument_location.cpp:17
cover_instrumenterst
A collection of instrumenters to be run.
Definition: cover_instrument.h:103
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:30