[Cranelift] add simplification rules (#12937)

Author: myunbin

cranelift/codegen/src/opts/bitops.isle

@@ -579,4 +579,121 @@
 (rule (simplify (bxor ty (band ty x (bnot ty y)) (bnot ty x))) (bnot ty (band ty x y)))
 (rule (simplify (bxor ty (bnot ty x) (band ty x (bnot ty y)))) (bnot ty (band ty x y)))
 (rule (simplify (bxor ty (band ty (bnot ty y) x) (bnot ty x))) (bnot ty (band ty x y)))
-(rule (simplify (bxor ty (bnot ty x) (band ty (bnot ty y) x))) (bnot ty (band ty x y)))
+(rule (simplify (bxor ty (bnot ty x) (band ty (bnot ty y) x))) (bnot ty (band ty x y)))
+
+;; (~x & y) ^ x --> x | y
+(rule (simplify (bxor ty (band ty (bnot ty x) y) x)) (bor ty x y))
+(rule (simplify (bxor ty x (band ty (bnot ty x) y))) (bor ty x y))
+(rule (simplify (bxor ty (band ty y (bnot ty x)) x)) (bor ty x y))
+(rule (simplify (bxor ty x (band ty y (bnot ty x)))) (bor ty x y))
+
+;; (x | y) & ~(x ^ y) --> x & y
+(rule (simplify (band ty (bor ty x y) (bnot ty (bxor ty x y)))) (band ty x y))
+(rule (simplify (band ty (bnot ty (bxor ty x y)) (bor ty x y))) (band ty x y))
+(rule (simplify (band ty (bor ty x y) (bnot ty (bxor ty y x)))) (band ty x y))
+(rule (simplify (band ty (bnot ty (bxor ty y x)) (bor ty x y))) (band ty x y))
+(rule (simplify (band ty (bor ty y x) (bnot ty (bxor ty x y)))) (band ty x y))
+(rule (simplify (band ty (bnot ty (bxor ty x y)) (bor ty y x))) (band ty x y))
+(rule (simplify (band ty (bor ty y x) (bnot ty (bxor ty y x)))) (band ty x y))
+(rule (simplify (band ty (bnot ty (bxor ty y x)) (bor ty y x))) (band ty x y))
+
+;; x | ~(x ^ y) --> x | ~y
+(rule (simplify (bor ty x (bnot ty (bxor ty x y)))) (bor ty x (bnot ty y)))
+(rule (simplify (bor ty (bnot ty (bxor ty x y)) x)) (bor ty x (bnot ty y)))
+(rule (simplify (bor ty x (bnot ty (bxor ty y x)))) (bor ty x (bnot ty y)))
+(rule (simplify (bor ty (bnot ty (bxor ty y x)) x)) (bor ty x (bnot ty y)))
+
+;; x | ((~x) ^ y) --> x | ~y
+(rule (simplify (bor ty x (bxor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
+(rule (simplify (bor ty (bxor ty (bnot ty x) y) x)) (bor ty x (bnot ty y)))
+(rule (simplify (bor ty x (bxor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
+(rule (simplify (bor ty (bxor ty y (bnot ty x)) x)) (bor ty x (bnot ty y)))
+
+;; x & ~(x ^ y) --> x & y
+(rule (simplify (band ty x (bnot ty (bxor ty x y)))) (band ty x y))
+(rule (simplify (band ty (bnot ty (bxor ty x y)) x)) (band ty x y))
+(rule (simplify (band ty x (bnot ty (bxor ty y x)))) (band ty x y))
+(rule (simplify (band ty (bnot ty (bxor ty y x)) x)) (band ty x y))
+
+;; x & ((~x) ^ y) --> x & y
+(rule (simplify (band ty x (bxor ty (bnot ty x) y))) (band ty x y))
+(rule (simplify (band ty (bxor ty (bnot ty x) y) x)) (band ty x y))
+(rule (simplify (band ty x (bxor ty y (bnot ty x)))) (band ty x y))
+(rule (simplify (band ty (bxor ty y (bnot ty x)) x)) (band ty x y))
+
+;; (x | y) | (x ^ y) --> (x | y)
+(rule (simplify (bor ty (bor ty x y) (bxor ty x y))) (bor ty x y))
+(rule (simplify (bor ty (bxor ty x y) (bor ty x y))) (bor ty x y))
+(rule (simplify (bor ty (bor ty x y) (bxor ty y x))) (bor ty x y))
+(rule (simplify (bor ty (bxor ty y x) (bor ty x y))) (bor ty x y))
+(rule (simplify (bor ty (bor ty y x) (bxor ty x y))) (bor ty x y))
+(rule (simplify (bor ty (bxor ty x y) (bor ty y x))) (bor ty x y))
+(rule (simplify (bor ty (bor ty y x) (bxor ty y x))) (bor ty x y))
+(rule (simplify (bor ty (bxor ty y x) (bor ty y x))) (bor ty x y))
+
+;; (x ^ y) & (x ^ (y ^ z)) --> (x ^ y) & ~z
+(rule (simplify (band ty (bxor ty x y) (bxor ty (bxor ty y z) x))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty (bxor ty y z) x) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty x y) (bxor ty x (bxor ty y z)))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty x (bxor ty y z)) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty x y) (bxor ty (bxor ty z y) x))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty (bxor ty z y) x) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty x y) (bxor ty x (bxor ty z y)))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty x (bxor ty z y)) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty y x) (bxor ty (bxor ty y z) x))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty (bxor ty y z) x) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty y x) (bxor ty x (bxor ty y z)))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty x (bxor ty y z)) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty y x) (bxor ty (bxor ty z y) x))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty (bxor ty z y) x) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty y x) (bxor ty x (bxor ty z y)))) (band ty (bxor ty x y) (bnot ty z)))
+(rule (simplify (band ty (bxor ty x (bxor ty z y)) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
+
+;; (~x & y) ^ z --> (x & y) ^ (z ^ y)
+(rule (simplify (bxor ty (band ty (bnot ty x) y) z)) (bxor ty (band ty x y) (bxor ty z y)))
+(rule (simplify (bxor ty z (band ty (bnot ty x) y))) (bxor ty (band ty x y) (bxor ty z y)))
+(rule (simplify (bxor ty (band ty y (bnot ty x)) z)) (bxor ty (band ty x y) (bxor ty z y)))
+(rule (simplify (bxor ty z (band ty y (bnot ty x)))) (bxor ty (band ty x y) (bxor ty z y)))
+
+;; ~x - ~y --> y - x
+(rule (simplify (isub ty (bnot ty x) (bnot ty y))) (isub ty y x))
+
+;; (~x & y) | ~(x | y) --> ~x
+(rule (simplify (bor ty (band ty (bnot ty x) y) (bnot ty (bor ty x y)))) (bnot ty x))
+(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty (bnot ty x) y))) (bnot ty x))
+(rule (simplify (bor ty (band ty (bnot ty x) y) (bnot ty (bor ty y x)))) (bnot ty x))
+(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty (bnot ty x) y))) (bnot ty x))
+(rule (simplify (bor ty (band ty y (bnot ty x)) (bnot ty (bor ty x y)))) (bnot ty x))
+(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty y (bnot ty x)))) (bnot ty x))
+(rule (simplify (bor ty (band ty y (bnot ty x)) (bnot ty (bor ty y x)))) (bnot ty x))
+(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty y (bnot ty x)))) (bnot ty x))
+
+;; (~x | y) & ~(x & y) --> ~x
+(rule (simplify (band ty (bor ty (bnot ty x) y) (bnot ty (band ty x y)))) (bnot ty x))
+(rule (simplify (band ty (bnot ty (band ty x y)) (bor ty (bnot ty x) y))) (bnot ty x))
+(rule (simplify (band ty (bor ty (bnot ty x) y) (bnot ty (band ty y x)))) (bnot ty x))
+(rule (simplify (band ty (bnot ty (band ty y x)) (bor ty (bnot ty x) y))) (bnot ty x))
+(rule (simplify (band ty (bor ty y (bnot ty x)) (bnot ty (band ty x y)))) (bnot ty x))
+(rule (simplify (band ty (bnot ty (band ty x y)) (bor ty y (bnot ty x)))) (bnot ty x))
+(rule (simplify (band ty (bor ty y (bnot ty x)) (bnot ty (band ty y x)))) (bnot ty x))
+(rule (simplify (band ty (bnot ty (band ty y x)) (bor ty y (bnot ty x)))) (bnot ty x))
+
+;; (x & y) | ~(x | y) --> ~(x ^ y)
+(rule (simplify (bor ty (band ty x y) (bnot ty (bor ty x y)))) (bnot ty (bxor ty x y)))
+(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty x y))) (bnot ty (bxor ty x y)))
+(rule (simplify (bor ty (band ty x y) (bnot ty (bor ty y x)))) (bnot ty (bxor ty x y)))
+(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty x y))) (bnot ty (bxor ty x y)))
+(rule (simplify (bor ty (band ty y x) (bnot ty (bor ty x y)))) (bnot ty (bxor ty x y)))
+(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty y x))) (bnot ty (bxor ty x y)))
+(rule (simplify (bor ty (band ty y x) (bnot ty (bor ty y x)))) (bnot ty (bxor ty x y)))
+(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty y x))) (bnot ty (bxor ty x y)))
+
+;; (~x | y) ^ (x ^ y) --> x | ~y
+(rule (simplify (bxor ty (bor ty (bnot ty x) y) (bxor ty x y))) (bor ty x (bnot ty y)))
+(rule (simplify (bxor ty (bxor ty x y) (bor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
+(rule (simplify (bxor ty (bor ty (bnot ty x) y) (bxor ty y x))) (bor ty x (bnot ty y)))
+(rule (simplify (bxor ty (bxor ty y x) (bor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
+(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)))

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

@@ -263,7 +263,234 @@ block0(v0: i32, v1: i32):
 
 ; function %test_bxor_band_bnot_to_bnot_band(i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32):
+;     v8 = band v1, v0
+;     v12 = bnot v8
+;     return v12
+; }
+
+;; (~x & y) ^ x --> x | y
+function %test_bxor_band_bnot_x(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bnot v0
+    v3 = band v2, v1
+    v4 = bxor v3, v0
+    return v4
+}
+
+; function %test_bxor_band_bnot_x(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = bor v0, v1
+;     return v5
+; }
+
+;; (x | y) & ~(x ^ y) --> x & y
+function %test_band_bor_bnot_bxor(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bor v0, v1
+    v3 = bxor v0, v1
+    v4 = bnot v3
+    v5 = band v2, v4
+    return v5
+}
+
+; function %test_band_bor_bnot_bxor(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v7 = band v1, v0
+;     return v7
+; }
+
+;; x | ~(x ^ y) --> x | ~y
+function %test_bor_bnot_bxor(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bxor v0, v1
+    v3 = bnot v2
+    v4 = bor v0, v3
+    return v4
+}
+
+; function %test_bor_bnot_bxor(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = bnot v1
+;     v6 = bor v0, v5
+;     return v6
+; }
+
+;; x | ((~x) ^ y) --> x | ~y
+function %test_bor_bxor_bnot_x(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bnot v0
+    v3 = bxor v2, v1
+    v4 = bor v0, v3
+    return v4
+}
+
+; function %test_bor_bxor_bnot_x(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = bnot v1
+;     v6 = bor v0, v5
+;     return v6
+; }
+
+;; x & ~(x ^ y) --> x & y
+function %test_band_bnot_bxor(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bxor v0, v1
+    v3 = bnot v2
+    v4 = band v0, v3
+    return v4
+}
+
+; function %test_band_bnot_bxor(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = band v0, v1
+;     return v5
+; }
+
+;; x & ((~x) ^ y) --> x & y
+function %test_band_bxor_bnot_x(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bnot v0
+    v3 = bxor v2, v1
+    v4 = band v0, v3
+    return v4
+}
+
+; function %test_band_bxor_bnot_x(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = band v0, v1
+;     return v5
+; }
+
+;; (x | y) | (x ^ y) --> (x | y)
+function %test_bor_bor_bxor_same(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bor v0, v1
+    v3 = bxor v0, v1
+    v4 = bor v2, v3
+    return v4
+}
+
+; function %test_bor_bor_bxor_same(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = bor v1, v0
+;     return v5
+; }
+
+;; (x ^ y) & ((y ^ z) ^ x) --> (x ^ y) & ~z
+function %test_band_bxor_bxor_bnot(i32, i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32, v2: i32):
+    v3 = bxor v0, v1
+    v4 = bxor v1, v2
+    v5 = bxor v4, v0
+    v6 = band v3, v5
+    return v6
+}
+
+; function %test_band_bxor_bxor_bnot(i32, i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32, v2: i32):
+;     v3 = bxor v0, v1
+;     v7 = bnot v2
+;     v8 = band v3, v7
+;     return v8
+; }
+
+;; (~x & y) ^ z --> (x & y) ^ (z ^ y)
+function %test_bxor_band_bnot_general(i32, i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32, v2: i32):
+    v3 = bnot v0
+    v4 = band v3, v1
+    v5 = bxor v4, v2
+    return v5
+}
+
+; function %test_bxor_band_bnot_general(i32, i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32, v2: i32):
 ;     v6 = band v0, v1
-;     v7 = bnot v6
+;     v7 = bxor v2, v1
+;     v8 = bxor v6, v7
+;     return v8
+; }
+
+;; ~x - ~y --> y - x
+function %test_isub_bnot_bnot(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bnot v0
+    v3 = bnot v1
+    v4 = isub v2, v3
+    return v4
+}
+
+; function %test_isub_bnot_bnot(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v5 = isub v1, v0
+;     return v5
+; }
+
+;; (~x & y) | ~(x | y) --> ~x
+function %test_bor_band_bnot_bor_to_bnot(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bnot v0
+    v3 = band v2, v1
+    v4 = bor v0, v1
+    v5 = bnot v4
+    v6 = bor v3, v5
+    return v6
+}
+
+; function %test_bor_band_bnot_bor_to_bnot(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = bnot v0
+;     return v2
+; }
+
+;; (~x | y) & ~(x & y) --> ~x
+function %test_band_bor_bnot_band_to_bnot(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bnot v0
+    v3 = bor v2, v1
+    v4 = band v0, v1
+    v5 = bnot v4
+    v6 = band v3, v5
+    return v6
+}
+
+; function %test_band_bor_bnot_band_to_bnot(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v2 = bnot v0
+;     return v2
+; }
+
+;; (x & y) | ~(x | y) --> ~(x ^ y)
+function %test_bor_band_bnot_bor_to_bnot_bxor(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = band v0, v1
+    v3 = bor v0, v1
+    v4 = bnot v3
+    v5 = bor v2, v4
+    return v5
+}
+
+; function %test_bor_band_bnot_bor_to_bnot_bxor(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v8 = bxor v1, v0
+;     v9 = bnot v8
+;     return v9
+; }
+
+;; (~x | y) ^ (x ^ y) --> x | ~y
+function %test_bxor_bor_bnot_bxor(i32, i32) -> i32 fast {
+block0(v0: i32, v1: i32):
+    v2 = bnot v0
+    v3 = bor v2, v1
+    v4 = bxor v0, v1
+    v5 = bxor v3, v4
+    return v5
+}
+
+; function %test_bxor_bor_bnot_bxor(i32, i32) -> i32 fast {
+; block0(v0: i32, v1: i32):
+;     v6 = bnot v1
+;     v7 = bor v0, v6
 ;     return v7
 ; }
+