<table border="1" cellspacing="0" cellpadding="8">
    <tr>
        <th>Issue</th>
        <td>
            <a href=https://github.com/llvm/llvm-project/issues/58074>58074</a>
        </td>
    </tr>

    <tr>
        <th>Summary</th>
        <td>
            [SCEV] Missing implication opportunity: cannot infer inequality from 2 guarding conditions
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            new issue
      </td>
    </tr>

    <tr>
      <th>Assignees</th>
      <td>
      </td>
    </tr>

    <tr>
      <th>Reporter</th>
      <td>
          max-quazan
      </td>
    </tr>
</table>

<pre>
    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()

```
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJztVs-vmzgQ_mvgYr0IDMlLDhzaZJ9UrbqXVr1GBg_grbFZY5L3-td3bJIAL0l3K7U9VCtFBM_P7xvPJJNr_pK9s6QDaDpia2bJO8U_MdMFdItno_uqJh-2f3wiommlKJgVWhFQlVDgTEomJDpq0hp9ANLpBlBW2I6IEv3hhTADgy9wkr8Qe9SEi7IEA8oSrhuhMKaqSNUzw7sF2WrVCQ7GeZNSS6mPTg3PDINAkLwJol0QnZ5_Kn1UQ8JRs4pOH3_EBHsJigTJNkh2BF8HuTg4ETmpb7oOz78AkZ8Z3styivbtSB9rX05bCyxPR3R-ELr3lRazK3DMr8tNCqaUtqTtpfRlHOpsdQXoYMZLwKxzclPuiAjzHWtR1A4DNDkzrOuwxIsp1PfaisOQ3UJn79HmUDpkIqEkSCNnuY_igK69gC47y4z1_IazAzCezqWnGxI8vh0CYlOYl0s2QnJDJMtBem-t2ylGfx5N0cLT3pG2FkOO5dsZCnz38VGx8-dBLw4LBc9ni5wVn4FX4I3G0K2BQisufElcElE0LeklXLHZnpmOFET8OoQzuxDzrQ98H8-kU_O9mzPgU_aj06wERQ3F5308hWjPEMXhhG7W9BOEJ-eb4OhMOljeR0VvoaLfRnUf0Tz3-Yb-E6CL8atG8Vfu8TDO51DiiaHrsb27Bm9aMBw9ByyNnAwbHZv3CvPFZwbQd-tUAM_CXjINze8kI04D0xpNON3qjNGtVwZYUbMcfy0nTrMCXSd5OLEOHndTr_tjTn_kmP_kAbuq_b_M1i_9ZflZE_s98_r_tP4W08qhkH7fukn61T94CFm8WqXLeLOK45BnCd8kGxZaYSVk2MBu68NOJe-FXw9mG4luW21sr4R1U3zeTITCtQ6f8E_PJKpIaXRD6LDauRCXOnRhb2RWW9v6vY0-4acStu7zRaEbPEh5OH894FbzNxQ4RU-IpAdcmJ6W6-gxDeuMc54k0TLa0BVLcshXaUKREi3WacHYJg_9_XWOTkCpgiPxIfAdmYUioxGl0SaJolWSJPEC1mmZQsIjiIGX6xSLCA3ewcLhWGhThSbzkPK-6lApRWe7Uen2qEqBr56Lz3pba5M17PkBK_KFqdBnzzz6r1yPYEI">