;; The strength reductions.
;;
;; Tier two of `spec/optimizer/13-rewrite-rules.md` section 13.4: an operation replaced by a
;; cheaper one that computes the same thing. Where tier one takes an operation away, these swap
;; one for another, so each of them is a claim about cost as well as a claim about value, and the
;; cost claim is the one a rule file cannot check. Every rule here replaces a multiply or a divide
;; with an add, a subtract or a mask, and there is no machine rucc targets where that is the wrong
;; way round.
;;
;; What a rule means and how it is proved is the same as tier one, and the header of
;; `simplify.rules` says it: the pattern and the replacement are both written out at the width they
;; hold at, `rucc-verify` proves each of them against `crates/rucc-ir/rules/ir.model` before it may
;; be used, and the `spec` clause states by hand what the rule claims so that the claim is checked
;; rather than trusted.
;;
;; The one thing that is new here is the shape of the replacement. Tier one leaves a value or a
;; number, and both of those are answers about the instruction that matched. These leave another
;; instruction, which the matched one becomes where it stands. That is what `crate::simplify`
;; learned in order to have this file, and it is the reason the file exists as a tier of its own
;; rather than as more lines in `simplify.rules`.
;;
;; What is not here yet is most of tier two, and it is out for one reason. Multiplying by any power
;; of two is a shift by the log of it, dividing an unsigned value by one is a shift the same way,
;; and taking the remainder is a mask, and each of those needs the replacement to work a number out
;; of the number the pattern matched. A replacement can only write a number it was written with, so
;; the general forms would have to be written once per power of two per width, which is three
;; hundred and forty eight rules for what the spec asks for as one line each. Issue 523 is that
;; missing piece. Everything here is a case where the answer is a literal and no arithmetic is
;; needed to reach it, which is why these are the ones that could be written first, and none of
;; them is subsumed by the general forms when those arrive: multiplying by two is an addition
;; rather than a shift, and minus one is not a power of two at all.
;; Multiplying by two.
;;
;; An addition rather than a shift, which is the one place a power of two is worth a special case.
;; A doubling is an add on every machine rucc targets and is a shift on the same ones, and the add
;; is the one the register allocator and the address mode matcher have more to do with: `lea` takes
;; an addition and takes no shift by a variable, and an add of a value with itself is the form the
;; back end already reads. So this stays when the general shift rule arrives, and stays above it.
;;
;; Both orders, because nothing puts the constant on the right yet. That is tier three.
(rule (simplify (mul.i8 (value.i8 x) (iconst.i8 2)))
(add.i8 (value.i8 x) (value.i8 x))
(spec (= (bvmul x 2) (result))))
(rule (simplify (mul.i8 (iconst.i8 2) (value.i8 x)))
(add.i8 (value.i8 x) (value.i8 x))
(spec (= (bvmul 2 x) (result))))
(rule (simplify (mul.i16 (value.i16 x) (iconst.i16 2)))
(add.i16 (value.i16 x) (value.i16 x))
(spec (= (bvmul x 2) (result))))
(rule (simplify (mul.i16 (iconst.i16 2) (value.i16 x)))
(add.i16 (value.i16 x) (value.i16 x))
(spec (= (bvmul 2 x) (result))))
(rule (simplify (mul.i32 (value.i32 x) (iconst.i32 2)))
(add.i32 (value.i32 x) (value.i32 x))
(spec (= (bvmul x 2) (result))))
(rule (simplify (mul.i32 (iconst.i32 2) (value.i32 x)))
(add.i32 (value.i32 x) (value.i32 x))
(spec (= (bvmul 2 x) (result))))
(rule (simplify (mul.i64 (value.i64 x) (iconst.i64 2)))
(add.i64 (value.i64 x) (value.i64 x))
(spec (= (bvmul x 2) (result))))
(rule (simplify (mul.i64 (iconst.i64 2) (value.i64 x)))
(add.i64 (value.i64 x) (value.i64 x))
(spec (= (bvmul 2 x) (result))))
;; Multiplying by minus one.
;;
;; A subtraction from nothing, which is what every machine spells as a negate. Minus one is not a
;; power of two and no shift computes this, so no later rule reaches it and this is the whole of
;; the case.
;;
;; The number written into the replacement is where the second shape of replacement earns itself.
;; Nothing in the function holds a zero for the rule to point at, so the rewrite has to define one,
;; and an `iconst` in front of the instruction is what that means.
(rule (simplify (mul.i8 (value.i8 x) (iconst.i8 -1)))
(sub.i8 (iconst.i8 0) (value.i8 x))
(spec (= (bvmul x -1) (result))))
(rule (simplify (mul.i8 (iconst.i8 -1) (value.i8 x)))
(sub.i8 (iconst.i8 0) (value.i8 x))
(spec (= (bvmul -1 x) (result))))
(rule (simplify (mul.i16 (value.i16 x) (iconst.i16 -1)))
(sub.i16 (iconst.i16 0) (value.i16 x))
(spec (= (bvmul x -1) (result))))
(rule (simplify (mul.i16 (iconst.i16 -1) (value.i16 x)))
(sub.i16 (iconst.i16 0) (value.i16 x))
(spec (= (bvmul -1 x) (result))))
(rule (simplify (mul.i32 (value.i32 x) (iconst.i32 -1)))
(sub.i32 (iconst.i32 0) (value.i32 x))
(spec (= (bvmul x -1) (result))))
(rule (simplify (mul.i32 (iconst.i32 -1) (value.i32 x)))
(sub.i32 (iconst.i32 0) (value.i32 x))
(spec (= (bvmul -1 x) (result))))
(rule (simplify (mul.i64 (value.i64 x) (iconst.i64 -1)))
(sub.i64 (iconst.i64 0) (value.i64 x))
(spec (= (bvmul x -1) (result))))
(rule (simplify (mul.i64 (iconst.i64 -1) (value.i64 x)))
(sub.i64 (iconst.i64 0) (value.i64 x))
(spec (= (bvmul -1 x) (result))))
;; Dividing by minus one.
;;
;; The same negation, and the one rule here worth reading twice, because in C this is the division
;; that can trap. `INT_MIN / -1` has no answer in the type and x86 raises on it, which is why the
;; C standard leaves it undefined. The IR does not: `spec/optimizer/13-rewrite-rules.md` asks every
;; rule to be proved against the model, the model gives signed division the SMT meaning, and there
;; the answer at that one input is `INT_MIN` because the multiplication wraps. Subtracting `INT_MIN`
;; from nothing wraps to `INT_MIN` as well, so the two agree at every input including that one and
;; the rewrite needs nothing assumed about the operand.
;;
;; The program that reaches the divide with `INT_MIN` was undefined before this rule and is
;; undefined after it. What changes is that it stops raising, which is a better answer to give a
;; program that has already gone wrong than a signal is, and it is what GCC does too.
(rule (simplify (sdiv.i8 (value.i8 x) (iconst.i8 -1)))
(sub.i8 (iconst.i8 0) (value.i8 x))
(spec (= (bvsdiv x -1) (result))))
(rule (simplify (sdiv.i16 (value.i16 x) (iconst.i16 -1)))
(sub.i16 (iconst.i16 0) (value.i16 x))
(spec (= (bvsdiv x -1) (result))))
(rule (simplify (sdiv.i32 (value.i32 x) (iconst.i32 -1)))
(sub.i32 (iconst.i32 0) (value.i32 x))
(spec (= (bvsdiv x -1) (result))))
(rule (simplify (sdiv.i64 (value.i64 x) (iconst.i64 -1)))
(sub.i64 (iconst.i64 0) (value.i64 x))
(spec (= (bvsdiv x -1) (result))))
;; The remainder of minus one.
;;
;; Nothing, at every input, for the reason the division above gives: the quotient times minus one
;; is the value back again even where it wraps, so there is never anything left over. This one
;; leaves a number rather than an instruction, which tier one's shape already covers, and it is
;; here rather than there because a divide becoming a constant is a strength reduction and the
;; tiers are about what a rule does rather than about what it leaves.
(rule (simplify (srem.i8 (value.i8 x) (iconst.i8 -1)))
(iconst.i8 0)
(spec (= (bvsrem x -1) (result))))
(rule (simplify (srem.i16 (value.i16 x) (iconst.i16 -1)))
(iconst.i16 0)
(spec (= (bvsrem x -1) (result))))
(rule (simplify (srem.i32 (value.i32 x) (iconst.i32 -1)))
(iconst.i32 0)
(spec (= (bvsrem x -1) (result))))
(rule (simplify (srem.i64 (value.i64 x) (iconst.i64 -1)))
(iconst.i64 0)
(spec (= (bvsrem x -1) (result))))