[InstCombine] Missing fold for x == y when x > y + 1 assumed

[Kmeakin]

x == y is correctly folded to false when x > y is assumed, or when x >= y + 1 is assumed, but not when x > y + 1 is assumed:

godbolt

; folded to false
define i1 @assume_x_ugt_y(i64  %x, i64  %y)  {
  %1 = icmp ugt i64 %x, %y
  tail call void @llvm.assume(i1 %1)
  %2 = icmp eq i64 %x, %y
  ret i1 %2
}

; folded to false
define i1 @assume_x_uge_y_plus_1(i64  %x, i64  %y)  {
  %1 = add nuw i64 %y, 1
  %2 = icmp uge i64 %x, %1
  tail call void @llvm.assume(i1 %2)
  %3 = icmp eq i64 %x, %y
  ret i1 %3
}

; not folded to false
define i1 @assume_x_ugt_y_plus_1(i64  %x, i64  %y)  {
  %1 = add nuw i64 %y, 1
  %2 = icmp ugt i64 %x, %1
  tail call void @llvm.assume(i1 %2)
  %3 = icmp eq i64 %x, %y
  ret i1 %3
}

declare void @llvm.assume(i1) 

alive proof

define i1 @src(i64 %x, i64 %y)  {
  %1 = add nuw i64 %y, 1
  %2 = icmp ugt i64 %x, %1
  tail call void @llvm.assume(i1 %2)
  %3 = icmp eq i64 %x, %y
  ret i1 %3
}
=>
define i1 @tgt(i64 %x, i64 %y)  {
  ret i1 false
}

declare void @llvm.assume(i1) 

[floatshadow]

This happens as x >= y + 1 is equivalent to x > y . Thus the latter cmp can be folded naturely.
But x > y + 1 is not the case and y+1 is not captured by AssumptionCache

[antoniofrighetto]

On this. It seems that simplifyICmpWithDominatingAssume is not capturing that case. Whilst a possible solution for this could be in ConstraintElimination, I'm gradually convincing myself the right place to fix this should be in ValueTracking::isImpliedCondICmps. Indeed, when the predicate of the two comparisons is the same as here below:

define i1 @assume_x_ugt_y_plus_1(i64  %x, i64  %y)  {
  %1 = add nuw i64 %y, 1
  %2 = icmp ugt i64 %x, %1
  tail call void @llvm.assume(i1 %2)
  %3 = icmp ugt i64 %x, %y
  ret i1 %3
}

The second comparison (x > y) is correctly folded to true by EarlyCSE via ValueTracking when x > y + 1 is assumed.

[antoniofrighetto]

Closing this as it should be solved by this (Godbolt: https://godbolt.org/z/3ej4sxqaa), feel free to reopen should a similar issue arise (signed comparisons still to be handled).