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
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
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:93
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:82
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:55
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:171
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:115
cover_branch_instrumentert::cover_branch_instrumentert
cover_branch_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:153
cover_instrumenter_baset::ns
const namespacet ns
Definition: cover_instrument.h:71
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
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:72
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:233
cover_location_instrumentert
Basic block coverage instrumenter.
Definition: cover_instrument.h:131
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:193
cover_cover_instrumentert::cover_cover_instrumentert
cover_cover_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:273
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:126
cover_mcdc_instrumentert::cover_mcdc_instrumentert
cover_mcdc_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:213
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
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:47
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:31
cover_cover_instrumentert
__CPROVER_cover coverage instrumenter
Definition: cover_instrument.h:271
cover_path_instrumentert
Path coverage instrumenter.
Definition: cover_instrument.h:231
cover_blocks_baset
Definition: cover_basic_blocks.h:24
cover_decision_instrumentert
Decision coverage instrumenter.
Definition: cover_instrument.h:191
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:113
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:41
cover_branch_instrumentert
Branch coverage instrumenter.
Definition: cover_instrument.h:151
source_locationt
Definition: source_location.h:20
cover_condition_instrumentert::cover_condition_instrumentert
cover_condition_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:173
cover_instrumenter_baset::coverage_criterion
const irep_idt coverage_criterion
Definition: cover_instrument.h:68
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:19
cover_instrumenter_baset::property_class
const irep_idt property_class
Definition: cover_instrument.h:67
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:253
cover_location_instrumentert::cover_location_instrumentert
cover_location_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Definition: cover_instrument.h:133
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
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 assertion_factoryt &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_other.cpp:18
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.
message.h
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:179
cover_mcdc_instrumentert
MC/DC coverage instrumenter.
Definition: cover_instrument.h:211
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
cover_assertion_instrumentert
Assertion coverage instrumenter.
Definition: cover_instrument.h:251
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:102
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