Add missing subsume uses in egraph rules (#7879)

elliottt · web-flow · commit 7464bbcb3b9b · 2024-02-06T20:16:03.000Z
* 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
diff --git a/cranelift/codegen/src/opts/README.md b/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
diff --git a/cranelift/codegen/src/opts/extends.isle b/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)))
diff --git a/cranelift/codegen/src/opts/icmp.isle b/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
