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 
38  const irep_idt &function_id,
39  goto_programt &goto_program,
40  const cover_instrumenterst &instrumenters,
41  const irep_idt &mode,
42  message_handlert &message_handler,
44 {
45  const std::unique_ptr<cover_blocks_baset> basic_blocks =
46  mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
47  new cover_basic_blocks_javat(goto_program))
48  : std::unique_ptr<cover_blocks_baset>(
49  new cover_basic_blockst(goto_program));
50 
51  basic_blocks->report_block_anomalies(
52  function_id, goto_program, message_handler);
53  instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
54 }
55 
61  coverage_criteriont criterion,
62  const symbol_tablet &symbol_table,
63  const goal_filterst &goal_filters)
64 {
65  switch(criterion)
66  {
68  instrumenters.push_back(
69  util_make_unique<cover_location_instrumentert>(
70  symbol_table, goal_filters));
71  break;
73  instrumenters.push_back(
74  util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
75  break;
77  instrumenters.push_back(
78  util_make_unique<cover_decision_instrumentert>(
79  symbol_table, goal_filters));
80  break;
82  instrumenters.push_back(
83  util_make_unique<cover_condition_instrumentert>(
84  symbol_table, goal_filters));
85  break;
87  instrumenters.push_back(
88  util_make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
89  break;
91  instrumenters.push_back(
92  util_make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
93  break;
95  instrumenters.push_back(
96  util_make_unique<cover_assertion_instrumentert>(
97  symbol_table, goal_filters));
98  break;
100  instrumenters.push_back(
101  util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
102  }
103 }
104 
109 parse_coverage_criterion(const std::string &criterion_string)
110 {
112 
113  if(criterion_string == "assertion" || criterion_string == "assertions")
115  else if(criterion_string == "path" || criterion_string == "paths")
117  else if(criterion_string == "branch" || criterion_string == "branches")
119  else if(criterion_string == "location" || criterion_string == "locations")
121  else if(criterion_string == "decision" || criterion_string == "decisions")
123  else if(criterion_string == "condition" || criterion_string == "conditions")
125  else if(criterion_string == "mcdc")
127  else if(criterion_string == "cover")
129  else
130  {
131  std::stringstream s;
132  s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
133  throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
134  }
135 
136  return c;
137 }
138 
142 void parse_cover_options(const cmdlinet &cmdline, optionst &options)
143 {
144  options.set_option("cover", cmdline.get_values("cover"));
145 
146  // allow retrieving full traces
147  options.set_option("simple-slice", false);
148 
149  options.set_option(
150  "cover-include-pattern", cmdline.get_value("cover-include-pattern"));
151  options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));
152 
153  std::string cover_only = cmdline.get_value("cover-only");
154 
155  if(!cover_only.empty() && cmdline.isset("cover-function-only"))
157  "at most one of --cover-only and --cover-function-only can be used",
158  "--cover-only");
159 
160  options.set_option("cover-only", cmdline.get_value("cover-only"));
161  if(cmdline.isset("cover-function-only"))
162  options.set_option("cover-only", "function");
163 
164  options.set_option(
165  "cover-traces-must-terminate",
166  cmdline.isset("cover-traces-must-terminate"));
167  options.set_option(
168  "cover-failed-assertions", cmdline.isset("cover-failed-assertions"));
169 
170  options.set_option("show-test-suite", cmdline.isset("show-test-suite"));
171 }
172 
181  const optionst &options,
182  const symbol_tablet &symbol_table,
183  message_handlert &message_handler)
184 {
185  cover_configt cover_config;
186  function_filterst &function_filters =
187  cover_config.cover_configt::function_filters;
188  std::unique_ptr<goal_filterst> &goal_filters = cover_config.goal_filters;
189  cover_instrumenterst &instrumenters = cover_config.cover_instrumenters;
190 
191  function_filters.add(util_make_unique<internal_functions_filtert>());
192 
193  goal_filters->add(util_make_unique<internal_goals_filtert>());
194 
195  optionst::value_listt criteria_strings = options.get_list_option("cover");
196 
197  cover_config.keep_assertions = false;
198  for(const auto &criterion_string : criteria_strings)
199  {
200  coverage_criteriont c = parse_coverage_criterion(criterion_string);
201 
203  cover_config.keep_assertions = true;
204 
205  instrumenters.add_from_criterion(c, symbol_table, *goal_filters);
206  }
207 
208  if(cover_config.keep_assertions && criteria_strings.size() > 1)
209  {
210  std::stringstream s;
211  s << "assertion coverage cannot currently be used together with other"
212  << "coverage criteria";
213  throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
214  }
215 
216  std::string cover_include_pattern =
217  options.get_option("cover-include-pattern");
218  if(!cover_include_pattern.empty())
219  {
220  function_filters.add(
221  util_make_unique<include_pattern_filtert>(cover_include_pattern));
222  }
223 
224  if(options.get_bool_option("no-trivial-tests"))
225  function_filters.add(util_make_unique<trivial_functions_filtert>());
226 
227  cover_config.traces_must_terminate =
228  options.get_bool_option("cover-traces-must-terminate");
229 
230  cover_config.cover_failed_assertions =
231  options.get_bool_option("cover-failed-assertions");
232 
233  return cover_config;
234 }
235 
244  const optionst &options,
245  const irep_idt &main_function_id,
246  const symbol_tablet &symbol_table,
247  message_handlert &message_handler)
248 {
249  cover_configt cover_config =
250  get_cover_config(options, symbol_table, message_handler);
251 
252  std::string cover_only = options.get_option("cover-only");
253 
254  // cover entry point function only
255  if(cover_only == "function")
256  {
257  const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
258  cover_config.function_filters.add(
259  util_make_unique<single_function_filtert>(main_symbol.name));
260  }
261  else if(cover_only == "file")
262  {
263  const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
264  cover_config.function_filters.add(
265  util_make_unique<file_filtert>(main_symbol.location.get_file()));
266  }
267  else if(!cover_only.empty())
268  {
269  std::stringstream s;
270  s << "Argument to --cover-only not recognized: " << cover_only;
271  throw invalid_command_line_argument_exceptiont(s.str(), "--cover-only");
272  }
273 
274  return cover_config;
275 }
276 
283  const cover_configt &cover_config,
284  const symbolt &function_symbol,
286  message_handlert &message_handler)
287 {
288  if(!cover_config.keep_assertions)
289  {
290  Forall_goto_program_instructions(i_it, function.body)
291  {
292  // Simplify the common case where we have ASSERT(x); ASSUME(x):
293  if(i_it->is_assert())
294  {
295  if(!cover_config.cover_failed_assertions)
296  {
297  auto successor = std::next(i_it);
298  if(
299  successor != function.body.instructions.end() &&
300  successor->is_assume() &&
301  successor->get_condition() == i_it->get_condition())
302  {
303  successor->turn_into_skip();
304  }
306  }
307  else
308  {
309  i_it->turn_into_skip();
310  }
311  }
312  }
313  }
314 
315  bool changed = false;
316 
317  if(cover_config.function_filters(function_symbol, function))
318  {
319  messaget msg(message_handler);
320  msg.debug() << "Instrumenting coverage for function "
321  << id2string(function_symbol.name) << messaget::eom;
323  function_symbol.name,
324  function.body,
325  cover_config.cover_instrumenters,
326  function_symbol.mode,
327  message_handler,
328  cover_config.make_assertion);
329  changed = true;
330  }
331 
332  if(
333  cover_config.traces_must_terminate &&
334  function_symbol.name == goto_functionst::entry_point())
335  {
337  function_symbol.name, function.body, cover_config.make_assertion);
338  changed = true;
339  }
340 
341  if(changed)
342  remove_skip(function.body);
343 }
344 
350  const cover_configt &cover_config,
351  goto_model_functiont &function,
352  message_handlert &message_handler)
353 {
354  const symbolt function_symbol =
355  function.get_symbol_table().lookup_ref(function.get_function_id());
357  cover_config,
358  function_symbol,
359  function.get_goto_function(),
360  message_handler);
361 
362  function.compute_location_numbers();
363 }
364 
371  const cover_configt &cover_config,
372  const symbol_tablet &symbol_table,
373  goto_functionst &goto_functions,
374  message_handlert &message_handler)
375 {
376  messaget msg(message_handler);
377  msg.status() << "Rewriting existing assertions as assumptions"
378  << messaget::eom;
379 
380  if(
381  cover_config.traces_must_terminate &&
382  !goto_functions.function_map.count(goto_functions.entry_point()))
383  {
384  msg.error() << "cover-traces-must-terminate: invalid entry point ["
385  << goto_functions.entry_point() << "]" << messaget::eom;
386  return true;
387  }
388 
389  for(auto &gf_entry : goto_functions.function_map)
390  {
391  const symbolt function_symbol = symbol_table.lookup_ref(gf_entry.first);
393  cover_config, function_symbol, gf_entry.second, message_handler);
394  }
395  goto_functions.compute_location_numbers();
396 
397  cover_config.function_filters.report_anomalies();
398  cover_config.goal_filters->report_anomalies();
399 
400  return false;
401 }
402 
408  const cover_configt &cover_config,
409  goto_modelt &goto_model,
410  message_handlert &message_handler)
411 {
412  return instrument_cover_goals(
413  cover_config,
414  goto_model.symbol_table,
415  goto_model.goto_functions,
416  message_handler);
417 }
std::string get_value(char option) const
Definition: cmdline.cpp:47
virtual bool isset(char option) const
Definition: cmdline.cpp:29
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
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_tablet &, const goal_filterst &)
Create and add an instrumenter based on the given criterion.
Definition: cover.cpp:60
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:65
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:69
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:90
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:102
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:183
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
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
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:20
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
irep_idt mode
Language mode.
Definition: symbol.h:49
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:37
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:180
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:142
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
Definition: cover.cpp:109
Coverage Instrumentation.
coverage_criteriont
Definition: cover.h:41
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 &)
#define Forall_goto_program_instructions(it, program)
@ ASSUME
Definition: goto_program.h:36
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
Options.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
Program Transformation.
bool traces_must_terminate
Definition: cover.h:56
bool keep_assertions
Definition: cover.h:54
cover_instrumenterst cover_instrumenters
Definition: cover.h:62
bool cover_failed_assertions
Definition: cover.h:55
cover_instrumenter_baset::assertion_factoryt make_assertion
Definition: cover.h:63
function_filterst function_filters
Definition: cover.h:58
std::unique_ptr< goal_filterst > goal_filters
Definition: cover.h:60