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

[Michael Kruse via llvm-commits]

2016-04-02 0:48 GMT+02:00 Tobias Grosser <tobias at grosser.es>:
>> 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?

With "not supported by Polly" I meant some constraints count>=0
count2>0 added to the assumed and checked context.



>> 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[] };

loop-succ-cond-4.ll also has B1+B2.


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

I think that for each loop
  Context \cap dom(EntryBB) == Context \cap \bigcup_{E \in LoopExits}  dom(E)
is a necessary condition for correctness. Currently Polly does not
have this, as show in unroll_loop.

We can either ensure
1) dom(EntryBB) == \bigcup_{E \in LoopExits} dom(E)
- or -
2) that Context excludes all cases where 1) is false.

My patch tried 1). 2) Is also a viable solution but harder to ensure.
We don't even agree yet what domain/context are supposed to be. Hence
IMHO, maybe even just for robustness, we should do 1) and maybe 2) as
well.


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

It fixes loop_unroll, so it obviously has to do with correctness ?!?


> 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?

This happens in loop-succ-cond.ll

Do you have another issue in mind?


Michael