[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
- Previous message: [llvm] [InstCombine] Optimize icmp(sub(a, c), sub(b, c)) to icmp(a, b) if a, b, and c are pointers (PR #161698)
- Next message: [llvm] [InstCombine] Optimize icmp(sub(a, c), sub(b, c)) to icmp(a, b) if a, b, and c are pointers (PR #161698)
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
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
- Previous message: [llvm] [InstCombine] Optimize icmp(sub(a, c), sub(b, c)) to icmp(a, b) if a, b, and c are pointers (PR #161698)
- Next message: [llvm] [InstCombine] Optimize icmp(sub(a, c), sub(b, c)) to icmp(a, b) if a, b, and c are pointers (PR #161698)
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
More information about the llvm-commits
mailing list