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 #include <util/deprecate.h>
22 
24 
25 #include "cover_basic_blocks.h"
26 
34  goto_programt &goto_program,
35  const cover_instrumenterst &instrumenters,
36  const irep_idt &mode,
37  message_handlert &message_handler)
38 {
39  const std::unique_ptr<cover_blocks_baset> basic_blocks =
40  mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
41  new cover_basic_blocks_javat(goto_program))
42  : std::unique_ptr<cover_blocks_baset>(
43  new cover_basic_blockst(goto_program));
44 
45  basic_blocks->report_block_anomalies(goto_program, message_handler);
46  instrumenters(goto_program, *basic_blocks);
47 }
48 
57 DEPRECATED("use instrument_cover_goals(goto_programt &...) instead")
60  goto_programt &goto_program,
61  coverage_criteriont criterion,
62  message_handlert &message_handler)
63 {
64  goal_filterst goal_filters;
65  goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
66 
67  cover_instrumenterst instrumenters;
68  instrumenters.add_from_criterion(criterion, symbol_table, goal_filters);
69 
71  goto_program, instrumenters, ID_unknown, message_handler);
72 }
73 
79  coverage_criteriont criterion,
81  const goal_filterst &goal_filters)
82 {
83  switch(criterion)
84  {
86  instrumenters.push_back(
87  util_make_unique<cover_location_instrumentert>(
88  symbol_table, goal_filters));
89  break;
91  instrumenters.push_back(
92  util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
93  break;
95  instrumenters.push_back(
96  util_make_unique<cover_decision_instrumentert>(
97  symbol_table, goal_filters));
98  break;
100  instrumenters.push_back(
101  util_make_unique<cover_condition_instrumentert>(
102  symbol_table, goal_filters));
103  break;
105  instrumenters.push_back(
106  util_make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
107  break;
109  instrumenters.push_back(
110  util_make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
111  break;
113  instrumenters.push_back(
114  util_make_unique<cover_assertion_instrumentert>(
115  symbol_table, goal_filters));
116  break;
118  instrumenters.push_back(
119  util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
120  }
121 }
122 
127 parse_coverage_criterion(const std::string &criterion_string)
128 {
130 
131  if(criterion_string == "assertion" || criterion_string == "assertions")
133  else if(criterion_string == "path" || criterion_string == "paths")
135  else if(criterion_string == "branch" || criterion_string == "branches")
137  else if(criterion_string == "location" || criterion_string == "locations")
139  else if(criterion_string == "decision" || criterion_string == "decisions")
141  else if(criterion_string == "condition" || criterion_string == "conditions")
143  else if(criterion_string == "mcdc")
145  else if(criterion_string == "cover")
147  else
148  {
149  std::stringstream s;
150  s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
151  throw s.str();
152  }
153 
154  return c;
155 }
156 
160 void parse_cover_options(const cmdlinet &cmdline, optionst &options)
161 {
162  options.set_option("cover", cmdline.get_values("cover"));
163  std::string cover_include_pattern =
164  cmdline.get_value("cover-include-pattern");
165  if(cmdline.isset("cover-function-only"))
166  {
167  std::regex special_characters(
168  "\\.|\\\\|\\*|\\+|\\?|\\{|\\}|\\[|\\]|\\(|\\)|\\^|\\$|\\|");
169  cover_include_pattern =
170  ".*" + std::regex_replace(config.main, special_characters, "\\$&") + ".*";
171  }
172  options.set_option("cover-include-pattern", cover_include_pattern);
173  options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));
174  options.set_option(
175  "cover-traces-must-terminate",
176  cmdline.isset("cover-traces-must-terminate"));
177 }
178 
184 std::unique_ptr<cover_configt> get_cover_config(
185  const optionst &options,
187  message_handlert &message_handler)
188 {
189  messaget msg(message_handler);
190  std::unique_ptr<cover_configt> config = util_make_unique<cover_configt>();
191  function_filterst &function_filters = config->function_filters;
192  goal_filterst &goal_filters = config->goal_filters;
193  cover_instrumenterst &instrumenters = config->cover_instrumenters;
194 
195  function_filters.add(
196  util_make_unique<internal_functions_filtert>(message_handler));
197 
198  goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
199 
200  optionst::value_listt criteria_strings = options.get_list_option("cover");
201 
202  config->keep_assertions = false;
203  for(const auto &criterion_string : criteria_strings)
204  {
205  try
206  {
207  coverage_criteriont c = parse_coverage_criterion(criterion_string);
208 
210  config->keep_assertions = true;
211 
212  instrumenters.add_from_criterion(c, symbol_table, goal_filters);
213  }
214  catch(const std::string &e)
215  {
216  msg.error() << e << messaget::eom;
217  return {};
218  }
219  }
220 
221  if(config->keep_assertions && criteria_strings.size()>1)
222  {
223  msg.error() << "assertion coverage cannot currently be used together with "
224  << "other coverage criteria" << messaget::eom;
225  return {};
226  }
227 
228  // cover entry point function only
229  std::string cover_include_pattern =
230  options.get_option("cover-include-pattern");
231  if(!cover_include_pattern.empty())
232  {
233  function_filters.add(
234  util_make_unique<include_pattern_filtert>(
235  message_handler, cover_include_pattern));
236  }
237 
238  if(options.get_bool_option("no-trivial-tests"))
239  function_filters.add(
240  util_make_unique<trivial_functions_filtert>(message_handler));
241 
242  config->traces_must_terminate =
243  options.get_bool_option("cover-traces-must-terminate");
244 
245  return config;
246 }
247 
254  const cover_configt &config,
255  const irep_idt &function_id,
257  message_handlert &message_handler)
258 {
259  if(!config.keep_assertions)
260  {
261  Forall_goto_program_instructions(i_it, function.body)
262  {
263  // Simplify the common case where we have ASSERT(x); ASSUME(x):
264  if(i_it->is_assert())
265  {
266  auto successor = std::next(i_it);
267  if(successor != function.body.instructions.end() &&
268  successor->is_assume() &&
269  successor->guard == i_it->guard)
270  {
271  successor->make_skip();
272  }
274  }
275  }
276  }
277 
278  bool changed = false;
279 
280  if(config.function_filters(function_id, function))
281  {
283  function.body, config.cover_instrumenters, config.mode, message_handler);
284  changed = true;
285  }
286 
287  if(config.traces_must_terminate &&
288  function_id == goto_functionst::entry_point())
289  {
290  cover_instrument_end_of_function(function_id, function.body);
291  changed = true;
292  }
293 
294  if(changed)
295  remove_skip(function.body);
296 }
297 
303  const cover_configt &config,
304  goto_model_functiont &function,
305  message_handlert &message_handler)
306 {
308  config,
309  function.get_function_id(),
310  function.get_goto_function(),
311  message_handler);
312 
313  function.compute_location_numbers();
314 }
315 
322  const optionst &options,
325  message_handlert &message_handler)
326 {
327  messaget msg(message_handler);
328  msg.status() << "Rewriting existing assertions as assumptions"
329  << messaget::eom;
330 
331  std::unique_ptr<cover_configt> config =
332  get_cover_config(options, symbol_table, message_handler);
333  if(!config)
334  return true;
335 
336  if(config->traces_must_terminate &&
338  {
339  msg.error() << "cover-traces-must-terminate: invalid entry point ["
341  return true;
342  }
343 
345  {
346  config->mode = symbol_table.lookup(f_it->first)->mode;
348  *config, f_it->first, f_it->second, message_handler);
349  }
351 
352  config->function_filters.report_anomalies();
353  config->goal_filters.report_anomalies();
354 
355  return false;
356 }
357 
363  const optionst &options,
364  goto_modelt &goto_model,
365  message_handlert &message_handler)
366 {
367  return instrument_cover_goals(
368  options,
369  goto_model.symbol_table,
370  goto_model.goto_functions,
371  message_handler);
372 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
cover.h
coverage_criteriont::COVER
@ COVER
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
optionst
Definition: options.h:22
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
messaget::status
mstreamt & status() const
Definition: message.h:401
configt::main
std::string main
Definition: config.h:172
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
coverage_criteriont::PATH
@ PATH
goal_filterst::add
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:116
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
goto_modelt
Definition: goto_model.h:24
parse_coverage_criterion
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
Definition: cover.cpp:127
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:78
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
messaget::eom
static eomt eom
Definition: message.h:284
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:25
coverage_criteriont::ASSERTION
@ ASSERTION
coverage_criteriont::CONDITION
@ CONDITION
coverage_criteriont::LOCATION
@ LOCATION
cover_basic_blocks_javat
Definition: cover_basic_blocks.h:123
cover_instrumenterst::instrumenters
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
Definition: cover_instrument.h:105
cmdlinet
Definition: cmdline.h:19
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:386
coverage_criteriont::DECISION
@ DECISION
cover_blocks_baset::report_block_anomalies
virtual void report_block_anomalies(const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
Definition: cover_basic_blocks.h:48
deprecate.h
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
message_handlert
Definition: message.h:24
parse_cover_options
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:160
goal_filterst
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:111
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:81
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
config
configt config
Definition: config.cpp:24
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
cover_basic_blockst
Definition: cover_basic_blocks.h:58
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
instrument_cover_goals
void instrument_cover_goals(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
cmdline.h
ASSUME
@ ASSUME
Definition: goto_program.h:35
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
coverage_criteriont::BRANCH
@ BRANCH
get_cover_config
std::unique_ptr< 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:184
cover_basic_blocks.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
coverage_criteriont::MCDC
@ MCDC
config.h
cover_configt
Definition: cover.h:37
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
remove_skip.h
message.h
function_filterst
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:74
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
function_filterst::add
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:79
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:78
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
cover_instrument_end_of_function
void cover_instrument_end_of_function(const irep_idt &function, goto_programt &goto_program)
Definition: cover_instrument_other.cpp:72
cover_instrumenterst
A collection of instrumenters to be run.
Definition: cover_instrument.h:85