[llvm] [InstCombine] Support division of numbers that can be converted to a shift (PR #88220)

via llvm-commits llvm-commits at lists.llvm.org
Wed Apr 10 10:04:56 PDT 2024


================
@@ -1638,6 +1638,30 @@ define i32 @sdiv_mul_sub_nsw(i32 %x, i32 %y) {
   ret i32 %d
 }
 
+  define i32 @mul_by_150_udiv_by_100 (i32 %0) {
----------------
goldsteinn wrote:

> Hard to do in Alive 2 so I'll do a formal proof:
> 
Typically we do alive2 not because we are unable to reason through a transform, but
because of human error.
The same applies to a formal proof. The same human error that may make someone
miss an edge case in a transform can also make them overlook a missing detail in your
proof.
This should be doable with alive2, so please do so.

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


More information about the llvm-commits mailing list