Implement natural loop rotation/canonicalization in GOTO programs

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

Problem description

Let us consider a natural loop and the sequence of its instructions in the order in which they appear in the goto program.

The problem is that the sequence of loop instructions not necessarily densely packed in the goto program instruction sequence, meaning, the span of instructions between the first and the last loop instruction can contain instructions that are not part of the loop (typically, code that is only run once when breaking out of the loop)

This makes it difficult to apply loop transformations (in particular assigns clause instrumentation and loop contracts transformations), because these foreign instructions need to be preserved in the transformed loop.

LLVM loop canonicalisation could be a source of inspiration. loop canonicalisation ensures that loop instruction sequences are densely packed in the program's instruction sequence and that the loop has a single entry point and single exit point. The body of the loop can be swapped as a block, and code that needs to be hoisted out of the loop can safely be moved either to the single loop entry or the single loop exit location.

https://llvm.org/docs/LoopTerminology.html
https://llvm.org/devmtg/2009-10/ScalarEvolutionAndLoopOptimization.pdf
https://llvm.org/devmtg/2018-10/slides/Kruse-LoopTransforms.pdf

[feliperodri]

It would greatly simplify our work on contracts.

[TGWDB]

@diffblue/diffblue-opensource This tag might work where we cannot "assign" this to the Team.

[tautschnig]

Just a note that #7321 might partially take care of this.

[thomasspriggs]

I am scheduled to look at this issue once I finish my currently assigned task.

[thomasspriggs]

This relates to #7518

My team has re-prioritised some of the work. I now have other documentation to write first.