Refactor coverage instrumentation #1419

peterschrammel · 2017-09-24T18:03:28Z

Splits cover.cpp into several files and class-ifies various instrumenters and filters applied

Companions:

subsumes #1348
depends on: #1685 (first commit of this PR)

smowton

One significant problem to look at and a few cleanups that might be worth getting in while we're touching every line

smowton · 2017-09-26T09:15:45Z

src/goto-instrument/cover_basic_blocks.cpp

+
+void cover_basic_blockst::output(std::ostream &out) const
+{
+  for(block_mapt::const_iterator


Convert to for-each loop while we're here?

smowton · 2017-09-26T09:20:00Z

src/goto-instrument/cover_basic_blocks.cpp

+  INVARIANT(!cover_set.empty(),
+            "covered lines set must not be empty");
+  std::vector<unsigned>
+    line_list{cover_set.begin(), cover_set.end()};


@reuk will no doubt know better, but is there any advantage to using init-list-style construction here (briefly suggesting a list of iterators) rather than constructor notation (line_list(cover_set.begin(), cover_set.end()))?

Basically no difference, but I prefer the curly brace syntax as it allows constructor calls to be distinguished from free function calls.

Ahh, I always expect something behaving like aggregate init (e.g. std::vector<int> {1,2,3}) when I see braced init. Matter of taste I suppose, but we should arrive at some convention for the codebase and exercise it consistently.

smowton · 2017-09-26T09:22:17Z

src/goto-instrument/cover_filter.cpp

+    id2string(identifier), string_matcher, regex_matcher);
+}
+
+/// Call a goto_program non-trivial if it has: * Any declarations * At least 2


Line-break bulleted list

smowton · 2017-09-26T09:37:39Z

src/goto-instrument/cover_instrument_branch.cpp

+  goto_programt::targett &i_it,
+  const cover_basic_blockst &basic_blocks) const
+{
+  if(i_it->is_assert())


In the case where several instrumenters are being run, this will destroy the previous one's work. These may be redundant in the face of assert-to-assume always preceding instrumentation, or if this is needed for other reasons then we should simply rule out multiple coverage types for now.

Well spotted.

smowton · 2017-09-26T09:39:30Z

src/goto-instrument/cover_instrument_branch.cpp

+    i_it->source_location=source_location;
+    initialize_source_location(i_it, false_comment, function);
+
+    i_it++;


Suggest std::advance(i_it, 2) to make clear this isn't a typo

tautschnig · 2017-11-30T11:51:48Z

@peterschrammel Requires a rebase.

martin-cs

A few concerns about language specific things and a few places where it could perhaps be cleaner but over-all, pretty good.

martin-cs · 2017-12-15T22:57:44Z

src/goto-instrument/cover.cpp

+/// \return a coverage criterion or throws an exception
+coverage_criteriont
+parse_coverage_criterion(const std::string &criterion_string)
+{


Is this a violation of the "command line parsing should be done in the binary / front-end directories" principle?

Command line parsing is a bit involved here. Repeating the code for each binary cannot be the solution. I've provided utility functions here that should be used by the binary to avoid duplication.

martin-cs · 2017-12-15T23:00:10Z

src/goto-instrument/cover.cpp

-    }
+    std::stringstream s;
+    s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
+    throw s.str();


This feels a bit wrong as I'd want a user error to give a meaningful error message, not throw an exception.

martin-cs · 2017-12-15T23:01:43Z

src/goto-instrument/cover.cpp

+  std::string cover_include_pattern =
+    cmdline.get_value("cover-include-pattern");
+  if(cmdline.isset("cover-function-only"))
+  {


I think command line parsing should be done in the binary directories.

martin-cs · 2017-12-15T23:03:51Z

src/goto-instrument/cover.h

+  PATH,
+  MCDC,
+  ASSERTION,
+  COVER


This option is far from obvious. Isn't this enum to saw what to cover?

martin-cs · 2017-12-15T23:04:24Z

src/goto-instrument/cover.h

-  coverage_goalst &,
-  bool function_only=false,
-  bool ignore_trivial=false,
-  const std::string &cover_inclue_pattern="");


A definite improvement.

martin-cs · 2017-12-15T23:20:40Z

src/goto-instrument/cover_filter.cpp

+
+Module: Coverage Instrumentation
+
+Author: Daniel Kroening


Again; cut and paste issue.

martin-cs · 2017-12-15T23:22:26Z

src/goto-instrument/cover_filter.cpp

+///  * Any declarations
+///  * At least 2 branches
+///  * At least 5 assignments
+/// \param identifier: a function name


Is this just an arbitrary choice or is there some deeper significance?

martin-cs · 2017-12-15T23:24:25Z

src/goto-instrument/cover_filter.cpp

+  const std::string &filename,
+  const irep_idt &mode)
+  : goal_filter_baset(message_handler)
+{


This seems pretty involved for a constructor.

martin-cs · 2017-12-15T23:25:40Z

src/goto-instrument/cover_filter.cpp

+  if(parse_json(filename, message_handler, json))
+  {
+    throw filename + " file is not a valid json file";
+  }


Would it be better to write the reasons to error()?

martin-cs · 2017-12-15T23:31:03Z

src/goto-instrument/cover_instrument_decision.cpp

+    }
+
+    for(std::size_t i = 0; i < decisions.size() * 2; i++)
+      i_it++;


What's this for?

peterschrammel · 2017-12-29T20:27:51Z

@smowton, @martin-cs, ready for re-review. I've rebased it on #1685.

smowton

Looks good, could improve clarity by factoring the is-non-coverage-assertion test.

Relatedly, is there ever a situation where assertion -> skip is a sensible thing to do? It seems like it would always lead to code being accessible with its preconditions unchecked leading to crazy behaviour, hence our always running assert-to-assume in the product. Should we perhaps issue a warning if there are somehow still live non-coverage assertions present? If I were writing this from scratch I'd recommend an invariant that there are no non-coverage assertions, but I guess that might break some existing user?

smowton · 2017-12-30T12:54:08Z

src/goto-instrument/cover_instrument_condition.cpp

+{
+  if(
+    i_it->is_assert() &&
+    i_it->source_location.get_property_class() != property_class)


At first reading I thought this would consider "location", "mcdc", and so on different classes, but it doesn't. Therefore suggest factoring this out into a function named is_non_coverage_assertion or something, and explain there that all coverage assertions are of the same class.

Factored out. I also don't think that there are many use cases where replacing assert by skip makes sense.

cover-function-only (instrumentating coverage goals in the entry point function only) is now implemented with the help of cover-include-pattern (regex matching of functions to be instrumented). This is to avoid potential consistencies due to providing two mechanisms for filtering functions. cover-function-only has priority over the given cover-include-pattern.

chrisr-diffblue

Looks good to me from my understanding of the code.

d190fd8 Merge remote-tracking branch 'upstream/develop' into pull-support-20180112 5bd5962 Merge pull request diffblue#1667 from romainbrenguier/feature/type_cast 8ecb55a Merge pull request diffblue#1717 from smowton/smowton/feature/remove_virtual_functions_per_function 0d7310a Merge pull request diffblue#1691 from romainbrenguier/bugfix/getClass#TG-1245 2064849 Use type_checked_cast in boolbv_width c5fc351 Validate data in pointer_typet in to_pointer_typet 35905c6 Add can_cast_type, validate_type for pointer_typet b72bacf Define type_try_dynamic_cast and type_checked_cast 23c3561 Unit test for string symbol resolution c13e602 Adding only needed equations in symbol resolution ae4deff Debug information for string equations 912828d JBMC: Run remove-virtual-functions as each function is converted a711c64 Introduce mechanism for renumbering an individual GOTO program e308a32 Merge pull request diffblue#1679 from NlightNFotis/nondet_extra_test e6ceb91 Merge pull request diffblue#1724 from tautschnig/fix-visitor ea74bed Add extra test for nondet-static flag and arrays 4f74896 Use irept API, not implementation-level API c55b4a5 Merge pull request diffblue#1682 from martin-cs/fix/dependence-graph-namespace-lifespan 1a2c14b Merge pull request diffblue#1722 from diffblue/unsafe_type_constructors 957a568 Merge pull request diffblue#1677 from NlightNFotis/pb4_develop 9c5add4 remove deprecated constructors for three bitvector types c96e02a no longer use deprecated constructors for some bitvector types 954060e Add unit test for has_subtype 3dd3877 Refactor has_char_pointer_subtype with has_subtype 4699c13 Extend symbol resolution to string_typet 74144fc Handle if_exprt in add_axioms_for_string_literal c6c1b3f Add an optional guard to add_axioms_for_constant 933d635 Merge pull request diffblue#1716 from mgudemann/fix/null_check_for_java_instanceof 1659314 Merge pull request diffblue#1715 from smowton/smowton/cleanup/jbmc_unused_passes 9c457b7 Add regression test for null instanceof. 2080cd3 Complete instanceof for Java. d4300d0 Merge pull request diffblue#1697 from diffblue/nondet_symbol_exprt 1c68dd4 Merge pull request diffblue#1714 from tautschnig/c-library-strcat 44b5bae Merge pull request diffblue#1698 from thomasspriggs/tg1633 c4304ba JBMC: Remove C-only passes bb8cfaa C library: Check upper bounds in memset, memcpy, memmove 7d4984f C library: Implement strcat, strncat 2a5cea2 This introduces nondet_symbol_exprt, which is generated by symbolic execution in response to side_effect_expr_nondett 85193a0 Merge pull request diffblue#1694 from NathanJPhillips/feature/add-raw-lhs-to-trace d9122dc Merge pull request diffblue#1710 from NathanJPhillips/feature/remove_instanceof_per_function 092df69 Switch from custom file / path routines to Boost-filesystem c8821b2 Allow to remove instanceof when remove exceptions 94b7658 Don't pass iterators into function calls a9c4e4f Added regression tests 76318ce Protect extended trace behind a command line option 69b0ff1 Added base_name in comments for all symbols e86080a Add raw LHS irep field to trace output ddd1b7a Add remove_instanceof overload to remove from a particular instruction 1c227b7 Merge pull request diffblue#1660 from smowton/smowton/fix/lazy_methods_array_parameters ae89c94 Lazy loading: assume concrete generic parameter types are needed 80eb6a6 TG-1877: Include array pointer types in needed classes 1053e5f Fix for [TG-1633] Inner generic types have incorrect type identifier e2cda1a Merge pull request diffblue#1704 from tautschnig/fix-copy-paste ef4a65e Fix op1/op0 copy&paste typo 21ea31f Merge pull request diffblue#1702 from peterschrammel/goto-diff-java c4bc953 Merge pull request diffblue#1701 from peterschrammel/allow-instrument-jdk 2811363 Java regression test for goto-diff 43d2e09 Also reset fresh temporary symbol counter 9ef28f4 Compare relative goto target offsets eaf3a7d Get source location from symbol table ab59659 Allow instrumentation of java.* and org.cprover.* 6fbd59c Merge pull request diffblue#1631 from tautschnig/fix-pointer-minus 7c04b5c Merge pull request diffblue#1699 from NathanJPhillips/feature/reset-main-in-tests 5e0f186 Pointer difference over void* is difference over char* faf8f00 Merge commit 'a83b52cddbed22304372c276512c63701eb3aedb' into pull-support-20180104 8236db4 Merge pull request diffblue#1419 from peterschrammel/refactor/cover-instrument a580e27 Merge pull request diffblue#1689 from smowton/smowton/feature/get_this 591511a Allow callers of load_java_class to pass the name of the main function 1b86b27 Merge pull request diffblue#1687 from smowton/smowton/feature/class-hierarchy-dot fd2bf6a Merge pull request diffblue#1688 from smowton/smowton/feature/parameter_indices f570ce5 Merge pull request diffblue#1696 from smowton/smowton/fix/identical_struct_equality 61b0d6d Merge pull request diffblue#1666 from mgudemann/bugfix/removed_required_virtual_calls 3365054 Add regression test 2b6dc8b Resolve concrete function call if no implementation is found 3f1fd64 Add code_typet::get_parameter_indices 42cf61a Fix testing for empty line in test desc file 2090000 Fix missing newline at end of desc file e448d5f Fix unsatisfiable test line f7f033d String smoke tests: ensure no type mismatches are seen b627c3d Replace unsound struct-cast simplification 8fa42b3 Class hierarchy: add DOT output, unit tests 04f2faf Mark GOTO instructions with unresolved virtual calls aac181f Pass command line options via optionst b6fa3e8 Factorize source location initialization 8da5395 Document cover functions a7f0c3d Introduce cover instrumenter 873627a Split cover into several files 0fc08f3 Replace cover-function-only by cover-include-pattern 1f2102c Add code_typet::get_this 2801f0f Avoid crashing when --dependence-graph is used by correcting namespace scoping. acac776 Add a test for the same-named static functions crashing dependence graph in the goto-analyser 05f46a9 Fix the problem where two static functions with the same name would cause the dependency graph to fail. git-subtree-dir: cbmc git-subtree-split: d190fd8

peterschrammel added the do not merge label Sep 24, 2017

peterschrammel force-pushed the refactor/cover-instrument branch 3 times, most recently from 5ab705d to f17599e Compare September 25, 2017 08:11

peterschrammel removed the do not merge label Sep 25, 2017

peterschrammel requested review from smowton and thk123 September 25, 2017 09:19

peterschrammel mentioned this pull request Sep 25, 2017

Update lib/cbmc to cbmc#1419 diffblue/symex#2

Closed

smowton suggested changes Sep 26, 2017

View reviewed changes

peterschrammel force-pushed the refactor/cover-instrument branch from f17599e to 04ae3b5 Compare September 26, 2017 18:13

peterschrammel force-pushed the refactor/cover-instrument branch from 04ae3b5 to ff0db6e Compare October 13, 2017 22:18

peterschrammel force-pushed the refactor/cover-instrument branch from ff0db6e to 69b3b84 Compare November 22, 2017 15:24

peterschrammel requested review from chrisr-diffblue, kroening, martin-cs and tautschnig as code owners November 22, 2017 15:24

tautschnig assigned peterschrammel Nov 30, 2017

peterschrammel force-pushed the refactor/cover-instrument branch from 69b3b84 to 30331eb Compare December 3, 2017 00:02

peterschrammel requested review from cesaro and mgudemann as code owners December 3, 2017 00:02

peterschrammel force-pushed the refactor/cover-instrument branch 4 times, most recently from 62c75c6 to 1a47697 Compare December 5, 2017 07:18

martin-cs reviewed Dec 15, 2017

View reviewed changes

peterschrammel force-pushed the refactor/cover-instrument branch 2 times, most recently from dde4c38 to 146aa51 Compare December 29, 2017 20:03

smowton approved these changes Dec 30, 2017

View reviewed changes

peterschrammel added 6 commits January 2, 2018 18:57

Split cover into several files

873627a

Introduce cover instrumenter

a7f0c3d

Document cover functions

8da5395

Factorize source location initialization

b6fa3e8

Pass command line options via optionst

aac181f

peterschrammel force-pushed the refactor/cover-instrument branch from 146aa51 to aac181f Compare January 2, 2018 18:27

chrisr-diffblue approved these changes Jan 3, 2018

View reviewed changes

peterschrammel merged commit 8236db4 into diffblue:develop Jan 5, 2018

peterschrammel deleted the refactor/cover-instrument branch January 5, 2018 12:30

peterschrammel mentioned this pull request Jan 5, 2018

Replace cover-function-only by cover-include-pattern #1348

Closed

smowton mentioned this pull request Jan 5, 2018

TG-1877: Include array pointer types in needed classes #1660

Merged

peterschrammel mentioned this pull request Jan 5, 2018

Allow coverage instrumentation of JDK methods #1701

Merged

peterschrammel mentioned this pull request Sep 11, 2018

Refactor coverage instrumentation #1315

Closed

1 task

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor coverage instrumentation #1419

Refactor coverage instrumentation #1419

peterschrammel commented Sep 24, 2017 •

edited

Loading

smowton left a comment

smowton Sep 26, 2017

smowton Sep 26, 2017

reuk Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

peterschrammel Oct 3, 2017

smowton Sep 26, 2017

tautschnig commented Nov 30, 2017

martin-cs left a comment

martin-cs Dec 15, 2017

peterschrammel Dec 29, 2017

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

peterschrammel commented Dec 29, 2017

smowton left a comment

smowton Dec 30, 2017

peterschrammel Jan 3, 2018

chrisr-diffblue left a comment

Refactor coverage instrumentation #1419

Refactor coverage instrumentation #1419

Conversation

peterschrammel commented Sep 24, 2017 • edited Loading

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Nov 30, 2017

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented Dec 29, 2017

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrisr-diffblue left a comment

Choose a reason for hiding this comment

peterschrammel commented Sep 24, 2017 •

edited

Loading