Cranelift: add note to opts/README.md describing new mid-end rule guidance after #7999. (#8015)

While debugging #7999, we learned of a possible, extremely subtle,
interaction between the design of o

Cranelift: add note to opts/README.md describing new mid-end rule guidance after #7999. (#8015)

While debugging #7999, we learned of a possible, extremely subtle,
interaction between the design of our ISLE mid-end prelude and matching
rules with a certain structure. Because a `Value` represents an entire
eclass, separate left-hand sides (as in helper rules or if-let clauses)
that match on the value may match against different enodes returned by
the multi-match extractor's iterator. We then may infer some property of
one enode, another property of another enode, and perform a rewrite that
is only valid if both of those matches are on the same enode.

The precise distinction is whether it is a property of the *value* -- e.g.,
nonzero, or even, or within a range -- or a property of the *operation*
and matched subpieces. The former is fine, the latter runs into
trouble. We found that #7719 added a helper that determined whether a
value "was a certain operator" -- actually, had any enode of a certain
operator -- and separately, matched "the operator" and extracted its
opcode and parameters (actually, *any* binary operator). The first half
can match an opcode we support simplifying, and the second half can get
the arguments and `op` and blindly use them in the rewrite.

This PR adds new guidance to avoid complex helpers and be aware of
multi-matching behavior, preferring to write patterns directly (as the
fix in #8005 does) instead. Longer-term, we also have other ideas, e.g.
@jameysharp's suggestion to disallow at-patterns on multi-extractors in
left hand sides to reduce the chance of hitting this footgun.

show more ...

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

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

show more ...

Cranelift: Use a fixpoint loop to compute the best value for each eclass (#7859)

* Cranelift: Use a fixpoint loop to compute the best value for each eclass

Fixes #7857

* Remove fixpoint loop early

Cranelift: Use a fixpoint loop to compute the best value for each eclass (#7859)

* Cranelift: Use a fixpoint loop to compute the best value for each eclass

Fixes #7857

* Remove fixpoint loop early-continue optimization

* Add document describing optimization rule invariants

* Make select optimizations use subsume

* Remove invalid debug assert

* Remove now-unused methods

* Add commutative adds to cost tests

show more ...

ISLE: split algebraic.isle into several files (#6140)

* ISLE: split algebraic.isle into several files

* delete `algebraic.clif`

* Add `README.md`

* Remove old `algebraic.clif` tests

---------

C

ISLE: split algebraic.isle into several files (#6140)

* ISLE: split algebraic.isle into several files

* delete `algebraic.clif`

* Add `README.md`

* Remove old `algebraic.clif` tests

---------

Co-authored-by: Jamey Sharp <[email protected]>

show more ...