Define coverage blocks so as to be terminated by all assumptions

[thomasspriggs]

This PR is a variation on #7810 which is raised in response to this comment here - #7810 (comment)

I have kept these changes as a separate PR/branch for the moment as they are functionally different from the ones which have been previously been approved and I would like confirmation from @remi-delmas-3000 before we continue with the approach in this PR.

The key difference between this PR and the original PR is that the original PR will produce a single block for the case where there are multiple consecutive assumptions which map to the same source line. Kind of like a transformation from assume(a); assume(b); to assume(a && b);. This PR will create a coverage block for each of the assumptions. This tends to be the case where we add assertions during instrumentation passes, which become assumptions for the purposes of coverage checks.

The drawback with the presence of multiple coverage blocks on the same line of code is that the coverage reporting only reports at a granularity of source lines rather than goto instructions. This can make the output appear somewhat odd. Only source lines are included in the output regardless of whether we are using the default plain text UI or --xml-ui or --json-ui. To illustrate this issue I have taken one of the examples from our test suite and run it against develop, my first PR and this PR.

C source

#include <stdlib.h>

int main()
{
  int *ptr = malloc(sizeof(*ptr));
  int a;

  // pointer check would detect the dereference of a null pointer here
  // default --cover lines behaviour is to treat non-cover assertions as
  // assumptions instead, so in the ptr == NULL case we don't get past this line
  // leading to failed coverage for the body of the if statement down below
  a = *ptr;

  if(ptr == NULL)
    a = 1;

  return 0;
}

For this example we run cbmc test.c --cover location --pointer-check --malloc-may-fail --malloc-fail-null

Coverage reporting on develop.

** coverage results:
[main.coverage.1] file test.c line 5 function main block 1 (lines test.c:main:5): SATISFIED
[main.coverage.2] file test.c line 5 function main block 2 (lines test.c:main:5,6,12,14): SATISFIED
[main.coverage.3] file test.c line 15 function main block 3 (lines test.c:main:15): FAILED
[main.coverage.4] file test.c line 17 function main block 4 (lines test.c:main:17,18): SATISFIED

** 3 of 4 covered (75.0%)
** Used 2 iterations

The above results combine lines 12 and 14 in the same block, even though line 14 would be unreachable if the instrumentation assertions could not be satisfied. This demonstrates the problem from original issue.

Coverage reporting from https://github.com//pull/7810

** coverage results:
[main.coverage.1] file test.c line 5 function main block 1 (lines test.c:main:5): SATISFIED
[main.coverage.2] file test.c line 5 function main block 2 (lines test.c:main:5,6,12): SATISFIED
[main.coverage.3] file test.c line 12 function main block 3 (lines test.c:main:12,14): SATISFIED
[main.coverage.4] file test.c line 15 function main block 4 (lines test.c:main:15): FAILED
[main.coverage.5] file test.c line 17 function main block 5 (lines test.c:main:17,18): SATISFIED

The above coverage output includes an additional block for line 14. This is correctly shown as SATISFIED / reachable as the conditions added by the instrumentation can be satisfied in this case.

Coverage reporting from this PR

** coverage results:
[main.coverage.1] file test.c line 5 function main block 1 (lines test.c:main:5): SATISFIED
[main.coverage.2] file test.c line 5 function main block 2 (lines test.c:main:5,6,12): SATISFIED
[main.coverage.3] file test.c line 12 function main block 3 (lines test.c:main:12): SATISFIED
[main.coverage.4] file test.c line 12 function main block 4 (lines test.c:main:12): SATISFIED
[main.coverage.5] file test.c line 12 function main block 5 (lines test.c:main:12): SATISFIED
[main.coverage.6] file test.c line 12 function main block 6 (lines test.c:main:12): SATISFIED
[main.coverage.7] file test.c line 12 function main block 7 (lines test.c:main:12): SATISFIED
[main.coverage.8] file test.c line 12 function main block 8 (lines test.c:main:12,14): SATISFIED
[main.coverage.9] file test.c line 15 function main block 9 (lines test.c:main:15): FAILED
[main.coverage.10] file test.c line 17 function main block 10 (lines test.c:main:17,18): SATISFIED

The coverage output now shows 5 blocks which each cover line 12 alone. In this example they aren't too difficult to consolidate. However it is conceivable that some of them could report as SATISFIED with others for the same line showing as FAILED. This could occur in the case where the first check is satisifyable but one of the following checks is not.

• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (d01fa33) 79.09% compared to head (e6c4e19) 79.09%.
Report is 2 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7944   +/-   ##
========================================
  Coverage    79.09%   79.09%           
========================================
  Files         1701     1701           
  Lines       196625   196625           
========================================
  Hits        155527   155527           
  Misses       41098    41098           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[thomasspriggs]

@remi-delmas-3000 Please could you try out the changes in this PR and co-ordinate with @kroening to work out whether it is better to proceed with this PR, or with #7810 ?

[thomasspriggs]

I am now closing this out as I don't expect to have time available to take this further forwards.