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

This reverts commit 57e42d0c46.

Fixes #6185.
This commit is contained in:
Chris Fallin
2023-04-10 11:43:15 -07:00
committed by GitHub
parent dbd000c1ce
commit 8f1a7773a3
5 changed files with 78 additions and 711 deletions

View File

@@ -47,36 +47,11 @@
(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))
@@ -109,11 +84,6 @@
(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)))
@@ -124,11 +94,6 @@
(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)))
@@ -159,11 +124,6 @@
(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))