[Cranelift] (x * y) (==/!=) z --> x (==/!=) (y / z) (#11994)

* add opt

* add tests

* add tests

* update opt

* fix desc

* change desc

* fix

* fix

Author: bongjunj

cranelift/codegen/src/opts/arithmetic.isle

@@ -347,3 +347,48 @@
 ;; (x - y) - x => -y
 (rule (simplify (isub ty (isub ty x y) x))(ineg ty y))
 
+;; (x * C) (==/!=) D --> x (==/!=) (D / C) when C is odd and divides D
+(rule
+  (simplify (ne ty (iconst_u ty1 x) (imul ty1 y (iconst_u ty1 z))))
+  (if-let 0 (u64_rem x z))
+  (if-let 1 (u64_rem z 2))
+  (ne ty y (iconst ty1 (imm64 (u64_div x z)))))
+(rule
+  (simplify (ne ty (iconst_u ty1 x) (imul ty1 (iconst_u ty1 y) z)))
+  (if-let 0 (u64_rem x y))
+  (if-let 1 (u64_rem y 2))
+  (ne ty z (iconst ty1 (imm64 (u64_div x y)))))
+(rule
+  (simplify (ne ty (imul ty1 x (iconst_u ty1 y)) (iconst_u ty1 z)))
+  (if-let 0 (u64_rem z y))
+  (if-let 1 (u64_rem y 2))
+  (ne ty x (iconst ty1 (imm64 (u64_div z y)))))
+(rule
+  (simplify (ne ty (imul ty1 (iconst_u ty1 x) y) (iconst_u ty1 z)))
+  (if-let 0 (u64_rem z x))
+  (if-let 1 (u64_rem x 2))
+  (ne ty y (iconst ty1 (imm64 (u64_div z x)))))
+
+
+(rule
+  (simplify (eq ty (iconst_u ty1 x) (imul ty1 y (iconst_u ty1 z))))
+  (if-let 0 (u64_rem x z))
+  (if-let 1 (u64_rem z 2))
+  (eq ty y (iconst ty1 (imm64 (u64_div x z)))))
+(rule
+  (simplify (eq ty (iconst_u ty1 x) (imul ty1 (iconst_u ty1 y) z)))
+  (if-let 0 (u64_rem x y))
+  (if-let 1 (u64_rem y 2))
+  (eq ty z (iconst ty1 (imm64 (u64_div x y)))))
+(rule
+  (simplify (eq ty (imul ty1 x (iconst_u ty1 y)) (iconst_u ty1 z)))
+  (if-let 0 (u64_rem z y))
+  (if-let 1 (u64_rem y 2))
+  (eq ty x (iconst ty1 (imm64 (u64_div z y)))))
+(rule
+  (simplify (eq ty (imul ty1 (iconst_u ty1 x) y) (iconst_u ty1 z)))
+  (if-let 0 (u64_rem z x))
+  (if-let 1 (u64_rem x 2))
+  (eq ty y (iconst ty1 (imm64 (u64_div z x)))))
+
+

cranelift/filetests/filetests/egraph/arithmetic.clif

@@ -404,7 +404,6 @@ block0(v0: i32, v1: i32):
     ; check: return v5
 }
 
-
 ;; (x - y) - x => -y
 function %simplify_sub_sub_self(i32, i32) -> i32 {
 block0(v0: i32, v1: i32):
@@ -415,3 +414,28 @@ block0(v0: i32, v1: i32):
     ; check: return v4
 }
 
+;; (x * y) (==/!=) z --> x (==/!=) (y / z) when z is odd and divides y
+function %eq_mul_odd(i32) -> i8 {
+block0(v0: i32):
+	v1 = iconst.i32 7
+	v2 = iconst.i32 42
+  v3 = imul v0, v1
+  v4 = icmp eq v3, v2
+  return v4
+  ; check: v5 = iconst.i32 6
+  ; check: v6 = icmp eq v0, v5
+  ; return v6
+}
+
+function %ne_mul_odd(i32) -> i8 {
+block0(v0: i32):
+	v1 = iconst.i32 7
+	v2 = iconst.i32 42
+  v3 = imul v0, v1
+  v4 = icmp ne v3, v2
+  return v4
+  ; check: v5 = iconst.i32 6
+  ; check: v6 = icmp ne v0, v5
+  ; return v6
+}
+

cranelift/filetests/filetests/runtests/arithmetic.clif

@@ -608,3 +608,27 @@ block0(v0: i32, v1: i32):
 
 ; run: %simplify_sub_sub_self(42, 5) == -5
 
+;; (x * y) (==/!=) z --> x (==/!=) (y / z) when z is odd and divides y
+function %eq_mul_odd(i32) -> i8 {
+block0(v0: i32):
+	v1 = iconst.i32 7
+	v2 = iconst.i32 42
+  v3 = imul v0, v1
+  v4 = icmp eq v3, v2
+  return v4
+}
+
+; run: %eq_mul_odd(6) == 1
+; run: %eq_mul_odd(7) == 0
+
+function %ne_mul_odd(i32) -> i8 {
+block0(v0: i32):
+	v1 = iconst.i32 7
+	v2 = iconst.i32 42
+  v3 = imul v0, v1
+  v4 = icmp ne v3, v2
+  return v4
+}
+
+; run: %ne_mul_odd(6) == 0
+; run: %ne_mul_odd(7) == 1