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

[Michael Kruse via llvm-commits]

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.

For the others, count<0 && count2<0 should still be possible, but
maybe not supported by Polly. Shouldn't Polly reject loops without nsw
flag?

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


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> }. D18450 cannot help when the loop
has multiple exits.


Michael




2016-03-27 18:59 GMT+02:00 Tobias Grosser <tobias at grosser.es>:
> On 03/27/2016 02:34 PM, Johannes Doerfert via llvm-commits wrote:
>>
>> Hey Michael,
>>
>> I think this patch needs some more discussion. Could you revert it and
>> we start a new thread to tackle the problem? There is also a chance that
>> the problem in the lnt fails is something different [PR26683] that was
>> prevented from happening due to the domain simplification of this patch.
>> Nevertheless, I think we need to change the domain generation part you
>> modified here (wrt. your comment about
>> isl_set_drop_constraints_involving_dims) and use a simplification scheme
>> similar to D18450.
>
>
> Hi Michael,
>
> thanks again for all your work on this bug until now. This seems to be
> indeed a rather difficult problem. I had another look, also with the goal to
> answer a question Johannes raised: Does this change simplify the domains
> only or indeed fixes a correctness issue with these domains?
>
> I was personally convinced this change was indeed a correctness fix. To
> show this I went again to the test case you committed (loop-succ-cond.ll).
> It seems for this test case there is no correctness issue. The domain before
> your patch was:
>
>         count <= 0 or (count > 0 and p_1 >= 0)
>
> which means only for count > 0 and p_1 < 0, this condition would be false.
> However, for count > 0, the zext from %count to %p_1 would result
> in %p_1 being positive as well. Consequently, this condition will not arise
> and the domain is -- just because of the zext -- correct.
>
> Now, Polly currently does not look at the zext and in fact the same problem
> should be visible even without exploiting zext. I made p_1 a new parameter
> (loop-succ-cond-2.ll) to make it very clear that there is no relation
> between the two parameters.
>
> Without your patch we again get { Stmt_if_end12[] : count <= 0 or (count > 0
> and count2 >= 0)} and we again see that count > 0 and count2 < 0 is the only
> condition that is missing. However, when looking further, in case of count2
> being smaller than 0 we will run into the 'nsw' in the induction variable
> increment:
>
>   %indvars.iv.next64 = add nsw i63 %indvars.iv63, 1
>
> So this specific parameter configuration actually triggers undefined
> behavior. Which means the domain is still correct. Now, we can obviously
> drop the nsw to make this behavior defined (loop-succ-cond-3.ll). However,
> as soon as we drop the 'nsw' the condition
> count > 0 and count2 <= 0 shows up in the invalid context, as Polly
> correctly derives that these parameters would result in an infinite loop. We
> could avoid an infinite loop by using sge instead of eq in the exit
> condition (loop-succ-cond-4.ll), but in this case the old code
> suddenly does produce an unconstrained domain for
> Stmt_if_end12. You seem to have already realized this as you state in
> the commit message: "is logically impossible for non-infinite loops"
>
> For what I tried, it seems the domains we generate have already been correct
> before this patch thanks to the non-infinite-loop assumption we take.
> Johannes/Michael, did I miss anything in my reasoning?
>
> As both of you stated, there are still good reason to simplify such domains.
> However, I think it is still important to understand if there
> inherent correctness issues involved or if this change is important mostly
> for not causing trouble with error hoisting or the complexity of
> domains.
>
> Best,
> Tobias