Added basic block source lines to source_locationt #3967

tautschnig · 2019-01-27T18:56:07Z

This is a rebased version of #1439.

Block coverage obtained with "cbmc --cover locations" now reports the file name
and line number of every line of source code contributing to a basic block in
the "description" field of the xml output. (The lines contributing to a block
can come from multiple files via function inlining and definitions in include
files, so reporting line numbers alone is not sufficient.)

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

martin-cs

Seems reasonable. I wonder if @peterschrammel or whoever is in charge of Diffblue's test case generator wants to comment as this seems like the kind of thing that would change their output.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 31727ed).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98753027

smowton · 2019-01-28T15:43:36Z

src/goto-instrument/source_lines.cpp

+{
+  if(loc.get_file().empty() || loc.is_built_in())
+    return;
+  std::string file = id2string(loc.get_file());


Indeed, done.

smowton · 2019-01-28T15:43:41Z

src/goto-instrument/source_lines.cpp

+  std::string file = id2string(loc.get_file());
+
+  // the function of a source location can fail to be set
+  std::string func = id2string(loc.get_function());


peterschrammel · 2019-01-28T22:59:32Z

regression/cbmc-cover/block-coverage-report2/test.desc

+block 5 \(lines main.c:main:20\): SATISFIED
+block 6 \(lines main.c:main:15,21,22\): SATISFIED
+block 7 \(lines main.c:main:24,25\): SATISFIED
+block 1 \(lines main.c:foo:6,7,8,9\): SATISFIED


Suggest to use util/format_number_range for a more compact representation

Yes, we should do that. As Mark explained in #1439 we have a tool (to be open sourced) that uses this information, so I'll first make sure it can cope with both the explicit enumeration as well as the ranges.

In practice, blocks are so small it makes almost no difference.

But the essential thing is to continue listing filename-numberset pairs, because the lines contributing to a block can come from more than one file.

That should be preserved, yes. The only change (and really the only change that was necessary to the regression tests) is that instead of 6,7,8,9 we now print 6-9.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: b70f696).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99099532
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: b3209a0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99113365

tautschnig · 2019-02-04T00:39:22Z

Marking do-not-merge: I would like to ask for explicit approval that this doesn't break TG (as this PR changes the output) and also I need to co-ordinate the merge on our end.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: b1a2804).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99575601

tautschnig · 2019-02-04T16:49:58Z

Thanks @jeannielynnmoulton! This PR is now rebased.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 77ae56c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99673839
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: a51d007).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99704188

jeannielynnmoulton · 2019-02-07T10:25:05Z

@tautschnig I've had to update some tests on test-gen for this change, but it doesn't seem to break anything. The one curious thing that I see is that some lines are blank like this:

[java::Test.privateStatic:(I)I.coverage.1] file Test.java line 28 function java::Test.privateStatic:(I)I bytecode-index 1 block 1 (lines ): SATISFIED

Is this expected?

jeannielynnmoulton · 2019-02-07T13:23:55Z

Bump passes. It would be good to get an answer to the above question before this is merged though.

tautschnig · 2019-02-07T13:31:02Z

Thanks @jeannielynnmoulton - I'll look into this, it is reproducible on one of the regression tests.

tautschnig · 2019-02-07T19:37:49Z

@jeannielynnmoulton Thank you very much for not letting me be lazy - I have now added code to cover_basic_blocks_javat to actually hold the desired info, not just the non-Java one... May I ask you to do another test run as the output should now be non-empty? (It certainly is non-empty in the jdiff test included in the repository.)

Block coverage obtained with "cbmc --cover locations" now reports the file name and line number of every line of source code contributing to a basic block in the "description" field of the xml output. (The lines contributing to a block can come from multiple files via function inlining and definitions in include files, so reporting line numbers alone is not sufficient.)

jeannielynnmoulton · 2019-02-08T10:29:20Z

@tautschnig Seems to be non-empty now. [java::Test.privateStatic:(I)I.coverage.1] file Test.java line 28 function java::Test.privateStatic:(I)I bytecode-index 1 block 1 (lines Test.java:java::Test.privateStatic:(I)I:28): SATISFIED

tautschnig · 2019-02-08T10:33:59Z

@jeannielynnmoulton Many thanks for confirming! Does it still pass TG tests, or should I hold back on merging this one (once Travis has settled)?

jeannielynnmoulton · 2019-02-08T10:38:33Z

I'm updating the tests to be more specific so we don't have the blank lines regression. I'll run CI one more time to be safe and let you know when it's safe to merge. (Sorry about closing the PR accidentally, my laptop track pad is so sensitive)

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 01f4ee2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100217199

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 01f4ee2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100219604

jeannielynnmoulton · 2019-02-08T13:19:04Z

@tautschnig Bump passed!

tautschnig requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli and smowton as code owners January 27, 2019 18:56

tautschnig mentioned this pull request Jan 27, 2019

Block coverage now reports all source code lines contributing to a ba… #1439

Closed

tautschnig force-pushed the 1439-rebased branch from 0512088 to ee35009 Compare January 27, 2019 19:39

martin-cs approved these changes Jan 27, 2019

View reviewed changes

tautschnig force-pushed the 1439-rebased branch from ee35009 to 31727ed Compare January 27, 2019 22:52

tautschnig requested review from cesaro and cristina-david as code owners January 27, 2019 22:52

allredj reviewed Jan 28, 2019

View reviewed changes

tautschnig assigned peterschrammel Jan 28, 2019

smowton approved these changes Jan 28, 2019

View reviewed changes

tautschnig force-pushed the 1439-rebased branch from 31727ed to e92a5c6 Compare January 28, 2019 16:20

peterschrammel reviewed Jan 28, 2019

View reviewed changes

tautschnig self-assigned this Jan 29, 2019

tautschnig force-pushed the 1439-rebased branch from e92a5c6 to b70f696 Compare January 30, 2019 09:17

tautschnig removed their assignment Jan 30, 2019

allredj reviewed Jan 30, 2019

View reviewed changes

tautschnig force-pushed the 1439-rebased branch from b70f696 to b3209a0 Compare January 30, 2019 11:16

allredj reviewed Jan 30, 2019

View reviewed changes

peterschrammel approved these changes Feb 3, 2019

View reviewed changes

peterschrammel assigned tautschnig and unassigned peterschrammel Feb 3, 2019

tautschnig added the do not merge label Feb 4, 2019

tautschnig force-pushed the 1439-rebased branch from b3209a0 to b1a2804 Compare February 4, 2019 00:40

allredj reviewed Feb 4, 2019

View reviewed changes

tautschnig force-pushed the 1439-rebased branch from b1a2804 to 77ae56c Compare February 4, 2019 16:49

allredj reviewed Feb 4, 2019

View reviewed changes

tautschnig force-pushed the 1439-rebased branch from 77ae56c to a51d007 Compare February 4, 2019 22:35

allredj reviewed Feb 4, 2019

View reviewed changes

tautschnig assigned tautschnig and unassigned jeannielynnmoulton Feb 7, 2019

tautschnig removed the do not merge label Feb 7, 2019

tautschnig force-pushed the 1439-rebased branch from a51d007 to 4707ed5 Compare February 7, 2019 19:35

tautschnig assigned jeannielynnmoulton and unassigned tautschnig Feb 7, 2019

tautschnig added the do not merge label Feb 7, 2019

tautschnig force-pushed the 1439-rebased branch from 4707ed5 to 01f4ee2 Compare February 7, 2019 20:45

tautschnig requested review from danpoe and hannes-steffenhagen-diffblue as code owners February 7, 2019 20:45

jeannielynnmoulton closed this Feb 8, 2019

jeannielynnmoulton reopened this Feb 8, 2019

allredj reviewed Feb 8, 2019

View reviewed changes

tautschnig merged commit cdaeb50 into diffblue:develop Feb 8, 2019

tautschnig deleted the 1439-rebased branch February 8, 2019 13:57

Added basic block source lines to source_locationt #3967

Added basic block source lines to source_locationt #3967

Uh oh!

Conversation

tautschnig commented Jan 27, 2019

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 4, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 4, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

jeannielynnmoulton commented Feb 7, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jeannielynnmoulton commented Feb 7, 2019

Uh oh!

tautschnig commented Feb 7, 2019

Uh oh!

tautschnig commented Feb 7, 2019

Uh oh!

jeannielynnmoulton commented Feb 8, 2019

Uh oh!

tautschnig commented Feb 8, 2019

Uh oh!

jeannielynnmoulton commented Feb 8, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

jeannielynnmoulton commented Feb 8, 2019

Uh oh!

Uh oh!

jeannielynnmoulton commented Feb 7, 2019 •

edited

Loading

jeannielynnmoulton commented Feb 8, 2019 •

edited

Loading