Rewrite loops with multiple back edges to having a single back edge only#1117
Rewrite loops with multiple back edges to having a single back edge only#1117danielsn merged 1 commit intomodel-checking:mainfrom
Conversation
There was a problem hiding this comment.
Discussed with @tautschnig. This rewrite has no known soundness issues. The only relevent effect is that it affects how CBMC counts loop unwindings, which is what was causing the test failure.
Interesting, do we have any idea when that's the case? It doesn't seem to affect all loop unwinding. BTW, I don't see this option documented anywhere in their public documents or Is this transformation pass similar to LoopSimplify in LLVM? |
|
I believe its cases where the final statement of the loop body is an |
rustc reasonably translates if statements at end of a loop body to backwards jumps to the loop head. This, however, causes CBMC's symbolic execution to spuriously treat these as nested loops. This commit now enables a rewrite step that had previously been built for exactly such cases. This treatment as nested loops implied that seemingly lower unwinding bounds were sufficient (as the loop unwinding counter got reset). Three of the tests exhibited this behaviour, which now makes larger unwinding bounds necessary. Fixes: model-checking#1046 Co-authored-by: Daniel Schwartz-Narbonne <dsn@amazon.com>
It was really only a problem when there were multiple back-edges in a loop. This is entirely reasonable for a compiler to generate, but it catches CBMC's symbolic execution off guard for CBMC's C front-end (and goto conversion) will never generate this. (The choice is for what to do with
I'm pretty sure it just was forgotten about when it was built. Presumably it was built to deal with code originating from
It's not quite as elaborate, it does only one part of it, the "This pass also guarantees that loops will have exactly one backedge." |
|
Added #1046 to "Resolved issues". |
This is a re-creation of #900 after the Kani history rewrite. I can't force-push to that branch to do the rebase, so I'm just recreating it.
Description of changes:
rustc reasonably translates if statements at end of a loop body to
backwards jumps to the loop head. This, however, causes CBMC's symbolic
execution to spuriously treat these as nested loops. This commit now
enables a rewrite step that had previously been built for exactly such
cases.
Resolved issues:
Resolves #1046
Call-outs:
Testing:
How is this change tested?
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.