Omitting property checking flags changes coverage checking

[markrtuttle]

CBMC version: 5.17.0 (cbmc-5.17.0-12-ga46f12d66
Operating system: Ubuntu 20
Exact command line resulting in the issue: see below
What behaviour did you expect: see below
What happened instead: see below

Summary

My coverage checking results are affected by whether or not I include property checking flags on the command line.

I had been in the habit of doing property checking with flags like --pointer-check, and doing coverage checking with the same set of flags. I was advised that I could accelerate coverage checking by omitting the property checking flags when I'm doing coverage checking. But omitting the flags changes the coverage results.

Decreased coverage

Omitting property checking flags when doing coverage checking results in lower coverage (lower percentage of lines hit).

Consider the attached file example2.c containing

#include <stdlib.h>

int foo(int x, int y) { return x; }

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

  foo(1,
      *ptr);

  if (0) {
    *ptr = 0;
  }

  return 0;
}

My results are

cbmc example2.c --cover location --malloc-may-fail --malloc-fail-null --pointer-check

** coverage results:
[foo.coverage.1] file example2.c line 3 function foo block 1 (lines example2.c:foo:3): SATISFIED
[main.coverage.5] file example2.c line 15 function main block 5 (lines example2.c:main:15,16): SATISFIED
[main.coverage.4] file example2.c line 12 function main block 4 (lines example2.c:main:12): FAILED
[main.coverage.3] file example2.c line 11 function main block 3 (lines example2.c:main:11): SATISFIED
[main.coverage.2] file example2.c line 6 function main block 2 (lines example2.c:main:6,8,9): SATISFIED
[main.coverage.1] file example2.c line 6 function main block 1 (lines example2.c:main:6): SATISFIED

and

cbmc example2.c --cover location --malloc-may-fail --malloc-fail-null

** coverage results:
[foo.coverage.1] file example2.c line 3 function foo block 1 (lines example2.c:foo:3): SATISFIED
[main.coverage.5] file example2.c line 15 function main block 5 (lines example2.c:main:15,16): SATISFIED
[main.coverage.4] file example2.c line 12 function main block 4 (lines example2.c:main:12): FAILED
[main.coverage.3] file example2.c line 11 function main block 3 (lines example2.c:main:11): SATISFIED
[main.coverage.2] file example2.c line 6 function main block 2 (lines example2.c:main:6,8): SATISFIED
[main.coverage.1] file example2.c line 6 function main block 1 (lines example2.c:main:6): SATISFIED

The differences are the lines

[main.coverage.2] file example2.c line 6 function main block 2 (lines example2.c:main:6,8,9): SATISFIED
[main.coverage.2] file example2.c line 6 function main block 2 (lines example2.c:main:6,8): SATISFIED

and the missing line 9 is the second argument *ptr to the invocation of foo.

• With pointer check (the first case), I get 1 line missed (line 12) and 8 lines hit (lines 3, 6, 8, 9, 11, 12, 15, 16) or 8/9 coverage.
• Without pointer check, I get 1 line missed (line 12) and 7 lines hit (lines 3, 6, 8, 11, 12, 15, 16) or 7/8 coverage.

So omitting property checking flags when doing coverage checking results in lower coverage (percent of lines hit).

Incorrect coverage

Including property checking flags when doing coverage changes coverage results.

Consider the attached file example1.c containing

#include <stdlib.h>

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

  a = *ptr;

  if (ptr == NULL)
    a = 1;

  return 0;
}

My results are

cbmc example1.c --cover location --malloc-may-fail --malloc-fail-null

** coverage results:
[main.coverage.4] file example1.c line 12 function main block 4 (lines example1.c:main:12,13): SATISFIED
[main.coverage.3] file example1.c line 10 function main block 3 (lines example1.c:main:10): SATISFIED
[main.coverage.2] file example1.c line 4 function main block 2 (lines example1.c:main:4,5,7,9): SATISFIED
[main.coverage.1] file example1.c line 4 function main block 1 (lines example1.c:main:4): SATISFIED

and

cbmc example1.c --cover location --malloc-may-fail --malloc-fail-null --pointer-check

** coverage results:
[main.coverage.4] file example1.c line 12 function main block 4 (lines example1.c:main:12,13): SATISFIED
[main.coverage.3] file example1.c line 10 function main block 3 (lines example1.c:main:10): FAILED
[main.coverage.2] file example1.c line 4 function main block 2 (lines example1.c:main:4,5,7,9): SATISFIED
[main.coverage.1] file example1.c line 4 function main block 1 (lines example1.c:main:4): SATISFIED

The results differ only in line 10 which is a = 1;. Without pointer checking the line is considered hit and with pointer checking the line is considered missed.

[danielsn]

For the second case, we have UB at the line a = *ptr; if ptr == null. So I'm not surprised that we don't see the then case of the conditional.

[thomasspriggs]

For your first case example2.c, the line coverage is the same in terms of our analysis either with or without --pointer-check. The issue is to do with the reporting of the coverage. The whole of the call to the foo function including the dereference of ptr is included in block 2, regardless of whether --pointer-check is specified or not. The reporting was including the line where a multiple line statement begins only. The additional checks we add for --pointer-check were just "nudging" the reporting into correctly including the extra line number.

I have now merged PR#5635 which will cause all lines of a multiple line statement to be included in the reporting. This will mean that running cbmc both with and without --pointer-check will now show lines 6,8 and 9 as being covered in this example.

@hannes-steffenhagen-diffblue and @NlightNFotis are currently looking into your second case, example1.c.

[hannes-steffenhagen-diffblue]

As to your second issue: The coverage here is changing because the default behavior is that in coverage assertions are turned into assumptions – including the ones added by the various checks. So as @danielsn correctly guessed, the problem here is that the dereference would be an error in the null case, which is caught by pointer-check so there's no coverage afterwards. This is usually the expected behaviour when analysing regular programs where assertion failure means that the program should be terminated, so anything aftwards ceases being reachable. If you want to just check which assertions can be hit the easiest way to do that is via --cover assertion.

If you do want line coverage for lines that are guarded by failing assertions, that currently doesn’t seem to be possible but I’ve added PR #5636 to address this, which will add a flag to change the behaviour for that instead.

[hannes-steffenhagen-diffblue]

@markrtuttle I have added the --cover-failed-assertions flag, when passed with --cover locations it will prevent assertions from affecting coverage.

[feliperodri]

@markrtuttle @hannes-steffenhagen-diffblue any updates on this issue? Should we close it?

[hannes-steffenhagen-diffblue]

@markrtuttle From our perspective it doesn't seem like there's anything left to do. Let us know if you're having a related issue.