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

[Tobias Grosser via llvm-commits]

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
-------------- next part --------------
; RUN: opt %loadPolly -polly-scops -analyze < %s | FileCheck %s
; RUN: opt %loadPolly -polly-codegen -S < %s

; Bugpoint-reduced from
; test-suite/SingleSource/Benchmarks/Adobe-C++/loop_unroll.cpp
;
; Check that the loop %loop_start does not narrow the domain (the domain when
; entering and leaving the loop must be identical)
;
; What happened in detail:
;
; 1) if.end5 checks %count whether there will be at least one iteration of
;    loop_start. The domain condition added to loop_start therefore is
;      [count] -> { [] : count > 0 }
; 2) The loop exit condition of loop_start tests whether
;    %indvars.iv.next64 == %0 (which is zext i32 %count to i64, NOT %count
;    itself). %0 and %count have to be treated as independent parameters. The
;    loop exit condition is
;      [p_0] -> { [i0] : i0 = p_0 - 1 }
; 3) Normalized loop induction variables are always non-negative. The domain
;    condition for this is loop
;      { [i0] : i0 >= 0 }
; 4) The intersection of all three sets (condition of executing/entering loop,
;    non-negative induction variables, loop exit condition) is
;      [count, p_0] -> { [i0] : count > 0 and i0 >= 0 and i0 = p_0 - 1 }
; 5) from which ISL can derive
;     [count, p_0] -> { [i0] : p_0 > 0 }
; 6) if.end5 is either executed when skipping the loop
;    (domain [count] -> { [] : count <= 0 })
;    or though the loop.
; 7) Assuming the loop is guaranteed to exit, Polly computes the after-the-loop
;    domain by taking the loop exit condition and projecting-out the induction
;    variable. This yields
;       [count, p_0] -> { [] : count > 0 and p_0 > 0 }
; 8) The disjunction of both cases, 6) and 7)
;    (the two incoming edges of if.end12) is
;      [count, p_0] -> { [] : count <= 0 or (count > 0 and p_0 > 0) }
; 9) Notice that if.end12 is logically _always_ executed in every scop
;    execution. Both cases of if.end5 will eventually land in if.end12

define void @func(i64 %count, i64 %count2, float* %A) {
entry:
  br i1 undef, label %if.end5.preheader, label %for.end

if.end5.preheader:
  %cmp6 = icmp sgt i64 %count, 0
  br label %if.end5

if.end5:
  br i1 %cmp6, label %loop_start, label %if.end12

loop_start:
  %indvars.iv63 = phi i64 [ %indvars.iv.next64, %loop_start ], [ 0, %if.end5 ]
  %add8 = add i32 undef, undef
  store float 0.0, float* %A
  %indvars.iv.next64 = add nsw i64 %indvars.iv63, 1
  %cmp9 = icmp eq i64 %indvars.iv.next64, %count2
  br i1 %cmp9, label %if.end12, label %loop_start

if.end12:
  store float 0.0, float* %A
  br label %for.end

for.end:
  ret void
}


; CHECK:      Statements {
; CHECK-NEXT:     Stmt_if_end12
; CHECK-NEXT:         Domain :=
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] };
; CHECK-NEXT:         Schedule :=
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] -> [] };
; CHECK-NEXT:         MustWriteAccess :=    [Reduction Type: NONE] [Scalar: 0]
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] -> MemRef_A[0] };
; CHECK-NEXT: }
-------------- next part --------------
; RUN: opt %loadPolly -polly-scops -analyze < %s | FileCheck %s
; RUN: opt %loadPolly -polly-codegen -S < %s

; Bugpoint-reduced from
; test-suite/SingleSource/Benchmarks/Adobe-C++/loop_unroll.cpp
;
; Check that the loop %loop_start does not narrow the domain (the domain when
; entering and leaving the loop must be identical)
;
; What happened in detail:
;
; 1) if.end5 checks %count whether there will be at least one iteration of
;    loop_start. The domain condition added to loop_start therefore is
;      [count] -> { [] : count > 0 }
; 2) The loop exit condition of loop_start tests whether
;    %indvars.iv.next64 == %0 (which is zext i32 %count to i64, NOT %count
;    itself). %0 and %count have to be treated as independent parameters. The
;    loop exit condition is
;      [p_0] -> { [i0] : i0 = p_0 - 1 }
; 3) Normalized loop induction variables are always non-negative. The domain
;    condition for this is loop
;      { [i0] : i0 >= 0 }
; 4) The intersection of all three sets (condition of executing/entering loop,
;    non-negative induction variables, loop exit condition) is
;      [count, p_0] -> { [i0] : count > 0 and i0 >= 0 and i0 = p_0 - 1 }
; 5) from which ISL can derive
;     [count, p_0] -> { [i0] : p_0 > 0 }
; 6) if.end5 is either executed when skipping the loop
;    (domain [count] -> { [] : count <= 0 })
;    or though the loop.
; 7) Assuming the loop is guaranteed to exit, Polly computes the after-the-loop
;    domain by taking the loop exit condition and projecting-out the induction
;    variable. This yields
;       [count, p_0] -> { [] : count > 0 and p_0 > 0 }
; 8) The disjunction of both cases, 6) and 7)
;    (the two incoming edges of if.end12) is
;      [count, p_0] -> { [] : count <= 0 or (count > 0 and p_0 > 0) }
; 9) Notice that if.end12 is logically _always_ executed in every scop
;    execution. Both cases of if.end5 will eventually land in if.end12

define void @func(i64 %count, i64 %count2, float* %A) {
entry:
  br i1 undef, label %if.end5.preheader, label %for.end

if.end5.preheader:
  %cmp6 = icmp sgt i64 %count, 0
  br label %if.end5

if.end5:
  br i1 %cmp6, label %loop_start, label %if.end12

loop_start:
  %indvars.iv63 = phi i64 [ %indvars.iv.next64, %loop_start ], [ 0, %if.end5 ]
  %add8 = add i32 undef, undef
  store float 0.0, float* %A
  %indvars.iv.next64 = add i64 %indvars.iv63, 1
  %cmp9 = icmp eq i64 %indvars.iv.next64, %count2
  br i1 %cmp9, label %if.end12, label %loop_start

if.end12:
  store float 0.0, float* %A
  br label %for.end

for.end:
  ret void
}


; CHECK:      Statements {
; CHECK-NEXT:     Stmt_if_end12
; CHECK-NEXT:         Domain :=
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] };
; CHECK-NEXT:         Schedule :=
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] -> [] };
; CHECK-NEXT:         MustWriteAccess :=    [Reduction Type: NONE] [Scalar: 0]
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] -> MemRef_A[0] };
; CHECK-NEXT: }
-------------- next part --------------
; RUN: opt %loadPolly -polly-scops -analyze < %s | FileCheck %s
; RUN: opt %loadPolly -polly-codegen -S < %s

; Bugpoint-reduced from
; test-suite/SingleSource/Benchmarks/Adobe-C++/loop_unroll.cpp
;
; Check that the loop %loop_start does not narrow the domain (the domain when
; entering and leaving the loop must be identical)
;
; What happened in detail:
;
; 1) if.end5 checks %count whether there will be at least one iteration of
;    loop_start. The domain condition added to loop_start therefore is
;      [count] -> { [] : count > 0 }
; 2) The loop exit condition of loop_start tests whether
;    %indvars.iv.next64 == %0 (which is zext i32 %count to i64, NOT %count
;    itself). %0 and %count have to be treated as independent parameters. The
;    loop exit condition is
;      [p_0] -> { [i0] : i0 = p_0 - 1 }
; 3) Normalized loop induction variables are always non-negative. The domain
;    condition for this is loop
;      { [i0] : i0 >= 0 }
; 4) The intersection of all three sets (condition of executing/entering loop,
;    non-negative induction variables, loop exit condition) is
;      [count, p_0] -> { [i0] : count > 0 and i0 >= 0 and i0 = p_0 - 1 }
; 5) from which ISL can derive
;     [count, p_0] -> { [i0] : p_0 > 0 }
; 6) if.end5 is either executed when skipping the loop
;    (domain [count] -> { [] : count <= 0 })
;    or though the loop.
; 7) Assuming the loop is guaranteed to exit, Polly computes the after-the-loop
;    domain by taking the loop exit condition and projecting-out the induction
;    variable. This yields
;       [count, p_0] -> { [] : count > 0 and p_0 > 0 }
; 8) The disjunction of both cases, 6) and 7)
;    (the two incoming edges of if.end12) is
;      [count, p_0] -> { [] : count <= 0 or (count > 0 and p_0 > 0) }
; 9) Notice that if.end12 is logically _always_ executed in every scop
;    execution. Both cases of if.end5 will eventually land in if.end12

define void @func(i64 %count, i64 %count2, float* %A) {
entry:
  br i1 undef, label %if.end5.preheader, label %for.end

if.end5.preheader:
  %cmp6 = icmp sgt i64 %count, 0
  br label %if.end5

if.end5:
  br i1 %cmp6, label %loop_start, label %if.end12

loop_start:
  %indvars.iv63 = phi i64 [ %indvars.iv.next64, %loop_start ], [ 0, %if.end5 ]
  %add8 = add i32 undef, undef
  store float 0.0, float* %A
  %indvars.iv.next64 = add i64 %indvars.iv63, 1
  %cmp9 = icmp sge i64 %indvars.iv.next64, %count2
  br i1 %cmp9, label %if.end12, label %loop_start

if.end12:
  store float 0.0, float* %A
  br label %for.end

for.end:
  ret void
}


; CHECK:      Statements {
; CHECK-NEXT:     Stmt_if_end12
; CHECK-NEXT:         Domain :=
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] };
; CHECK-NEXT:         Schedule :=
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] -> [] };
; CHECK-NEXT:         MustWriteAccess :=    [Reduction Type: NONE] [Scalar: 0]
; CHECK-NEXT:             [count, p_1] -> { Stmt_if_end12[] -> MemRef_A[0] };
; CHECK-NEXT: }