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 
36  const irep_idt &mode,
38 {
39  const std::unique_ptr<cover_blocks_baset> basic_blocks =
40  mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
42  : std::unique_ptr<cover_blocks_baset>(
44 
46  instrumenters(goto_program, *basic_blocks);
47 }
48 
58  "use instrument_cover_goals(goto_programt &goto_program,"
59  "const cover_instrumenterst &instrumenters,"
60  "message_handlert &message_handler, const irep_idt mode) instead")
66 {
67  goal_filterst goal_filters;
68  goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
69 
72 
75 }
76 
84  const goal_filterst &goal_filters)
85 {
86  switch(criterion)
87  {
89  instrumenters.push_back(
90  util_make_unique<cover_location_instrumentert>(
91  symbol_table, goal_filters));
92  break;
94  instrumenters.push_back(
95  util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
96  break;
98  instrumenters.push_back(
99  util_make_unique<cover_decision_instrumentert>(
100  symbol_table, goal_filters));
101  break;
103  instrumenters.push_back(
104  util_make_unique<cover_condition_instrumentert>(
105  symbol_table, goal_filters));
106  break;
108  instrumenters.push_back(
109  util_make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
110  break;
112  instrumenters.push_back(
113  util_make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
114  break;
116  instrumenters.push_back(
117  util_make_unique<cover_assertion_instrumentert>(
118  symbol_table, goal_filters));
119  break;
121  instrumenters.push_back(
122  util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
123  }
124 }
125 
130 parse_coverage_criterion(const std::string &criterion_string)
131 {
133 
134  if(criterion_string == "assertion" || criterion_string == "assertions")
136  else if(criterion_string == "path" || criterion_string == "paths")
138  else if(criterion_string == "branch" || criterion_string == "branches")
140  else if(criterion_string == "location" || criterion_string == "locations")
142  else if(criterion_string == "decision" || criterion_string == "decisions")
144  else if(criterion_string == "condition" || criterion_string == "conditions")
146  else if(criterion_string == "mcdc")
148  else if(criterion_string == "cover")
150  else
151  {
152  std::stringstream s;
153  s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
154  throw s.str();
155  }
156 
157  return c;
158 }
159 
163 void parse_cover_options(const cmdlinet &cmdline, optionst &options)
164 {
165  options.set_option("cover", cmdline.get_values("cover"));
166  std::string cover_include_pattern =
167  cmdline.get_value("cover-include-pattern");
168  if(cmdline.isset("cover-function-only"))
169  {
170  std::regex special_characters(
171  "\\.|\\\\|\\*|\\+|\\?|\\{|\\}|\\[|\\]|\\(|\\)|\\^|\\$|\\|");
172  cover_include_pattern =
173  ".*" + std::regex_replace(config.main, special_characters, "\\$&") + ".*";
174  }
175  options.set_option("cover-include-pattern", cover_include_pattern);
176  options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));
177  options.set_option(
178  "cover-traces-must-terminate",
179  cmdline.isset("cover-traces-must-terminate"));
180 }
181 
187 std::unique_ptr<cover_configt> get_cover_config(
188  const optionst &options,
191 {
193  std::unique_ptr<cover_configt> config = util_make_unique<cover_configt>();
194  function_filterst &function_filters = config->function_filters;
195  goal_filterst &goal_filters = config->goal_filters;
196  cover_instrumenterst &instrumenters = config->cover_instrumenters;
197 
198  function_filters.add(
199  util_make_unique<internal_functions_filtert>(message_handler));
200 
201  goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
202 
203  optionst::value_listt criteria_strings = options.get_list_option("cover");
204 
205  config->keep_assertions = false;
206  for(const auto &criterion_string : criteria_strings)
207  {
208  try
209  {
210  coverage_criteriont c = parse_coverage_criterion(criterion_string);
211 
213  config->keep_assertions = true;
214 
216  }
217  catch(const std::string &e)
218  {
219  msg.error() << e << messaget::eom;
220  return {};
221  }
222  }
223 
224  if(config->keep_assertions && criteria_strings.size()>1)
225  {
226  msg.error() << "assertion coverage cannot currently be used together with "
227  << "other coverage criteria" << messaget::eom;
228  return {};
229  }
230 
231  // cover entry point function only
232  std::string cover_include_pattern =
233  options.get_option("cover-include-pattern");
234  if(!cover_include_pattern.empty())
235  {
236  function_filters.add(
237  util_make_unique<include_pattern_filtert>(
238  message_handler, cover_include_pattern));
239  }
240 
241  if(options.get_bool_option("no-trivial-tests"))
242  function_filters.add(
243  util_make_unique<trivial_functions_filtert>(message_handler));
244 
245  config->traces_must_terminate =
246  options.get_bool_option("cover-traces-must-terminate");
247 
248  return config;
249 }
250 
257  const cover_configt &config,
258  const irep_idt &function_id,
261 {
262  if(!config.keep_assertions)
263  {
264  Forall_goto_program_instructions(i_it, function.body)
265  {
266  // Simplify the common case where we have ASSERT(x); ASSUME(x):
267  if(i_it->is_assert())
268  {
269  auto successor = std::next(i_it);
270  if(successor != function.body.instructions.end() &&
271  successor->is_assume() &&
272  successor->guard == i_it->guard)
273  {
274  successor->make_skip();
275  }
277  }
278  }
279  }
280 
281  bool changed = false;
282 
283  if(config.function_filters(function_id, function))
284  {
286  function.body, config.cover_instrumenters, config.mode, message_handler);
287  changed = true;
288  }
289 
290  if(config.traces_must_terminate &&
291  function_id == goto_functionst::entry_point())
292  {
293  cover_instrument_end_of_function(function_id, function.body);
294  changed = true;
295  }
296 
297  if(changed)
298  remove_skip(function.body);
299 }
300 
306  const cover_configt &config,
307  goto_model_functiont &function,
309 {
311  config,
312  function.get_function_id(),
313  function.get_goto_function(),
315 
316  function.compute_location_numbers();
317 }
318 
325  const optionst &options,
329 {
331  msg.status() << "Rewriting existing assertions as assumptions"
332  << messaget::eom;
333 
334  std::unique_ptr<cover_configt> config =
336  if(!config)
337  return true;
338 
339  if(config->traces_must_terminate &&
341  {
342  msg.error() << "cover-traces-must-terminate: invalid entry point ["
344  return true;
345  }
346 
348  {
349  config->mode = symbol_table.lookup(f_it->first)->mode;
351  *config, f_it->first, f_it->second, message_handler);
352  }
354 
355  config->function_filters.report_anomalies();
356  config->goal_filters.report_anomalies();
357 
358  return false;
359 }
360 
366  const optionst &options,
367  goto_modelt &goto_model,
369 {
370  return instrument_cover_goals(
371  options,
372  goto_model.symbol_table,
373  goto_model.goto_functions,
375 }
coverage_criteriont
Definition: cover.h:25
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:74
irep_idt mode
Language mode.
Definition: symbol.h:52
std::string get_value(char option) const
Definition: cmdline.cpp:45
function_mapt function_map
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:78
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
void cover_instrument_end_of_function(const irep_idt &function, goto_programt &goto_program)
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
Basic blocks detection for Coverage Instrumentation.
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:163
void compute_location_numbers()
virtual bool isset(char option) const
Definition: cmdline.cpp:27
virtual void report_block_anomalies(const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
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:87
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
std::string main
Definition: config.h:171
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:116
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
std::list< std::string > value_listt
Definition: options.h:22
::goto_functiont goto_functiont
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
Definition: cover.cpp:130
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
static irep_idt entry_point()
mstreamt & status() const
Definition: message.h:317
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#define Forall_goto_functions(it, functions)
goto_programt coverage_criteriont criterion
Definition: cover.cpp:63
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Options.
Coverage Instrumentation.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
Program Transformation.
A collection of instrumenters to be run.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
cover_instrumenterst instrumenters
Definition: cover.cpp:70
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:111
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
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:187
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:81
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147