Rewrite never_loop
as a strict reachability pass
#11447
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #11004. This is a "more principled" rewrite of
never_loop
which does a proper reachability analysis ofcontinue 'main_loop
.IgnoreUntilEnd(label)
which had an unclear (and ultimately incorrect) relationship to reachability of labels and divergence, local label reachability is now being tracked once per label in thelocal_labels
list (previouslyignore_ids
)AlwaysBreak
andOtherwise
have been renamed toDiverging
andNormal
respectivelyMayContinueMainLoop
- this was the source of one of the bugs.The constant check from #11005 was removed, because it is no longer necessary to avoid the FP and it is necessarily quite approximate (it only checks for a literal
true
in the if statement, which would already be caught by another lint). Since we are using a sound underapproximation now, any if statement will simply be treated as if both branches are reachable, no matter the condition. This ensures no FPs at the cost of some FNs (which IIUC is the desired error direction). But we could put that check back in (or something like it) if desired.changelog: [
never_loop
]: Handles more edge cases involving labeled breaks