Reset unwinding counters when leaving a loop at the loop head #988
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
force-pushed
the
fix-unwind-count
branch
from
344c6c6 to
aedc5bf
Compare
peterschrammel
approved these changes
Jun 25, 2017
Member
peterschrammel
left a comment
peterschrammel
left a comment
There was a problem hiding this comment.
Wow, that's a major fix.
Collaborator
Author
I am yet to (re-)run SV-COMP experiments; I'd guess there could be some nested loops, which previously we have necessarily aborted way too early. |
tautschnig
force-pushed
the
fix-unwind-count
branch
from
aedc5bf to
64589b2
Compare
Constant propagation and simplification may determine that a loop cannot be unrolled further. This is determined at the loop head, which is a forward goto in case of for or while (but not do-while) loops. Before this patch, forward gotos would never cause loop counters to be reset. In nested loops, the inner loop(s) would thus have their unwinding counts added to previous (complete) loop executions.
tautschnig
force-pushed
the
fix-unwind-count
branch
from
64589b2 to
a4945f3
Compare
The previous approach would reset loop counters when reaching an unwinding bound, which was broken as shown by newly added regression tests.
Collaborator
Author
|
@kroening Please review whether this approach is as discussed and reasonable. I'll then clean up the commits and will remove the do-not-merge label. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
Constant propagation and simplification may determine that a loop cannot be
unrolled further. This is determined at the loop head, which is a forward goto
in case of for or while (but not do-while) loops. Before this patch, forward
gotos would never cause loop counters to be reset. In nested loops, the inner
loop(s) would thus have their unwinding counts added to previous (complete) loop
executions.