From 5f86b04eecfe231d6c3e2e2788d0fbac162a973c Mon Sep 17 00:00:00 2001
From: myunbin <akim9905@gmail.com>
Date: Thu, 16 Apr 2026 09:45:03 +0900
Subject: [PATCH] [Cranelift] rule restore

---
 cranelift/codegen/src/opts/arithmetic.isle    | 78 +++++++++++++++++--
 cranelift/codegen/src/opts/bitops.isle        | 36 +++++++++
 .../filetests/egraph/arithmetic-precise.clif  | 69 +++++++---------
 .../filetests/egraph/fold-bitops.clif         | 27 +++----
 tests/disas/x64-optimize-vector-types.wat     | 22 +++---
 5 files changed, 153 insertions(+), 79 deletions(-)

diff --git a/cranelift/codegen/src/opts/arithmetic.isle b/cranelift/codegen/src/opts/arithmetic.isle
index d92ffedf7bbb..22390d42c2c7 100644
--- a/cranelift/codegen/src/opts/arithmetic.isle
+++ b/cranelift/codegen/src/opts/arithmetic.isle
@@ -321,6 +321,77 @@
 (rule (simplify (iadd ty (bnot ty x) x)) (iconst_s ty -1))
 (rule (simplify (iadd ty x (bnot ty x))) (iconst_s ty -1))
 
+;; ((x + y) - (x + z)) --> (y - z)
+(rule (simplify (isub ty (iadd ty x y) (iadd ty x z))) (isub ty y z))
+(rule (simplify (isub ty (iadd ty x y) (iadd ty z x))) (isub ty y z))
+(rule (simplify (isub ty (iadd ty y x) (iadd ty x z))) (isub ty y z))
+(rule (simplify (isub ty (iadd ty y x) (iadd ty z x))) (isub ty y z))
+
+;; ((x - z) - (y - z)) --> (x - y)
+(rule (simplify (isub ty (isub ty x z) (isub ty y z))) (isub ty x y))
+
+;; ((x - y) - (x - z)) --> (z - y)
+(rule (simplify (isub ty (isub ty x y) (isub ty x z))) (isub ty z y))
+
+;; umin(x, y) + umax(x, y) --> x + y
+(rule (simplify (iadd ty (umin ty x y) (umax ty x y))) (iadd ty x y))
+(rule (simplify (iadd ty (umax ty x y) (umin ty x y))) (iadd ty x y))
+(rule (simplify (iadd ty (umin ty x y) (umax ty y x))) (iadd ty x y))
+(rule (simplify (iadd ty (umax ty y x) (umin ty x y))) (iadd ty x y))
+(rule (simplify (iadd ty (umin ty y x) (umax ty x y))) (iadd ty x y))
+(rule (simplify (iadd ty (umax ty x y) (umin ty y x))) (iadd ty x y))
+(rule (simplify (iadd ty (umin ty y x) (umax ty y x))) (iadd ty x y))
+(rule (simplify (iadd ty (umax ty y x) (umin ty y x))) (iadd ty x y))
+
+;; smin(x, y) + smax(x, y) --> x + y
+(rule (simplify (iadd ty (smin ty x y) (smax ty x y))) (iadd ty x y))
+(rule (simplify (iadd ty (smax ty x y) (smin ty x y))) (iadd ty x y))
+(rule (simplify (iadd ty (smin ty x y) (smax ty y x))) (iadd ty x y))
+(rule (simplify (iadd ty (smax ty y x) (smin ty x y))) (iadd ty x y))
+(rule (simplify (iadd ty (smin ty y x) (smax ty x y))) (iadd ty x y))
+(rule (simplify (iadd ty (smax ty x y) (smin ty y x))) (iadd ty x y))
+(rule (simplify (iadd ty (smin ty y x) (smax ty y x))) (iadd ty x y))
+(rule (simplify (iadd ty (smax ty y x) (smin ty y x))) (iadd ty x y))
+
+;; ((x + z) - (y + z)) --> (x - y)
+(rule (simplify (isub ty (iadd ty x z) (iadd ty y z))) (isub ty x y))
+(rule (simplify (isub ty (iadd ty x z) (iadd ty z y))) (isub ty x y))
+(rule (simplify (isub ty (iadd ty z x) (iadd ty y z))) (isub ty x y))
+(rule (simplify (isub ty (iadd ty z x) (iadd ty z y))) (isub ty x y))
+
+;; ((x - y) + (y + z)) --> (x + z)
+(rule (simplify (iadd ty (isub ty x y) (iadd ty y z))) (iadd ty x z))
+(rule (simplify (iadd ty (iadd ty y z) (isub ty x y))) (iadd ty x z))
+(rule (simplify (iadd ty (isub ty x y) (iadd ty z y))) (iadd ty x z))
+(rule (simplify (iadd ty (iadd ty z y) (isub ty x y))) (iadd ty x z))
+
+;; (x - (x + y)) --> -y
+(rule (simplify (isub ty x (iadd ty x y))) (ineg ty y))
+(rule (simplify (isub ty x (iadd ty y x))) (ineg ty y))
+
+;; (x + (y + (z - x))) --> (y + z)
+(rule (simplify (iadd ty x (iadd ty y (isub ty z x)))) (iadd ty y z))
+(rule (simplify (iadd ty (iadd ty y (isub ty z x)) x)) (iadd ty y z))
+(rule (simplify (iadd ty x (iadd ty (isub ty z x) y))) (iadd ty y z))
+(rule (simplify (iadd ty (iadd ty (isub ty z x) y) x)) (iadd ty y z))
+
+;; Helper to create a "true" value for a comparison. For scalar integers this is
+;; a value of 1 but for vectors this is -1 since each lane is filled with all
+;; 1s.
+(decl cmp_true (Type) Value)
+(rule 0 (cmp_true (ty_int ty)) (iconst_u ty 1))
+(rule 1 (cmp_true (ty_vec128 ty)) (iconst_s ty -1))
+
+;; (x + y) == (y + x) --> true
+(rule (simplify (eq ty (iadd cty x y) (iadd cty y x))) (cmp_true ty))
+(rule (simplify (eq ty (iadd cty y x) (iadd cty x y))) (cmp_true ty))
+(rule (simplify (eq ty (iadd cty x y) (iadd cty x y))) (cmp_true ty))
+(rule (simplify (eq ty (iadd cty y x) (iadd cty y x))) (cmp_true ty))
+
+;; (x - y) != x --> y != 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)))
@@ -338,13 +409,6 @@
 (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))
 
-;; Helper to create a "true" value for a comparison. For scalar integers this is
-;; a value of 1 but for vectors this is -1 since each lane is filled with all
-;; 1s.
-(decl cmp_true (Type) Value)
-(rule 0 (cmp_true (ty_int ty)) (iconst_u ty 1))
-(rule 1 (cmp_true (ty_vec128 ty)) (iconst_s ty -1))
-
 ;; max(x, y) >= x
 (rule (simplify (sge ty (smax ty x y) x)) (cmp_true ty))
 (rule (simplify (sge ty (smax ty y x) x)) (cmp_true ty))
diff --git a/cranelift/codegen/src/opts/bitops.isle b/cranelift/codegen/src/opts/bitops.isle
index 0bc815a7f734..28b7f6f99a94 100644
--- a/cranelift/codegen/src/opts/bitops.isle
+++ b/cranelift/codegen/src/opts/bitops.isle
@@ -545,6 +545,42 @@
 (rule (simplify (bor ty y (band ty x (bnot ty y)))) (bor ty y x))
 (rule (simplify (bor ty (band ty x (bnot ty y)) y)) (bor ty y x))
 
+;; ((x & ~y) - (x & y)) --> ((x ^ y) - y)
+(rule (simplify (isub ty (band ty x (bnot ty y)) (band ty x y))) (isub ty (bxor ty x y) y))
+(rule (simplify (isub ty (band ty x (bnot ty y)) (band ty y x))) (isub ty (bxor ty x y) y))
+(rule (simplify (isub ty (band ty (bnot ty y) x) (band ty x y))) (isub ty (bxor ty x y) y))
+(rule (simplify (isub ty (band ty (bnot ty y) x) (band ty y x))) (isub ty (bxor ty x y) y))
+(rule (simplify (isub ty (band ty x y) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
+(rule (simplify (isub ty (band ty x y) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
+(rule (simplify (isub ty (band ty y x) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
+(rule (simplify (isub ty (band ty y x) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
+
+;; (x & ~y) | (~x & y) --> (x ^ y)
+(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty (bnot ty x) y))) (bxor ty x y))
+(rule (simplify (bor ty (band ty (bnot ty x) y) (band ty x (bnot ty y)))) (bxor ty x y))
+(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty y (bnot ty x)))) (bxor ty x y))
+(rule (simplify (bor ty (band ty y (bnot ty x)) (band ty x (bnot ty y)))) (bxor ty x y))
+(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty (bnot ty x) y))) (bxor ty x y))
+(rule (simplify (bor ty (band ty (bnot ty x) y) (band ty (bnot ty y) x))) (bxor ty x y))
+(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty y (bnot ty x)))) (bxor ty x y))
+(rule (simplify (bor ty (band ty y (bnot ty x)) (band ty (bnot ty y) x))) (bxor ty x y))
+
+;; (x & ~y) | (x ^ y) --> (x ^ y)
+(rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty x y))) (bxor ty x y))
+(rule (simplify (bor ty (bxor ty x y) (band ty x (bnot ty y)))) (bxor ty x y))
+(rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty y x))) (bxor ty x y))
+(rule (simplify (bor ty (bxor ty y x) (band ty x (bnot ty y)))) (bxor ty x y))
+(rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty x y))) (bxor ty x y))
+(rule (simplify (bor ty (bxor ty x y) (band ty (bnot ty y) x))) (bxor ty x y))
+(rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty y x))) (bxor ty x y))
+(rule (simplify (bor ty (bxor ty y x) (band ty (bnot ty y) x))) (bxor ty x y))
+
+;; (x & ~y) ^ ~x --> ~(x & y)
+(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)))
+
 ;; (~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))
diff --git a/cranelift/filetests/filetests/egraph/arithmetic-precise.clif b/cranelift/filetests/filetests/egraph/arithmetic-precise.clif
index dd6473f2edbd..b006c8aa3f81 100644
--- a/cranelift/filetests/filetests/egraph/arithmetic-precise.clif
+++ b/cranelift/filetests/filetests/egraph/arithmetic-precise.clif
@@ -96,10 +96,8 @@ block0(v0: i32, v1: i32, v2: i32):
 
 ; function %test_isub_iadd_iadd_cancel(i32, i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32, v2: i32):
-;     v3 = iadd v0, v1
-;     v4 = iadd v0, v2
-;     v5 = isub v3, v4
-;     return v5
+;     v6 = isub v1, v2
+;     return v6
 ; }
 
 ;; ((x - z) - (y - z)) --> (x - y)
@@ -113,10 +111,8 @@ block0(v0: i32, v1: i32, v2: i32):
 
 ; function %test_isub_isub_isub_cancel(i32, i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32, v2: i32):
-;     v3 = isub v0, v2
-;     v4 = isub v1, v2
-;     v5 = isub v3, v4
-;     return v5
+;     v6 = isub v0, v1
+;     return v6
 ; }
 
 ;; ((x - y) - (x - z)) --> (z - y)
@@ -130,10 +126,8 @@ block0(v0: i32, v1: i32, v2: i32):
 
 ; function %test_isub_isub_isub_swap_cancel(i32, i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32, v2: i32):
-;     v3 = isub v0, v1
-;     v4 = isub v0, v2
-;     v5 = isub v3, v4
-;     return v5
+;     v6 = isub v2, v1
+;     return v6
 ; }
 
 ;; umin(x, y) + umax(x, y) --> x + y
@@ -147,10 +141,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_iadd_umin_umax(i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = umin v0, v1
-;     v3 = umax v0, v1
-;     v4 = iadd v2, v3
-;     return v4
+;     v6 = iadd v1, v0
+;     return v6
 ; }
 
 ;; smin(x, y) + smax(x, y) --> x + y
@@ -164,10 +156,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_iadd_smin_smax(i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = smin v0, v1
-;     v3 = smax v0, v1
-;     v4 = iadd v2, v3
-;     return v4
+;     v6 = iadd v1, v0
+;     return v6
 ; }
 
 ;; ((x + z) - (y + z)) --> (x - y)
@@ -181,10 +171,8 @@ block0(v0: i32, v1: i32, v2: i32):
 
 ; function %test_isub_iadd_iadd_common_rhs(i32, i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32, v2: i32):
-;     v3 = iadd v0, v2
-;     v4 = iadd v1, v2
-;     v5 = isub v3, v4
-;     return v5
+;     v6 = isub v0, v1
+;     return v6
 ; }
 
 ;; ((x - y) + (y + z)) --> (x + z)
@@ -198,10 +186,8 @@ block0(v0: i32, v1: i32, v2: i32):
 
 ; function %test_iadd_isub_iadd_cancel(i32, i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32, v2: i32):
-;     v3 = isub v0, v1
-;     v4 = iadd v1, v2
-;     v5 = iadd v3, v4
-;     return v5
+;     v6 = iadd v0, v2
+;     return v6
 ; }
 
 ;; (x - (x + y)) --> -y
@@ -214,9 +200,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_isub_iadd_to_ineg(i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = iadd v0, v1
-;     v3 = isub v0, v2
-;     return v3
+;     v4 = ineg v1
+;     return v4
 ; }
 
 ;; (x + (y + (z - x))) --> (y + z)
@@ -230,10 +215,8 @@ block0(v0: i32, v1: i32, v2: i32):
 
 ; function %test_iadd_iadd_isub_cancel(i32, i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32, v2: i32):
-;     v3 = isub v2, v0
-;     v4 = iadd v1, v3
-;     v5 = iadd v0, v4
-;     return v5
+;     v6 = iadd v1, v2
+;     return v6
 ; }
 
 ;; (eq ty (iadd cty x y) (iadd cty y x)) -> 1
@@ -247,8 +230,8 @@ block0(v0: i32, v1: i32):
 
 ; function %simplify_icmp_eq_iadd_commute(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v6 = iconst.i8 1
-;     return v6  ; v6 = 1
+;     v5 = iconst.i8 1
+;     return v5  ; v5 = 1
 ; }
 
 ;; (eq ty (iadd cty x y) (iadd cty y x)) -> 1
@@ -261,9 +244,11 @@ block0(v0: i32x4, v1: i32x4):
 }
 
 ; function %simplify_vector_icmp_eq_iadd_commute(i32x4, i32x4) -> i32x4 fast {
+;     const0 = 0xffffffffffffffffffffffffffffffff
+;
 ; block0(v0: i32x4, v1: i32x4):
-;     v5 = icmp eq v0, v0
-;     return v5
+;     v9 = icmp eq v0, v0
+;     return v9
 ; }
 
 ;; (x - y) != x --> y != 0
@@ -276,9 +261,9 @@ block0(v0: i32, v1: i32):
 
 ; function %simplify_icmp_ne_isub_x(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = isub v0, v1
-;     v3 = icmp ne v2, v0
-;     return v3
+;     v4 = iconst.i32 0
+;     v5 = icmp ne v1, v4  ; v4 = 0
+;     return v5
 ; }
 
 ;; (x - y) == x --> y == 0
diff --git a/cranelift/filetests/filetests/egraph/fold-bitops.clif b/cranelift/filetests/filetests/egraph/fold-bitops.clif
index d02fcb177b17..b5e6d76f8053 100644
--- a/cranelift/filetests/filetests/egraph/fold-bitops.clif
+++ b/cranelift/filetests/filetests/egraph/fold-bitops.clif
@@ -213,11 +213,9 @@ block0(v0: i32, v1: i32):
 
 ; function %test_isub_band_band_bnot(i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = bnot v1
-;     v3 = band v0, v2
-;     v4 = band v0, v1
-;     v5 = isub v3, v4
-;     return v5
+;     v6 = bxor v0, v1
+;     v7 = isub v6, v1
+;     return v7
 ; }
 
 ;; (x & ~y) | (~x & y) --> (x ^ y)
@@ -233,12 +231,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_bor_band_bnot_to_bxor(i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = bnot v1
-;     v3 = band v0, v2
-;     v4 = bnot v0
-;     v5 = band v4, v1
-;     v6 = bor v3, v5
-;     return v6
+;     v8 = bxor v1, v0
+;     return v8
 ; }
 
 ;; (x & ~y) | (x ^ y) --> (x ^ y)
@@ -253,11 +247,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_bor_band_bnot_bxor_absorb(i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = bnot v1
-;     v3 = band v0, v2
 ;     v4 = bxor v0, v1
-;     v5 = bor v3, v4
-;     return v5
+;     return v4
 ; }
 
 ;; (x & ~y) ^ ~x --> ~(x & y)
@@ -272,9 +263,9 @@ block0(v0: i32, v1: i32):
 
 ; function %test_bxor_band_bnot_to_bnot_band(i32, i32) -> i32 fast {
 ; block0(v0: i32, v1: i32):
-;     v6 = band v1, v0
-;     v10 = bnot v6
-;     return v10
+;     v8 = band v1, v0
+;     v12 = bnot v8
+;     return v12
 ; }
 
 ;; (~x & y) ^ x --> x | y
diff --git a/tests/disas/x64-optimize-vector-types.wat b/tests/disas/x64-optimize-vector-types.wat
index 805e50f2f133..28316f6823fc 100644
--- a/tests/disas/x64-optimize-vector-types.wat
+++ b/tests/disas/x64-optimize-vector-types.wat
@@ -212,12 +212,11 @@
 ;; wasm[0]::function[9]:
 ;;       pushq   %rbp
 ;;       movq    %rsp, %rbp
-;;       movdqa  %xmm0, %xmm2
-;;       psubd   %xmm1, %xmm0
-;;       movdqa  %xmm2, %xmm1
-;;       pcmpeqd %xmm1, %xmm0
-;;       pcmpeqd %xmm1, %xmm1
-;;       pxor    %xmm1, %xmm0
+;;       pxor    %xmm0, %xmm0
+;;       pcmpeqd %xmm0, %xmm1
+;;       pcmpeqd %xmm2, %xmm2
+;;       movdqa  %xmm1, %xmm0
+;;       pxor    %xmm2, %xmm0
 ;;       movq    %rbp, %rsp
 ;;       popq    %rbp
 ;;       retq
@@ -244,12 +243,11 @@
 ;; wasm[0]::function[12]:
 ;;       pushq   %rbp
 ;;       movq    %rsp, %rbp
-;;       movdqa  %xmm0, %xmm2
-;;       psubw   %xmm1, %xmm0
-;;       movdqa  %xmm2, %xmm1
-;;       pcmpeqw %xmm1, %xmm0
-;;       pcmpeqd %xmm1, %xmm1
-;;       pxor    %xmm1, %xmm0
+;;       pxor    %xmm0, %xmm0
+;;       pcmpeqw %xmm0, %xmm1
+;;       pcmpeqd %xmm2, %xmm2
+;;       movdqa  %xmm1, %xmm0
+;;       pxor    %xmm2, %xmm0
 ;;       movq    %rbp, %rsp
 ;;       popq    %rbp
 ;;       retq