Skip to content
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

Jump to bottom

egraphs: Canonicalize loose inequalities to strict inequalities (2nd attempt) #9040

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

egraphs: Canonicalize loose inequalities to strict inequalities (2nd attempt) #9040

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
88cea55
test: regression test for issue #6185
Kmeakin Jul 27, 2024
978e7e6
egraphs: canonicalize `icmp`
Kmeakin Jul 27, 2024
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
44 changes: 42 additions & 2 deletions cranelift/codegen/src/opts/icmp.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,14 @@

;; Optimize icmp-of-icmp.
;; ne(icmp(ty, cc, x, y), 0) == icmp(ty, cc, x, y)
;; e.g. neq(ugt(x, y), 0) == ugt(x, y)
;; e.g. neq(ugt(x, y), 0) == ugt(x, y)
(rule (simplify (ne ty
(uextend_maybe _ inner @ (icmp ty _ _ _))
(iconst_u _ 0)))
(subsume inner))

;; eq(icmp(ty, cc, x, y), 0) == icmp(ty, cc_complement, x, y)
;; e.g. eq(ugt(x, y), 0) == ule(x, y)
;; e.g. eq(ugt(x, y), 0) == ule(x, y)
(rule (simplify (eq ty
(uextend_maybe _ (icmp ty cc x y))
(iconst_u _ 0)))
Expand Down Expand Up @@ -65,11 +65,36 @@
(iconst_u _ 1)))
extend)

;; Rewrite loose inequalities to strict inequalities:
;; ule(x, c) == ult(x, c+1), for c != UMAX.
(rule (simplify (ule (fits_in_64 (ty_int bty)) x (iconst cty (u64_from_imm64 c))))
(if-let $false (u64_eq c (ty_umax cty)))
(ult bty x (iconst cty (imm64 (u64_add c 1)))))

;; uge(x, c) == ugt(x, c-1), for c != 0.
(rule (simplify (uge (fits_in_64 (ty_int bty)) x (iconst cty (u64_from_imm64 c))))
(if-let $false (u64_eq c 0))
(ugt bty x (iconst cty (imm64 (u64_sub c 1)))))

;; sle(x, c) == slt(x, c+1), for c != SMAX.
(rule (simplify (sle (fits_in_64 (ty_int bty)) x (iconst cty (u64_from_imm64 c))))
(if-let $false (u64_eq c (ty_smax cty)))
(slt bty x (iconst cty (imm64 (u64_add c 1)))))

;; sge(x, c) == sgt(x, c-1), for c != SMIN.
;; (rule (simplify (sge (fits_in_64 (ty_int bty)) x (iconst cty (u64_from_imm64 c))))
;; (if-let $false (u64_eq c (ty_smin cty)))
;; (sgt bty x (iconst cty (imm64 (u64_sub c 1)))))

;; Comparisons against largest/smallest signed/unsigned values:
;; ult(x, 0) == false.
(rule (simplify (ult (fits_in_64 (ty_int bty)) x zero @ (iconst_u _ 0)))
(subsume (iconst_u bty 0)))

;; ult(x, 1) == eq(x, 0)
(rule (simplify (ult (fits_in_64 (ty_int bty)) x (iconst cty (u64_from_imm64 0))))
(eq bty x (iconst cty (imm64 0))))

;; ule(x, 0) == eq(x, 0)
(rule (simplify (ule (fits_in_64 (ty_int bty)) x zero @ (iconst_u _ 0)))
(eq bty x zero))
Expand All @@ -78,6 +103,11 @@
(rule (simplify (ugt (fits_in_64 (ty_int bty)) x zero @ (iconst_u _ 0)))
(ne bty x zero))

;; ugt(x, UMAX-1) == eq(x, UMAX).
(rule (simplify (ugt (fits_in_64 (ty_int bty)) x (iconst cty (u64_from_imm64 y))))
(if-let $true (u64_eq y (u64_sub (ty_umax cty) 1)))
(eq bty x (iconst cty (imm64 (ty_umax cty)))))

;; uge(x, 0) == true.
(rule (simplify (uge (fits_in_64 (ty_int bty)) x zero @ (iconst_u _ 0)))
(subsume (iconst_u bty 1)))
Expand Down Expand Up @@ -112,6 +142,11 @@
(if-let $true (u64_eq y (ty_smin cty)))
(eq bty x smin))

;; slt(x, SMIN+1) == eq(x, SMIN).
(rule (simplify (slt (fits_in_64 (ty_int bty)) x (iconst cty (u64_from_imm64 y))))
(if-let $true (u64_eq y (u64_add (ty_smin cty) 1)))
(eq bty x (iconst cty (imm64 (ty_smin cty)))))

;; sgt(x, SMIN) == ne(x, SMIN).
(rule (simplify (sgt (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
(if-let $true (u64_eq y (ty_smin cty)))
Expand Down Expand Up @@ -142,6 +177,11 @@
(if-let $true (u64_eq y (ty_smax cty)))
(eq bty x smax))

;; sgt(x, SMAX-1) == eq(x, SMAX).
(rule (simplify (sgt (fits_in_64 (ty_int bty)) x (iconst cty (u64_from_imm64 y))))
(if-let $true (u64_eq y (u64_sub (ty_smax cty) 1)))
(eq bty x (iconst cty (imm64 (ty_smax cty)))))

;; `band`/`bor` of 2 comparisons:
(rule (simplify (band (fits_in_64 ty) (icmp ty cc1 x y) (icmp ty cc2 x y)))
(if-let signed (intcc_comparable cc1 cc2))
Expand Down
12 changes: 6 additions & 6 deletions cranelift/filetests/filetests/egraph/cprop.clif
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -162,8 +162,8 @@ block0:
return v2
}

; check: v3 = iconst.i8 1
; nextln: return v3
; check: v5 = iconst.i8 1
; nextln: return v5

function %icmp_uge_i32() -> i8 {
block0:
Expand All @@ -173,8 +173,8 @@ block0:
return v2
}

; check: v3 = iconst.i8 0
; nextln: return v3
; check: v4 = iconst.i8 0
; nextln: return v4

function %icmp_ugt_i32() -> i8 {
block0:
Expand Down Expand Up @@ -206,8 +206,8 @@ block0:
return v2
}

; check: v3 = iconst.i8 1
; nextln: return v3
; check: v5 = iconst.i8 1
; nextln: return v5

function %icmp_sge_i32() -> i8 {
block0:
Expand Down
Loading