[Cranelift] add simplification rules

cranelift/codegen/src/opts/arithmetic.isle

@@ -386,5 +386,54 @@
 (rule (simplify (eq (ty_int ty) (iadd cty y x) (iadd cty y x))) (iconst_u ty 1))
 
 ;; (x - y) != x --> y != 0
-(rule (simplify (ne cty (isub (ty_int ty) x y) x)) (ne cty y (iconst_u ty 0)))
-(rule (simplify (ne cty x (isub (ty_int ty) x y))) (ne cty y (iconst_u ty 0)))
+(rule (simplify (ne cty (isub ty x y) x)) (ne cty y (iconst_u ty 0)))
+(rule (simplify (ne cty x (isub ty x y))) (ne cty y (iconst_u ty 0)))
+
+;; (x - y) == x --> y == 0
+(rule (simplify (eq cty (isub ty x y) x)) (eq cty y (iconst_u ty 0)))
+(rule (simplify (eq cty x (isub ty x y))) (eq cty y (iconst_u ty 0)))
+
+;; (x + y) == y --> x == 0
+(rule (simplify (eq cty (iadd ty x y) y)) (eq cty x (iconst_u ty 0)))
+(rule (simplify (eq cty (iadd ty y x) y)) (eq cty x (iconst_u ty 0)))
+(rule (simplify (eq cty y (iadd ty x y))) (eq cty x (iconst_u ty 0)))
+(rule (simplify (eq cty y (iadd ty y x))) (eq cty x (iconst_u ty 0)))
+
+;; -x == -y --> x == y
+(rule (simplify (eq ty (ineg ty x) (ineg ty y))) (eq ty x y))
+
+;; -((-y) * x) --> x * y
+(rule (simplify (ineg ty (imul ty (ineg ty y) x))) (imul ty x y))
+(rule (simplify (ineg ty (imul ty x (ineg ty y)))) (imul ty x y))
+
+;; ireduce(xext(a) + xext(b)) --> a + b
+(rule (simplify (ireduce ty (iadd cty (sextend cty x) (sextend cty y)))) (iadd ty x y))
+(rule (simplify (ireduce ty (iadd cty (sextend cty x) (uextend cty y)))) (iadd ty x y))
+(rule (simplify (ireduce ty (iadd cty (uextend cty x) (sextend cty y)))) (iadd ty x y))
+(rule (simplify (ireduce ty (iadd cty (uextend cty x) (uextend cty y)))) (iadd ty x y))
+
+;; ireduce(xext(a) - xext(b)) --> a - b
+(rule (simplify (ireduce ty (isub cty (sextend cty x) (sextend cty y)))) (isub ty x y))
+(rule (simplify (ireduce ty (isub cty (sextend cty x) (uextend cty y)))) (isub ty x y))
+(rule (simplify (ireduce ty (isub cty (uextend cty x) (sextend cty y)))) (isub ty x y))
+(rule (simplify (ireduce ty (isub cty (uextend cty x) (uextend cty y)))) (isub ty x y))
+
+;; max(x, y) >= x
+(rule (simplify (sge ty (smax ty x y) x)) (iconst_u ty 1))
+(rule (simplify (sge ty (smax ty y x) x)) (iconst_u ty 1))
+(rule (simplify (sle ty x (smax ty x y))) (iconst_u ty 1))
+(rule (simplify (sle ty x (smax ty y x))) (iconst_u ty 1))
+(rule (simplify (uge ty (umax ty x y) x)) (iconst_u ty 1))
+(rule (simplify (uge ty (umax ty y x) x)) (iconst_u ty 1))
+(rule (simplify (ule ty x (umax ty x y))) (iconst_u ty 1))
+(rule (simplify (ule ty x (umax ty y x))) (iconst_u ty 1))
+
+;; x >= min(x, y)
+(rule (simplify (sge ty x (smin ty x y))) (iconst_u ty 1))
+(rule (simplify (sge ty x (smin ty y x))) (iconst_u ty 1))
+(rule (simplify (sle ty (smin ty x y) x)) (iconst_u ty 1))
+(rule (simplify (sle ty (smin ty y x) x)) (iconst_u ty 1))
+(rule (simplify (uge ty x (umin ty x y))) (iconst_u ty 1))
+(rule (simplify (uge ty x (umin ty y x))) (iconst_u ty 1))
+(rule (simplify (ule ty (umin ty x y) x)) (iconst_u ty 1))
+(rule (simplify (ule ty (umin ty y x) x)) (iconst_u ty 1))

cranelift/codegen/src/opts/bitops.isle

@@ -696,4 +696,22 @@
 (rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty x y))) (bor ty x (bnot ty y)))
 (rule (simplify (bxor ty (bxor ty x y) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
 (rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty y x))) (bor ty x (bnot ty y)))
-(rule (simplify (bxor ty (bxor ty y x) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
+(rule (simplify (bxor ty (bxor ty y x) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
+
+;; (x & ~y) == ~y  <=>  (x | y) == -1
+(rule (simplify (eq rty (band cty (bnot cty y) x) (bnot cty y))) (eq rty (bor cty y x) (iconst_s cty -1)))
+(rule (simplify (eq rty (band cty x (bnot cty y)) (bnot cty y))) (eq rty (bor cty y x) (iconst_s cty -1)))
+(rule (simplify (eq rty (bnot cty y) (band cty (bnot cty y) x))) (eq rty (bor cty y x) (iconst_s cty -1)))
+(rule (simplify (eq rty (bnot cty y) (band cty x (bnot cty y)))) (eq rty (bor cty y x) (iconst_s cty -1)))
+
+;; x >=_u (x & y), and (x & y) <=_u x, are always true.
+(rule (simplify (uge ty x (band ty x y))) (iconst_u ty 1))
+(rule (simplify (uge ty x (band ty y x))) (iconst_u ty 1))
+(rule (simplify (ule ty (band ty x y) x)) (iconst_u ty 1))
+(rule (simplify (ule ty (band ty y x) x)) (iconst_u ty 1))
+
+;; (x | y) >=_u x, and x <=_u (x | y), are always true.
+(rule (simplify (uge ty (bor ty x y) x)) (iconst_u ty 1))
+(rule (simplify (uge ty (bor ty y x) x)) (iconst_u ty 1))
+(rule (simplify (ule ty x (bor ty x y))) (iconst_u ty 1))
+(rule (simplify (ule ty x (bor ty y x))) (iconst_u ty 1))

cranelift/filetests/filetests/egraph/arithmetic-precise.clif

@@ -264,17 +264,171 @@ block0(v0: i32, v1: i32):
 ;     return v5
 ; }
 
-;; (x - y) != x --> y != 0 (vector)
-function %simplify_vector_icmp_ne_isub_x(i32x4, i32x4) -> i32x4 fast {
-block0(v0: i32x4, v1: i32x4):
+;; (x - y) == x --> y == 0
+function %test_eq_isub_same(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
     v2 = isub v0, v1
-    v3 = icmp ne v2, v0
+    v3 = icmp eq v2, v0
     return v3
 }
 
-; function %simplify_vector_icmp_ne_isub_x(i32x4, i32x4) -> i32x4 fast {
-; block0(v0: i32x4, v1: i32x4):
-;     v2 = isub v0, v1
-;     v3 = icmp ne v2, v0
+; function %test_eq_isub_same(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v4 = iconst.i32 0
+;     v5 = icmp eq v1, v4  ; v4 = 0
+;     return v5
+; }
+
+;; (x + y) == y --> x == 0
+function %test_eq_iadd_same_rhs(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = iadd v0, v1
+    v3 = icmp eq v2, v1
+    return v3
+}
+
+; function %test_eq_iadd_same_rhs(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v4 = iconst.i32 0
+;     v5 = icmp eq v0, v4  ; v4 = 0
+;     return v5
+; }
+
+;; -x == -y --> x == y
+function %test_eq_ineg_ineg(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = ineg v0
+    v3 = ineg v1
+    v4 = icmp eq v2, v3
+    return v4
+}
+
+; function %test_eq_ineg_ineg(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = ineg v0
+;     v3 = ineg v1
+;     v4 = icmp eq v2, v3
+;     return v4
+; }
+
+;; -((-y) * x) --> x * y
+function %test_ineg_imul_ineg_lhs(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = ineg v1
+    v3 = imul v2, v0
+    v4 = ineg v3
+    return v4
+}
+
+; function %test_ineg_imul_ineg_lhs(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = imul v0, v1
+;     return v5
+; }
+
+function %test_ineg_imul_ineg_rhs(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = ineg v1
+    v3 = imul v0, v2
+    v4 = ineg v3
+    return v4
+}
+
+; function %test_ineg_imul_ineg_rhs(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = imul v0, v1
+;     return v5
+; }
+
+;; ireduce(sextend(x) + uextend(y)) --> x + y
+function %test_ireduce_iadd_extends(i8, i8) -> i8 fast {
+block0(v0: i8, v1: i8):
+    v2 = sextend.i16 v0
+    v3 = uextend.i16 v1
+    v4 = iadd v2, v3
+    v5 = ireduce.i8 v4
+    return v5
+}
+
+; function %test_ireduce_iadd_extends(i8, i8) -> i8 fast {
+; block0(v0: i8, v1: i8):
+;     v6 = iadd v0, v1
+;     return v6
+; }
+
+;; ireduce(sextend(x) - uextend(y)) --> x - y
+function %test_ireduce_isub_extends(i8, i8) -> i8 fast {
+block0(v0: i8, v1: i8):
+    v2 = sextend.i16 v0
+    v3 = uextend.i16 v1
+    v4 = isub v2, v3
+    v5 = ireduce.i8 v4
+    return v5
+}
+
+; function %test_ireduce_isub_extends(i8, i8) -> i8 fast {
+; block0(v0: i8, v1: i8):
+;     v6 = isub v0, v1
+;     return v6
+; }
+
+;; smax(x, y) >= x --> true
+function %test_sge_smax_x(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = smax v0, v1
+    v3 = icmp sge v2, v0
+    return v3
+}
+
+; function %test_sge_smax_x(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = smax v0, v1
+;     v3 = icmp sge v2, v0
+;     return v3
+; }
+
+;; x <=_u umax(x, y) --> true
+function %test_ule_x_umax(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = umax v0, v1
+    v3 = icmp ule v0, v2
+    return v3
+}
+
+; function %test_ule_x_umax(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = umax v0, v1
+;     v3 = icmp ule v0, v2
 ;     return v3
 ; }
+
+;; x >= smin(x, y) --> true
+function %test_sge_x_smin(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = smin v0, v1
+    v3 = icmp sge v0, v2
+    return v3
+}
+
+; function %test_sge_x_smin(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = smin v0, v1
+;     v3 = icmp sge v0, v2
+;     return v3
+; }
+
+;; umin(x, y) <=_u x --> true
+function %test_ule_umin_x(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = umin v0, v1
+    v3 = icmp ule v2, v0
+    return v3
+}
+
+; function %test_ule_umin_x(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = umin v0, v1
+;     v3 = icmp ule v2, v0
+;     return v3
+; }
+

cranelift/filetests/filetests/egraph/arithmetic.clif

@@ -363,8 +363,8 @@ block0(v0: i16, v1: i16, v2: i16):
     return v8
 }
 
-; check: v12 = iadd v0, v1
-; check: v15 = iadd v12, v2
+; check: v10 = iadd v0, v1
+; check: v15 = iadd v10, v2
 ; check: return v15
 
 ;; or(x, C) + (-C)  -->  and(x, ~C)

cranelift/filetests/filetests/egraph/extends.clif

@@ -179,8 +179,8 @@ block0(v0: i16, v1: i16):
     return v5
 }
 
-; check: v8 = iadd v0, v1
-; check: return v8
+; check: v6 = iadd v0, v1
+; check: return v6
 
 function %extend_bxor_reduce(i64, i64) -> i64 {
 block0(v0: i64, v1: i64):

cranelift/filetests/filetests/egraph/fold-bitops.clif

@@ -494,3 +494,80 @@ block0(v0: i32, v1: i32):
 ;     return v7
 ; }
 
+;; (x & ~y) == ~y --> (x | y) == -1
+function %test_eq_band_bnot_fullmask(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = bnot v1
+    v3 = band v0, v2
+    v4 = icmp eq v3, v2
+    return v4
+}
+
+; function %test_eq_band_bnot_fullmask(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = bor v1, v0
+;     v6 = iconst.i32 -1
+;     v7 = icmp eq v5, v6  ; v6 = -1
+;     return v7
+; }
+
+;; x >=_u (x & y) --> true
+function %test_uge_x_band(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = band v0, v1
+    v3 = icmp uge v0, v2
+    return v3
+}
+
+; function %test_uge_x_band(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = band v0, v1
+;     v3 = icmp uge v0, v2
+;     return v3
+; }
+
+;; (x & y) <=_u x --> true
+function %test_ule_band_x(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = band v0, v1
+    v3 = icmp ule v2, v0
+    return v3
+}
+
+; function %test_ule_band_x(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = band v0, v1
+;     v3 = icmp ule v2, v0
+;     return v3
+; }
+
+;; (x | y) >=_u x --> true
+function %test_uge_bor_x(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = bor v0, v1
+    v3 = icmp uge v2, v0
+    return v3
+}
+
+; function %test_uge_bor_x(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = bor v0, v1
+;     v3 = icmp uge v2, v0
+;     return v3
+; }
+
+;; x <=_u (x | y) --> true
+function %test_ule_x_bor(i32, i32) -> i8 fast {
+block0(v0: i32, v1: i32):
+    v2 = bor v0, v1
+    v3 = icmp ule v0, v2
+    return v3
+}
+
+; function %test_ule_x_bor(i32, i32) -> i8 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = bor v0, v1
+;     v3 = icmp ule v0, v2
+;     return v3
+; }
+