[polly] r264118 - [ScopInfo] Fix domains after loops.

[Tobias Grosser via llvm-commits]

On 04/01/2016 03:04 PM, Michael Kruse wrote:
> Sorry for my absence in the discussion.
>
>
> Thanks Tobias for his analysis. In some details it can be improved.
> Lets give the changes to the test case a letter:
>
>
> A: Make %count and %0/%count2 independent by removing the zext.
> B1: Remove nuw in induction variable increment
> B2: Remove nsw in induction variable increment
> C: Use sge instead of eq in loop exit condition
>
> In plain loop-succ-cond.ll (and wtih/without any B,C), there is
> neither undefined behaviour nor an infinite loop. ScEv might know, but
> not Polly. This can cause another set of problems.
>
> With A and count2<0 (>= 2^61 as unsigned) we have undefined behaviour.
> indvar will eventually hit the nsw limit (2^61-1). One possible effect
> of undefined behaviour is an infinite loop.
>
> With A+B1 and count2<0 as before, because we hit the nsw first.
>
> With A+B2, we have completely defined behaviour. indvar will iterate
> through 0..2^61-1 and eventually be equal to count to in the range
> 2^61..2^62-1
>
> With A+C (with/without any B) and count2<0  the loop body is executed
> exactly once because 0 (+1) is greater than any negative count2.
>
>
> In summary, we have no infinite loop in any case. Any analysis
> including ScalarEvolution and Polly can assume that undefined
> behaviour does not occur. ScEv can give us a trip count when it sees
> the nsw flag.
>
> For the cases that trigger undefined behaviour (A [+B1]), we might
> want to add count2>=1 to the assumption context.  Not sure why this
> isn't done yet.

Right. This could be added. I suggest to keep this in mind and to look 
again into this after having resolved the actual bug we see.

> For the others, count<0 && count2<0 should still be possible, but
> maybe not supported by Polly.

I am not sure to understand this sentence. Are you saying our current 
modeling is incorrect for some of the test cases I attached in my last 
email?

 > Shouldn't Polly reject loops without nsw
> flag?

No, we do not need to reject them. Polly assumes that all loops are 
finite (do not wrap) and generates constraints (and as a result run-time 
checks), that verify this assumption dynamically. For 
loop-succ-cond-3.ll we would get a wrapping loop in case 'count > 0 and 
count2 <= 0'. This condition is added by Polly to the 'Invalid Context',
and is verified to not hold before entering the scop at run-time.

> Case A+C remains to be handled even if we add proper assumed context
> and enforce nsw/nuw flags.

A+C corresponds to /tmp/loop-succ-cond-4.ll, right? The domain we obtain 
today (without your patch) is:

	[count, count2] -> { Stmt_if_end12[] };

To me this seems correct. It seems you believe that some of the modeling 
is currently still incorrect. Could you name the example file I added 
and the constraints/conditions that are required to changed to ensure 
_correctness_. I am currently not seen where this would be necessary.

> In all cases, I think we should add domain lower and upper bound only
> together and we shouldn't allow ISL to add new contraints when leaving
> the loop. It might find other contraints in  [p] -> { [i0] : i0 > 0
> and <contraints found in the loop> }.

I think it might be good to do what you did in your patch, but before 
moving ahead I would like to understand if this is a correctness issue
or just constraints that we can make simpler.

Your example above suggests that you have a correctness issue in mind. 
As said above, do we already have (or can we draft) such a test case?

 > D18450 cannot help when the loop
> has multiple exits.

Agreed. And for whatever reason it also did not fix the bug we see on LNT.

Best,
Tobias