Skip to content

Commit

Permalink
ISLE: rewrite and/or of icmp
Browse files Browse the repository at this point in the history
  • Loading branch information
@Kmeakin
Kmeakin committed Mar 23, 2023
1 parent 6f66abd commit 5b7f8af
Show file tree
Hide file tree
Showing 5 changed files with 1,388 additions and 11 deletions.
48 changes: 48 additions & 0 deletions cranelift/codegen/src/ir/condcodes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,54 @@ impl IntCC {
UnsignedLessThanOrEqual => "ule",
}
}

/// Return true if self interprets arguments as unsigned integers
pub fn is_unsigned(self) -> bool {
match self {
IntCC::Equal
| IntCC::NotEqual
| IntCC::UnsignedLessThan
| IntCC::UnsignedGreaterThanOrEqual
| IntCC::UnsignedGreaterThan
| IntCC::UnsignedLessThanOrEqual => true,
_ => false,
}
}

/// Return true if self interprets arguments as signed integers
pub fn is_signed(self) -> bool {
match self {
IntCC::SignedLessThan
| IntCC::SignedGreaterThanOrEqual
| IntCC::SignedGreaterThan
| IntCC::SignedLessThanOrEqual => true,
_ => false,
}
}

/// Return true if self tests for integer equality
pub fn is_equality(self) -> bool {
match self {
IntCC::Equal
| IntCC::SignedGreaterThanOrEqual
| IntCC::SignedLessThanOrEqual
| IntCC::UnsignedGreaterThanOrEqual
| IntCC::UnsignedLessThanOrEqual => true,
_ => false,
}
}

/// Return true if self tests for strict integer inequality
pub fn is_inequality(self) -> bool {
match self {
IntCC::NotEqual
| IntCC::SignedLessThan
| IntCC::SignedGreaterThan
| IntCC::UnsignedLessThan
| IntCC::UnsignedGreaterThan => true,
_ => false,
}
}
}

impl Display for IntCC {
Expand Down
33 changes: 22 additions & 11 deletions cranelift/codegen/src/isle_prelude.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -720,17 +720,10 @@ macro_rules! isle_common_prelude_methods {

#[inline]
fn signed_cond_code(&mut self, cc: &condcodes::IntCC) -> Option<condcodes::IntCC> {
match cc {
IntCC::Equal
| IntCC::UnsignedGreaterThanOrEqual
| IntCC::UnsignedGreaterThan
| IntCC::UnsignedLessThanOrEqual
| IntCC::UnsignedLessThan
| IntCC::NotEqual => None,
IntCC::SignedGreaterThanOrEqual
| IntCC::SignedGreaterThan
| IntCC::SignedLessThanOrEqual
| IntCC::SignedLessThan => Some(*cc),
if cc.is_signed() {
Some(*cc)
} else {
None
}
}

Expand All @@ -744,6 +737,24 @@ macro_rules! isle_common_prelude_methods {
cc.inverse()
}

#[inline]
fn intcc_equality(&mut self, cc: &IntCC) -> Option<IntCC> {
if cc.is_equality() {
Some(*cc)
} else {
None
}
}

#[inline]
fn intcc_inequality(&mut self, cc: &IntCC) -> Option<IntCC> {
if cc.is_inequality() {
Some(*cc)
} else {
None
}
}

#[inline]
fn floatcc_reverse(&mut self, cc: &FloatCC) -> FloatCC {
cc.reverse()
Expand Down
174 changes: 174 additions & 0 deletions cranelift/codegen/src/opts/algebraic.isle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -479,6 +479,180 @@
(iconst _ (u64_from_imm64 0))))
(iconst ty (imm64 1)))

;; eq(x, y) && ne(x, y) == ne(x, y) && eq(x, y) == false.
;; eq(x, y) && ult(x, y) == ult(x, y) && eq(x, y) == false.
;; eq(x, y) && ugt(x, y) == ugt(x, y) && eq(x, y) == false.
;; eq(x, y) && slt(x, y) == slt(x, y) && eq(x, y) == false.
;; eq(x, y) && sgt(x, y) == sgt(x, y) && eq(x, y) == false.
(rule (simplify (band ty (eq ty x y) (icmp_inequality ty x y))) (subsume (iconst ty (imm64 0))))
(rule (simplify (band ty (icmp_inequality ty x y) (eq ty x y))) (subsume (iconst ty (imm64 0))))

;; eq(x, y) && ule(x, y) == ule(x, y) && eq(x, y) == eq(x, y).
;; eq(x, y) && uge(x, y) == uge(x, y) && eq(x, y) == eq(x, y).
;; eq(x, y) && sle(x, y) == sle(x, y) && eq(x, y) == eq(x, y).
;; eq(x, y) && sge(x, y) == sge(x, y) && eq(x, y) == eq(x, y).
(rule (simplify (band ty eq @ (eq ty x y) (icmp_equality ty x y))) (subsume eq))
(rule (simplify (band ty (icmp_equality ty x y) eq @ (eq ty x y))) (subsume eq))

;; ne(x, y) && ult(x, y) == ult(x, y) && ne(x, y) == ult(x, y).
;; ne(x, y) && ugt(x, y) == ugt(x, y) && ne(x, y) == ugt(x, y).
;; ne(x, y) && slt(x, y) == slt(x, y) && ne(x, y) == slt(x, y).
;; ne(x, y) && sgt(x, y) == sgt(x, y) && ne(x, y) == sgt(x, y).
(rule (simplify (band ty (ne ty x y) icmp @ (icmp_inequality ty x y))) (subsume icmp))
(rule (simplify (band ty icmp @ (icmp_inequality ty x y) (ne ty x y))) (subsume icmp))

;; ne(x, y) && ule(x, y) == ule(x, y) && ne(x, y) == ult(x, y).
(rule (simplify (band ty (ne ty x y) (ule ty x y))) (subsume (ult ty x y)))
(rule (simplify (band ty (ule ty x y) (ne ty x y))) (subsume (ult ty x y)))

;; ne(x, y) && uge(x, y) == uge(x, y) && ne(x, y) == ugt(x, y).
(rule (simplify (band ty (ne ty x y) (uge ty x y))) (subsume (ugt ty x y)))
(rule (simplify (band ty (uge ty x y) (ne ty x y))) (subsume (ugt ty x y)))

;; ne(x, y) && sle(x, y) == sle(x, y) && ne(x, y) == slt(x, y).
(rule (simplify (band ty (ne ty x y) (sle ty x y))) (subsume (slt ty x y)))
(rule (simplify (band ty (sle ty x y) (ne ty x y))) (subsume (slt ty x y)))

;; ne(x, y) && sge(x, y) == sge(x, y) && ne(x, y) == sgt(x, y).
(rule (simplify (band ty (ne ty x y) (sge ty x y))) (subsume (sgt ty x y)))
(rule (simplify (band ty (sge ty x y) (ne ty x y))) (subsume (sgt ty x y)))

;; ult(x, y) && ule(x, y) == ule(x, y) && ult(x, y) == ult(x, y).
(rule (simplify (band ty (ult ty x y) (ule ty x y))) (subsume (ult ty x y)))
(rule (simplify (band ty (ule ty x y) (ult ty x y))) (subsume (ult ty x y)))

;; ult(x, y) && ugt(x, y) == ugt(x, y) && ult(x, y) == false.
(rule (simplify (band ty (ult ty x y) (ugt ty x y))) (subsume (iconst ty (imm64 0))))
(rule (simplify (band ty (ugt ty x y) (ult ty x y))) (subsume (iconst ty (imm64 0))))

;; ult(x, y) && uge(x, y) == uge(x, y) && ult(x, y) == false.
(rule (simplify (band ty (ult ty x y) (uge ty x y))) (subsume (iconst ty (imm64 0))))
(rule (simplify (band ty (uge ty x y) (ult ty x y))) (subsume (iconst ty (imm64 0))))

;; ule(x, y) && ugt(x, y) == ugt(x, y) && ule(x, y) == false.
(rule (simplify (band ty (ule ty x y) (ugt ty x y))) (subsume (iconst ty (imm64 0))))
(rule (simplify (band ty (ugt ty x y) (ule ty x y))) (subsume (iconst ty (imm64 0))))

;; ule(x, y) && uge(x, y) == uge(x, y) && ule(x, y) == eq(x, y).
(rule (simplify (band ty (ule ty x y) (uge ty x y))) (subsume (eq ty x y)))
(rule (simplify (band ty (uge ty x y) (ule ty x y))) (subsume (eq ty x y)))

;; ugt(x, y) && uge(x, y) == uge(x, y) && ugt(x, y) == ugt(x, y).
(rule (simplify (band ty (ugt ty x y) (uge ty x y))) (subsume (ugt ty x y)))
(rule (simplify (band ty (uge ty x y) (ugt ty x y))) (subsume (ugt ty x y)))

;; slt(x, y) && sle(x, y) == sle(x, y) && slt(x, y) == slt(x, y).
(rule (simplify (band ty (slt ty x y) (sle ty x y))) (subsume (slt ty x y)))
(rule (simplify (band ty (sle ty x y) (slt ty x y))) (subsume (slt ty x y)))

;; slt(x, y) && sgt(x, y) == sgt(x, y) && slt(x, y) == false.
(rule (simplify (band ty (slt ty x y) (sgt ty x y))) (subsume (iconst ty (imm64 0))))
(rule (simplify (band ty (sgt ty x y) (slt ty x y))) (subsume (iconst ty (imm64 0))))

;; slt(x, y) && sge(x, y) == sge(x, y) && slt(x, y) == false.
(rule (simplify (band ty (slt ty x y) (sge ty x y))) (subsume (iconst ty (imm64 0))))
(rule (simplify (band ty (sge ty x y) (slt ty x y))) (subsume (iconst ty (imm64 0))))

;; sle(x, y) && sgt(x, y) == sgt(x, y) && sle(x, y) == false.
(rule (simplify (band ty (sle ty x y) (sgt ty x y))) (subsume (iconst ty (imm64 0))))
(rule (simplify (band ty (sgt ty x y) (sle ty x y))) (subsume (iconst ty (imm64 0))))

;; sle(x, y) && sge(x, y) == sge(x, y) && sle(x, y) == eq(x, y).
(rule (simplify (band ty (sle ty x y) (sge ty x y))) (subsume (eq ty x y)))
(rule (simplify (band ty (sge ty x y) (sle ty x y))) (subsume (eq ty x y)))

;; sgt(x, y) && sge(x, y) == sge(x, y) && sgt(x, y) == sgt(x, y).
(rule (simplify (band ty (sgt ty x y) (sge ty x y))) (subsume (sgt ty x y)))
(rule (simplify (band ty (sge ty x y) (sgt ty x y))) (subsume (sgt ty x y)))

;; eq(x, y) || ne(x, y) == ne(x, y) || eq(x, y) == true.
(rule (simplify (bor ty (eq ty x y) (ne ty x y))) (subsume (iconst ty (imm64 1))))
(rule (simplify (bor ty (ne ty x y) (eq ty x y))) (subsume (iconst ty (imm64 1))))

;; eq(x, y) || ule(x, y) == ule(x, y) || eq(x, y) == ule(x, y).
;; eq(x, y) || uge(x, y) == uge(x, y) || eq(x, y) == uge(x, y).
;; eq(x, y) || sle(x, y) == sle(x, y) || eq(x, y) == sle(x, y).
;; eq(x, y) || sge(x, y) == sge(x, y) || eq(x, y) == sge(x, y).
(rule (simplify (bor ty (eq ty x y) icmp @ (icmp_equality ty x y))) (subsume icmp))
(rule (simplify (bor ty icmp @ (icmp_equality ty x y) (eq ty x y))) (subsume icmp))

;; eq(x, y) || ult(x, y) == ult(x, y) || eq(x, y) == ule(x, y).
(rule (simplify (bor ty (eq ty x y) (ult ty x y))) (subsume (ule ty x y)))
(rule (simplify (bor ty (ult ty x y) (eq ty x y))) (subsume (ule ty x y)))

;; eq(x, y) || ugt(x, y) == ugt(x, y) || eq(x, y) == uge(x, y).
(rule (simplify (bor ty (eq ty x y) (ugt ty x y))) (subsume (uge ty x y)))
(rule (simplify (bor ty (ugt ty x y) (eq ty x y))) (subsume (uge ty x y)))

;; eq(x, y) || slt(x, y) == slt(x, y) || eq(x, y) == sle(x, y).
(rule (simplify (bor ty (eq ty x y) (slt ty x y))) (subsume (sle ty x y)))
(rule (simplify (bor ty (slt ty x y) (eq ty x y))) (subsume (sle ty x y)))

;; eq(x, y) || sgt(x, y) == sgt(x, y) || eq(x, y) == sge(x, y).
(rule (simplify (bor ty (eq ty x y) (sgt ty x y))) (subsume (sge ty x y)))
(rule (simplify (bor ty (sgt ty x y) (eq ty x y))) (subsume (sge ty x y)))

;; ne(x, y) || ult(x, y) == ult(x, y) || ne(x, y) == ne(x, y).
;; ne(x, y) || ugt(x, y) == ugt(x, y) || ne(x, y) == ne(x, y).
;; ne(x, y) || slt(x, y) == slt(x, y) || ne(x, y) == ne(x, y).
;; ne(x, y) || sgt(x, y) == sgt(x, y) || ne(x, y) == ne(x, y).
(rule (simplify (bor ty ne @ (ne ty x y) (icmp_inequality ty x y))) (subsume ne))
(rule (simplify (bor ty (icmp_inequality ty x y) ne @ (ne ty x y))) (subsume ne))

;; ne(x, y) || ule(x, y) == ule(x, y) || ne(x, y) == true.
;; ne(x, y) || uge(x, y) == uge(x, y) || ne(x, y) == true.
;; ne(x, y) || sle(x, y) == sle(x, y) || ne(x, y) == true.
;; ne(x, y) || sge(x, y) == sge(x, y) || ne(x, y) == true.
(rule (simplify (bor ty (ne ty x y) (icmp_equality ty x y))) (subsume (iconst ty (imm64 1))))
(rule (simplify (bor ty (icmp_equality ty x y) (ne ty x y))) (subsume (iconst ty (imm64 1))))

;; ult(x, y) || ule(x, y) == ule(x, y) || ult(x, y) == ule(x, y).
(rule (simplify (bor ty (ult ty x y) (ule ty x y))) (subsume (ule ty x y)))
(rule (simplify (bor ty (ule ty x y) (ult ty x y))) (subsume (ule ty x y)))

;; ult(x, y) || ugt(x, y) == ugt(x, y) || ult(x, y) == ne(x, y).
(rule (simplify (bor ty (ult ty x y) (ugt ty x y))) (subsume (ne ty x y)))
(rule (simplify (bor ty (ugt ty x y) (ult ty x y))) (subsume (ne ty x y)))

;; ult(x, y) || uge(x, y) == uge(x, y) || ult(x, y) == true.
(rule (simplify (bor ty (ult ty x y) (uge ty x y))) (subsume (iconst ty (imm64 1))))
(rule (simplify (bor ty (uge ty x y) (ult ty x y))) (subsume (iconst ty (imm64 1))))

;; ule(x, y) || ugt(x, y) == ugt(x, y) || ule(x, y) == true.
(rule (simplify (bor ty (ule ty x y) (ugt ty x y))) (subsume (iconst ty (imm64 1))))
(rule (simplify (bor ty (ugt ty x y) (ule ty x y))) (subsume (iconst ty (imm64 1))))

;; ule(x, y) || uge(x, y) == uge(x, y) || ule(x, y) == true.
(rule (simplify (bor ty (ule ty x y) (uge ty x y))) (subsume (iconst ty (imm64 1))))
(rule (simplify (bor ty (uge ty x y) (ule ty x y))) (subsume (iconst ty (imm64 1))))

;; ugt(x, y) || uge(x, y) == uge(x, y) || ugt(x, y) == uge(x, y).
(rule (simplify (bor ty (ugt ty x y) (uge ty x y))) (subsume (uge ty x y)))
(rule (simplify (bor ty (uge ty x y) (ugt ty x y))) (subsume (uge ty x y)))

;; slt(x, y) || sle(x, y) == sle(x, y) || slt(x, y) == sle(x, y).
(rule (simplify (bor ty (slt ty x y) (sle ty x y))) (subsume (sle ty x y)))
(rule (simplify (bor ty (sle ty x y) (slt ty x y))) (subsume (sle ty x y)))

;; slt(x, y) || sgt(x, y) == sgt(x, y) || slt(x, y) == ne(x, y).
(rule (simplify (bor ty (slt ty x y) (sgt ty x y))) (subsume (ne ty x y)))
(rule (simplify (bor ty (sgt ty x y) (slt ty x y))) (subsume (ne ty x y)))

;; slt(x, y) || sge(x, y) == sge(x, y) || slt(x, y) == true.
(rule (simplify (bor ty (slt ty x y) (sge ty x y))) (subsume (iconst ty (imm64 1))))
(rule (simplify (bor ty (sge ty x y) (slt ty x y))) (subsume (iconst ty (imm64 1))))

;; sle(x, y) || sgt(x, y) == sgt(x, y) || sle(x, y) == true.
(rule (simplify (bor ty (sle ty x y) (sgt ty x y))) (subsume (iconst ty (imm64 1))))
(rule (simplify (bor ty (sgt ty x y) (sle ty x y))) (subsume (iconst ty (imm64 1))))

;; sle(x, y) || sge(x, y) == sge(x, y) || sle(x, y) == true.
(rule (simplify (bor ty (sle ty x y) (sge ty x y))) (subsume (iconst ty (imm64 1))))
(rule (simplify (bor ty (sge ty x y) (sle ty x y))) (subsume (iconst ty (imm64 1))))

;; sgt(x, y) || sge(x, y) == sge(x, y) || sgt(x, y) == sge.
(rule (simplify (bor ty (sgt ty x y) (sge ty x y))) (subsume (sge ty x y)))
(rule (simplify (bor ty (sge ty x y) (sgt ty x y))) (subsume (sge ty x y)))

;; 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))
Expand Down
12 changes: 12 additions & 0 deletions cranelift/codegen/src/prelude.isle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -315,6 +315,18 @@
(decl sge (Type Value Value) Value)
(extractor (sge ty x y) (icmp ty (IntCC.SignedGreaterThanOrEqual) x y))

(decl intcc_equality (IntCC) IntCC)
(extern extractor intcc_equality intcc_equality)

(decl intcc_inequality (IntCC) IntCC)
(extern extractor intcc_inequality intcc_inequality)

(decl icmp_equality (Type Value Value) Value)
(extractor (icmp_equality ty x y) (icmp ty (intcc_equality _) x y))

(decl icmp_inequality (Type Value Value) Value)
(extractor (icmp_inequality ty x y) (icmp ty (intcc_inequality _) x y))

;; An extractor that only matches types that can fit in 16 bits.
(decl fits_in_16 (Type) Type)
(extern extractor fits_in_16 fits_in_16)
Expand Down
Loading

0 comments on commit 5b7f8af

Please sign in to comment.