Skip to content

[Cranelift] rule restore from #13081 #13119

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
myunbin wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[Cranelift] rule restore from #13081 #13119

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 71 additions & 7 deletions cranelift/codegen/src/opts/arithmetic.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand All @@ -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))
Expand Down
36 changes: 36 additions & 0 deletions cranelift/codegen/src/opts/bitops.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
69 changes: 27 additions & 42 deletions cranelift/filetests/filetests/egraph/arithmetic-precise.clif
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
27 changes: 9 additions & 18 deletions cranelift/filetests/filetests/egraph/fold-bitops.clif
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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
Expand Down
22 changes: 10 additions & 12 deletions tests/disas/x64-optimize-vector-types.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
Loading