Maintain loop invariant annotation when converting do .. while #8417
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
requested review from
kroening,
peterschrammel and
remi-delmas-3000
as code owners
tautschnig
force-pushed
the
fix-do-while-loop-invariant
branch
from
bfd5e66 to
612191a
Compare
tautschnig
force-pushed
the
fix-do-while-loop-invariant
branch
2 times, most recently
from
60d7d4a to
88d2091
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8417 +/- ##
===========================================
- Coverage 77.93% 77.88% -0.05%
===========================================
Files 1726 1726
Lines 189657 189804 +147
Branches 18255 18234 -21
===========================================
+ Hits 147805 147826 +21
- Misses 41852 41978 +126 ☔ View full report in Codecov by Sentry. |
remi-delmas-3000
requested changes
Aug 20, 2024
| @@ -7,3 +7,4 @@ main.c | |||
| -- | |||
| -- | |||
| This test checks that loop contracts work correctly on do/while loops. | |||
| Fails because contracts are not yet supported on do while loops. | |||
There was a problem hiding this comment.
Contracts are supported on do-while thanks to latch normalization, here you need to fix the loop invariant to 0 <= x && x < 10
There was a problem hiding this comment.
Fixed for the dfcc variant.
remi-delmas-3000
approved these changes
Aug 20, 2024
With the changes in bbd9de4 we newly made do .. while converted instructions subject to `optimize_guarded_gotos`, which previously rewrote conditions without retaining annotations related to loop invariants. The included tests now show that the annotations are preserved, but still fail for an unrelated bug in how do .. while loops are instrumented.
The incoming edge from a `goto` instruction may also be the non-branching case, which must not result in redirecting this goto.
tautschnig
force-pushed
the
fix-do-while-loop-invariant
branch
from
88d2091 to
6009066
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
With the changes in bbd9de4 we newly made do .. while converted instructions subject to
optimize_guarded_gotos, which previously rewrote conditions without retaining annotations related to loop invariants.