We've found a serious issue with the current implementation of loop predication. The current implementation relies on SCEV and this turned out to be problematic. To fix the problem we had to rework the pass substantially. We have had the reworked implementation in our downstream tree for a while. This is the initial patch of the series of changes to upstream the new implementation.

The problem.

Consider the loop:

for (int i = b; i != e; i++) guard(i u< len)

The current implementation will ask SCEV if the guard condition is monotonic and if it is will replace the IV in the condition with the value of the IV at the end of the loop. In this loop the increment will be marked as nuw because of the guard. Basing on that SCEV will mark the corresponding add recurrence as nuw, which makes the guard condition monotonic. So, loop predication replaces the guard condition with e <u len condition. This transformation is not correct, for example, the loop is now broken for b = 5, e = 4.

Generally the facts SCEV provides are true if the backedge of the loop is taken, which implicitly assumes that the guard doesn't fail. Using these facts to optimize the guard results in a circular logic where the guard is optimized under the assumption that it never fails.

The fix.

An alternative way to reason about loop predication is to use an inductive proof

approach. Given the loop:

if (B(S)) { do { I = PHI(S, I.INC) I.INC = I + S guard(G(I)); } while (B(I.INC)); }

where B(x) and G(x) are predicates that map integers to booleans, we want a

loop invariant expression M such the following program has the same semantics

as the above:

if (B(S)) { do { I = PHI(S, I.INC) I.INC = I + S guard(G(S) && M); } while (B(I.INC)); }

One solution for M is `M = forall X . (G(X) && B(X + S)) => G(X + S)`

For now the transformation is limited to the following case:

- The loop has a single latch with either ult or slt icmp condition.
- The step of the IV used in the latch condition is 1.
- The IV of the latch condition is the same as the post increment IV of the guard condition.
- The guard condition is ult.

In this case the latch is of the from:

`++i u< latchLimit or ++i s< latchLimit`

and the guard is of the form:

`i u< guardLimit`

For the unsigned latch comparison case M is:

`forall X . X u< guardLimit && (X + 1) u< latchLimit => (X + 1) u< guardLimit`

This is true if `latchLimit u<= guardLimit` since then

`(X + 1) u< latchLimit u<= guardLimit == (X + 1) u< guardLimit`.

So the widened condition is:

`i.start u< guardLimit && latchLimit u<= guardLimit`

For the signed latch comparison case M is:

`forall X . X u< guardLimit && (X + 1) s< latchLimit => (X + 1) u< guardLimit`

The only way the antecedent can be true and the consequent can be false is if

`X == guardLimit - 1`

(and guardLimit is non-zero, but we won't use this latter fact).

If `X == guardLimit - 1` then the second half of the antecedent is

`guardLimit s< latchLimit`

and its negation is

`latchLimit s<= guardLimit`.

So the widened condition is:

` i.start u< guardLimit && latchLimit s<= guardLimit`

This patch implements the logic above. In the follow up changes the following will be supported:

- ule, sle as the latch conditions
- the guard IV and the latch IV start from different values (like, latch IV is {1,+,1}, range check IV {2,+,1})