-
Notifications
You must be signed in to change notification settings - Fork 271
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix failed coverage in if then else with return statements #8001
Fix failed coverage in if then else with return statements #8001
Conversation
When the parsed AST is transformed in GOTO language the if conditions are translated in: `if (!c) goto else; then_branch; goto endif; else: else_branch; endif: nop` and `if (!c) goto endif; then_branch; endif: nop`. This commit avoids to add the `goto endif` command and the `endif` label if the `then_branch` ends with a `return` or a `goto` statement. The benefit is that the `--cover location` command returns a more precise result as unreachable code blocks that are added by CBMC's frontend are not marked as unreachable.
This commit fixes the regression tests failing because of the optimization to the way `if` statements are translated to GOTO. Specifically it fixes - the expected result of `--cover location` in 2 `cbmc-cover` regression tests - the index of blocks in 3 regression tests from `cbmc` and `cprover`.
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## develop #8001 +/- ##
===========================================
+ Coverage 77.75% 77.92% +0.17%
===========================================
Files 1701 1701
Lines 196465 196468 +3
===========================================
+ Hits 152762 153101 +339
+ Misses 43703 43367 -336
☔ View full report in Codecov by Sentry. |
@kroening This PR involves some changes to a regression test of the Can you please have a look that the changes are ok? |
I am on the fence on this PR. It's of course true that the code after a |
@kroening I was on the fence as per my comments on #7974 C exampleint nondet_int();
int main() {
if (nondet_int())
return -1;
else if (nondet_int())
return -1;
else
return -1;
return 0;
} coverage output
In this example there is no closing This output also demonstrates that we are being inconsistent with how we are defining coverage. We have the helpful result in the case that the final return is unreachable (block 8). There are unhelpful goal results stating that the end of each "then true case" code block is unreachable (blocks 3 and 6). But we are missing the equivalent "unhelpful" result for the unreachable end of the "else false case" code block. Therefore the output appears to be inconsistent from a user/source perspective. I would agree with you that we should not be partially solving the reachability problem by performing dead code elimination as part of the coverage instrumentation for example. However the way we report coverage at the moment either requires additional manual interpretation of the coverage results or mismatched goal elimination by a post-processing tool. Either solution seems potentially error-prone to me. Therefore I think it would be beneficial if we could do better in terms of our coverage reporting, rather than deferring to solutions outside of cbmc. With regards to drawing the line between performing a full reachability analysis and improving the coverage output - I think I would currently draw the line at "we should not introduce dead code during during conversion which does not correspond to source language statements or source language branches". For a goal to really be useful it needs to map back to the source language in a way that makes sense. The change proposed in this PR gets us closer to that ideal in my opinion. With the way coverage instrumentation currently fits into the code base fixing this issue in the conversion is about as close as we can get to avoiding performing a reachability analysis to define reachability/coverage goals. The solution would look more like a reachability analysis the later we were to do it. There may be other ways the coverage analysis could be archectected in order to avoid issues like this one. But I don't see these longer term alternatives as a reason not to merge this PR, which is an improvement from a user perspective. To refer back to the example of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I believe this is an improvement in the right place. It might not be perfect, but it does improve our code generation.
// When the `then` branch of a balanced `if` condition ends with a `return` or | ||
// a `goto` statement, it is not necessary to add the `goto z` and `z:` goto | ||
// elements as they are never used. | ||
// This helps for example when using `--cover location` as such command are | ||
// marked unreachable, but are not part of the user-provided code to analyze. | ||
bool then_branch_returns = dest.instructions.rbegin()->is_goto(); | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit pick: I would suggest to move this block just after CHECK_RETURN(!tmp_w.instructions.empty());
and use tmp_w
instead of dest
.
Fixes #7974
Avoid adding useless goto blocks in
if
statements withreturn
statements.When the parsed AST is transformed in GOTO language the
if
statements are translated in:if (!c) goto else; then_branch; goto endif; else: else_branch; endif: nop
andif (!c) goto endif; then_branch; endif: nop
.This PR avoids to add the
goto endif
command and theendif
label if thethen_branch
already ends with areturn
or agoto
statement.