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

    <tr>
        <th>Summary</th>
        <td>
            [ConstraintElimination] A miscompile in presence of `shl nuw nsw` and `llvm.umin`
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            miscompilation,
            llvm:transforms
      </td>
    </tr>

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

    <tr>
      <th>Reporter</th>
      <td>
          DaniilSuchkov
      </td>
    </tr>
</table>

<pre>
    The following commit: https://github.com/llvm/llvm-project/commit/71f56e49ceca75dbf82cbb9537c2545c2d2e51c9
Triggered this miscompile: https://alive2.llvm.org/ce/z/oBg-u8

Now `opt -passes=constraint-elimination -S` turns
```
define i1 @test(i32 %arg) {
  %icmp = icmp slt i32 %arg, 0
  %shl = shl nuw nsw i32 %arg, 3
 %call4 = call i32 @llvm.umin.i32(i32 %shl, i32 80)
  ret i1 %icmp
}

declare i32 @llvm.umin.i32(i32, i32) #0

attributes #0 = { nocallback nofree nosync nounwind speculatable willreturn memory(none) }
```
into
```
define i1 @test(i32 %arg) {
  %shl = shl nuw nsw i32 %arg, 3
  %call4 = call i32 @llvm.umin.i32(i32 %shl, i32 80)
 ret i1 false
}

declare i32 @llvm.umin.i32(i32, i32) #0

attributes #0 = { nocallback nofree nosync nounwind speculatable willreturn memory(none) }
```

Given this debug output:
```
opt -passes=constraint-elimination before-constr-elim-renamed.ll -S -debug-only=constraint-elimination,constraint-system
Processing fact to add to the system: icmp ule i32 %call4, %shl
Adding 'icmp ule i32 %call4, %shl'
  constraint: -8 * %srem + %call4 <= 0

---
-1 * %srem <= 0
-8 * %srem + %call4 <= 0
-1 * %call4 <= 0
8 * %srem <= -1
unsat
Adding 'icmp sge i32 %call4, 0'
  constraint: -1 * %call4 <= 0

Adding 'icmp sle i32 %call4, %shl'
  constraint: -8 * %srem + %call4 <= 0

Processing fact to add to the system: icmp ule i32 %call4, 80
Adding 'icmp ule i32 %call4, 80'
  constraint: %call4 <= 80

Adding 'icmp sge i32 %call4, 0'
  constraint: -1 * %call4 <= 0

Adding 'icmp sle i32 %call4, 80'
  constraint: %call4 <= 80

Top of stack : 0 1
CB: 0 1
Processing condition to simplify: %icmp = icmp slt i32 %srem, 0
Checking   %icmp = icmp slt i32 %srem, 0
---
-1 * %call4 <= 0
-8 * %srem + %call4 <= 0
-1 * %call4 <= 0
%call4 <= 80
-1 * %srem <= 0
sat
---
-1 * %call4 <= 0
-8 * %srem + %call4 <= 0
-1 * %call4 <= 0
%call4 <= 80
%srem <= -1
unsat
Condition icmp sge i32 %srem, 0 implied by dominating constraints
-1 * %call4 <= 0
-8 * %srem + %call4 <= 0
-1 * %call4 <= 0
%call4 <= 80
```
I'm not 100% sure if the aforementioned patch causes the miscompile, of if it merely triggers it on this specific reproducer. The fact that something like `-1 * %call4 <= 0` is reported as a "dominating constraint" seems suspicious to a person who's not familiar with the logic of ConstraintElimination and it doesn't look directly related to that patch. However, if I replace the `shl nuw nsw i32 %arg, 3
` with `mul nuw nsw i32 %arg, 8`, the miscompile doesn't happen: https://alive2.llvm.org/ce/z/EL2bCh.
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzcV-9u2zgSfxr6y0CGRMmS_MEfEru5K3A4HNC-AEWNLF4oUuBQMbxPvyClJE7qpOluF1ssEESSOZw_v99wOCOI1NEg7tjmlnFu1L2SjHO2OazE5HvrdgdhlNJfJtnf24dVY9vz7muP0Fmt7UmZI0g7DMqz_AZ670di-Q3jd4zfHZXvp2Yt7cD4ndYPj49kdPb_KD3jd8tWfldl3abEYitRimrTNl3NZdNsN3kl-abYSN5y3GRyy9IDS2--OnU8osMWfK8IBkXSDqPS-K0TQqsH5Otgd23dMdhExu9-Y_zO3h6TqZ41zv__a0_AytSOHpJRECGx_CCtIe-EMj5BrQZlhFfWQPKFlSn4yRlaVJTp8hc_W-yUQVAZsCL1SJ7xWuUcGN-I4McWWHU7i0L4UclhBJYfIL6Q9nApvYf0QpZ6HUXD00wnMHR6JZ0v0oxvpNC6iOLhbZYr0gjINCizVjl_do16HbaHrzplfPto1KGPocx-LgFXh0vwWpRaOHzHwKI5xs7z9HKz8N6pZvJIcSm6y6pbMDY43Qh5D8Z2DhGMpbORYOxkTsq0QCPKSQsvGo1wUlo7DKTAgIN1Z8ZrYw3OcB-uEqWMtz-FwY-z8rNoWVjphCb8R3Ey__-XekAzH_EWm-kIdvLjFCrN1U0fOrYNdtZhMq_GlcShEQO2a60h-QJJNJVYo89vamF8f7FAZ_I4zD78z1mJRKEsdkJ68BZE24aH7xEWyfxmPuSTxscEidkQuFjIjspu2jYoYrz6njivHjPr2a9gJqmB8VgFyOEAjN9ept4-MPoC8SRJlpfs5cYXsh_X-qzm2mp9zUaSzYuTIeGv4kDHb3FI34bgXReuG_jrgf7TeVKnH86R-m1wXvtYvwvL34H7H3b-qx3BdkA-1KkgnsKSWfvbF58XVEhrWhXLhLdAahi16s6LqTfv50D4xQW971HeB2Xv3-qvdl05eFfP0086eW9B9-6xfzqPv4iz3y8c-yc-XyfwE_wQWcYWmjO0di7wcyYsmUa_RKgvb7rPjFcDGOshS1PGN0BTuOS7WDxEuOAGNCFubGEUXvYgxURIcf2iW-b7cERUB8rDgA71GfzcWlP4yS6Xb7jOVackOBydbSeJbg1xBoilqxceyA7o-4CcVvcYmug3Ay1TUBRUWeexBUEggHF-FXzGORDiQEATjUoqO1GslTCiI2vg1FvGK4pYdGJQWgkHJ-X7GKq2RyVDiPsnjZ8uegFh2hBma5EM45UHbe09tMqh9PoMDrUIHsaiLPyM5Br-bU_4gC42Th18DpFoITEaZGX63e4vABA9ZGU6TG8J14Fsvn_F2IWvvRhHND808Hz6D2_2_XrV7vJ2m2_FCndZlW7KLCuKYtXvirrLM6y32yLNu67sClFuswazlvOslqlYqR1PeZFmWc3TTcWLtSzDWiWKjtdtUxasSHEQSj-ZXymiCXdVXfJspUWDmpZJ8ymopaMKnSjjPM6J-Y13wlBn3UDLMOp2cXRspiOFRlaRp2cjXnkdJ9irPLPNAW4uQVQGRoeERmJIjpekBXpCYrDyuV1mZbqanN798Hwbo6cw3wYAfg8AAP__7_Z6PQ">