cprover
Loading...
Searching...
No Matches
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
62 const symbol_table_baset &symbol_table,
63 const goal_filterst &goal_filters)
64{
65 switch(criterion)
66 {
68 instrumenters.push_back(
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(
79 symbol_table, goal_filters));
80 break;
82 instrumenters.push_back(
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(
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
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" || criterion_string == "assumes")
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{
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
198
199 goal_filters->add(util_make_unique<internal_goals_filtert>());
200
202
203 cover_config.keep_assertions = false;
204 for(const auto &criterion_string : criteria_strings)
205 {
207
209 cover_config.keep_assertions = true;
210 // Make sure that existing assertions don't get replaced by assumes
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(
231 }
232
233 if(options.get_bool_option("no-trivial-tests"))
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,
255 const symbol_tablet &symbol_table,
256 message_handlert &message_handler)
257{
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(
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(
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
295 message_handlert &message_handler)
296{
297 if(!cover_config.keep_assertions)
298 {
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->condition() == i_it->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 "
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 &&
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
361 goto_model_functiont &function,
362 message_handlert &message_handler)
363{
365 function.get_symbol_table().lookup_ref(function.get_function_id());
369 function.get_goto_function(),
370 message_handler);
371
372 function.compute_location_numbers();
373}
374
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
419 goto_modelt &goto_model,
420 message_handlert &message_handler)
421{
424 goto_model.symbol_table,
425 goto_model.goto_functions,
426 message_handler);
427}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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_table_baset &, 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:39
A collection of function filters to be applied in conjunction.
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
A collection of goal filters to be applied in conjunction.
A collection of goto functions.
function_mapt function_map
void compute_location_numbers()
::goto_functiont goto_functiont
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:190
const irep_idt & get_function_id()
Get function id.
Definition goto_model.h:239
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition goto_model.h:232
void compute_location_numbers()
Re-number our goto_function.
Definition goto_model.h:216
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition goto_model.h:225
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
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
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
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
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:46
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
Program Transformation.