Browse Source

Add missing subsume uses in egraph rules (#7879)

* Fix a few egraph rules that needed `subsume`

There were a few rules that dropped value references from the LHS
without using subsume. I think they were probably benign as they
produced constant results, but this change is in the spirit of our
revised guidelines for egraph rules.

* Augment egraph rule guideline 2 to talk about constants
pull/7882/head
Trevor Elliott 9 months ago
committed by GitHub
parent
commit
7464bbcb3b
No known key found for this signature in database GPG Key ID: B5690EEEBB952194
  1. 6
      cranelift/codegen/src/opts/README.md
  2. 4
      cranelift/codegen/src/opts/extends.isle
  3. 20
      cranelift/codegen/src/opts/icmp.isle

6
cranelift/codegen/src/opts/README.md

@ -38,6 +38,12 @@ of it boils down to the fact that, unlike traditional e-graphs, our rules are
place of `x` in such cases would introduce uses of `y` where it is not
defined.
An exception to this rule is discarding constants, as they can be
rematerialized anywhere without introducing correctness issues. For example,
the (admittedly silly) rule `(select 1 x (iconst_u _)) => x` would be a good
candidate for not using `subsume`, as it does not discard any non-constant
values introduced in its LHS.
3. Avoid overly general rewrites like commutativity and associativity. Instead,
prefer targeted instances of the rewrite (for example, canonicalizing adds
where one operand is a constant such that the constant is always the add's

4
cranelift/codegen/src/opts/extends.isle

@ -29,12 +29,12 @@
(slt ty
(uextend $I64 x @ (value_type $I32))
(iconst_u _ 0)))
(iconst_u ty 0))
(subsume (iconst_u ty 0)))
(rule (simplify
(sge ty
(uextend $I64 x @ (value_type $I32))
(iconst_u _ 0)))
(iconst_u ty 1))
(subsume (iconst_u ty 1)))
;; Sign-extending can't change whether a number is zero nor how it signed-compares to zero
(rule (simplify (eq _ (sextend _ x@(value_type ty)) (iconst_s _ 0)))

20
cranelift/codegen/src/opts/icmp.isle

@ -2,16 +2,16 @@
;; `x == x` is always true for integers; `x != x` is false. Strict
;; inequalities are false, and loose inequalities are true.
(rule (simplify (eq (ty_int ty) x x)) (iconst_u ty 1))
(rule (simplify (ne (ty_int ty) x x)) (iconst_u ty 0))
(rule (simplify (ugt (ty_int ty) x x)) (iconst_u ty 0))
(rule (simplify (uge (ty_int ty) x x)) (iconst_u ty 1))
(rule (simplify (sgt (ty_int ty) x x)) (iconst_u ty 0))
(rule (simplify (sge (ty_int ty) x x)) (iconst_u ty 1))
(rule (simplify (ult (ty_int ty) x x)) (iconst_u ty 0))
(rule (simplify (ule (ty_int ty) x x)) (iconst_u ty 1))
(rule (simplify (slt (ty_int ty) x x)) (iconst_u ty 0))
(rule (simplify (sle (ty_int ty) x x)) (iconst_u ty 1))
(rule (simplify (eq (ty_int ty) x x)) (subsume (iconst_u ty 1)))
(rule (simplify (ne (ty_int ty) x x)) (subsume (iconst_u ty 0)))
(rule (simplify (ugt (ty_int ty) x x)) (subsume (iconst_u ty 0)))
(rule (simplify (uge (ty_int ty) x x)) (subsume (iconst_u ty 1)))
(rule (simplify (sgt (ty_int ty) x x)) (subsume (iconst_u ty 0)))
(rule (simplify (sge (ty_int ty) x x)) (subsume (iconst_u ty 1)))
(rule (simplify (ult (ty_int ty) x x)) (subsume (iconst_u ty 0)))
(rule (simplify (ule (ty_int ty) x x)) (subsume (iconst_u ty 1)))
(rule (simplify (slt (ty_int ty) x x)) (subsume (iconst_u ty 0)))
(rule (simplify (sle (ty_int ty) x x)) (subsume (iconst_u ty 1)))
;; Optimize icmp-of-icmp.
(rule (simplify (ne ty

Loading…
Cancel
Save