CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/cover.cpp Source File

CBMC
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/cmdline.h>
18#include <util/options.h>
19
20#include <goto-programs/goto_model.h>
21#include <goto-programs/remove_skip.h>
22
23#include "cover_basic_blocks.h"
24
37 const irep_idt &function_id,
38 goto_programt &goto_program,
39 const cover_instrumenterst &instrumenters,
40 const irep_idt &mode,
41 message_handlert &message_handler,
43{
44 const std::unique_ptr<cover_blocks_baset> basic_blocks =
45 mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
46 new cover_basic_blocks_javat(goto_program))
47 : std::unique_ptr<cover_blocks_baset>(
48 new cover_basic_blockst(goto_program));
49
50 basic_blocks->report_block_anomalies(
51 function_id, goto_program, message_handler);
52 instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
53}
54
61 const symbol_table_baset &symbol_table,
62 const goal_filterst &goal_filters)
63{
64 switch(criterion)
65 {
67 instrumenters.push_back(std::make_unique<cover_location_instrumentert>(
68 symbol_table, goal_filters));
69 break;
71 instrumenters.push_back(
72 std::make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
73 break;
75 instrumenters.push_back(std::make_unique<cover_decision_instrumentert>(
76 symbol_table, goal_filters));
77 break;
79 instrumenters.push_back(std::make_unique<cover_condition_instrumentert>(
80 symbol_table, goal_filters));
81 break;
83 instrumenters.push_back(
84 std::make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
85 break;
87 instrumenters.push_back(
88 std::make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
89 break;
91 instrumenters.push_back(std::make_unique<cover_assertion_instrumentert>(
92 symbol_table, goal_filters));
93 break;
95 instrumenters.push_back(
96 std::make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
97 break;
99 instrumenters.push_back(
100 std::make_unique<cover_assume_instrumentert>(symbol_table, goal_filters));
101 }
102}
103
107coverage_criteriont
109{
111
112 if(criterion_string == "assertion" || criterion_string == "assertions")
114 else if(criterion_string == "path" || criterion_string == "paths")
116 else if(criterion_string == "branch" || criterion_string == "branches")
118 else if(criterion_string == "location" || criterion_string == "locations")
120 else if(criterion_string == "decision" || criterion_string == "decisions")
122 else if(criterion_string == "condition" || criterion_string == "conditions")
124 else if(criterion_string == "mcdc")
126 else if(criterion_string == "cover")
128 else if(criterion_string == "assume" || criterion_string == "assumes")
130 else
131 {
132 std::stringstream s;
133 s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
134 throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
135 }
136
137 return c;
138}
139
143 void parse_cover_options(const cmdlinet &cmdline, optionst &options)
144{
145 options.set_option("cover", cmdline.get_values("cover"));
146
147 // allow retrieving full traces
148 options.set_option("simple-slice", false);
149
150 options.set_option(
151 "cover-include-pattern", cmdline.get_value("cover-include-pattern"));
152 options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));
153
154 std::string cover_only = cmdline.get_value("cover-only");
155
156 if(!cover_only.empty() && cmdline.isset("cover-function-only"))
158 "at most one of --cover-only and --cover-function-only can be used",
159 "--cover-only");
160
161 options.set_option("cover-only", cmdline.get_value("cover-only"));
162 if(cmdline.isset("cover-function-only"))
163 options.set_option("cover-only", "function");
164
165 options.set_option(
166 "cover-traces-must-terminate",
167 cmdline.isset("cover-traces-must-terminate"));
168 options.set_option(
169 "cover-failed-assertions", cmdline.isset("cover-failed-assertions"));
170
171 options.set_option("show-test-suite", cmdline.isset("show-test-suite"));
172}
173
182 const optionst &options,
183 const symbol_tablet &symbol_table,
184 message_handlert &message_handler)
185{
187 function_filterst &function_filters =
188 cover_config.cover_configt::function_filters;
189 std::unique_ptr<goal_filterst> &goal_filters = cover_config.goal_filters;
190 cover_instrumenterst &instrumenters = cover_config.cover_instrumenters;
191
192 function_filters.add(std::make_unique<internal_functions_filtert>());
193
194 goal_filters->add(std::make_unique<internal_goals_filtert>());
195
197
198 cover_config.keep_assertions = false;
199 for(const auto &criterion_string : criteria_strings)
200 {
202
204 cover_config.keep_assertions = true;
205 // Make sure that existing assertions don't get replaced by assumes
207 cover_config.keep_assertions = true;
208
209 instrumenters.add_from_criterion(c, symbol_table, *goal_filters);
210 }
211
212 if(cover_config.keep_assertions && criteria_strings.size() > 1)
213 {
214 std::stringstream s;
215 s << "assertion coverage cannot currently be used together with other"
216 << "coverage criteria";
217 throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
218 }
219
220 std::string cover_include_pattern =
221 options.get_option("cover-include-pattern");
222 if(!cover_include_pattern.empty())
223 {
224 function_filters.add(
225 std::make_unique<include_pattern_filtert>(cover_include_pattern));
226 }
227
228 if(options.get_bool_option("no-trivial-tests"))
229 function_filters.add(std::make_unique<trivial_functions_filtert>());
230
231 cover_config.traces_must_terminate =
232 options.get_bool_option("cover-traces-must-terminate");
233
234 cover_config.cover_failed_assertions =
235 options.get_bool_option("cover-failed-assertions");
236
237 return cover_config;
238}
239
248 const optionst &options,
250 const symbol_tablet &symbol_table,
251 message_handlert &message_handler)
252{
254 get_cover_config(options, symbol_table, message_handler);
255
256 std::string cover_only = options.get_option("cover-only");
257
258 // cover entry point function only
259 if(cover_only == "function")
260 {
261 const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
262 cover_config.function_filters.add(
263 std::make_unique<single_function_filtert>(main_symbol.name));
264 }
265 else if(cover_only == "file")
266 {
267 const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
268 cover_config.function_filters.add(
269 std::make_unique<file_filtert>(main_symbol.location.get_file()));
270 }
271 else if(!cover_only.empty())
272 {
273 std::stringstream s;
274 s << "Argument to --cover-only not recognized: " << cover_only;
275 throw invalid_command_line_argument_exceptiont(s.str(), "--cover-only");
276 }
277
278 return cover_config;
279}
280
290 message_handlert &message_handler)
291{
292 if(!cover_config.keep_assertions)
293 {
295 {
296 // Simplify the common case where we have ASSERT(x); ASSUME(x):
297 if(i_it->is_assert())
298 {
299 if(!cover_config.cover_failed_assertions)
300 {
301 auto successor = std::next(i_it);
302 if(
303 successor != function.body.instructions.end() &&
304 successor->is_assume() &&
305 successor->condition() == i_it->condition())
306 {
307 successor->turn_into_skip();
308 }
309
310 i_it->turn_into_assume();
311 }
312 else
313 {
314 i_it->turn_into_skip();
315 }
316 }
317 }
318 }
319
320 bool changed = false;
321
322 if(cover_config.function_filters(function_symbol, function))
323 {
324 messaget msg(message_handler);
325 msg.debug() << "Instrumenting coverage for function "
328 function_symbol.name,
329 function.body,
330 cover_config.cover_instrumenters,
331 function_symbol.mode,
332 message_handler,
333 cover_config.make_assertion);
334 changed = true;
335 }
336
337 if(
338 cover_config.traces_must_terminate &&
340 {
342 function_symbol.name, function.body, cover_config.make_assertion);
343 changed = true;
344 }
345
346 if(changed)
347 remove_skip(function.body);
348}
349
356 goto_model_functiont &function,
357 message_handlert &message_handler)
358{
360 function.get_symbol_table().lookup_ref(function.get_function_id());
364 function.get_goto_function(),
365 message_handler);
366
367 function.compute_location_numbers();
368}
369
377 const symbol_tablet &symbol_table,
378 goto_functionst &goto_functions,
379 message_handlert &message_handler)
380{
381 messaget msg(message_handler);
382 msg.status() << "Rewriting existing assertions as assumptions"
383 << messaget::eom;
384
385 if(
386 cover_config.traces_must_terminate &&
387 !goto_functions.function_map.count(goto_functions.entry_point()))
388 {
389 msg.error() << "cover-traces-must-terminate: invalid entry point ["
390 << goto_functions.entry_point() << "]" << messaget::eom;
391 return true;
392 }
393
394 for(auto &gf_entry : goto_functions.function_map)
395 {
396 const symbolt function_symbol = symbol_table.lookup_ref(gf_entry.first);
398 cover_config, function_symbol, gf_entry.second, message_handler);
399 }
400 goto_functions.compute_location_numbers();
401
402 cover_config.function_filters.report_anomalies();
403 cover_config.goal_filters->report_anomalies();
404
405 return false;
406}
407
414 goto_modelt &goto_model,
415 message_handlert &message_handler)
416{
419 goto_model.symbol_table,
420 goto_model.goto_functions,
421 message_handler);
422}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
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:135
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:59
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A collection of function filters to be applied in conjunction.
Definition cover_filter.h:64
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
Definition cover_filter.h:68
A collection of goal filters to be applied in conjunction.
Definition cover_filter.h:101
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: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
Definition goto_model.h:27
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.
Definition goto_program.h:72
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition message.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
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.
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
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:36
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:181
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition cover.cpp:143
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
Definition cover.cpp:108
Coverage Instrumentation.
coverage_criteriont
Definition cover.h:45
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:44
Options.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition remove_skip.cpp:87
Program Transformation.
Definition cover.h:58

AltStyle によって変換されたページ (->オリジナル) /