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

    <tr>
        <th>Summary</th>
        <td>
            [IndVars] Miscompile caused by invalid nuw nsw on SCEVAddRecExpr
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
      </td>
    </tr>

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

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

<pre>
    Miscompile since this patch
```
commit a3d1fb3b59b473e4f262a05f187de6474b7721e7
Author: Max Kazantsev <mkazantsev@azul.com>
Date:   Fri Aug 12 13:27:01 2022 +0700

    [SCEV] Prove condition invariance via context

    Contextual knowledge may be used to prove invariance of some conditions.
    For example, in this case:
    ```
      ; %len >= 0
      guard(%iv = {start,+,1}<nuw> <s %len)
      guard(%iv = {start,+,1}<nuw> <u %len)
    ```
    the 2nd check always fails if `start` is negative and always passes otherwise.

    It looks like there are more opportunities of this kind that are still to be
    implemented in the future.

    Differential Revision: https://reviews.llvm.org/D129753
    Reviewed By: apilipenko
```

Test: opt -passes=indvars on
```

define i32 @foo() {
entry:
  br label %for.body.i

for.body.i:                                       ; preds = %for.inc32.i, %entry
  %storemerge13.i = phi i32 [ 0, %entry ], [ %dec.i, %for.inc32.i ]
  %cmp22.not.i = icmp ult i32 %storemerge13.i, 2
  br label %for.cond8.preheader.i

for.cond8.preheader.i:                            ; preds = %for.inc27.i, %for.body.i
  %storemerge611.i = phi i64 [ 0, %for.body.i ], [ %add.i, %for.inc27.i ]
  br i1 %cmp22.not.i, label %for.inc27.i, label %func_1.exit

for.inc27.i:                                      ; preds = %for.cond8.preheader.i
  %add.i = add i64 %storemerge611.i, 1
  %cmp5.i = icmp ult i64 %storemerge611.i, 11
  br i1 %cmp5.i, label %for.cond8.preheader.i, label %for.inc32.i

for.inc32.i:                                      ; preds = %for.inc27.i
  %dec.i = add i32 %storemerge13.i, -1
  br label %for.body.i

func_1.exit:                                      ; preds = %for.cond8.preheader.i
  ret i32 %storemerge13.i
}
```
With this patch, check
```
%cmp22.not.i = icmp ult i32 %storemerge13.i, 2
```
gets replaced with 1st iteration check
```
%cmp22.not.i = icmp ult i32 0, 2
```
which is incorrect, because when the loop goes on 2nd iteration, this check should fail. Digging into it, I see that by the moment of query in patch in question SCEV sees
```
 ArLHS = {0,+,-1}<nuw><nsw><%for.body.i>
RHS = 2
CtxI =   %cmp22.not.i = icmp ult i32 %storemerge13.i, 2
```
Flags `nuw nsw` look incorrect here, but the patch takes decision basing on `nuw`. When running `opt "-passes=print<scalar-evolution>"` on it, this AddRec has no nuw nsw:
```
Printing analysis 'Scalar Evolution Analysis' for function 'foo':
Classifying expressions for: @foo
  %storemerge13.i = phi i32 [ 0, %entry ], [ %dec.i, %for.inc32.i ]
  -->  {0,+,-1}<%for.body.i> U: [-1,1) S: [-1,1)                Exits: -1               LoopDispositions: { %for.body.i: Computable, %for.cond8.preheader.i: Invariant }
  %storemerge611.i = phi i64 [ 0, %for.body.i ], [ %add.i, %for.inc27.i ]
  -->  {0,+,1}<%for.cond8.preheader.i> U: [0,12) S: [0,12)              Exits: <<Unknown>>              LoopDispositions: { %for.cond8.preheader.i: Computable, %for.body.i: Variant }
  %add.i = add i64 %storemerge611.i, 1
  -->  {1,+,1}<%for.cond8.preheader.i> U: [1,13) S: [1,13)              Exits: <<Unknown>>              LoopDispositions: { %for.cond8.preheader.i: Computable, %for.body.i: Variant }
  %dec.i = add i32 %storemerge13.i, -1
  -->  {-1,+,-1}<%for.body.i> U: [-2,0) S: [-2,0)               Exits: -2               LoopDispositions: { %for.body.i: Computable, %for.cond8.preheader.i: Invariant }
Determining loop execution counts for: @foo
Loop %for.cond8.preheader.i: <multiple exits> Unpredictable backedge-taken count.
  exit count for for.cond8.preheader.i: ***COULDNOTCOMPUTE***
  exit count for for.inc27.i: 11
Loop %for.cond8.preheader.i: max backedge-taken count is 11
Loop %for.cond8.preheader.i: Unpredictable predicated backedge-taken count.
Loop %for.body.i: backedge-taken count is 1
Loop %for.body.i: max backedge-taken count is 1
Loop %for.body.i: Predicated backedge-taken count is 1
 Predicates:

Loop %for.body.i: Trip multiple is 2

```

Current theory is that a wrong no-wrap flag was inferred somewhere, and then patch made miscompile basing on it.
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzNWFFzozYQ_jX4ZcceELGJH_yQ2Mk007vezeXu-tgRIGzVgDhJxEl_fXcFNtjBbtOba-txCBba1e63K-3Hxip9WbyXJlFFJXMBRpaJALuRBipuk43nrzz_xpv57df9xMmFtMDDNMjiMJ7O46soFFcZmzHuT7PgOkrF7Cq6iqOIBSJqhG5qu1HaC2_gPX-Gn_kfvLRGPIEXLovt_pd35fM_6nyCK3jhXSO44laQGMC9lnBTryFgEIQ4xCK8-AEwnzHw2K0f-a2FzRVFwJvePi7vvnrTFXzU6klAospUWqlKkOUT15KTw0-S0wMrnu2pgmUzXPMctqXa5SJdCyj4C8QCaiNSsAoqp7mnT2VgVNFbzEw6jfdKg3jmRZULjy1RrME74Yb87Jl-jDq4jxfeoqvTXJRACIUrOHq8rrlOPXaNUyRhuwIvujWWa4tLIUR4DbxohaCX9Q4VEPymVeix-feqqodUDfhhNwJYmUKyEckWeL7jLwYyLnMDMiOBZp2ZDwhMKdbcSgSYo0Q7t-LGCAMKFemdNGJyGrYHC7lSWwO53FJCC43y-FcovKiqUtrWJYaGlGRNALYS9dsNt26isTLPKbix6LRKClohMCPSJm4CstrW-vX6K5lluGZpJSbOJ_EkDWYBpfHG2spQnNk9fjU-ETszyfOnYqL0GodWAZtH07BT9cnNwRVvX0gBx40qK1Fu1eDmbK6fhbE0WVUWxg1YGEF0EFMUPS4viKYikyVmc4h76srPlHI5MKfoNxPQKf3Sy9RYQ85jkVPsM6UnMZ4pE9lX2RsN2-z6yw8leqVFaprUa1Tj6RQy1ILbBkcaQ1or8LexGNxC6LUIwol0ctVGNp5Mb3Gj9MRwZOV-T91-SkVyUNtbyM3qFkiKirFJqWyrXeIA1Lltljg1gNSxcyDRyXA9QQc3gqdCv8br9YTL0J3Di0VHjvWDcwLaLAj6qM2ujlDrhE-g42l6Ch2t2YcOnZfBCYAkcYRIz9ZuvC6T34KJeJb2FJ_99L-bUIP4nIkCHPxyk_GugeMVWmRscJwg01e5cV4yGAJoOoDNazsH0HM74zVKbvi7UNpD3fnptkuHzbnsHwdvOCN6of4xMdXi3EZtzIhWg6fir9Ju-owI_XJla_gI_Y5D4kTVWliDNlc5T_Ds35EVgUEtVmju-Ms_t8I_v-puI5MNVV0MutJaJFTtsQYmHMkO7DaiqXpYWytYK6qepavkB7NoesNnXG03G1XnqavtEyyK67Us16gb66p0mh_ACNFU3fjFqS4UFViqyt9qgQc11lkHPN3giHG-E6cjSTPoBNzodz897jmLf-Ar4yPCQjemvTlOyz31_NQqaaFa2ucH9_v7isGJsfc5XxviPGgVkEHIeoi6dBEAYi8uDLV1EDV4WL5F_HErOm4BMTeELd41uvA6gV8pYLouS3qEI8QHPMY6SlBpDAaRwITnXI_Fk8prF0bEgDGyhZiyPUT1Jk0_iQQ2HHmZgr3JezJw4tpHUk4r85LnL0YS04we3Upwt18JbtqH-AwwCEAngXuAA45-RAf9yxztltkL6RTPuMcNuW5IjA6Nlq_8W4xgPCbaO5xipwkFX5yB01ucQMQZCdXjq5GTzx2ehUQV8Rw9efIOt99KmkqZ5u3CaYpuT05XHFzie11tedy8apw9IXHmQ_v2gvkRrQYh_HH8YAjIYxwHTO4gJaGA9SHtRoYBJcXh8ktJb3Qu1Wn5NwA8iOAg1l0ovg7C-2aW0WEV_BOsXK6Ffay6kf87Vm9mHR1W4-ANOxQTZ-kf7dDDyLkNyv6TDboSWHUL6Q53V5HFs0iaQzVRdWkHD0Yy7eJC1JHBOibxVRdE4yGCUxLRkokzFWtNsqVGyJhqULvYocNBMs1Qc5yfXYfdNN_lhy_vVr98-Lz88P7jl893h_ELCnvsf8-i_9Kvgj8PGk5s528rOcahuefUDrgASV9pF_mzplwSuujDJcGPly3tyXdTTVfXL2j-rGUFh4RBPawvM9hiWNaaWiPEZRQxPNO2XWCnFaZyqcY7zSvIkBnBjhMXzQRKpK6pttuzIe7aNWJPDwsMEhRdK7PjQ9JORmIRzGb-PPCDKRulizCdh3M-stLmYoE7_KFM8cwx1CbsdUMd6U2JmFJvL5fpnvBAS0EbNnSHTGRU63xx3NtZI2WvY9fLZPfU4Gn_jSutfnfE-l4ag4wWb6YRu4pGm8U8maVxkl3HaRrFQeSLbJ5eZ-G1CAMx50k4cm9RhkxGW0dyQb1P_zqYB8F0OmUTf5ZkSRClwYzF6Ww2x40vCuLe-wbTSC-cDXG9Nvgwl8Z23acRsat1KcReP3dN2wVm3fhbTU3akbN44cz9E4qibvE">