[llvm] [InstCombine] Optimize icmp(sub(a, c), sub(b, c)) to icmp(a, b) if a, b, and c are pointers (PR #161698)

Ryan Buchner via llvm-commits llvm-commits at lists.llvm.org
Thu Oct 2 16:04:26 PDT 2025


bababuck wrote:

> > Alive proof has some issues with undef that I don't quite understand, https://alive2.llvm.org/ce/z/AdZoWJ
> > Particularly %p2 = ptrtoint ptr %2 to i2 is solved different, in Src, i2 %p2 = #x3 (3, -1), while in Tgt: i2 %p2 = #x0 (0)
> 
> Each use of undef can observe a different value. See https://llvm.org/docs/UndefinedBehavior.html#undef-values You can pass `--disable-undef-input` to Alive2.
Is that alright since it won't fully prove correctness.

Posted an updated proof.

https://github.com/llvm/llvm-project/pull/161698


More information about the llvm-commits mailing list