Define coverage blocks so as to be terminated by assumptions

[thomasspriggs]

If a coverage block has an assumption in the middle then then an assertion at the end of the block could be reported as covered but actually be unreachable due to the preceding the assumption. Therefore coverage blocks should be terminated by assumptions in order to ensure than coverage reporting is accurate.

Addresses #7806

• 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 (ac26185) 79.09%.
Report is 2 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7810   +/-   ##
========================================
  Coverage    79.09%   79.09%           
========================================
  Files         1701     1701           
  Lines       196625   196633    +8     
========================================
+ Hits        155527   155535    +8     
  Misses       41098    41098           

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

[remi-delmas-3000]

Hi @thomasspriggs ! If a goto-instrument pass adds assumptions in the middle of basic blocs, and the resulting model analysed with --cover locations, with the modification proposed in this PR would the basic blocks be split again in sub blocks before the cover analysis is executed ?

After running instrumentation passes we usually call goto_model::update() to update instruction numbers, jump targets, etc. But here goto_model::update() does not seem to be splitting basic blocks on assumptions.

[thomasspriggs]

Hi @thomasspriggs ! If a goto-instrument pass adds assumptions in the middle of basic blocs, and the resulting model analysed with --cover locations, with the modification proposed in this PR would the basic blocks be split again in sub blocks before the cover analysis is executed ?

My understanding is that a hand-written assumption would be treated by the coverage checking in the same way as an assumption added by a proceeding pass. However the various check passes add assertions rather than assumptions. Therefore my source comment on multiple assumptions from instrumentation may not be accurate and I should re-visit the comment.

After running instrumentation passes we usually call goto_model::update() to update instruction numbers, jump targets, etc. But here goto_model::update() does not seem to be splitting basic blocks on assumptions.

"basic blocks" as are defined for coverage instrumentation are held in a temporary data structure. This is generated at the start of the instrument_cover_goals pass and discarded when the pass is complete. Therefore goto_model::update() does cannot read or write to the basic blocks data structure. Though the generation of the basic blocks data structure may use information written to by goto_model::update() such as an instructions set of incoming_edges.

[thomasspriggs]

Hi @remi-delmas-3000

I have now run an example though this in order to confirm the behaviour. The assertions added by the instrumentation are converted to assumptions, which then become block boundaries.

Source C file

int main()
{
  int x;
  int y;
  y = x;
  x = x / 0;
  x = y;
  assert(0);
  return 0;
}

Testing commands

goto-cc ./instrumentation_example.c -o ./instrumentation_example.gb
goto-instrument --div-by-zero-check ./instrumentation_example.gb instrumentation_example_instrumented.gb
cbmc ./instrumentation_example_instrumented.gb --cover location

The current output from a --cover location run is -

cbmc output

CBMC version 5.89.0 (cbmc-5.89.0-11-gbcf6f4fd09) 64-bit x86_64 linux
Reading GOTO program from file ./instrumentation_example_instrumented.gb
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Rewriting existing assertions as assumptions
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
aborting path on assume(false) at file ./instrumentation_example.c line 7 function main thread 0: division by zero in x / 0
aborting path on assume(false) at file ./instrumentation_example.c line 9 function main thread 0: assertion 0
Runtime Symex: 0.000893022s
size of program expression: 21 steps
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.7022e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000219295s
Running propositional reduction
Post-processing
Runtime Post-process: 6.728e-06s
Solving with MiniSAT 2.2.1 with simplifier
64 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 6.332e-05s
Runtime decision procedure: 0.000336729s

** coverage results:
[main.coverage.1] file ./instrumentation_example.c line 4 function main block 1 (lines ./instrumentation_example.c:main:4-11): SATISFIED

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

With the changes proposed in this PR, the output is -

cbmc output

CBMC version 5.87.0 (cbmc-5.87.0-28-g4693734ea3) 64-bit x86_64 linux
Reading GOTO program from file ./instrumentation_example_instrumented.gb
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Rewriting existing assertions as assumptions
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
aborting path on assume(false) at file ./instrumentation_example.c line 7 function main thread 0: division by zero in x / 0
aborting path on assume(false) at file ./instrumentation_example.c line 9 function main thread 0: assertion 0
Runtime Symex: 0.000731948s
size of program expression: 21 steps
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.298e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000192357s
Running propositional reduction
Post-processing
Runtime Post-process: 6.111e-06s
Solving with MiniSAT 2.2.1 with simplifier
64 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 5.6264e-05s
Runtime decision procedure: 0.000291085s

** coverage results:
[main.coverage.1] file ./instrumentation_example.c line 4 function main block 1 (lines ./instrumentation_example.c:main:4-7): SATISFIED
[main.coverage.2] file ./instrumentation_example.c line 7 function main block 2 (lines ./instrumentation_example.c:main:7-9): FAILED
[main.coverage.3] file ./instrumentation_example.c line 10 function main block 3 (lines ./instrumentation_example.c:main:10,11): FAILED

** 1 of 3 covered (33.3%)
** Used 2 iterations

So the old output misleadingly suggests that all lines are reachable due to the single coverage block. With the update there are 3 blocks which are the result of splitting based on the instrumentation check and the user assertion.

Do the changes in this PR resolve #7806 or is something different required?

[remi-delmas-3000]

Do the changes in this PR resolve #7806 or is something different required?

This works for #7806

[tautschnig]

It seems this is the correct route forward, just needs tests.

[martin-cs]

Does not seem unreasonable

[kroening]

I doubt that the line number check meets the intent of #7806. I'd drop it.

[thomasspriggs]

I doubt that the line number check meets the intent of #7806. I'd drop it.

The alternative code which causes every assumption to be placed in a new block was ifdef'd out with a comment that it is "Disabled for being too messy". Indeed I tried this version and found that it introduced many new blocks due to check instrumentations adding multiple assertions which become assumptions before coverage checking. Many of these will be on the same source line of code. My reasoning is effectively that assume(a); assume(b); is equivalent to assume(a && b); therefore it is reasonable to include sets of assumptions in the same block in the case of multiple assumptions from check instrumentation. The same_source_line check in my implementation is an approximate attempt to avoid combining user assertions/assumptions from separate lines together, whilst still combining the check assumptions.

Are you suggesting that I remove the line number check from my implementation such that user assertions/assumptions from separate lines of code are combined together resulting in fewer blocks? Or are you asking for the version which is ifdef'd out which result in many more blocks?

#7806 was raised by @remi-delmas-3000 who has confirmed that this PR as it currently stands works for the issue.

[kroening]

More blocks. I'd keep in mind that the reader of the output is likely a tool.

[thomasspriggs]

Given that this PR is approved, I am going to merge it. If we want more blocks, then this alternative PR can be rebased on top of develop instead - #7944