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 32b7ad6
Show file tree
Hide file tree
Showing 3 changed files with 179 additions and 0 deletions.
115 changes: 115 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,121 @@
(iconst _ (u64_from_imm64 0))))
(iconst ty (imm64 1)))

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

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

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

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

;; eq(x, y) && sgt(x, y) == sgt(x, y) && eq(x, y) == false.
(rule (simplify (band ty (eq ty x y) (sgt ty x y))) (subsume (iconst ty (imm64 0))))
(rule (simplify (band ty (sgt 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).
(rule (simplify (band ty (eq ty x y) (ule ty x y))) (subsume (eq ty x y)))
(rule (simplify (band ty (ule ty x y) (eq ty x y))) (subsume (eq ty x y)))

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

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

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

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

;; ne(x, y) && ule(x, y) == ult(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) && ugt(x, y) == ugt(x, y) && ne(x, y) == ugt(x, y).
(rule (simplify (band ty (ne ty x y) (ugt ty x y))) (subsume (ugt ty x y)))
(rule (simplify (band ty (ugt ty x y) (ne ty x y))) (subsume (ugt ty x y)))

;; ne(x, y) && uge(x, y) == ugt(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) && slt(x, y) == slt(x, y) && ne(x, y) == slt(x, y).
(rule (simplify (band ty (ne ty x y) (slt ty x y))) (subsume (slt ty x y)))
(rule (simplify (band ty (slt ty x y) (ne ty x y))) (subsume (slt ty x y)))

;; ne(x, y) && sle(x, y) == slt(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) && sgt(x, y) == sgt(x, y) && ne(x, y) == sgt(x, y).
(rule (simplify (band ty (ne ty x y) (sgt ty x y))) (subsume (sgt ty x y)))
(rule (simplify (band ty (sgt ty x y) (ne ty x y))) (subsume (sgt ty x y)))

;; ne(x, y) && sge(x, y) == sgt(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)))

;; 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
14 changes: 14 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,20 @@
(decl sge (Type Value Value) Value)
(extractor (sge ty x y) (icmp ty (IntCC.SignedGreaterThanOrEqual) x y))

;; (decl icmp_inequality (Type Value Value) Value)
;; (extractor (icmp_inequality ty x y)
;; (or
;; (icmp ty (IntCC.NotEqual) x y)
;; (icmp ty (IntCC.NotEqual) y x)
;; (icmp ty (IntCC.UnsignedLessThan) x y)
;; (icmp ty (IntCC.UnsignedLessThan) y x)
;; (icmp ty (IntCC.UnsignedGreaterThan) x y)
;; (icmp ty (IntCC.UnsignedGreaterThan) y x)
;; (icmp ty (IntCC.SignedLessThan) x y)
;; (icmp ty (IntCC.SignedLessThan) y x)
;; (icmp ty (IntCC.SignedGreaterThan) x y)
;; (icmp ty (IntCC.SignedGreaterThan) y x)))

;; 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
50 changes: 50 additions & 0 deletions cranelift/filetests/filetests/egraph/algebraic.clif
View file
Original file line number Diff line number Diff line change
Expand Up @@ -610,6 +610,56 @@ block0(v0: i32):
; check: return v3
}

function %and_eq_ne(i32, i32) -> i8 {
block0(v0: i32, v1: i32):
v2 = icmp eq v0, v1
v3 = icmp ne v0, v1
v4 = band v2, v3
return v4
; check: v5 = iconst.i8 0
; check: return v5
}

function %and_eq_ult(i32, i32) -> i8 {
block0(v0: i32, v1: i32):
v2 = icmp eq v0, v1
v3 = icmp ult v0, v1
v4 = band v2, v3
return v4
; check: v5 = iconst.i8 0
; check: return v5
}

function %and_eq_ugt(i32, i32) -> i8 {
block0(v0: i32, v1: i32):
v2 = icmp eq v0, v1
v3 = icmp ugt v0, v1
v4 = band v2, v3
return v4
; check: v5 = iconst.i8 0
; check: return v5
}

function %and_eq_slt(i32, i32) -> i8 {
block0(v0: i32, v1: i32):
v2 = icmp eq v0, v1
v3 = icmp slt v0, v1
v4 = band v2, v3
return v4
; check: v5 = iconst.i8 0
; check: return v5
}

function %and_eq_sgt(i32, i32) -> i8 {
block0(v0: i32, v1: i32):
v2 = icmp eq v0, v1
v3 = icmp sgt v0, v1
v4 = band v2, v3
return v4
; check: v5 = iconst.i8 0
; check: return v5
}

function %extend_always_above_zero(i32) -> i8 {
block0(v1: i32):
v2 = uextend.i64 v1
Expand Down

0 comments on commit 32b7ad6

Please sign in to comment.