Skip to content

[Cranelift] add simplification rules #12978

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
+416 −2
Open

[Cranelift] add simplification rules #12978

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
138 changes: 137 additions & 1 deletion cranelift/codegen/src/opts/arithmetic.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -436,4 +436,140 @@
(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))
(rule (simplify (ule ty (umin ty y x) x)) (iconst_u ty 1))

;; min/max(x,x) --> x
(rule (simplify (umin ty x x)) x)
(rule (simplify (smin ty x x)) x)
(rule (simplify (umax ty x x)) x)
(rule (simplify (smax ty x x)) x)

;; max(max(x, y), x) --> max(x, y)
(rule (simplify (smax ty (smax ty x y) x)) (smax ty x y))
(rule (simplify (smax ty (smax ty y x) x)) (smax ty x y))
(rule (simplify (smax ty x (smax ty x y))) (smax ty x y))
(rule (simplify (smax ty x (smax ty y x))) (smax ty x y))
(rule (simplify (umax ty (umax ty x y) x)) (umax ty x y))
(rule (simplify (umax ty (umax ty y x) x)) (umax ty x y))
(rule (simplify (umax ty x (umax ty x y))) (umax ty x y))
(rule (simplify (umax ty x (umax ty y x))) (umax ty x y))

;; min(min(x, y), x) --> min(x, y)
(rule (simplify (smin ty (smin ty x y) x)) (smin ty x y))
(rule (simplify (smin ty (smin ty y x) x)) (smin ty x y))
(rule (simplify (smin ty x (smin ty x y))) (smin ty x y))
(rule (simplify (smin ty x (smin ty y x))) (smin ty x y))
(rule (simplify (umin ty (umin ty x y) x)) (umin ty x y))
(rule (simplify (umin ty (umin ty y x) x)) (umin ty x y))
(rule (simplify (umin ty x (umin ty x y))) (umin ty x y))
(rule (simplify (umin ty x (umin ty y x))) (umin ty x y))

;; min(max(x, y), y) --> y ; max(min(x, y), y) --> y
(rule (simplify (smin ty (smax ty x y) y)) y)
(rule (simplify (smin ty (smax ty y x) y)) y)
(rule (simplify (smin ty y (smax ty x y))) y)
(rule (simplify (smin ty y (smax ty y x))) y)
(rule (simplify (umin ty (umax ty x y) y)) y)
(rule (simplify (umin ty (umax ty y x) y)) y)
(rule (simplify (umin ty y (umax ty x y))) y)
(rule (simplify (umin ty y (umax ty y x))) y)
(rule (simplify (smax ty (smin ty x y) y)) y)
(rule (simplify (smax ty (smin ty y x) y)) y)
(rule (simplify (smax ty y (smin ty x y))) y)
(rule (simplify (smax ty y (smin ty y x))) y)
(rule (simplify (umax ty (umin ty x y) y)) y)
(rule (simplify (umax ty (umin ty y x) y)) y)
(rule (simplify (umax ty y (umin ty x y))) y)
(rule (simplify (umax ty y (umin ty y x))) y)

;; min(min(x, y), max(x, y)) --> min(x,y)
(rule (simplify (smin ty (smax ty x y) (smin ty x y))) (smin ty x y))
(rule (simplify (smin ty (smax ty x y) (smin ty y x))) (smin ty x y))
(rule (simplify (smin ty (smax ty x y) (umin ty x y))) (umin ty x y))
(rule (simplify (smin ty (smax ty x y) (umin ty y x))) (umin ty x y))

(rule (simplify (smin ty (smin ty x y) (smax ty x y))) (smin ty x y))
(rule (simplify (smin ty (smin ty x y) (smax ty y x))) (smin ty x y))
(rule (simplify (smin ty (smin ty x y) (umax ty x y))) (smin ty x y))
(rule (simplify (smin ty (smin ty x y) (umax ty y x))) (smin ty x y))

(rule (simplify (smin ty (umax ty x y) (smin ty x y))) (smin ty x y))
(rule (simplify (smin ty (umax ty x y) (smin ty y x))) (smin ty x y))
(rule (simplify (smin ty (umax ty x y) (umin ty x y))) (smin ty x y))
(rule (simplify (smin ty (umax ty x y) (umin ty y x))) (smin ty x y))

(rule (simplify (smin ty (umin ty x y) (smax ty x y))) (umin ty x y))
(rule (simplify (smin ty (umin ty x y) (smax ty y x))) (umin ty x y))
(rule (simplify (smin ty (umin ty x y) (umax ty x y))) (smin ty x y))
(rule (simplify (smin ty (umin ty x y) (umax ty y x))) (smin ty x y))

(rule (simplify (umin ty (smax ty x y) (smin ty x y))) (umin ty x y))
(rule (simplify (umin ty (smax ty x y) (smin ty y x))) (umin ty x y))
(rule (simplify (umin ty (smax ty x y) (umin ty x y))) (umin ty x y))
(rule (simplify (umin ty (smax ty x y) (umin ty y x))) (umin ty x y))

(rule (simplify (umin ty (smin ty x y) (smax ty x y))) (umin ty x y))
(rule (simplify (umin ty (smin ty x y) (smax ty y x))) (umin ty x y))
(rule (simplify (umin ty (smin ty x y) (umax ty x y))) (smin ty x y))
(rule (simplify (umin ty (smin ty x y) (umax ty y x))) (smin ty x y))

(rule (simplify (umin ty (umax ty x y) (smin ty x y))) (smin ty x y))
(rule (simplify (umin ty (umax ty x y) (smin ty y x))) (smin ty x y))
(rule (simplify (umin ty (umax ty x y) (umin ty x y))) (umin ty x y))
(rule (simplify (umin ty (umax ty x y) (umin ty y x))) (umin ty x y))

(rule (simplify (umin ty (umin ty x y) (smax ty x y))) (umin ty x y))
(rule (simplify (umin ty (umin ty x y) (smax ty y x))) (umin ty x y))
(rule (simplify (umin ty (umin ty x y) (umax ty x y))) (umin ty x y))
(rule (simplify (umin ty (umin ty x y) (umax ty y x))) (umin ty x y))

;; max(min(x, y), max(x, y)) --> max(x, y)
(rule (simplify (smax ty (smax ty x y) (smin ty x y))) (smax ty x y))
(rule (simplify (smax ty (smax ty x y) (smin ty y x))) (smax ty x y))
(rule (simplify (smax ty (smax ty x y) (umin ty x y))) (smax ty x y))
(rule (simplify (smax ty (smax ty x y) (umin ty y x))) (smax ty x y))

(rule (simplify (smax ty (smin ty x y) (smax ty x y))) (smax ty x y))
(rule (simplify (smax ty (smin ty x y) (smax ty y x))) (smax ty x y))
(rule (simplify (smax ty (smin ty x y) (umax ty x y))) (umax ty x y))
(rule (simplify (smax ty (smin ty x y) (umax ty y x))) (umax ty x y))

(rule (simplify (smax ty (umax ty x y) (smin ty x y))) (umax ty x y))
(rule (simplify (smax ty (umax ty x y) (smin ty y x))) (umax ty x y))
(rule (simplify (smax ty (umax ty x y) (umin ty x y))) (smax ty x y))
(rule (simplify (smax ty (umax ty x y) (umin ty y x))) (smax ty x y))

(rule (simplify (smax ty (umin ty x y) (smax ty x y))) (smax ty x y))
(rule (simplify (smax ty (umin ty x y) (smax ty y x))) (smax ty x y))
(rule (simplify (smax ty (umin ty x y) (umax ty x y))) (smax ty x y))
(rule (simplify (smax ty (umin ty x y) (umax ty y x))) (smax ty x y))

(rule (simplify (umax ty (smax ty x y) (smin ty x y))) (umax ty x y))
(rule (simplify (umax ty (smax ty x y) (smin ty y x))) (umax ty x y))
(rule (simplify (umax ty (smax ty x y) (umin ty x y))) (smax ty x y))
(rule (simplify (umax ty (smax ty x y) (umin ty y x))) (smax ty x y))

(rule (simplify (umax ty (smin ty x y) (smax ty x y))) (umax ty x y))
(rule (simplify (umax ty (smin ty x y) (smax ty y x))) (umax ty x y))
(rule (simplify (umax ty (smin ty x y) (umax ty x y))) (umax ty x y))
(rule (simplify (umax ty (smin ty x y) (umax ty y x))) (umax ty x y))

(rule (simplify (umax ty (umax ty x y) (smin ty x y))) (umax ty x y))
(rule (simplify (umax ty (umax ty x y) (smin ty y x))) (umax ty x y))
(rule (simplify (umax ty (umax ty x y) (umin ty x y))) (umax ty x y))
(rule (simplify (umax ty (umax ty x y) (umin ty y x))) (umax ty x y))

(rule (simplify (umax ty (umin ty x y) (smax ty x y))) (smax ty x y))
(rule (simplify (umax ty (umin ty x y) (smax ty y x))) (smax ty x y))
(rule (simplify (umax ty (umin ty x y) (umax ty x y))) (umax ty x y))
(rule (simplify (umax ty (umin ty x y) (umax ty y x))) (umax ty x y))

;; x > max(x, y) --> 0
(rule (simplify (sgt ty x (smax ty x y))) (iconst_u ty 0))
(rule (simplify (sgt ty x (smax ty y x))) (iconst_u ty 0))
(rule (simplify (slt ty (smax ty x y) x)) (iconst_u ty 0))
(rule (simplify (slt ty (smax ty y x) x)) (iconst_u ty 0))
(rule (simplify (ugt ty x (umax ty x y))) (iconst_u ty 0))
(rule (simplify (ugt ty x (umax ty y x))) (iconst_u ty 0))
(rule (simplify (ult ty (umax ty x y) x)) (iconst_u ty 0))
(rule (simplify (ult ty (umax ty y x) x)) (iconst_u ty 0))
160 changes: 160 additions & 0 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 @@ -432,3 +432,163 @@ block0(v0: i32, v1: i32):
; return v3
; }

;; umin(x, x) --> x
function %test_umin_same(i32) -> i32 fast {
block0(v0: i32):
v1 = umin v0, v0
return v1
}

; function %test_umin_same(i32) -> i32 fast {
; block0(v0: i32):
; return v0
; }

;; smin(x, x) --> x
function %test_smin_same(i32) -> i32 fast {
block0(v0: i32):
v1 = smin v0, v0
return v1
}

; function %test_smin_same(i32) -> i32 fast {
; block0(v0: i32):
; return v0
; }

;; umax(x, x) --> x
function %test_umax_same(i32) -> i32 fast {
block0(v0: i32):
v1 = umax v0, v0
return v1
}

; function %test_umax_same(i32) -> i32 fast {
; block0(v0: i32):
; return v0
; }

;; smax(x, x) --> x
function %test_smax_same(i32) -> i32 fast {
block0(v0: i32):
v1 = smax v0, v0
return v1
}

; function %test_smax_same(i32) -> i32 fast {
; block0(v0: i32):
; return v0
; }

;; smax(smax(x, y), x) --> smax(x, y)
function %test_smax_nested_absorb(i32, i32) -> i32 fast {
block0(v0: i32, v1: i32):
v2 = smax v0, v1
v3 = smax v2, v0
return v3
}

; function %test_smax_nested_absorb(i32, i32) -> i32 fast {
; block0(v0: i32, v1: i32):
; v2 = smax v0, v1
; return v2
; }

;; umax(umax(x, y), x) --> umax(x, y)
function %test_umax_nested_absorb(i32, i32) -> i32 fast {
block0(v0: i32, v1: i32):
v2 = umax v0, v1
v3 = umax v2, v0
return v3
}

; function %test_umax_nested_absorb(i32, i32) -> i32 fast {
; block0(v0: i32, v1: i32):
; v2 = umax v0, v1
; return v2
; }

;; smin(smin(x, y), x) --> smin(x, y)
function %test_smin_nested_absorb(i32, i32) -> i32 fast {
block0(v0: i32, v1: i32):
v2 = smin v0, v1
v3 = smin v2, v0
return v3
}

; function %test_smin_nested_absorb(i32, i32) -> i32 fast {
; block0(v0: i32, v1: i32):
; v2 = smin v0, v1
; return v2
; }

;; umin(umin(x, y), x) --> umin(x, y)
function %test_umin_nested_absorb(i32, i32) -> i32 fast {
block0(v0: i32, v1: i32):
v2 = umin v0, v1
v3 = umin v2, v0
return v3
}

; function %test_umin_nested_absorb(i32, i32) -> i32 fast {
; block0(v0: i32, v1: i32):
; v2 = umin v0, v1
; return v2
; }

;; smin(smax(x, y), y) --> y
function %test_smin_smax_absorb(i32, i32) -> i32 fast {
block0(v0: i32, v1: i32):
v2 = smax v0, v1
v3 = smin v2, v1
return v3
}

; function %test_smin_smax_absorb(i32, i32) -> i32 fast {
; block0(v0: i32, v1: i32):
; return v1
; }

;; umax(umin(x, y), y) --> y
function %test_umax_umin_absorb(i32, i32) -> i32 fast {
block0(v0: i32, v1: i32):
v2 = umin v0, v1
v3 = umax v2, v1
return v3
}

; function %test_umax_umin_absorb(i32, i32) -> i32 fast {
; block0(v0: i32, v1: i32):
; return v1
; }

;; x > smax(x, y) --> false
function %test_sgt_x_smax(i32, i32) -> i8 fast {
block0(v0: i32, v1: i32):
v2 = smax v0, v1
v3 = icmp sgt v0, v2
return v3
}

; function %test_sgt_x_smax(i32, i32) -> i8 fast {
; block0(v0: i32, v1: i32):
; v2 = smax v0, v1
; v3 = icmp sgt v0, v2
; return v3
; }

;; x >_u umax(x, y) --> false
function %test_ugt_x_umax(i32, i32) -> i8 fast {
block0(v0: i32, v1: i32):
v2 = umax v0, v1
v3 = icmp ugt v0, v2
return v3
}

; function %test_ugt_x_umax(i32, i32) -> i8 fast {
; block0(v0: i32, v1: i32):
; v2 = umax v0, v1
; v3 = icmp ugt v0, v2
; return v3
; }

Loading
Loading