;; 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`.
;;
;; The other thing that is new is the general forms at the end of the file. 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 unsigned remainder is a mask, and each of those needs the replacement to
;; work a number out of the number the pattern matched. A replacement used to be able to write only
;; a number it was written with, so the general forms would have had 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 the piece that was missing and `(ctz.iN k)` is what it added: a term in
;; a replacement whose head is arithmetic is compiled into a function of the bindings the way a
;; guard already was, and the model says what it means at each width so that the rule is proved as
;; it stands rather than as sixty three instances of it.
;;
;; The special cases above the general forms are not subsumed by them and none of them is dead.
;; Multiplying by two is an addition rather than a shift, minus one is not a power of two at all,
;; and a rule naming its constant is more specific than a rule taking whatever constant is there,
;; so the trie tries it first without anything having to sort them.
;; 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))))
;; Multiplying by a power of two.
;;
;; A shift by the log of it, which is the first rule in the tree whose replacement holds a number
;; nobody wrote down. `(ctz.i32 k)` counts the zero bits the matched constant ends in, which is its
;; log when the guard has said it is a power of two, and that is the whole of what issue 523 was
;; about: without it this is thirty one rules at this width and sixty three at the next.
;;
;; The guard does two jobs. It refuses a constant that is not a power of two, and it refuses zero,
;; which matters twice over: zero is not a power of two, and a count of trailing zeros in a number
;; with none set is the width rather than a shift the machine could do.
;;
;; The count fits the width in every case the guard lets through, so the shift is never one the IR
;; has to take modulo anything. That is why the proof goes through against a model that masks the
;; count: the mask takes nothing off a number below the width.
;;
;; Both orders, for the reason the doubling above gives: nothing puts the constant on the right
;; yet, and that is tier three.
(rule (simplify (mul.i8 (value.i8 x) (iconst.i8 k)))
(if (power_of_two.i8 k))
(shl.i8 (value.i8 x) (iconst.i8 (ctz.i8 k)))
(spec (= (bvmul x k) (result))))
(rule (simplify (mul.i8 (iconst.i8 k) (value.i8 x)))
(if (power_of_two.i8 k))
(shl.i8 (value.i8 x) (iconst.i8 (ctz.i8 k)))
(spec (= (bvmul k x) (result))))
(rule (simplify (mul.i16 (value.i16 x) (iconst.i16 k)))
(if (power_of_two.i16 k))
(shl.i16 (value.i16 x) (iconst.i16 (ctz.i16 k)))
(spec (= (bvmul x k) (result))))
(rule (simplify (mul.i16 (iconst.i16 k) (value.i16 x)))
(if (power_of_two.i16 k))
(shl.i16 (value.i16 x) (iconst.i16 (ctz.i16 k)))
(spec (= (bvmul k x) (result))))
(rule (simplify (mul.i32 (value.i32 x) (iconst.i32 k)))
(if (power_of_two.i32 k))
(shl.i32 (value.i32 x) (iconst.i32 (ctz.i32 k)))
(spec (= (bvmul x k) (result))))
(rule (simplify (mul.i32 (iconst.i32 k) (value.i32 x)))
(if (power_of_two.i32 k))
(shl.i32 (value.i32 x) (iconst.i32 (ctz.i32 k)))
(spec (= (bvmul k x) (result))))
(rule (simplify (mul.i64 (value.i64 x) (iconst.i64 k)))
(if (power_of_two.i64 k))
(shl.i64 (value.i64 x) (iconst.i64 (ctz.i64 k)))
(spec (= (bvmul x k) (result))))
(rule (simplify (mul.i64 (iconst.i64 k) (value.i64 x)))
(if (power_of_two.i64 k))
(shl.i64 (value.i64 x) (iconst.i64 (ctz.i64 k)))
(spec (= (bvmul k x) (result))))
;; Dividing an unsigned value by a power of two.
;;
;; A shift the other way, and unsigned only. The signed division is not this rule and is not one
;; line: a negative value divided by a power of two rounds towards zero and an arithmetic shift
;; rounds away from it, so the signed form needs a bias added before the shift and that is a
;; sequence rather than a rewrite. `spec/optimizer/13-rewrite-rules.md` leaves it to the pass that
;; can write more than one instruction.
;;
;; One order only, since nothing divides the other way round.
(rule (simplify (udiv.i8 (value.i8 x) (iconst.i8 k)))
(if (power_of_two.i8 k))
(lshr.i8 (value.i8 x) (iconst.i8 (ctz.i8 k)))
(spec (= (bvudiv x k) (result))))
(rule (simplify (udiv.i16 (value.i16 x) (iconst.i16 k)))
(if (power_of_two.i16 k))
(lshr.i16 (value.i16 x) (iconst.i16 (ctz.i16 k)))
(spec (= (bvudiv x k) (result))))
(rule (simplify (udiv.i32 (value.i32 x) (iconst.i32 k)))
(if (power_of_two.i32 k))
(lshr.i32 (value.i32 x) (iconst.i32 (ctz.i32 k)))
(spec (= (bvudiv x k) (result))))
(rule (simplify (udiv.i64 (value.i64 x) (iconst.i64 k)))
(if (power_of_two.i64 k))
(lshr.i64 (value.i64 x) (iconst.i64 (ctz.i64 k)))
(spec (= (bvudiv x k) (result))))
;; The unsigned remainder of a power of two.
;;
;; A mask of the bits below it, which is the one of the three that needs no count of anything: what
;; is left over after dividing by a power of two is exactly the bits the division shifted out. The
;; replacement works the mask out with the same arithmetic the guards use, which is what a computed
;; piece is for whether the sum is a count of bits or a subtraction.
;;
;; Unsigned only, for the reason the division above gives.
(rule (simplify (urem.i8 (value.i8 x) (iconst.i8 k)))
(if (power_of_two.i8 k))
(and.i8 (value.i8 x) (iconst.i8 (- k 1)))
(spec (= (bvurem x k) (result))))
(rule (simplify (urem.i16 (value.i16 x) (iconst.i16 k)))
(if (power_of_two.i16 k))
(and.i16 (value.i16 x) (iconst.i16 (- k 1)))
(spec (= (bvurem x k) (result))))
(rule (simplify (urem.i32 (value.i32 x) (iconst.i32 k)))
(if (power_of_two.i32 k))
(and.i32 (value.i32 x) (iconst.i32 (- k 1)))
(spec (= (bvurem x k) (result))))
(rule (simplify (urem.i64 (value.i64 x) (iconst.i64 k)))
(if (power_of_two.i64 k))
(and.i64 (value.i64 x) (iconst.i64 (- k 1)))
(spec (= (bvurem x k) (result))))