ISLE: move icmp rewrites to separate file. (#6120)
* ISLE: move `icmp` rewrites to separate file. Move `icmp`-related rewrite rules from `algebraic.isle` to `icmp.isle`. Also move `icmp`-related tests from `algebraic.clif` to `icmp.clif`. * Put parameterized and unparameterized `icmp` tests in separate files * Undo refactoring of (ir)reflexivity rewrites * Fix `icmp-parameterised.clif` * Undo formatting/comment changes
This commit is contained in:
@@ -220,11 +220,12 @@ fn get_isle_compilations(
|
|||||||
output: out_dir.join("isle_opt.rs"),
|
output: out_dir.join("isle_opt.rs"),
|
||||||
inputs: vec![
|
inputs: vec![
|
||||||
prelude_isle.clone(),
|
prelude_isle.clone(),
|
||||||
prelude_opt_isle.clone(),
|
prelude_opt_isle,
|
||||||
src_opts.join("algebraic.isle"),
|
src_opts.join("algebraic.isle"),
|
||||||
|
src_opts.join("icmp.isle"),
|
||||||
src_opts.join("cprop.isle"),
|
src_opts.join("cprop.isle"),
|
||||||
],
|
],
|
||||||
untracked_inputs: vec![clif_opt_isle.clone()],
|
untracked_inputs: vec![clif_opt_isle],
|
||||||
},
|
},
|
||||||
// The x86-64 instruction selector.
|
// The x86-64 instruction selector.
|
||||||
IsleCompilation {
|
IsleCompilation {
|
||||||
|
|||||||
@@ -322,151 +322,11 @@
|
|||||||
(rule (simplify x @ (f64const _ _))
|
(rule (simplify x @ (f64const _ _))
|
||||||
(remat x))
|
(remat x))
|
||||||
|
|
||||||
;; Optimize icmp-of-icmp.
|
|
||||||
(rule (simplify (ne ty
|
|
||||||
(uextend _ inner @ (icmp ty _ _ _))
|
|
||||||
(iconst _ (u64_from_imm64 0))))
|
|
||||||
(subsume inner))
|
|
||||||
|
|
||||||
(rule (simplify (eq ty
|
|
||||||
(uextend _ (icmp ty cc x y))
|
|
||||||
(iconst _ (u64_from_imm64 0))))
|
|
||||||
(subsume (icmp ty (intcc_inverse cc) x y)))
|
|
||||||
|
|
||||||
;; Optimize select-of-uextend-of-icmp to select-of-icmp, because
|
|
||||||
;; select can take an I8 condition too.
|
|
||||||
(rule (simplify
|
|
||||||
(select ty (uextend _ c @ (icmp _ _ _ _)) x y))
|
|
||||||
(select ty c x y))
|
|
||||||
(rule (simplify
|
|
||||||
(select ty (uextend _ c @ (icmp _ _ _ _)) x y))
|
|
||||||
(select ty c x y))
|
|
||||||
|
|
||||||
;; `x == x` is always true for integers; `x != x` is false. Strict
|
|
||||||
;; inequalities are false, and loose inequalities are true.
|
|
||||||
(rule (simplify (eq (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
|
||||||
(rule (simplify (ne (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
|
||||||
(rule (simplify (ugt (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
|
||||||
(rule (simplify (uge (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
|
||||||
(rule (simplify (sgt (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
|
||||||
(rule (simplify (sge (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
|
||||||
(rule (simplify (ult (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
|
||||||
(rule (simplify (ule (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
|
||||||
(rule (simplify (slt (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
|
||||||
(rule (simplify (sle (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
|
||||||
|
|
||||||
;; (x ^ -1) can be replaced with the `bnot` instruction
|
;; (x ^ -1) can be replaced with the `bnot` instruction
|
||||||
(rule (simplify (bxor ty x (iconst ty k)))
|
(rule (simplify (bxor ty x (iconst ty k)))
|
||||||
(if-let -1 (i64_sextend_imm64 ty k))
|
(if-let -1 (i64_sextend_imm64 ty k))
|
||||||
(bnot ty x))
|
(bnot ty x))
|
||||||
|
|
||||||
|
|
||||||
;; Masking the result of a comparison with 1 always results in the comparison
|
|
||||||
;; itself. Note that comparisons in wasm may sometimes be hidden behind
|
|
||||||
;; extensions.
|
|
||||||
(rule (simplify
|
|
||||||
(band (ty_int _)
|
|
||||||
cmp @ (icmp _ _ _ _)
|
|
||||||
(iconst _ (u64_from_imm64 1))))
|
|
||||||
cmp)
|
|
||||||
(rule (simplify
|
|
||||||
(band (ty_int _)
|
|
||||||
extend @ (uextend _ (icmp _ _ _ _))
|
|
||||||
(iconst _ (u64_from_imm64 1))))
|
|
||||||
extend)
|
|
||||||
|
|
||||||
;; 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))))
|
|
||||||
|
|
||||||
;; 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))
|
|
||||||
|
|
||||||
;; ugt(x, 0) == ne(x, 0).
|
|
||||||
(rule (simplify
|
|
||||||
(ugt (fits_in_64 (ty_int bty)) x zero @ (iconst _ (u64_from_imm64 0))))
|
|
||||||
(ne bty x zero))
|
|
||||||
|
|
||||||
;; uge(x, 0) == true.
|
|
||||||
(rule (simplify
|
|
||||||
(uge (fits_in_64 (ty_int bty)) x zero @ (iconst _ (u64_from_imm64 0))))
|
|
||||||
(subsume (iconst bty (imm64 1))))
|
|
||||||
|
|
||||||
;; ult(x, UMAX) == ne(x, UMAX).
|
|
||||||
(rule (simplify
|
|
||||||
(ult (fits_in_64 (ty_int bty)) x umax @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_umax cty)))
|
|
||||||
(ne bty x umax))
|
|
||||||
|
|
||||||
;; ule(x, UMAX) == true.
|
|
||||||
(rule (simplify
|
|
||||||
(ule (fits_in_64 (ty_int bty)) x umax @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_umax cty)))
|
|
||||||
(subsume (iconst bty (imm64 1))))
|
|
||||||
|
|
||||||
;; ugt(x, UMAX) == false.
|
|
||||||
(rule (simplify
|
|
||||||
(ugt (fits_in_64 (ty_int bty)) x umax @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_umax cty)))
|
|
||||||
(subsume (iconst bty (imm64 0))))
|
|
||||||
|
|
||||||
;; uge(x, UMAX) == eq(x, UMAX).
|
|
||||||
(rule (simplify
|
|
||||||
(uge (fits_in_64 (ty_int bty)) x umax @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_umax cty)))
|
|
||||||
(eq bty x umax))
|
|
||||||
|
|
||||||
;; 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)))
|
|
||||||
(subsume (iconst bty (imm64 0))))
|
|
||||||
|
|
||||||
;; sle(x, SMIN) == eq(x, SMIN).
|
|
||||||
(rule (simplify
|
|
||||||
(sle (fits_in_64 (ty_int bty)) x smin @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_smin cty)))
|
|
||||||
(eq bty x smin))
|
|
||||||
|
|
||||||
;; 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)))
|
|
||||||
(ne bty x smin))
|
|
||||||
|
|
||||||
;; sge(x, SMIN) == true.
|
|
||||||
(rule (simplify
|
|
||||||
(sge (fits_in_64 (ty_int bty)) x smin @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_smin cty)))
|
|
||||||
(subsume (iconst bty (imm64 1))))
|
|
||||||
|
|
||||||
;; slt(x, SMAX) == ne(x, SMAX).
|
|
||||||
(rule (simplify
|
|
||||||
(slt (fits_in_64 (ty_int bty)) x smax @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_smax cty)))
|
|
||||||
(ne bty x smax))
|
|
||||||
|
|
||||||
;; sle(x, SMAX) == true.
|
|
||||||
(rule (simplify
|
|
||||||
(sle (fits_in_64 (ty_int bty)) x smax @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_smax cty)))
|
|
||||||
(subsume (iconst bty (imm64 1))))
|
|
||||||
|
|
||||||
;; sgt(x, SMAX) == false.
|
|
||||||
(rule (simplify
|
|
||||||
(sgt (fits_in_64 (ty_int bty)) x smax @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_smax cty)))
|
|
||||||
(subsume (iconst bty (imm64 0))))
|
|
||||||
|
|
||||||
;; sge(x, SMAX) == eq(x, SMAX).
|
|
||||||
(rule (simplify
|
|
||||||
(sge (fits_in_64 (ty_int bty)) x smax @ (iconst cty (u64_from_imm64 y))))
|
|
||||||
(if-let $true (u64_eq y (ty_smax cty)))
|
|
||||||
(eq bty x smax))
|
|
||||||
|
|
||||||
;; 32-bit integers zero-extended to 64-bit integers are never negative
|
;; 32-bit integers zero-extended to 64-bit integers are never negative
|
||||||
(rule (simplify
|
(rule (simplify
|
||||||
(slt ty
|
(slt ty
|
||||||
@@ -479,57 +339,6 @@
|
|||||||
(iconst _ (u64_from_imm64 0))))
|
(iconst _ (u64_from_imm64 0))))
|
||||||
(iconst ty (imm64 1)))
|
(iconst ty (imm64 1)))
|
||||||
|
|
||||||
(decl pure decompose_intcc (IntCC) u64)
|
|
||||||
(rule (decompose_intcc (IntCC.Equal)) 1)
|
|
||||||
(rule (decompose_intcc (IntCC.UnsignedLessThan)) 2)
|
|
||||||
(rule (decompose_intcc (IntCC.SignedLessThan)) 2)
|
|
||||||
(rule (decompose_intcc (IntCC.UnsignedLessThanOrEqual)) 3)
|
|
||||||
(rule (decompose_intcc (IntCC.SignedLessThanOrEqual)) 3)
|
|
||||||
(rule (decompose_intcc (IntCC.UnsignedGreaterThan)) 4)
|
|
||||||
(rule (decompose_intcc (IntCC.SignedGreaterThan)) 4)
|
|
||||||
(rule (decompose_intcc (IntCC.UnsignedGreaterThanOrEqual)) 5)
|
|
||||||
(rule (decompose_intcc (IntCC.SignedGreaterThanOrEqual)) 5)
|
|
||||||
(rule (decompose_intcc (IntCC.NotEqual)) 6)
|
|
||||||
|
|
||||||
(decl compose_icmp (Type u64 bool Value Value) Value)
|
|
||||||
(rule (compose_icmp ty 0 _ _ _) (subsume (iconst ty (imm64 0))))
|
|
||||||
(rule (compose_icmp ty 1 _ x y) (icmp ty (IntCC.Equal) x y))
|
|
||||||
(rule (compose_icmp ty 2 $false x y) (icmp ty (IntCC.UnsignedLessThan) x y))
|
|
||||||
(rule (compose_icmp ty 2 $true x y) (icmp ty (IntCC.SignedLessThan) x y))
|
|
||||||
(rule (compose_icmp ty 3 $false x y) (icmp ty (IntCC.UnsignedLessThanOrEqual) x y))
|
|
||||||
(rule (compose_icmp ty 3 $true x y) (icmp ty (IntCC.SignedLessThanOrEqual) x y))
|
|
||||||
(rule (compose_icmp ty 4 $false x y) (icmp ty (IntCC.UnsignedGreaterThan) x y))
|
|
||||||
(rule (compose_icmp ty 4 $true x y) (icmp ty (IntCC.SignedGreaterThan) x y))
|
|
||||||
(rule (compose_icmp ty 5 $false x y) (icmp ty (IntCC.UnsignedGreaterThanOrEqual) x y))
|
|
||||||
(rule (compose_icmp ty 5 $true x y) (icmp ty (IntCC.SignedGreaterThanOrEqual) x y))
|
|
||||||
(rule (compose_icmp ty 6 _ x y) (icmp ty (IntCC.NotEqual) x y))
|
|
||||||
(rule (compose_icmp ty 7 _ _ _) (subsume (iconst ty (imm64 1))))
|
|
||||||
|
|
||||||
(decl pure intcc_class (IntCC) u64)
|
|
||||||
(rule (intcc_class (IntCC.UnsignedLessThan)) 1)
|
|
||||||
(rule (intcc_class (IntCC.UnsignedLessThanOrEqual)) 1)
|
|
||||||
(rule (intcc_class (IntCC.UnsignedGreaterThan)) 1)
|
|
||||||
(rule (intcc_class (IntCC.UnsignedGreaterThanOrEqual)) 1)
|
|
||||||
(rule (intcc_class (IntCC.SignedLessThan)) 2)
|
|
||||||
(rule (intcc_class (IntCC.SignedLessThanOrEqual)) 2)
|
|
||||||
(rule (intcc_class (IntCC.SignedGreaterThan)) 2)
|
|
||||||
(rule (intcc_class (IntCC.SignedGreaterThanOrEqual)) 2)
|
|
||||||
(rule (intcc_class (IntCC.Equal)) 3)
|
|
||||||
(rule (intcc_class (IntCC.NotEqual)) 3)
|
|
||||||
|
|
||||||
(decl pure partial intcc_comparable (IntCC IntCC) bool)
|
|
||||||
(rule (intcc_comparable x y)
|
|
||||||
(if-let (u64_nonzero class) (u64_and (intcc_class x) (intcc_class y)))
|
|
||||||
(u64_eq 2 class))
|
|
||||||
|
|
||||||
(rule (simplify (band ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
|
|
||||||
(if-let signed (intcc_comparable cc1 cc2))
|
|
||||||
(compose_icmp ty (u64_and (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
|
|
||||||
|
|
||||||
(rule (simplify (bor ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
|
|
||||||
(if-let signed (intcc_comparable cc1 cc2))
|
|
||||||
(compose_icmp ty (u64_or (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
|
|
||||||
|
|
||||||
;; Transform select-of-icmp into {u,s}{min,max} instructions where possible.
|
;; Transform select-of-icmp into {u,s}{min,max} instructions where possible.
|
||||||
(rule (simplify (select ty (sgt _ x y) x y)) (smax ty x y))
|
(rule (simplify (select ty (sgt _ x y) x y)) (smax ty x y))
|
||||||
(rule (simplify (select ty (sge _ x y) x y)) (smax ty x y))
|
(rule (simplify (select ty (sge _ x y) x y)) (smax ty x y))
|
||||||
|
|||||||
177
cranelift/codegen/src/opts/icmp.isle
Normal file
177
cranelift/codegen/src/opts/icmp.isle
Normal file
@@ -0,0 +1,177 @@
|
|||||||
|
;; `icmp`-related rewrites
|
||||||
|
|
||||||
|
;; `x == x` is always true for integers; `x != x` is false. Strict
|
||||||
|
;; inequalities are false, and loose inequalities are true.
|
||||||
|
(rule (simplify (eq (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
||||||
|
(rule (simplify (ne (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
||||||
|
(rule (simplify (ugt (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
||||||
|
(rule (simplify (uge (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
||||||
|
(rule (simplify (sgt (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
||||||
|
(rule (simplify (sge (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
||||||
|
(rule (simplify (ult (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
||||||
|
(rule (simplify (ule (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
||||||
|
(rule (simplify (slt (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 0)))
|
||||||
|
(rule (simplify (sle (fits_in_64 (ty_int ty)) x x)) (iconst ty (imm64 1)))
|
||||||
|
|
||||||
|
;; Optimize icmp-of-icmp.
|
||||||
|
(rule (simplify (ne ty
|
||||||
|
(uextend _ inner @ (icmp ty _ _ _))
|
||||||
|
(iconst _ (u64_from_imm64 0))))
|
||||||
|
(subsume inner))
|
||||||
|
|
||||||
|
(rule (simplify (eq ty
|
||||||
|
(uextend _ (icmp ty cc x y))
|
||||||
|
(iconst _ (u64_from_imm64 0))))
|
||||||
|
(subsume (icmp ty (intcc_inverse cc) x y)))
|
||||||
|
|
||||||
|
;; Optimize select-of-uextend-of-icmp to select-of-icmp, because
|
||||||
|
;; select can take an I8 condition too.
|
||||||
|
(rule (simplify
|
||||||
|
(select ty (uextend _ c @ (icmp _ _ _ _)) x y))
|
||||||
|
(select ty c x y))
|
||||||
|
(rule (simplify
|
||||||
|
(select ty (uextend _ c @ (icmp _ _ _ _)) x y))
|
||||||
|
(select ty c x y))
|
||||||
|
|
||||||
|
;; Masking the result of a comparison with 1 always results in the comparison
|
||||||
|
;; itself. Note that comparisons in wasm may sometimes be hidden behind
|
||||||
|
;; extensions.
|
||||||
|
(rule (simplify
|
||||||
|
(band (ty_int _)
|
||||||
|
cmp @ (icmp _ _ _ _)
|
||||||
|
(iconst _ (u64_from_imm64 1))))
|
||||||
|
cmp)
|
||||||
|
(rule (simplify
|
||||||
|
(band (ty_int _)
|
||||||
|
extend @ (uextend _ (icmp _ _ _ _))
|
||||||
|
(iconst _ (u64_from_imm64 1))))
|
||||||
|
extend)
|
||||||
|
|
||||||
|
;; 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))))
|
||||||
|
|
||||||
|
;; 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))
|
||||||
|
|
||||||
|
;; ugt(x, 0) == ne(x, 0).
|
||||||
|
(rule (simplify (ugt (fits_in_64 (ty_int bty)) x zero @ (iconst _ (u64_from_imm64 0))))
|
||||||
|
(ne bty x zero))
|
||||||
|
|
||||||
|
;; uge(x, 0) == true.
|
||||||
|
(rule (simplify (uge (fits_in_64 (ty_int bty)) x zero @ (iconst _ (u64_from_imm64 0))))
|
||||||
|
(subsume (iconst bty (imm64 1))))
|
||||||
|
|
||||||
|
;; ult(x, UMAX) == ne(x, UMAX).
|
||||||
|
(rule (simplify (ult (fits_in_64 (ty_int bty)) x umax @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_umax cty)))
|
||||||
|
(ne bty x umax))
|
||||||
|
|
||||||
|
;; ule(x, UMAX) == true.
|
||||||
|
(rule (simplify (ule (fits_in_64 (ty_int bty)) x umax @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_umax cty)))
|
||||||
|
(subsume (iconst bty (imm64 1))))
|
||||||
|
|
||||||
|
;; ugt(x, UMAX) == false.
|
||||||
|
(rule (simplify (ugt (fits_in_64 (ty_int bty)) x umax @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_umax cty)))
|
||||||
|
(subsume (iconst bty (imm64 0))))
|
||||||
|
|
||||||
|
;; uge(x, UMAX) == eq(x, UMAX).
|
||||||
|
(rule (simplify (uge (fits_in_64 (ty_int bty)) x umax @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_umax cty)))
|
||||||
|
(eq bty x umax))
|
||||||
|
|
||||||
|
;; 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)))
|
||||||
|
(subsume (iconst bty (imm64 0))))
|
||||||
|
|
||||||
|
;; sle(x, SMIN) == eq(x, SMIN).
|
||||||
|
(rule (simplify (sle (fits_in_64 (ty_int bty)) x smin @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_smin cty)))
|
||||||
|
(eq bty x smin))
|
||||||
|
|
||||||
|
;; 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)))
|
||||||
|
(ne bty x smin))
|
||||||
|
|
||||||
|
;; sge(x, SMIN) == true.
|
||||||
|
(rule (simplify (sge (fits_in_64 (ty_int bty)) x smin @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_smin cty)))
|
||||||
|
(subsume (iconst bty (imm64 1))))
|
||||||
|
|
||||||
|
;; slt(x, SMAX) == ne(x, SMAX).
|
||||||
|
(rule (simplify (slt (fits_in_64 (ty_int bty)) x smax @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_smax cty)))
|
||||||
|
(ne bty x smax))
|
||||||
|
|
||||||
|
;; sle(x, SMAX) == true.
|
||||||
|
(rule (simplify (sle (fits_in_64 (ty_int bty)) x smax @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_smax cty)))
|
||||||
|
(subsume (iconst bty (imm64 1))))
|
||||||
|
|
||||||
|
;; sgt(x, SMAX) == false.
|
||||||
|
(rule (simplify (sgt (fits_in_64 (ty_int bty)) x smax @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_smax cty)))
|
||||||
|
(subsume (iconst bty (imm64 0))))
|
||||||
|
|
||||||
|
;; sge(x, SMAX) == eq(x, SMAX).
|
||||||
|
(rule (simplify (sge (fits_in_64 (ty_int bty)) x smax @ (iconst cty (u64_from_imm64 y))))
|
||||||
|
(if-let $true (u64_eq y (ty_smax cty)))
|
||||||
|
(eq bty x smax))
|
||||||
|
|
||||||
|
;; `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))
|
||||||
|
(compose_icmp ty (u64_and (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
|
||||||
|
|
||||||
|
(rule (simplify (bor ty (icmp ty cc1 x y) (icmp ty cc2 x y)))
|
||||||
|
(if-let signed (intcc_comparable cc1 cc2))
|
||||||
|
(compose_icmp ty (u64_or (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
|
||||||
|
|
||||||
|
(decl pure partial intcc_comparable (IntCC IntCC) bool)
|
||||||
|
(rule (intcc_comparable x y)
|
||||||
|
(if-let (u64_nonzero class) (u64_and (intcc_class x) (intcc_class y)))
|
||||||
|
(u64_eq 2 class))
|
||||||
|
|
||||||
|
(decl pure decompose_intcc (IntCC) u64)
|
||||||
|
(rule (decompose_intcc (IntCC.Equal)) 1)
|
||||||
|
(rule (decompose_intcc (IntCC.UnsignedLessThan)) 2)
|
||||||
|
(rule (decompose_intcc (IntCC.SignedLessThan)) 2)
|
||||||
|
(rule (decompose_intcc (IntCC.UnsignedLessThanOrEqual)) 3)
|
||||||
|
(rule (decompose_intcc (IntCC.SignedLessThanOrEqual)) 3)
|
||||||
|
(rule (decompose_intcc (IntCC.UnsignedGreaterThan)) 4)
|
||||||
|
(rule (decompose_intcc (IntCC.SignedGreaterThan)) 4)
|
||||||
|
(rule (decompose_intcc (IntCC.UnsignedGreaterThanOrEqual)) 5)
|
||||||
|
(rule (decompose_intcc (IntCC.SignedGreaterThanOrEqual)) 5)
|
||||||
|
(rule (decompose_intcc (IntCC.NotEqual)) 6)
|
||||||
|
|
||||||
|
(decl compose_icmp (Type u64 bool Value Value) Value)
|
||||||
|
(rule (compose_icmp ty 0 _ _ _) (subsume (iconst ty (imm64 0))))
|
||||||
|
(rule (compose_icmp ty 1 _ x y) (icmp ty (IntCC.Equal) x y))
|
||||||
|
(rule (compose_icmp ty 2 $false x y) (icmp ty (IntCC.UnsignedLessThan) x y))
|
||||||
|
(rule (compose_icmp ty 2 $true x y) (icmp ty (IntCC.SignedLessThan) x y))
|
||||||
|
(rule (compose_icmp ty 3 $false x y) (icmp ty (IntCC.UnsignedLessThanOrEqual) x y))
|
||||||
|
(rule (compose_icmp ty 3 $true x y) (icmp ty (IntCC.SignedLessThanOrEqual) x y))
|
||||||
|
(rule (compose_icmp ty 4 $false x y) (icmp ty (IntCC.UnsignedGreaterThan) x y))
|
||||||
|
(rule (compose_icmp ty 4 $true x y) (icmp ty (IntCC.SignedGreaterThan) x y))
|
||||||
|
(rule (compose_icmp ty 5 $false x y) (icmp ty (IntCC.UnsignedGreaterThanOrEqual) x y))
|
||||||
|
(rule (compose_icmp ty 5 $true x y) (icmp ty (IntCC.SignedGreaterThanOrEqual) x y))
|
||||||
|
(rule (compose_icmp ty 6 _ x y) (icmp ty (IntCC.NotEqual) x y))
|
||||||
|
(rule (compose_icmp ty 7 _ _ _) (subsume (iconst ty (imm64 1))))
|
||||||
|
|
||||||
|
(decl pure intcc_class (IntCC) u64)
|
||||||
|
(rule (intcc_class (IntCC.UnsignedLessThan)) 1)
|
||||||
|
(rule (intcc_class (IntCC.UnsignedLessThanOrEqual)) 1)
|
||||||
|
(rule (intcc_class (IntCC.UnsignedGreaterThan)) 1)
|
||||||
|
(rule (intcc_class (IntCC.UnsignedGreaterThanOrEqual)) 1)
|
||||||
|
(rule (intcc_class (IntCC.SignedLessThan)) 2)
|
||||||
|
(rule (intcc_class (IntCC.SignedLessThanOrEqual)) 2)
|
||||||
|
(rule (intcc_class (IntCC.SignedGreaterThan)) 2)
|
||||||
|
(rule (intcc_class (IntCC.SignedGreaterThanOrEqual)) 2)
|
||||||
|
(rule (intcc_class (IntCC.Equal)) 3)
|
||||||
|
(rule (intcc_class (IntCC.NotEqual)) 3)
|
||||||
@@ -394,24 +394,6 @@ block0(v0: i64):
|
|||||||
; check: return v4
|
; check: return v4
|
||||||
}
|
}
|
||||||
|
|
||||||
function %f2(i8) -> i8 {
|
|
||||||
block0(v1: i8):
|
|
||||||
v2 = icmp eq v1, v1
|
|
||||||
return v2
|
|
||||||
}
|
|
||||||
|
|
||||||
; check: v3 = iconst.i8 1
|
|
||||||
; check: return v3
|
|
||||||
|
|
||||||
function %f3(i8) -> i8 {
|
|
||||||
block0(v1: i8):
|
|
||||||
v2 = icmp ne v1, v1
|
|
||||||
return v2
|
|
||||||
}
|
|
||||||
|
|
||||||
; check: v3 = iconst.i8 0
|
|
||||||
; check: return v3
|
|
||||||
|
|
||||||
function %bnot1(i8) -> i8 {
|
function %bnot1(i8) -> i8 {
|
||||||
block0(v1: i8):
|
block0(v1: i8):
|
||||||
v2 = iconst.i8 -1
|
v2 = iconst.i8 -1
|
||||||
@@ -442,174 +424,6 @@ block0(v1: i64):
|
|||||||
; check: v5 = bnot v1
|
; check: v5 = bnot v1
|
||||||
; check: return v5
|
; check: return v5
|
||||||
|
|
||||||
function %mask_icmp_result(i64, i64) -> i8 {
|
|
||||||
block0(v1: i64, v2: i64):
|
|
||||||
v3 = icmp ult v1, v2
|
|
||||||
v4 = iconst.i8 1
|
|
||||||
v5 = band v3, v4
|
|
||||||
return v5
|
|
||||||
}
|
|
||||||
|
|
||||||
; check: v3 = icmp ult v1, v2
|
|
||||||
; check: return v3
|
|
||||||
|
|
||||||
function %mask_icmp_extend_result(i64, i64) -> i64 {
|
|
||||||
block0(v1: i64, v2: i64):
|
|
||||||
v3 = icmp ult v1, v2
|
|
||||||
v4 = uextend.i64 v3
|
|
||||||
v5 = iconst.i64 1
|
|
||||||
v6 = band v4, v5
|
|
||||||
return v6
|
|
||||||
}
|
|
||||||
|
|
||||||
; check: v3 = icmp ult v1, v2
|
|
||||||
; check: v4 = uextend.i64 v3
|
|
||||||
; check: return v4
|
|
||||||
|
|
||||||
function %icmp_ult_0(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0
|
|
||||||
v2 = icmp ult v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = iconst.i8 0
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_ule_0(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0
|
|
||||||
v2 = icmp ule v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = icmp eq v0, v1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_ugt_0(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0
|
|
||||||
v2 = icmp ugt v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = icmp ne v0, v1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_uge_0(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0
|
|
||||||
v2 = icmp uge v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = iconst.i8 1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_ult_umax(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0xffff_ffff
|
|
||||||
v2 = icmp ult v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = icmp ne v0, v1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_ule_umax(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0xffff_ffff
|
|
||||||
v2 = icmp ule v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = iconst.i8 1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_ugt_umax(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0xffff_ffff
|
|
||||||
v2 = icmp ugt v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = iconst.i8 0
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_uge_umax(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0xffff_ffff
|
|
||||||
v2 = icmp uge v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = icmp eq v0, v1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_slt_smin(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0x8000_0000
|
|
||||||
v2 = icmp slt v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = iconst.i8 0
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_sle_smin(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0x8000_0000
|
|
||||||
v2 = icmp sle v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = icmp eq v0, v1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_sgt_smin(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0x8000_0000
|
|
||||||
v2 = icmp sgt v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = icmp ne v0, v1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_sge_smin(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0x8000_0000
|
|
||||||
v2 = icmp sge v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = iconst.i8 1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_slt_smax(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0x7FFF_FFFF
|
|
||||||
v2 = icmp slt v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = icmp ne v0, v1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_sle_smax(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0x7FFF_FFFF
|
|
||||||
v2 = icmp sle v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = iconst.i8 1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_sgt_smax(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0x7FFF_FFFF
|
|
||||||
v2 = icmp sgt v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = iconst.i8 0
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %icmp_sge_smax(i32) -> i8 {
|
|
||||||
block0(v0: i32):
|
|
||||||
v1 = iconst.i32 0x7FFF_FFFF
|
|
||||||
v2 = icmp sge v0, v1
|
|
||||||
return v2
|
|
||||||
; check: v3 = icmp eq v0, v1
|
|
||||||
; check: return v3
|
|
||||||
}
|
|
||||||
|
|
||||||
function %extend_always_above_zero(i32) -> i8 {
|
function %extend_always_above_zero(i32) -> i8 {
|
||||||
block0(v1: i32):
|
block0(v1: i32):
|
||||||
v2 = uextend.i64 v1
|
v2 = uextend.i64 v1
|
||||||
|
|||||||
3732
cranelift/filetests/filetests/egraph/icmp-parameterized.clif
Normal file
3732
cranelift/filetests/filetests/egraph/icmp-parameterized.clif
Normal file
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
89
cranelift/filetests/filetests/egraph/make-icmp-parameterized-tests.sh
Executable file
89
cranelift/filetests/filetests/egraph/make-icmp-parameterized-tests.sh
Executable file
@@ -0,0 +1,89 @@
|
|||||||
|
#!/usr/bin/env bash
|
||||||
|
|
||||||
|
set -e
|
||||||
|
cd $(dirname "$0")
|
||||||
|
out=parameterized-icmp.clif
|
||||||
|
CCS="eq ne ult ule ugt uge slt sle sgt sge"
|
||||||
|
|
||||||
|
function main {
|
||||||
|
cat << EOF > $out
|
||||||
|
test optimize precise-output
|
||||||
|
set opt_level=speed
|
||||||
|
set use_egraphs=true
|
||||||
|
target x86_64
|
||||||
|
|
||||||
|
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||||
|
;; !!! GENERATED BY 'make-icmp-parameterized-tests.sh' DO NOT EDIT !!!
|
||||||
|
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||||
|
;; run with the 'CRANELIFT_TEST_BLESS=1' env var set to update this file
|
||||||
|
|
||||||
|
EOF
|
||||||
|
|
||||||
|
# Reflexivity/irreflexivity of `icmp`` cond codes:
|
||||||
|
# for reflexive cond codes, (icmp cc x x) == true.
|
||||||
|
# for irreflexive cond codes, (icmp cc x x) == false.
|
||||||
|
for cc in $CCS; do
|
||||||
|
cat << EOF >> $out
|
||||||
|
function %icmp_${cc}_self(i32) -> i8 {
|
||||||
|
block0(v0: i32):
|
||||||
|
v1 = icmp ${cc} v0, v0
|
||||||
|
return v1
|
||||||
|
}
|
||||||
|
|
||||||
|
EOF
|
||||||
|
done
|
||||||
|
|
||||||
|
# Comparisons against largest/smallest signed/unsigned values:
|
||||||
|
for cc in $CCS; do
|
||||||
|
cat << EOF >> $out
|
||||||
|
function %icmp_${cc}_umin(i32) -> i8 {
|
||||||
|
block0(v0: i32):
|
||||||
|
v1 = iconst.i32 0
|
||||||
|
v2 = icmp ${cc} v0, v1
|
||||||
|
return v2
|
||||||
|
}
|
||||||
|
|
||||||
|
function %icmp_${cc}_umax(i32) -> i8 {
|
||||||
|
block0(v0: i32):
|
||||||
|
v1 = iconst.i32 0xFFFF_FFFF
|
||||||
|
v2 = icmp ${cc} v0, v1
|
||||||
|
return v2
|
||||||
|
}
|
||||||
|
|
||||||
|
function %icmp_${cc}_smin(i32) -> i8 {
|
||||||
|
block0(v0: i32):
|
||||||
|
v1 = iconst.i32 0x8000_0000
|
||||||
|
v2 = icmp ${cc} v0, v1
|
||||||
|
return v2
|
||||||
|
}
|
||||||
|
|
||||||
|
function %icmp_${cc}_smax(i32) -> i8 {
|
||||||
|
block0(v0: i32):
|
||||||
|
v1 = iconst.i32 0x7FFF_FFFF
|
||||||
|
v2 = icmp ${cc} v0, v1
|
||||||
|
return v2
|
||||||
|
}
|
||||||
|
|
||||||
|
EOF
|
||||||
|
done
|
||||||
|
|
||||||
|
# `band`/`bor` of 2 comparisons:
|
||||||
|
for op in "and" "or"; do
|
||||||
|
for cc1 in $CCS; do
|
||||||
|
for cc2 in $CCS; do
|
||||||
|
cat << EOF >> $out
|
||||||
|
function %icmp_${op}_${cc1}_${cc2}(i32, i32) -> i8 {
|
||||||
|
block0(v0: i32, v1: i32):
|
||||||
|
v2 = icmp ${cc1} v0, v1
|
||||||
|
v3 = icmp ${cc2} v0, v1
|
||||||
|
v4 = b${op} v2, v3
|
||||||
|
return v4
|
||||||
|
}
|
||||||
|
|
||||||
|
EOF
|
||||||
|
done
|
||||||
|
done
|
||||||
|
done
|
||||||
|
}
|
||||||
|
|
||||||
|
main
|
||||||
@@ -1,38 +0,0 @@
|
|||||||
#!/usr/bin/env bash
|
|
||||||
|
|
||||||
set -e
|
|
||||||
cd $(dirname "$0")
|
|
||||||
out=icmp.clif
|
|
||||||
CCS="eq ne ult ule ugt uge slt sle sgt sge"
|
|
||||||
|
|
||||||
function main {
|
|
||||||
cat << EOF > $out
|
|
||||||
test optimize precise-output
|
|
||||||
set opt_level=speed
|
|
||||||
set use_egraphs=true
|
|
||||||
target x86_64
|
|
||||||
|
|
||||||
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
|
||||||
;; !!! GENERATED BY 'make-icmp-tests.sh' DO NOT EDIT !!!
|
|
||||||
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
|
||||||
;; run with the 'CRANELIFT_TEST_BLESS=1' env var set to update this file
|
|
||||||
|
|
||||||
EOF
|
|
||||||
for op in "and" "or"; do
|
|
||||||
for cc1 in $CCS; do
|
|
||||||
for cc2 in $CCS; do
|
|
||||||
cat << EOF >> $out
|
|
||||||
function %icmp_${op}_${cc1}_${cc2}(i32, i32) -> i8 {
|
|
||||||
block0(v0: i32, v1: i32):
|
|
||||||
v2 = icmp ${cc1} v0, v1
|
|
||||||
v3 = icmp ${cc2} v0, v1
|
|
||||||
v4 = b${op} v2, v3
|
|
||||||
return v4
|
|
||||||
}
|
|
||||||
EOF
|
|
||||||
done
|
|
||||||
done
|
|
||||||
done
|
|
||||||
}
|
|
||||||
|
|
||||||
main
|
|
||||||
Reference in New Issue
Block a user