Incorrect location coverage results in the presence of assumptions

[remi-delmas-3000]

Hi,

we have encountered a problem with the way coverage information is reported for --cover location in the presence of assumptions.

Consider this program:

int main() {
  int i;
  int j;
  j = i;
  __CPROVER_assume(j != i);
  j = i + 2;
  assert(j%2 == 0);
  return 0;
}

It compiles down to a single GOTO basic block that has an assumption in the middle.

The name of the switch--cover location makes it seem like it should produces location coverage information.

In reality it instruments each block with a reachability assertion and extrapolates block reachability to all instructions of the block, and their corresponding source lines.

On this program it makes it look like all locations are reachable:

** coverage results:
[main.coverage.1] file cover_assume.c line 2 function main block 1 (lines cover_assume.c:main:2-9): SATISFIED

** 1 of 1 covered (100.0%)
** Used 2 iterations

The problem is that an assumption can introduce a contradiction which can make subsequent instructions unreachable (lines 6-9) (the path constraint is infeasible).

To derive proper location coverage from block coverage, assumptions should be treated as delimiting the end of a basic block, since progress can stop if the assumption introduces a contradiction.

Correct location coverage results would then look like this:

** coverage results:
[main.coverage.1] file cover_assume.c line 2 function main block 1 (lines cover_assume.c:main:2-5): SATISFIED
[main.coverage.2] file cover_assume.c line 6 function main block 2 (lines cover_assume.c:main:6-9): FAILED

** 1 of 2 covered (50.0%)

I'm also suggesting to rename the option --cover basic_block to avoid the confusion with location/line coverage.

CBMC version: 5.87.0
Operating system: all
Exact command line resulting in the issue: cbmc --cover location
What behaviour did you expect: some locations in this program are not reachable
What happened instead: all locations are reported as reachable

[remi-delmas-3000]

Remark: rewriting assumptions from assume(c); to if (!c) assume(0); forces the creation of a basic block and kind of sidesteps the problem:

int main() {
  int i;
  int j;
  j = i;
  if(j == i) __CPROVER_assume(0);
  j = i + 2;
  assert(j % 2 == 0);
  return 0;
}

** coverage results:
[main.coverage.1] file cover_assume.c line 2 function main block 1 (lines cover_assume.c:main:2-5): SATISFIED
[main.coverage.2] file cover_assume.c line 5 function main block 2 (lines cover_assume.c:main:5): SATISFIED
[main.coverage.3] file cover_assume.c line 6 function main block 3 (lines cover_assume.c:main:6-9): FAILED

** 2 of 3 covered (66.7%)
** Used 2 iterations

But extrapolating block reachability to location reachability in the presence of assumptions is still basically unsound.

[thomasspriggs]

Just a quick comment to re-iterate what was said in our meeting this afternoon - We can resolve your immediate problems by adding a new coverage option to insert the kind of coverage instrumentation which you are looking for. In doing so we can leave the existing coverage options as is in order to avoid creating compatibly issues or surprise changes in behaviour for users of the existing options.

[thomasspriggs]

@remi-delmas-3000 Are you aware of the existing --cover assume option? Taking your original example as input, the output is -

** coverage results:
[main.coverage.1] file ./cover_assume.c line 5 function main assert(false) before assume(j != i): SATISFIED
[main.coverage.2] file ./cover_assume.c line 5 function main assert(false) after assume(j != i): FAILED

** 1 of 2 covered (50.0%)
** Used 2 iterations

I am aware that this doesn't necessarily fit your exact needs, but it seems to be half way there.

I am thinking that if we add something along the line of a --cover assume-blocks option which combines the coverage goals from --cover location with the after assumption goals of --cover assume then that would fit your needs.

[remi-delmas-3000]

Hi @thomasspriggs Indeed, by adding reachability assertions at block enty and after every assumption you could derive proper location coverage within a block without having to split the block.

However I really think that fixing --cover location itself is the way to go since in the worst case it prevents the detection of a vacuous proof. Existing users that do not have contradictory assumptions in their models should see no difference in coverage, and I am sure users that do have them would be happy to know about it.

[thomasspriggs]

Hi @remi-delmas-3000 I have begun working on implementing a fix for this issue. Here is a progress update. There is an '#ifdef`'d out option for terminating coverage blocks on the assume instructions in goto programs here - https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/cover_basic_blocks.cpp#L76-L81

However the results of flipping this are not quite what you might expect. When performing coverage checks the assertions are replaced with assumptions. So if the various coverage checks are enabled, the combined result is multiple coverage goals for same line of code. I will be looking at options for avoiding this somewhat counter intuitive result next.

[thomasspriggs]

@remi-delmas-3000 Could you try out the changes in the linked PR?

[thomasspriggs]

I have merged this PR - #7810
Merging the PR should resolve this issue. Feel free to re-open if it is still a problem.