ISLE: rewrite loose inequalities to strict inequalities and strict inequalities to equalities (#6130)

* ISLE: rewrite loose inequalities to strict inequalities

* Rewrite strict inequalities to equalities where possible
This commit is contained in:
Karl Meakin
2023-04-04 18:42:19 +01:00
committed by GitHub
parent c35c047fc3
commit 57e42d0c46
5 changed files with 711 additions and 78 deletions

View File

@@ -47,11 +47,36 @@
(iconst _ (u64_from_imm64 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 _ (u64_from_imm64 0))))
(subsume (iconst bty (imm64 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 _ (u64_from_imm64 0))))
(eq bty x zero))
@@ -84,6 +109,11 @@
(if-let $true (u64_eq y (ty_umax cty)))
(eq bty x umax))
;; 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)))))
;; slt(x, SMIN) == false.
(rule (simplify (slt (fits_in_64 (ty_int bty)) x smin @ (iconst cty (u64_from_imm64 y))))
(if-let $true (u64_eq y (ty_smin cty)))
@@ -94,6 +124,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 cty (u64_from_imm64 y))))
(if-let $true (u64_eq y (ty_smin cty)))
@@ -124,6 +159,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 ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
(if-let signed (intcc_comparable cc1 cc2))