cprover
cover.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: Daniel Kroening
6
7Date: May 2016
8
9\*******************************************************************/
10
13
14#include "cover.h"
15
16#include <util/message.h>
17#include <util/make_unique.h>
18#include <util/cmdline.h>
19#include <util/options.h>
20
23
24#include "cover_basic_blocks.h"
25
38 const irep_idt &function_id,
39 goto_programt &goto_program,
40 const cover_instrumenterst &instrumenters,
41 const irep_idt &mode,
42 message_handlert &message_handler,
44{
45 const std::unique_ptr<cover_blocks_baset> basic_blocks =
46 mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
47 new cover_basic_blocks_javat(goto_program))
48 : std::unique_ptr<cover_blocks_baset>(
49 new cover_basic_blockst(goto_program));
50
51 basic_blocks->report_block_anomalies(
52 function_id, goto_program, message_handler);
53 instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
54}
55
61 coverage_criteriont criterion,
62 const symbol_tablet &symbol_table,
63 const goal_filterst &goal_filters)
64{
65 switch(criterion)
66 {
68 instrumenters.push_back(
69 util_make_unique<cover_location_instrumentert>(
70 symbol_table, goal_filters));
71 break;
73 instrumenters.push_back(
74 util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
75 break;
77 instrumenters.push_back(
78 util_make_unique<cover_decision_instrumentert>(
79 symbol_table, goal_filters));
80 break;
82 instrumenters.push_back(
83 util_make_unique<cover_condition_instrumentert>(
84 symbol_table, goal_filters));
85 break;
87 instrumenters.push_back(
88 util_make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
89 break;
91 instrumenters.push_back(
92 util_make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
93 break;
95 instrumenters.push_back(
96 util_make_unique<cover_assertion_instrumentert>(
97 symbol_table, goal_filters));
98 break;
100 instrumenters.push_back(
101 util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
102 break;
104 instrumenters.push_back(
105 util_make_unique<cover_assume_instrumentert>(symbol_table, goal_filters));
106 }
107}
108
113parse_coverage_criterion(const std::string &criterion_string)
114{
116
117 if(criterion_string == "assertion" || criterion_string == "assertions")
119 else if(criterion_string == "path" || criterion_string == "paths")
121 else if(criterion_string == "branch" || criterion_string == "branches")
123 else if(criterion_string == "location" || criterion_string == "locations")
125 else if(criterion_string == "decision" || criterion_string == "decisions")
127 else if(criterion_string == "condition" || criterion_string == "conditions")
129 else if(criterion_string == "mcdc")
131 else if(criterion_string == "cover")
133 else if(criterion_string == "assume")
135 else
136 {
137 std::stringstream s;
138 s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
139 throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
140 }
141
142 return c;
143}
144
148void parse_cover_options(const cmdlinet &cmdline, optionst &options)
149{
150 options.set_option("cover", cmdline.get_values("cover"));
151
152 // allow retrieving full traces
153 options.set_option("simple-slice", false);
154
155 options.set_option(
156 "cover-include-pattern", cmdline.get_value("cover-include-pattern"));
157 options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));
158
159 std::string cover_only = cmdline.get_value("cover-only");
160
161 if(!cover_only.empty() && cmdline.isset("cover-function-only"))
163 "at most one of --cover-only and --cover-function-only can be used",
164 "--cover-only");
165
166 options.set_option("cover-only", cmdline.get_value("cover-only"));
167 if(cmdline.isset("cover-function-only"))
168 options.set_option("cover-only", "function");
169
170 options.set_option(
171 "cover-traces-must-terminate",
172 cmdline.isset("cover-traces-must-terminate"));
173 options.set_option(
174 "cover-failed-assertions", cmdline.isset("cover-failed-assertions"));
175
176 options.set_option("show-test-suite", cmdline.isset("show-test-suite"));
177}
178
187 const optionst &options,
188 const symbol_tablet &symbol_table,
189 message_handlert &message_handler)
190{
191 cover_configt cover_config;
192 function_filterst &function_filters =
193 cover_config.cover_configt::function_filters;
194 std::unique_ptr<goal_filterst> &goal_filters = cover_config.goal_filters;
195 cover_instrumenterst &instrumenters = cover_config.cover_instrumenters;
196
197 function_filters.add(util_make_unique<internal_functions_filtert>());
198
199 goal_filters->add(util_make_unique<internal_goals_filtert>());
200
201 optionst::value_listt criteria_strings = options.get_list_option("cover");
202
203 cover_config.keep_assertions = false;
204 for(const auto &criterion_string : criteria_strings)
205 {
206 coverage_criteriont c = parse_coverage_criterion(criterion_string);
207
209 cover_config.keep_assertions = true;
210 // Make sure that existing assertions don't get replaced by assumes
211 else if(c == coverage_criteriont::ASSUME)
212 cover_config.keep_assertions = true;
213
214 instrumenters.add_from_criterion(c, symbol_table, *goal_filters);
215 }
216
217 if(cover_config.keep_assertions && criteria_strings.size() > 1)
218 {
219 std::stringstream s;
220 s << "assertion coverage cannot currently be used together with other"
221 << "coverage criteria";
222 throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
223 }
224
225 std::string cover_include_pattern =
226 options.get_option("cover-include-pattern");
227 if(!cover_include_pattern.empty())
228 {
229 function_filters.add(
230 util_make_unique<include_pattern_filtert>(cover_include_pattern));
231 }
232
233 if(options.get_bool_option("no-trivial-tests"))
234 function_filters.add(util_make_unique<trivial_functions_filtert>());
235
236 cover_config.traces_must_terminate =
237 options.get_bool_option("cover-traces-must-terminate");
238
239 cover_config.cover_failed_assertions =
240 options.get_bool_option("cover-failed-assertions");
241
242 return cover_config;
243}
244
253 const optionst &options,
254 const irep_idt &main_function_id,
255 const symbol_tablet &symbol_table,
256 message_handlert &message_handler)
257{
258 cover_configt cover_config =
259 get_cover_config(options, symbol_table, message_handler);
260
261 std::string cover_only = options.get_option("cover-only");
262
263 // cover entry point function only
264 if(cover_only == "function")
265 {
266 const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
267 cover_config.function_filters.add(
268 util_make_unique<single_function_filtert>(main_symbol.name));
269 }
270 else if(cover_only == "file")
271 {
272 const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
273 cover_config.function_filters.add(
274 util_make_unique<file_filtert>(main_symbol.location.get_file()));
275 }
276 else if(!cover_only.empty())
277 {
278 std::stringstream s;
279 s << "Argument to --cover-only not recognized: " << cover_only;
280 throw invalid_command_line_argument_exceptiont(s.str(), "--cover-only");
281 }
282
283 return cover_config;
284}
285
292 const cover_configt &cover_config,
293 const symbolt &function_symbol,
295 message_handlert &message_handler)
296{
297 if(!cover_config.keep_assertions)
298 {
299 Forall_goto_program_instructions(i_it, function.body)
300 {
301 // Simplify the common case where we have ASSERT(x); ASSUME(x):
302 if(i_it->is_assert())
303 {
304 if(!cover_config.cover_failed_assertions)
305 {
306 auto successor = std::next(i_it);
307 if(
308 successor != function.body.instructions.end() &&
309 successor->is_assume() &&
310 successor->get_condition() == i_it->get_condition())
311 {
312 successor->turn_into_skip();
313 }
314
315 i_it->turn_into_assume();
316 }
317 else
318 {
319 i_it->turn_into_skip();
320 }
321 }
322 }
323 }
324
325 bool changed = false;
326
327 if(cover_config.function_filters(function_symbol, function))
328 {
329 messaget msg(message_handler);
330 msg.debug() << "Instrumenting coverage for function "
331 << id2string(function_symbol.name) << messaget::eom;
333 function_symbol.name,
334 function.body,
335 cover_config.cover_instrumenters,
336 function_symbol.mode,
337 message_handler,
338 cover_config.make_assertion);
339 changed = true;
340 }
341
342 if(
343 cover_config.traces_must_terminate &&
344 function_symbol.name == goto_functionst::entry_point())
345 {
347 function_symbol.name, function.body, cover_config.make_assertion);
348 changed = true;
349 }
350
351 if(changed)
352 remove_skip(function.body);
353}
354
360 const cover_configt &cover_config,
361 goto_model_functiont &function,
362 message_handlert &message_handler)
363{
364 const symbolt function_symbol =
365 function.get_symbol_table().lookup_ref(function.get_function_id());
367 cover_config,
368 function_symbol,
369 function.get_goto_function(),
370 message_handler);
371
372 function.compute_location_numbers();
373}
374
381 const cover_configt &cover_config,
382 const symbol_tablet &symbol_table,
383 goto_functionst &goto_functions,
384 message_handlert &message_handler)
385{
386 messaget msg(message_handler);
387 msg.status() << "Rewriting existing assertions as assumptions"
388 << messaget::eom;
389
390 if(
391 cover_config.traces_must_terminate &&
392 !goto_functions.function_map.count(goto_functions.entry_point()))
393 {
394 msg.error() << "cover-traces-must-terminate: invalid entry point ["
395 << goto_functions.entry_point() << "]" << messaget::eom;
396 return true;
397 }
398
399 for(auto &gf_entry : goto_functions.function_map)
400 {
401 const symbolt function_symbol = symbol_table.lookup_ref(gf_entry.first);
403 cover_config, function_symbol, gf_entry.second, message_handler);
404 }
405 goto_functions.compute_location_numbers();
406
407 cover_config.function_filters.report_anomalies();
408 cover_config.goal_filters->report_anomalies();
409
410 return false;
411}
412
418 const cover_configt &cover_config,
419 goto_modelt &goto_model,
420 message_handlert &message_handler)
421{
423 cover_config,
424 goto_model.symbol_table,
425 goto_model.goto_functions,
426 message_handler);
427}
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:62
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:66
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:87
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:99
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:232
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:225
void compute_location_numbers()
Re-number our goto_function.
Definition: goto_model.h:209
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:218
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
std::list< std::string > value_listt
Definition: options.h:25
const irep_idt & get_file() const
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt mode
Language mode.
Definition: symbol.h:49
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
Definition: cover.cpp:37
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
Definition: cover.cpp:186
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:148
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
Definition: cover.cpp:113
Coverage Instrumentation.
coverage_criteriont
Definition: cover.h:43
Basic blocks detection for Coverage Instrumentation.
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)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
Options.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
bool traces_must_terminate
Definition: cover.h:59
bool keep_assertions
Definition: cover.h:57
cover_instrumenterst cover_instrumenters
Definition: cover.h:65
bool cover_failed_assertions
Definition: cover.h:58
cover_instrumenter_baset::assertion_factoryt make_assertion
Definition: cover.h:66
function_filterst function_filters
Definition: cover.h:61
std::unique_ptr< goal_filterst > goal_filters
Definition: cover.h:63