Feature

We currently have simplification rules in opts/algebraic.isle to rewrite x/1 to x, and in opts/cprop.isle to constant-fold division when both operands are constant. But these rules can't fire, because simplify is only called on instructions which never have side effects, and division may trap if the divisor is 0.

I'd like to be able to use simplification rules like these on trapping arithmetic.

Benefit

We could optimize away more instructions. There are comments in algebraic.isle suggesting more desired optimizations that we can't implement today either:

;; TODO: strength reduction: div to shifts
;; TODO: div/rem by constants -> magic multiplications

In addition to replacing expressions with simpler equivalents, we could sometimes remove them entirely if they're unused. We currently can't do that because if the instruction would trap then we need to ensure that trap occurs. But if we have a valid rewrite from a possibly-trapping instruction to an expression which can't trap, then it's actually safe to treat it as a pure instruction.

I suspect this might be particularly valuable for uadd_overflow_trap, which is used in bounds checks for dynamic heaps in cranelift-wasm.

Implementation

One idea is in #5796, but that approach was not selected in #5800 because it "is a little more complex than I would like". I still like the idea of a force instruction to pull otherwise-pure instructions into the side-effecting skeleton, but it's possible some other approach is better.

Alternatives

We could maybe call simplify from the is_mergeable_for_egraph branch of optimize_skeleton_inst, or introduce a new ISLE term for simplifying idempotent instructions.