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/message.h>
17 #include <util/make_unique.h>
18 #include <util/cmdline.h>
19 #include <util/options.h>
20 
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 
60  coverage_criteriont criterion,
62  const goal_filterst &goal_filters)
63 {
64  switch(criterion)
65  {
67  instrumenters.push_back(
68  util_make_unique<cover_location_instrumentert>(
69  symbol_table, goal_filters));
70  break;
71  case coverage_criteriont::BRANCH:
72  instrumenters.push_back(
73  util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
74  break;
75  case coverage_criteriont::DECISION:
76  instrumenters.push_back(
77  util_make_unique<cover_decision_instrumentert>(
78  symbol_table, goal_filters));
79  break;
80  case coverage_criteriont::CONDITION:
81  instrumenters.push_back(
82  util_make_unique<cover_condition_instrumentert>(
83  symbol_table, goal_filters));
84  break;
85  case coverage_criteriont::PATH:
86  instrumenters.push_back(
87  util_make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
88  break;
89  case coverage_criteriont::MCDC:
90  instrumenters.push_back(
91  util_make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
92  break;
93  case coverage_criteriont::ASSERTION:
94  instrumenters.push_back(
95  util_make_unique<cover_assertion_instrumentert>(
96  symbol_table, goal_filters));
97  break;
99  instrumenters.push_back(
100  util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
101  }
102 }
103 
108 parse_coverage_criterion(const std::string &criterion_string)
109 {
111 
112  if(criterion_string == "assertion" || criterion_string == "assertions")
113  c = coverage_criteriont::ASSERTION;
114  else if(criterion_string == "path" || criterion_string == "paths")
115  c = coverage_criteriont::PATH;
116  else if(criterion_string == "branch" || criterion_string == "branches")
117  c = coverage_criteriont::BRANCH;
118  else if(criterion_string == "location" || criterion_string == "locations")
120  else if(criterion_string == "decision" || criterion_string == "decisions")
121  c = coverage_criteriont::DECISION;
122  else if(criterion_string == "condition" || criterion_string == "conditions")
123  c = coverage_criteriont::CONDITION;
124  else if(criterion_string == "mcdc")
125  c = coverage_criteriont::MCDC;
126  else if(criterion_string == "cover")
128  else
129  {
130  std::stringstream s;
131  s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
132  throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
133  }
134 
135  return c;
136 }
137 
141 void parse_cover_options(const cmdlinet &cmdline, optionst &options)
142 {
143  options.set_option("cover", cmdline.get_values("cover"));
144 
145  // allow retrieving full traces
146  options.set_option("simple-slice", false);
147 
148  options.set_option(
149  "cover-include-pattern", cmdline.get_value("cover-include-pattern"));
150  options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));
151 
152  std::string cover_only = cmdline.get_value("cover-only");
153 
154  if(!cover_only.empty() && cmdline.isset("cover-function-only"))
156  "at most one of --cover-only and --cover-function-only can be used",
157  "--cover-only");
158 
159  options.set_option("cover-only", cmdline.get_value("cover-only"));
160  if(cmdline.isset("cover-function-only"))
161  options.set_option("cover-only", "function");
162 
163  options.set_option(
164  "cover-traces-must-terminate",
165  cmdline.isset("cover-traces-must-terminate"));
166  options.set_option(
167  "cover-failed-assertions", cmdline.isset("cover-failed-assertions"));
168 
169  options.set_option("show-test-suite", cmdline.isset("show-test-suite"));
170 }
171 
180  const optionst &options,
182  message_handlert &message_handler)
183 {
184  cover_configt cover_config;
185  function_filterst &function_filters =
186  cover_config.cover_configt::function_filters;
187  std::unique_ptr<goal_filterst> &goal_filters = cover_config.goal_filters;
188  cover_instrumenterst &instrumenters = cover_config.cover_instrumenters;
189 
190  function_filters.add(util_make_unique<internal_functions_filtert>());
191 
192  goal_filters->add(util_make_unique<internal_goals_filtert>());
193 
194  optionst::value_listt criteria_strings = options.get_list_option("cover");
195 
196  cover_config.keep_assertions = false;
197  for(const auto &criterion_string : criteria_strings)
198  {
199  coverage_criteriont c = parse_coverage_criterion(criterion_string);
200 
201  if(c == coverage_criteriont::ASSERTION)
202  cover_config.keep_assertions = true;
203 
204  instrumenters.add_from_criterion(c, symbol_table, *goal_filters);
205  }
206 
207  if(cover_config.keep_assertions && criteria_strings.size() > 1)
208  {
209  std::stringstream s;
210  s << "assertion coverage cannot currently be used together with other"
211  << "coverage criteria";
212  throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
213  }
214 
215  std::string cover_include_pattern =
216  options.get_option("cover-include-pattern");
217  if(!cover_include_pattern.empty())
218  {
219  function_filters.add(
220  util_make_unique<include_pattern_filtert>(cover_include_pattern));
221  }
222 
223  if(options.get_bool_option("no-trivial-tests"))
224  function_filters.add(util_make_unique<trivial_functions_filtert>());
225 
226  cover_config.traces_must_terminate =
227  options.get_bool_option("cover-traces-must-terminate");
228 
229  cover_config.cover_failed_assertions =
230  options.get_bool_option("cover-failed-assertions");
231 
232  return cover_config;
233 }
234 
243  const optionst &options,
244  const irep_idt &main_function_id,
246  message_handlert &message_handler)
247 {
248  cover_configt cover_config =
249  get_cover_config(options, symbol_table, message_handler);
250 
251  std::string cover_only = options.get_option("cover-only");
252 
253  // cover entry point function only
254  if(cover_only == "function")
255  {
256  const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
257  cover_config.function_filters.add(
258  util_make_unique<single_function_filtert>(main_symbol.name));
259  }
260  else if(cover_only == "file")
261  {
262  const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
263  cover_config.function_filters.add(
264  util_make_unique<file_filtert>(main_symbol.location.get_file()));
265  }
266  else if(!cover_only.empty())
267  {
268  std::stringstream s;
269  s << "Argument to --cover-only not recognized: " << cover_only;
270  throw invalid_command_line_argument_exceptiont(s.str(), "--cover-only");
271  }
272 
273  return cover_config;
274 }
275 
282  const cover_configt &cover_config,
283  const symbolt &function_symbol,
285  message_handlert &message_handler)
286 {
287  if(!cover_config.keep_assertions)
288  {
289  Forall_goto_program_instructions(i_it, function.body)
290  {
291  // Simplify the common case where we have ASSERT(x); ASSUME(x):
292  if(i_it->is_assert())
293  {
294  if(!cover_config.cover_failed_assertions)
295  {
296  auto successor = std::next(i_it);
297  if(
298  successor != function.body.instructions.end() &&
299  successor->is_assume() &&
300  successor->get_condition() == i_it->get_condition())
301  {
302  successor->turn_into_skip();
303  }
305  }
306  else
307  {
308  i_it->turn_into_skip();
309  }
310  }
311  }
312  }
313 
314  bool changed = false;
315 
316  if(cover_config.function_filters(function_symbol, function))
317  {
318  messaget msg(message_handler);
319  msg.debug() << "Instrumenting coverage for function "
320  << id2string(function_symbol.name) << messaget::eom;
322  function_symbol.name,
323  function.body,
324  cover_config.cover_instrumenters,
325  function_symbol.mode,
326  message_handler,
327  cover_config.make_assertion);
328  changed = true;
329  }
330 
331  if(
332  cover_config.traces_must_terminate &&
333  function_symbol.name == goto_functionst::entry_point())
334  {
336  function_symbol.name, function.body, cover_config.make_assertion);
337  changed = true;
338  }
339 
340  if(changed)
341  remove_skip(function.body);
342 }
343 
349  const cover_configt &cover_config,
350  goto_model_functiont &function,
351  message_handlert &message_handler)
352 {
353  const symbolt function_symbol =
354  function.get_symbol_table().lookup_ref(function.get_function_id());
356  cover_config,
357  function_symbol,
358  function.get_goto_function(),
359  message_handler);
360 
361  function.compute_location_numbers();
362 }
363 
370  const cover_configt &cover_config,
373  message_handlert &message_handler)
374 {
375  messaget msg(message_handler);
376  msg.status() << "Rewriting existing assertions as assumptions"
377  << messaget::eom;
378 
379  if(
380  cover_config.traces_must_terminate &&
382  {
383  msg.error() << "cover-traces-must-terminate: invalid entry point ["
385  return true;
386  }
387 
388  for(auto &gf_entry : goto_functions.function_map)
389  {
390  const symbolt function_symbol = symbol_table.lookup_ref(gf_entry.first);
392  cover_config, function_symbol, gf_entry.second, message_handler);
393  }
395 
396  cover_config.function_filters.report_anomalies();
397  cover_config.goal_filters->report_anomalies();
398 
399  return false;
400 }
401 
407  const cover_configt &cover_config,
408  goto_modelt &goto_model,
409  message_handlert &message_handler)
410 {
411  return instrument_cover_goals(
412  cover_config,
413  goto_model.symbol_table,
414  goto_model.goto_functions,
415  message_handler);
416 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1185
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 Instrumentation.
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:90
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
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:74
cover_configt::goal_filters
std::unique_ptr< goal_filterst > goal_filters
Definition: cover.h:60
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:414
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:86
goal_filterst::add
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:106
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
cover_configt::cover_failed_assertions
bool cover_failed_assertions
Definition: cover.h:55
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:108
options.h
Options.
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:59
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:297
optionst::value_listt
std::list< std::string > value_listt
Definition: options.h:25
instrument_cover_goals
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
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
coverage_criteriont
coverage_criteriont
Definition: cover.h:41
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:179
cover_basic_blocks_javat
Definition: cover_basic_blocks.h:143
cover_instrumenterst::instrumenters
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
Definition: cover_instrument.h:126
cover_configt::cover_instrumenters
cover_instrumenterst cover_instrumenters
Definition: cover.h:62
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:399
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
cover_configt::traces_must_terminate
bool traces_must_terminate
Definition: cover.h:56
cover_configt::make_assertion
cover_instrumenter_baset::assertion_factoryt make_assertion
Definition: cover.h:63
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
message_handlert
Definition: message.h:28
parse_cover_options
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:141
goal_filterst
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:102
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_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
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
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:58
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:36
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
cover_basic_blocks.h
Basic blocks detection for Coverage Instrumentation.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
cover_configt
Definition: cover.h:53
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
messaget::debug
mstreamt & debug() const
Definition: message.h:429
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
Program Transformation.
message.h
function_filterst
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:65
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:108
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:69
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:54
cover_instrumenterst
A collection of instrumenters to be run.
Definition: cover_instrument.h:102