| Issue |
58074
|
| Summary |
[SCEV] Missing implication opportunity: cannot infer inequality from 2 guarding conditions
|
| Labels |
new issue
|
| Assignees |
|
| Reporter |
max-quazan
|
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:
```
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()
```
![]()
_______________________________________________
llvm-bugs mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-bugs
