[SCEV] Missing implication opportunity: cannot infer inequality from 2 guarding conditions

[xortator]

It seems that IndVars, through SCEV implication engine, fails to prove some facts if they are implied by two different dominating guards. Consider the following example:

Known facts:

min_len <= len
iv < min_len

Need to prove:

iv < len

Though this is obvious, it seems that the implication engine cannot pull two facts together to prove iv < min_len <= len, which is embarassing.

Motivation test opt -passes=indvars -S:

define i32 @test_01(i32 %start, i32 %len, i32 %min_len) {
entry:
  br label %loop

loop:
  %iv = phi i32 [ %start, %entry ], [ %iv.next, %backedge ]
  %precondition = icmp ule i32 %min_len, %len
  br i1 %precondition, label %guarded_1, label %precondition_failed

guarded_1:
  %check_1 = icmp ult i32 %iv, %min_len
  br i1 %check_1, label %guarded_2, label %check_failed

guarded_2:
  %check_2 = icmp ult i32 %iv, %len
  br i1 %check_2, label %backedge, label %check_failed

backedge:
  %iv.next = add i32 %iv, 1
  %loop_cond = call i1 @cond()
  br i1 %loop_cond, label %loop, label %exit
  
exit:
  ret i32 %iv

precondition_failed:
  unreachable

check_failed:
  ret i32 -1
}


define i32 @test_02(i32 %start, i32 %len, i32 %min_len) {
entry:
  %precondition = icmp ule i32 %min_len, %len
  br i1 %precondition, label %loop, label %precondition_failed

loop:
  %iv = phi i32 [ %start, %entry ], [ %iv.next, %backedge ]
  %check_1 = icmp ult i32 %iv, %min_len
  br i1 %check_1, label %guarded, label %check_failed

guarded:
  %check_2 = icmp ult i32 %iv, %len
  br i1 %check_2, label %backedge, label %check_failed

backedge:
  %iv.next = add i32 %iv, 1
  %loop_cond = call i1 @cond()
  br i1 %loop_cond, label %loop, label %exit
  
exit:
  ret i32 %iv

precondition_failed:
  unreachable

check_failed:
  ret i32 -1
}

declare i1 @cond()

[xortator]

We can remove the check in this case:

define i32 @test_03(i32 %start, i32 %len, i32 %min_len) {
entry:
  br label %loop

loop:
  %iv = phi i32 [ %start, %entry ], [ %iv.next, %backedge ]
  %umin.cmp = icmp ult i32 %len, %min_len
  %umin = select i1 %umin.cmp, i32 %len, i32 %min_len
  %check_1 = icmp ult i32 %iv, %umin
  br i1 %check_1, label %guarded, label %check_failed

guarded:
  %check_2 = icmp ult i32 %iv, %len
  br i1 %check_2, label %backedge, label %check_failed

backedge:
  %iv.next = add i32 %iv, 1
  %loop_cond = call i1 @cond()
  br i1 %loop_cond, label %loop, label %exit
  
exit:
  ret i32 %iv

precondition_failed:
  unreachable

check_failed:
  ret i32 -1
}

because it's inferrable from a sole condition.

[fhahn]

ConstraintElimination can handle cases like this: https://llvm.godbolt.org/z/n5ePssasn