cprover
cover.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 Date: May 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "cover.h"
15 
16 #include <util/config.h>
17 #include <util/message.h>
18 #include <util/make_unique.h>
19 #include <util/cmdline.h>
20 #include <util/options.h>
21 
23 
24 #include "cover_basic_blocks.h"
25 
34  const irep_idt &function_id,
35  goto_programt &goto_program,
36  const cover_instrumenterst &instrumenters,
37  const irep_idt &mode,
38  message_handlert &message_handler)
39 {
40  const std::unique_ptr<cover_blocks_baset> basic_blocks =
41  mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
42  new cover_basic_blocks_javat(goto_program))
43  : std::unique_ptr<cover_blocks_baset>(
44  new cover_basic_blockst(goto_program));
45 
46  basic_blocks->report_block_anomalies(
47  function_id, goto_program, message_handler);
48  instrumenters(function_id, goto_program, *basic_blocks);
49 }
50 
56  coverage_criteriont criterion,
58  const goal_filterst &goal_filters)
59 {
60  switch(criterion)
61  {
63  instrumenters.push_back(
64  util_make_unique<cover_location_instrumentert>(
65  symbol_table, goal_filters));
66  break;
68  instrumenters.push_back(
69  util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
70  break;
72  instrumenters.push_back(
73  util_make_unique<cover_decision_instrumentert>(
74  symbol_table, goal_filters));
75  break;
77  instrumenters.push_back(
78  util_make_unique<cover_condition_instrumentert>(
79  symbol_table, goal_filters));
80  break;
82  instrumenters.push_back(
83  util_make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
84  break;
86  instrumenters.push_back(
87  util_make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
88  break;
90  instrumenters.push_back(
91  util_make_unique<cover_assertion_instrumentert>(
92  symbol_table, goal_filters));
93  break;
95  instrumenters.push_back(
96  util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
97  }
98 }
99 
104 parse_coverage_criterion(const std::string &criterion_string)
105 {
107 
108  if(criterion_string == "assertion" || criterion_string == "assertions")
110  else if(criterion_string == "path" || criterion_string == "paths")
112  else if(criterion_string == "branch" || criterion_string == "branches")
114  else if(criterion_string == "location" || criterion_string == "locations")
116  else if(criterion_string == "decision" || criterion_string == "decisions")
118  else if(criterion_string == "condition" || criterion_string == "conditions")
120  else if(criterion_string == "mcdc")
122  else if(criterion_string == "cover")
124  else
125  {
126  std::stringstream s;
127  s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
128  throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
129  }
130 
131  return c;
132 }
133 
137 void parse_cover_options(const cmdlinet &cmdline, optionst &options)
138 {
139  options.set_option("cover", cmdline.get_values("cover"));
140 
141  // allow retrieving full traces
142  options.set_option("simple-slice", false);
143 
144  options.set_option(
145  "cover-include-pattern", cmdline.get_value("cover-include-pattern"));
146  options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));
147 
148  std::string cover_only = cmdline.get_value("cover-only");
149 
150  if(!cover_only.empty() && cmdline.isset("cover-function-only"))
152  "at most one of --cover-only and --cover-function-only can be used",
153  "--cover-only");
154 
155  options.set_option("cover-only", cmdline.get_value("cover-only"));
156  if(cmdline.isset("cover-function-only"))
157  options.set_option("cover-only", "function");
158 
159  options.set_option(
160  "cover-traces-must-terminate",
161  cmdline.isset("cover-traces-must-terminate"));
162 }
163 
172  const optionst &options,
174  message_handlert &message_handler)
175 {
176  cover_configt cover_config;
177  function_filterst &function_filters =
178  cover_config.cover_configt::function_filters;
179  std::unique_ptr<goal_filterst> &goal_filters = cover_config.goal_filters;
180  cover_instrumenterst &instrumenters = cover_config.cover_instrumenters;
181 
182  function_filters.add(
183  util_make_unique<internal_functions_filtert>(message_handler));
184 
185  goal_filters->add(util_make_unique<internal_goals_filtert>(message_handler));
186 
187  optionst::value_listt criteria_strings = options.get_list_option("cover");
188 
189  cover_config.keep_assertions = false;
190  for(const auto &criterion_string : criteria_strings)
191  {
192  coverage_criteriont c = parse_coverage_criterion(criterion_string);
193 
195  cover_config.keep_assertions = true;
196 
197  instrumenters.add_from_criterion(c, symbol_table, *goal_filters);
198  }
199 
200  if(cover_config.keep_assertions && criteria_strings.size() > 1)
201  {
202  std::stringstream s;
203  s << "assertion coverage cannot currently be used together with other"
204  << "coverage criteria";
205  throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
206  }
207 
208  std::string cover_include_pattern =
209  options.get_option("cover-include-pattern");
210  if(!cover_include_pattern.empty())
211  {
212  function_filters.add(
213  util_make_unique<include_pattern_filtert>(
214  message_handler, cover_include_pattern));
215  }
216 
217  if(options.get_bool_option("no-trivial-tests"))
218  function_filters.add(
219  util_make_unique<trivial_functions_filtert>(message_handler));
220 
221  cover_config.traces_must_terminate =
222  options.get_bool_option("cover-traces-must-terminate");
223 
224  return cover_config;
225 }
226 
235  const optionst &options,
236  const irep_idt &main_function_id,
238  message_handlert &message_handler)
239 {
240  cover_configt cover_config =
241  get_cover_config(options, symbol_table, message_handler);
242 
243  std::string cover_only = options.get_option("cover-only");
244 
245  // cover entry point function only
246  if(cover_only == "function")
247  {
248  const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
249  cover_config.function_filters.add(util_make_unique<single_function_filtert>(
250  message_handler, main_symbol.name));
251  }
252  else if(cover_only == "file")
253  {
254  const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
255  cover_config.function_filters.add(util_make_unique<file_filtert>(
256  message_handler, main_symbol.location.get_file()));
257  }
258  else if(!cover_only.empty())
259  {
260  std::stringstream s;
261  s << "Argument to --cover-only not recognized: " << cover_only;
262  throw invalid_command_line_argument_exceptiont(s.str(), "--cover-only");
263  }
264 
265  return cover_config;
266 }
267 
274  const cover_configt &cover_config,
275  const symbolt &function_symbol,
277  message_handlert &message_handler)
278 {
279  if(!cover_config.keep_assertions)
280  {
281  Forall_goto_program_instructions(i_it, function.body)
282  {
283  // Simplify the common case where we have ASSERT(x); ASSUME(x):
284  if(i_it->is_assert())
285  {
286  auto successor = std::next(i_it);
287  if(
288  successor != function.body.instructions.end() &&
289  successor->is_assume() &&
290  successor->get_condition() == i_it->get_condition())
291  {
292  successor->turn_into_skip();
293  }
294 
296  }
297  }
298  }
299 
300  bool changed = false;
301 
302  if(cover_config.function_filters(function_symbol, function))
303  {
304  messaget msg(message_handler);
305  msg.debug() << "Instrumenting coverage for function "
306  << id2string(function_symbol.name) << messaget::eom;
308  function_symbol.name,
309  function.body,
310  cover_config.cover_instrumenters,
311  function_symbol.mode,
312  message_handler);
313  changed = true;
314  }
315 
316  if(
317  cover_config.traces_must_terminate &&
318  function_symbol.name == goto_functionst::entry_point())
319  {
320  cover_instrument_end_of_function(function_symbol.name, function.body);
321  changed = true;
322  }
323 
324  if(changed)
325  remove_skip(function.body);
326 }
327 
333  const cover_configt &cover_config,
334  goto_model_functiont &function,
335  message_handlert &message_handler)
336 {
337  const symbolt function_symbol =
338  function.get_symbol_table().lookup_ref(function.get_function_id());
340  cover_config,
341  function_symbol,
342  function.get_goto_function(),
343  message_handler);
344 
345  function.compute_location_numbers();
346 }
347 
354  const cover_configt &cover_config,
357  message_handlert &message_handler)
358 {
359  messaget msg(message_handler);
360  msg.status() << "Rewriting existing assertions as assumptions"
361  << messaget::eom;
362 
363  if(
364  cover_config.traces_must_terminate &&
366  {
367  msg.error() << "cover-traces-must-terminate: invalid entry point ["
369  return true;
370  }
371 
373  {
374  const symbolt function_symbol = symbol_table.lookup_ref(f_it->first);
376  cover_config, function_symbol, f_it->second, message_handler);
377  }
379 
380  cover_config.function_filters.report_anomalies();
381  cover_config.goal_filters->report_anomalies();
382 
383  return false;
384 }
385 
391  const cover_configt &cover_config,
392  goto_modelt &goto_model,
393  message_handlert &message_handler)
394 {
395  return instrument_cover_goals(
396  cover_config,
397  goto_model.symbol_table,
398  goto_model.goto_functions,
399  message_handler);
400 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1177
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cover.h
coverage_criteriont::COVER
@ COVER
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
function_filterst::report_anomalies
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:101
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:28
cover_configt::goal_filters
std::unique_ptr< goal_filterst > goal_filters
Definition: cover.h:44
optionst
Definition: options.h:23
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::status
mstreamt & status() const
Definition: message.h:400
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
coverage_criteriont::PATH
@ PATH
goal_filterst::add
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:117
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
goto_modelt
Definition: goto_model.h:26
parse_coverage_criterion
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
Definition: cover.cpp:104
options.h
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:55
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
messaget::eom
static eomt eom
Definition: message.h:283
optionst::value_listt
std::list< std::string > value_listt
Definition: options.h:25
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
coverage_criteriont
coverage_criteriont
Definition: cover.h:26
coverage_criteriont::ASSERTION
@ ASSERTION
instrument_cover_goals
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)
Applies instrumenters to given goto program.
Definition: cover.cpp:33
coverage_criteriont::CONDITION
@ CONDITION
coverage_criteriont::LOCATION
@ LOCATION
get_cover_config
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:171
cover_basic_blocks_javat
Definition: cover_basic_blocks.h:138
cover_instrumenterst::instrumenters
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
Definition: cover_instrument.h:109
cover_configt::cover_instrumenters
cover_instrumenterst cover_instrumenters
Definition: cover.h:46
cmdlinet
Definition: cmdline.h:21
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:385
coverage_criteriont::DECISION
@ DECISION
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
cover_configt::traces_must_terminate
bool traces_must_terminate
Definition: cover.h:40
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:46
message_handlert
Definition: message.h:27
parse_cover_options
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:137
goal_filterst
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:113
cover_blocks_baset::report_block_anomalies
virtual void report_block_anomalies(const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
Definition: cover_basic_blocks.h:51
cover_instrument_end_of_function
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program)
Definition: cover_instrument_other.cpp:74
goto_modelt::get_goto_function
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
Definition: goto_model.h:82
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
cover_basic_blockst
Definition: cover_basic_blocks.h:64
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
cover_configt::function_filters
function_filterst function_filters
Definition: cover.h:42
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
cmdline.h
symbolt
Symbol table entry.
Definition: symbol.h:28
ASSUME
@ ASSUME
Definition: goto_program.h:35
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
coverage_criteriont::BRANCH
@ BRANCH
cover_basic_blocks.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
coverage_criteriont::MCDC
@ MCDC
config.h
cover_configt
Definition: cover.h:38
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
messaget::debug
mstreamt & debug() const
Definition: message.h:415
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
remove_skip.h
message.h
function_filterst
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:76
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:107
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
function_filterst::add
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:80
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
cover_configt::keep_assertions
bool keep_assertions
Definition: cover.h:39
cover_instrumenterst
A collection of instrumenters to be run.
Definition: cover_instrument.h:88