Rewrite loops with multiple back edges to having a single back edge only

[tedinski]

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

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[danielsn]

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.

[celinval]

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 goto-instrument --help. Do we know why that's not customer visible? @tautschnig

Is this transformation pass similar to LoopSimplify in LLVM?

[danielsn]

I believe its cases where the final statement of the loop body is an if with no matching else: CBMC was previously misidentifying them as nested loops, instead of as a single loop with multiple back-edges

[tautschnig]

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.

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 continue instructions: a compiler could either choose to generate a jump to the backwards goto at the end of a loop, or directly jump back to the loop head. CBMC's goto conversion does the former, but apparently rustc at least sometimes does the latter. And presumably javac also does the latter at times.)

BTW, I don't see this option documented anywhere in their public documents or goto-instrument --help. Do we know why that's not customer visible? @tautschnig

I'm pretty sure it just was forgotten about when it was built. Presumably it was built to deal with code originating from javac. We should fix the documentation problem, but there already is an item on my todo list to include automated checks in CI that all options are documented (unless intentionally left undocumented). So I'll get to this eventually...

Is this transformation pass similar to LoopSimplify in LLVM?

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."

[adpaco-aws]

Added #1046 to "Resolved issues".