;; Lowering AArch64.
;;
;; The same claim `x86-64.rules` makes, rule by rule: an IR term and a machine term compute the same
;; thing, and `rucc-verify` proves it against `aarch64.model` before the rule may be used. The IR
;; half of every rule is the one the x86-64 file matches, since the IR is not about a target.
;;
;; The machine has registers of thirty two and sixty four bits and nothing narrower, so a value of
;; eight or sixteen bits lives in the low end of a thirty two bit register and what is above it
;; means nothing. The arithmetic whose low bits do not depend on the high ones takes the thirty two
;; bit instruction at those widths, and the verifier holds it to the bits the IR term has. The
;; rest, which is right shifts, division and comparisons, widens first, so each of those is more
;; than one instruction at those widths.
;;
;; A machine term inside another one is an instruction of its own, built first into a register of its
;; own, which is how a remainder is written: the division, then a multiply subtract that takes the
;; quotient times the divisor away from the dividend. A constant too wide for one `mov` is built the
;; same way, as a `mov` of its low sixteen bits with a `movk` for each piece above them.
;; Constants. One `mov` builds anything sixteen bits wide and anything whose complement is, and
;; that covers every constant of eight and sixteen bits as the IR holds them, sign extended. A
;; wider one is built a piece at a time, unless all but one of its sixteen bit pieces are zero or
;; all of them ones, which is a single `movz` or `movn` with a shift and is what a `double` like
;; 3.0 looks like as bits. The rules for one width share a pattern and the first whose guard
;; holds is the one that fires, so a constant takes as few instructions as these rules know how
;; to give it.
(rule (lower (iconst.i1 k))
(a64.mov_ri_32 k)
(spec (= k (result))))
(rule (lower (iconst.i8 k))
(a64.mov_ri_32 k)
(spec (= k (result))))
(rule (lower (iconst.i16 k))
(a64.mov_ri_32 k)
(spec (= k (result))))
(rule (lower (iconst.i32 k))
(if (and (>= k -65536) (< k 65536)))
(a64.mov_ri_32 k)
(spec (= k (result))))
(rule (lower (iconst.i32 k))
(if (or (= (extract 15 0 k) 0) (= (extract 15 0 k) 65535)))
(a64.mov_ri_32 k)
(spec (= k (result))))
(rule (lower (iconst.i32 k))
(a64.movk_ri_16_32 (a64.mov_ri_32 (zero_extend 16 32 (extract 15 0 k)))
(zero_extend 16 32 (extract 31 16 k)))
(spec (= k (result))))
(rule (lower (iconst.i64 k))
(if (and (>= k -65536) (< k 65536)))
(a64.mov_ri_64 k)
(spec (= k (result))))
(rule (lower (iconst.i64 k))
(if (or (and (= (extract 15 0 k) 0) (= (extract 63 32 k) 0))
(and (= (extract 31 0 k) 0) (= (extract 63 48 k) 0))
(= (extract 47 0 k) 0)
(and (= (extract 15 0 k) 65535) (= (extract 63 32 k) 4294967295))
(and (= (extract 31 0 k) 4294967295) (= (extract 63 48 k) 65535))
(= (extract 47 0 k) 281474976710655)))
(a64.mov_ri_64 k)
(spec (= k (result))))
(rule (lower (iconst.i64 k))
(if (and (>= k 0) (< k 4294967296)))
(a64.movk_ri_16_64 (a64.mov_ri_64 (zero_extend 16 64 (extract 15 0 k)))
(zero_extend 16 64 (extract 31 16 k)))
(spec (= k (result))))
(rule (lower (iconst.i64 k))
(if (= (extract 63 48 k) 0))
(a64.movk_ri_32_64
(a64.movk_ri_16_64 (a64.mov_ri_64 (zero_extend 16 64 (extract 15 0 k)))
(zero_extend 16 64 (extract 31 16 k)))
(zero_extend 16 64 (extract 47 32 k)))
(spec (= k (result))))
(rule (lower (iconst.i64 k))
(a64.movk_ri_48_64
(a64.movk_ri_32_64
(a64.movk_ri_16_64 (a64.mov_ri_64 (zero_extend 16 64 (extract 15 0 k)))
(zero_extend 16 64 (extract 31 16 k)))
(zero_extend 16 64 (extract 47 32 k)))
(zero_extend 16 64 (extract 63 48 k)))
(spec (= k (result))))
;; Arithmetic, register with register.
(rule (lower (add.i8 (value.i8 x) (value.i8 y)))
(a64.add_rr_32 x y)
(spec (= (bvadd x y) (result))))
(rule (lower (add.i16 (value.i16 x) (value.i16 y)))
(a64.add_rr_32 x y)
(spec (= (bvadd x y) (result))))
(rule (lower (add.i32 (value.i32 x) (value.i32 y)))
(a64.add_rr_32 x y)
(spec (= (bvadd x y) (result))))
(rule (lower (add.i64 (value.i64 x) (value.i64 y)))
(a64.add_rr_64 x y)
(spec (= (bvadd x y) (result))))
(rule (lower (sub.i8 (value.i8 x) (value.i8 y)))
(a64.sub_rr_32 x y)
(spec (= (bvsub x y) (result))))
(rule (lower (sub.i16 (value.i16 x) (value.i16 y)))
(a64.sub_rr_32 x y)
(spec (= (bvsub x y) (result))))
(rule (lower (sub.i32 (value.i32 x) (value.i32 y)))
(a64.sub_rr_32 x y)
(spec (= (bvsub x y) (result))))
(rule (lower (sub.i64 (value.i64 x) (value.i64 y)))
(a64.sub_rr_64 x y)
(spec (= (bvsub x y) (result))))
(rule (lower (and.i8 (value.i8 x) (value.i8 y)))
(a64.and_rr_32 x y)
(spec (= (bvand x y) (result))))
(rule (lower (and.i16 (value.i16 x) (value.i16 y)))
(a64.and_rr_32 x y)
(spec (= (bvand x y) (result))))
(rule (lower (and.i32 (value.i32 x) (value.i32 y)))
(a64.and_rr_32 x y)
(spec (= (bvand x y) (result))))
(rule (lower (and.i64 (value.i64 x) (value.i64 y)))
(a64.and_rr_64 x y)
(spec (= (bvand x y) (result))))
(rule (lower (or.i8 (value.i8 x) (value.i8 y)))
(a64.orr_rr_32 x y)
(spec (= (bvor x y) (result))))
(rule (lower (or.i16 (value.i16 x) (value.i16 y)))
(a64.orr_rr_32 x y)
(spec (= (bvor x y) (result))))
(rule (lower (or.i32 (value.i32 x) (value.i32 y)))
(a64.orr_rr_32 x y)
(spec (= (bvor x y) (result))))
(rule (lower (or.i64 (value.i64 x) (value.i64 y)))
(a64.orr_rr_64 x y)
(spec (= (bvor x y) (result))))
(rule (lower (xor.i8 (value.i8 x) (value.i8 y)))
(a64.eor_rr_32 x y)
(spec (= (bvxor x y) (result))))
(rule (lower (xor.i16 (value.i16 x) (value.i16 y)))
(a64.eor_rr_32 x y)
(spec (= (bvxor x y) (result))))
(rule (lower (xor.i32 (value.i32 x) (value.i32 y)))
(a64.eor_rr_32 x y)
(spec (= (bvxor x y) (result))))
(rule (lower (xor.i64 (value.i64 x) (value.i64 y)))
(a64.eor_rr_64 x y)
(spec (= (bvxor x y) (result))))
(rule (lower (mul.i8 (value.i8 x) (value.i8 y)))
(a64.mul_rr_32 x y)
(spec (= (bvmul x y) (result))))
(rule (lower (mul.i16 (value.i16 x) (value.i16 y)))
(a64.mul_rr_32 x y)
(spec (= (bvmul x y) (result))))
(rule (lower (mul.i32 (value.i32 x) (value.i32 y)))
(a64.mul_rr_32 x y)
(spec (= (bvmul x y) (result))))
(rule (lower (mul.i64 (value.i64 x) (value.i64 y)))
(a64.mul_rr_64 x y)
(spec (= (bvmul x y) (result))))
;; The high half of a product, which is what a division by a constant multiplies for.
(rule (lower (umulh.i64 (value.i64 x) (value.i64 y)))
(a64.umulh_rr_64 x y)
(spec (= (extract 127 64 (bvmul (zero_extend 64 128 x) (zero_extend 64 128 y))) (result))))
(rule (lower (smulh.i64 (value.i64 x) (value.i64 y)))
(a64.smulh_rr_64 x y)
(spec (= (extract 127 64 (bvmul (sign_extend 64 128 x) (sign_extend 64 128 y))) (result))))
;; The three bitwise operations at one bit, which take zeros and ones to zeros and ones.
(rule (lower (and.i1 (value.i1 x) (value.i1 y)))
(a64.and_rr_32 x y)
(spec (= (bvand x y) (result))))
(rule (lower (or.i1 (value.i1 x) (value.i1 y)))
(a64.orr_rr_32 x y)
(spec (= (bvor x y) (result))))
(rule (lower (xor.i1 (value.i1 x) (value.i1 y)))
(a64.eor_rr_32 x y)
(spec (= (bvxor x y) (result))))
;; Arithmetic with an immediate. The instruction holds twelve bits, unsigned, and a negative one
;; would be the other instruction with the constant negated, which is a computation the verifier has
;; no way to read yet. A constant outside the range is left to the register form.
(rule (lower (add.i8 (value.i8 x) (iconst.i8 k)))
(if (and (>= k 0) (< k 4096)))
(a64.add_ri_32 x k)
(spec (= (bvadd x k) (result))))
(rule (lower (add.i16 (value.i16 x) (iconst.i16 k)))
(if (and (>= k 0) (< k 4096)))
(a64.add_ri_32 x k)
(spec (= (bvadd x k) (result))))
(rule (lower (add.i32 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.add_ri_32 x k)
(spec (= (bvadd x k) (result))))
(rule (lower (add.i64 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.add_ri_64 x k)
(spec (= (bvadd x k) (result))))
(rule (lower (sub.i8 (value.i8 x) (iconst.i8 k)))
(if (and (>= k 0) (< k 4096)))
(a64.sub_ri_32 x k)
(spec (= (bvsub x k) (result))))
(rule (lower (sub.i16 (value.i16 x) (iconst.i16 k)))
(if (and (>= k 0) (< k 4096)))
(a64.sub_ri_32 x k)
(spec (= (bvsub x k) (result))))
(rule (lower (sub.i32 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.sub_ri_32 x k)
(spec (= (bvsub x k) (result))))
(rule (lower (sub.i64 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.sub_ri_64 x k)
(spec (= (bvsub x k) (result))))
;; Negation and complement, which the IR writes as arithmetic against a constant.
(rule (lower (sub.i8 (iconst.i8 0) (value.i8 x)))
(a64.neg_r_32 x)
(spec (= (bvsub 0 x) (result))))
(rule (lower (sub.i16 (iconst.i16 0) (value.i16 x)))
(a64.neg_r_32 x)
(spec (= (bvsub 0 x) (result))))
(rule (lower (sub.i32 (iconst.i32 0) (value.i32 x)))
(a64.neg_r_32 x)
(spec (= (bvsub 0 x) (result))))
(rule (lower (sub.i64 (iconst.i64 0) (value.i64 x)))
(a64.neg_r_64 x)
(spec (= (bvsub 0 x) (result))))
(rule (lower (xor.i8 (value.i8 x) (iconst.i8 -1)))
(a64.mvn_r_32 x)
(spec (= (bvnot x) (result))))
(rule (lower (xor.i16 (value.i16 x) (iconst.i16 -1)))
(a64.mvn_r_32 x)
(spec (= (bvnot x) (result))))
(rule (lower (xor.i32 (value.i32 x) (iconst.i32 -1)))
(a64.mvn_r_32 x)
(spec (= (bvnot x) (result))))
(rule (lower (xor.i64 (value.i64 x) (iconst.i64 -1)))
(a64.mvn_r_64 x)
(spec (= (bvnot x) (result))))
;; Division. The IR never carries a division by zero, so what the machine does with one, which is
;; to give back zero rather than trap, is not something any rule here relies on.
(rule (lower (sdiv.i32 (value.i32 x) (value.i32 y)))
(a64.sdiv_rr_32 x y)
(spec (= (bvsdiv x y) (result))))
(rule (lower (sdiv.i64 (value.i64 x) (value.i64 y)))
(a64.sdiv_rr_64 x y)
(spec (= (bvsdiv x y) (result))))
(rule (lower (udiv.i32 (value.i32 x) (value.i32 y)))
(a64.udiv_rr_32 x y)
(spec (= (bvudiv x y) (result))))
(rule (lower (udiv.i64 (value.i64 x) (value.i64 y)))
(a64.udiv_rr_64 x y)
(spec (= (bvudiv x y) (result))))
;; Remainder, as what is left of the dividend once the quotient times the divisor is taken away.
(rule (lower (srem.i32 (value.i32 x) (value.i32 y)))
(a64.msub_rrr_32 (a64.sdiv_rr_32 x y) y x)
(spec (= (bvsrem x y) (result)))
(bounded "a remainder multiplies the quotient back by the divisor, and that is a multiply of two unknowns no solver settles at thirty two bits or more, while the same rule at eight bits is settled at once"))
(rule (lower (srem.i64 (value.i64 x) (value.i64 y)))
(a64.msub_rrr_64 (a64.sdiv_rr_64 x y) y x)
(spec (= (bvsrem x y) (result)))
(bounded "a remainder multiplies the quotient back by the divisor, and that is a multiply of two unknowns no solver settles at thirty two bits or more, while the same rule at eight bits is settled at once"))
(rule (lower (urem.i32 (value.i32 x) (value.i32 y)))
(a64.msub_rrr_32 (a64.udiv_rr_32 x y) y x)
(spec (= (bvurem x y) (result)))
(bounded "a remainder multiplies the quotient back by the divisor, and that is a multiply of two unknowns no solver settles at thirty two bits or more, while the same rule at eight bits is settled at once"))
(rule (lower (urem.i64 (value.i64 x) (value.i64 y)))
(a64.msub_rrr_64 (a64.udiv_rr_64 x y) y x)
(spec (= (bvurem x y) (result)))
(bounded "a remainder multiplies the quotient back by the divisor, and that is a multiply of two unknowns no solver settles at thirty two bits or more, while the same rule at eight bits is settled at once"))
;; A division of bytes or halves, which the width narrowing pass writes when both operands were
;; widened from the same narrow type. There is no divide narrower than thirty two bits, and the
;; bits above a narrow value in its register mean nothing, so each operand is widened the way the
;; division reads it, divided at thirty two bits, and the low end of the quotient is the answer.
;; That is the same quotient: a zero extension divides as the narrow unsigned value does, and a
;; sign extension divides as the narrow signed one does, including the most negative value over
;; minus one, whose thirty two bit quotient is the narrow one with its sign bit cleared and has
;; the same low bits. A remainder is the multiply subtract over the same widened operands.
(rule (lower (udiv.i8 (value.i8 x) (value.i8 y)))
(a64.low_8 (a64.udiv_rr_32 (a64.uxtb_32 x) (a64.uxtb_32 y)))
(spec (= (bvudiv x y) (result))))
(rule (lower (sdiv.i8 (value.i8 x) (value.i8 y)))
(a64.low_8 (a64.sdiv_rr_32 (a64.sxtb_32 x) (a64.sxtb_32 y)))
(spec (= (bvsdiv x y) (result))))
(rule (lower (urem.i8 (value.i8 x) (value.i8 y)))
(a64.low_8 (a64.msub_rrr_32 (a64.udiv_rr_32 (a64.uxtb_32 x) (a64.uxtb_32 y))
(a64.uxtb_32 y) (a64.uxtb_32 x)))
(spec (= (bvurem x y) (result))))
(rule (lower (srem.i8 (value.i8 x) (value.i8 y)))
(a64.low_8 (a64.msub_rrr_32 (a64.sdiv_rr_32 (a64.sxtb_32 x) (a64.sxtb_32 y))
(a64.sxtb_32 y) (a64.sxtb_32 x)))
(spec (= (bvsrem x y) (result))))
(rule (lower (udiv.i16 (value.i16 x) (value.i16 y)))
(a64.low_16 (a64.udiv_rr_32 (a64.uxth_32 x) (a64.uxth_32 y)))
(spec (= (bvudiv x y) (result))))
(rule (lower (sdiv.i16 (value.i16 x) (value.i16 y)))
(a64.low_16 (a64.sdiv_rr_32 (a64.sxth_32 x) (a64.sxth_32 y)))
(spec (= (bvsdiv x y) (result))))
(rule (lower (urem.i16 (value.i16 x) (value.i16 y)))
(a64.low_16 (a64.msub_rrr_32 (a64.udiv_rr_32 (a64.uxth_32 x) (a64.uxth_32 y))
(a64.uxth_32 y) (a64.uxth_32 x)))
(spec (= (bvurem x y) (result)))
(bounded "a remainder multiplies the quotient back by the divisor, and no solver settles that at sixteen bits, while the same rule over bytes is settled at its own width"))
(rule (lower (srem.i16 (value.i16 x) (value.i16 y)))
(a64.low_16 (a64.msub_rrr_32 (a64.sdiv_rr_32 (a64.sxth_32 x) (a64.sxth_32 y))
(a64.sxth_32 y) (a64.sxth_32 x)))
(spec (= (bvsrem x y) (result)))
(bounded "a remainder multiplies the quotient back by the divisor, and no solver settles that at sixteen bits, while the same rule over bytes is settled at its own width"))
;; Shifts by a constant. A left shift keeps its low bits whatever is above them, so it is the one
;; that reaches the narrow widths.
(rule (lower (shl.i8 (value.i8 x) (iconst.i8 k)))
(if (and (>= k 0) (< k 8)))
(a64.lsl_ri_32 x k)
(spec (= (bvshl x k) (result))))
(rule (lower (shl.i16 (value.i16 x) (iconst.i16 k)))
(if (and (>= k 0) (< k 16)))
(a64.lsl_ri_32 x k)
(spec (= (bvshl x k) (result))))
(rule (lower (shl.i32 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 32)))
(a64.lsl_ri_32 x k)
(spec (= (bvshl x k) (result))))
(rule (lower (shl.i64 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 64)))
(a64.lsl_ri_64 x k)
(spec (= (bvshl x k) (result))))
;; A right shift of a narrow value brings the bits above it down, and nothing says what those are,
;; so the instruction widens the value before it shifts. This is what reading a bitfield out of a
;; byte comes to.
(rule (lower (lshr.i8 (value.i8 x) (iconst.i8 k)))
(if (and (>= k 0) (< k 8)))
(a64.lsr_ri_8 x k)
(spec (= (bvlshr x k) (result))))
(rule (lower (lshr.i16 (value.i16 x) (iconst.i16 k)))
(if (and (>= k 0) (< k 16)))
(a64.lsr_ri_16 x k)
(spec (= (bvlshr x k) (result))))
(rule (lower (ashr.i8 (value.i8 x) (iconst.i8 k)))
(if (and (>= k 0) (< k 8)))
(a64.asr_ri_8 x k)
(spec (= (bvashr x k) (result))))
(rule (lower (ashr.i16 (value.i16 x) (iconst.i16 k)))
(if (and (>= k 0) (< k 16)))
(a64.asr_ri_16 x k)
(spec (= (bvashr x k) (result))))
(rule (lower (lshr.i32 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 32)))
(a64.lsr_ri_32 x k)
(spec (= (bvlshr x k) (result))))
(rule (lower (lshr.i64 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 64)))
(a64.lsr_ri_64 x k)
(spec (= (bvlshr x k) (result))))
(rule (lower (ashr.i32 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 32)))
(a64.asr_ri_32 x k)
(spec (= (bvashr x k) (result))))
(rule (lower (ashr.i64 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 64)))
(a64.asr_ri_64 x k)
(spec (= (bvashr x k) (result))))
;; Shifts by a register. The machine takes the count modulo the width, which is what the IR does,
;; so there is nothing to mask.
(rule (lower (shl.i32 (value.i32 x) (value.i32 y)))
(a64.lsl_rr_32 x y)
(spec (= (bvshl x (bvand y 31)) (result))))
(rule (lower (shl.i64 (value.i64 x) (value.i64 y)))
(a64.lsl_rr_64 x y)
(spec (= (bvshl x (bvand y 63)) (result))))
(rule (lower (lshr.i32 (value.i32 x) (value.i32 y)))
(a64.lsr_rr_32 x y)
(spec (= (bvlshr x (bvand y 31)) (result))))
(rule (lower (lshr.i64 (value.i64 x) (value.i64 y)))
(a64.lsr_rr_64 x y)
(spec (= (bvlshr x (bvand y 63)) (result))))
(rule (lower (ashr.i32 (value.i32 x) (value.i32 y)))
(a64.asr_rr_32 x y)
(spec (= (bvashr x (bvand y 31)) (result))))
(rule (lower (ashr.i64 (value.i64 x) (value.i64 y)))
(a64.asr_rr_64 x y)
(spec (= (bvashr x (bvand y 63)) (result))))
;; Comparisons. Each is a compare and the `cset` behind it, one term for the reason the x86-64 file
;; gives: the flags between the two are not a value. The IR's ten predicates are the machine's ten
;; integer conditions, with the unsigned ones under the names the architecture gives them.
(rule (lower (icmp_eq.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_eq_32 x y)
(spec (= (ite (= x y) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_ne_32 x y)
(spec (= (ite (not (= x y)) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_lt_32 x y)
(spec (= (ite (bvslt x y) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_le_32 x y)
(spec (= (ite (bvsle x y) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_gt_32 x y)
(spec (= (ite (bvsgt x y) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_ge_32 x y)
(spec (= (ite (bvsge x y) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_lo_32 x y)
(spec (= (ite (bvult x y) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_ls_32 x y)
(spec (= (ite (bvule x y) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_hi_32 x y)
(spec (= (ite (bvugt x y) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i32 x) (value.i32 y)))
(a64.cmp_set_hs_32 x y)
(spec (= (ite (bvuge x y) 1 0) (result))))
(rule (lower (icmp_eq.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_eq_64 x y)
(spec (= (ite (= x y) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_ne_64 x y)
(spec (= (ite (not (= x y)) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_lt_64 x y)
(spec (= (ite (bvslt x y) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_le_64 x y)
(spec (= (ite (bvsle x y) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_gt_64 x y)
(spec (= (ite (bvsgt x y) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_ge_64 x y)
(spec (= (ite (bvsge x y) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_lo_64 x y)
(spec (= (ite (bvult x y) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_ls_64 x y)
(spec (= (ite (bvule x y) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_hi_64 x y)
(spec (= (ite (bvugt x y) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i64 x) (value.i64 y)))
(a64.cmp_set_hs_64 x y)
(spec (= (ite (bvuge x y) 1 0) (result))))
;; A byte or a half is compared as the thirty two bit value it widens to, sign extended for the
;; signed predicates and zero extended for the rest, since the bits above it in the register are
;; whatever the instruction that wrote it left there. The optimizer narrows a comparison of two
;; `char` values to one of this width, so C reaches these at -O1 and above.
(rule (lower (icmp_eq.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_eq_32 (a64.uxtb_32 x) (a64.uxtb_32 y))
(spec (= (ite (= x y) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_ne_32 (a64.uxtb_32 x) (a64.uxtb_32 y))
(spec (= (ite (not (= x y)) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_lt_32 (a64.sxtb_32 x) (a64.sxtb_32 y))
(spec (= (ite (bvslt x y) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_le_32 (a64.sxtb_32 x) (a64.sxtb_32 y))
(spec (= (ite (bvsle x y) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_gt_32 (a64.sxtb_32 x) (a64.sxtb_32 y))
(spec (= (ite (bvsgt x y) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_ge_32 (a64.sxtb_32 x) (a64.sxtb_32 y))
(spec (= (ite (bvsge x y) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_lo_32 (a64.uxtb_32 x) (a64.uxtb_32 y))
(spec (= (ite (bvult x y) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_ls_32 (a64.uxtb_32 x) (a64.uxtb_32 y))
(spec (= (ite (bvule x y) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_hi_32 (a64.uxtb_32 x) (a64.uxtb_32 y))
(spec (= (ite (bvugt x y) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i8 x) (value.i8 y)))
(a64.cmp_set_hs_32 (a64.uxtb_32 x) (a64.uxtb_32 y))
(spec (= (ite (bvuge x y) 1 0) (result))))
(rule (lower (icmp_eq.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_eq_32 (a64.uxth_32 x) (a64.uxth_32 y))
(spec (= (ite (= x y) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_ne_32 (a64.uxth_32 x) (a64.uxth_32 y))
(spec (= (ite (not (= x y)) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_lt_32 (a64.sxth_32 x) (a64.sxth_32 y))
(spec (= (ite (bvslt x y) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_le_32 (a64.sxth_32 x) (a64.sxth_32 y))
(spec (= (ite (bvsle x y) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_gt_32 (a64.sxth_32 x) (a64.sxth_32 y))
(spec (= (ite (bvsgt x y) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_ge_32 (a64.sxth_32 x) (a64.sxth_32 y))
(spec (= (ite (bvsge x y) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_lo_32 (a64.uxth_32 x) (a64.uxth_32 y))
(spec (= (ite (bvult x y) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_ls_32 (a64.uxth_32 x) (a64.uxth_32 y))
(spec (= (ite (bvule x y) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_hi_32 (a64.uxth_32 x) (a64.uxth_32 y))
(spec (= (ite (bvugt x y) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i16 x) (value.i16 y)))
(a64.cmp_set_hs_32 (a64.uxth_32 x) (a64.uxth_32 y))
(spec (= (ite (bvuge x y) 1 0) (result))))
;; The same against a constant the compare can hold, which is twelve bits.
(rule (lower (icmp_eq.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_eq_ri_32 x k)
(spec (= (ite (= x k) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_ne_ri_32 x k)
(spec (= (ite (not (= x k)) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_lt_ri_32 x k)
(spec (= (ite (bvslt x k) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_le_ri_32 x k)
(spec (= (ite (bvsle x k) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_gt_ri_32 x k)
(spec (= (ite (bvsgt x k) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_ge_ri_32 x k)
(spec (= (ite (bvsge x k) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_lo_ri_32 x k)
(spec (= (ite (bvult x k) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_ls_ri_32 x k)
(spec (= (ite (bvule x k) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_hi_ri_32 x k)
(spec (= (ite (bvugt x k) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_hs_ri_32 x k)
(spec (= (ite (bvuge x k) 1 0) (result))))
(rule (lower (icmp_eq.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_eq_ri_64 x k)
(spec (= (ite (= x k) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_ne_ri_64 x k)
(spec (= (ite (not (= x k)) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_lt_ri_64 x k)
(spec (= (ite (bvslt x k) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_le_ri_64 x k)
(spec (= (ite (bvsle x k) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_gt_ri_64 x k)
(spec (= (ite (bvsgt x k) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_ge_ri_64 x k)
(spec (= (ite (bvsge x k) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_lo_ri_64 x k)
(spec (= (ite (bvult x k) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_ls_ri_64 x k)
(spec (= (ite (bvule x k) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_hi_ri_64 x k)
(spec (= (ite (bvugt x k) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i64 x) (iconst.i64 k)))
(if (and (>= k 0) (< k 4096)))
(a64.cmp_set_hs_ri_64 x k)
(spec (= (ite (bvuge x k) 1 0) (result))))
;; The choice between two values, which is a compare of the condition with zero and a `csel`. The
;; operands are in the order the x86-64 rules put them, the false arm first, so the two selectors
;; read one operand list the same way.
(rule (lower (select.i8 (value.i1 c) (value.i8 t) (value.i8 f)))
(a64.sel_32 f t c)
(spec (= (ite (not (= c 0)) t f) (result))))
(rule (lower (select.i16 (value.i1 c) (value.i16 t) (value.i16 f)))
(a64.sel_32 f t c)
(spec (= (ite (not (= c 0)) t f) (result))))
(rule (lower (select.i32 (value.i1 c) (value.i32 t) (value.i32 f)))
(a64.sel_32 f t c)
(spec (= (ite (not (= c 0)) t f) (result))))
(rule (lower (select.i64 (value.i1 c) (value.i64 t) (value.i64 f)))
(a64.sel_64 f t c)
(spec (= (ite (not (= c 0)) t f) (result))))
;; Conversions between widths. Widening a byte or a half to sixty four bits unsigned is the thirty
;; two bit instruction, since writing a W register clears the top half, and that is a second meaning
;; for one head, so it waits for a head of its own.
(rule (lower (sext.i8.i32 (value.i8 x)))
(a64.sxtb_32 x)
(spec (= (sign_extend 8 32 x) (result))))
(rule (lower (sext.i8.i64 (value.i8 x)))
(a64.sxtb_64 x)
(spec (= (sign_extend 8 64 x) (result))))
(rule (lower (sext.i16.i32 (value.i16 x)))
(a64.sxth_32 x)
(spec (= (sign_extend 16 32 x) (result))))
(rule (lower (sext.i16.i64 (value.i16 x)))
(a64.sxth_64 x)
(spec (= (sign_extend 16 64 x) (result))))
(rule (lower (sext.i32.i64 (value.i32 x)))
(a64.sxtw_64 x)
(spec (= (sign_extend 32 64 x) (result))))
(rule (lower (zext.i8.i32 (value.i8 x)))
(a64.uxtb_32 x)
(spec (= (zero_extend 8 32 x) (result))))
(rule (lower (zext.i16.i32 (value.i16 x)))
(a64.uxth_32 x)
(spec (= (zero_extend 16 32 x) (result))))
(rule (lower (zext.i32.i64 (value.i32 x)))
(a64.uxtw_64 x)
(spec (= (zero_extend 32 64 x) (result))))
;; A sixteen bit value lives in a W register the same as a thirty two bit one, so widening to it is
;; the thirty two bit instruction under a head held to the sixteen bits the result has.
(rule (lower (sext.i8.i16 (value.i8 x)))
(a64.sxtb_16 x)
(spec (= (sign_extend 8 16 x) (result))))
(rule (lower (zext.i8.i16 (value.i8 x)))
(a64.uxtb_16 x)
(spec (= (zero_extend 8 16 x) (result))))
(rule (lower (zext.i8.i64 (value.i8 x)))
(a64.uxtb_64 x)
(spec (= (zero_extend 8 64 x) (result))))
(rule (lower (zext.i16.i64 (value.i16 x)))
(a64.uxth_64 x)
(spec (= (zero_extend 16 64 x) (result))))
;; A one bit value is widened with an `and`, so nothing is taken on trust about the bits above it.
(rule (lower (zext.i1.i8 (value.i1 x)))
(a64.bit_to_8 x)
(spec (= (zero_extend 1 8 x) (result))))
(rule (lower (zext.i1.i16 (value.i1 x)))
(a64.bit_to_16 x)
(spec (= (zero_extend 1 16 x) (result))))
(rule (lower (zext.i1.i32 (value.i1 x)))
(a64.bit_to_32 x)
(spec (= (zero_extend 1 32 x) (result))))
(rule (lower (zext.i1.i64 (value.i1 x)))
(a64.bit_to_64 x)
(spec (= (zero_extend 1 64 x) (result))))
;; Narrowing. The narrow value is the low end of the wide register, and a `mov` of the W register
;; puts it in one of its own. Narrowing to one bit keeps that bit and clears the rest.
(rule (lower (trunc.i16.i8 (value.i16 x)))
(a64.low_8 x)
(spec (= (extract 7 0 x) (result))))
(rule (lower (trunc.i32.i8 (value.i32 x)))
(a64.low_8 x)
(spec (= (extract 7 0 x) (result))))
(rule (lower (trunc.i64.i8 (value.i64 x)))
(a64.low_8 x)
(spec (= (extract 7 0 x) (result))))
(rule (lower (trunc.i32.i16 (value.i32 x)))
(a64.low_16 x)
(spec (= (extract 15 0 x) (result))))
(rule (lower (trunc.i64.i16 (value.i64 x)))
(a64.low_16 x)
(spec (= (extract 15 0 x) (result))))
(rule (lower (trunc.i64.i32 (value.i64 x)))
(a64.low_32 x)
(spec (= (extract 31 0 x) (result))))
(rule (lower (trunc.i8.i1 (value.i8 x)))
(a64.bit_of_32 x 1)
(spec (= (extract 0 0 x) (result))))
(rule (lower (trunc.i16.i1 (value.i16 x)))
(a64.bit_of_32 x 1)
(spec (= (extract 0 0 x) (result))))
(rule (lower (trunc.i32.i1 (value.i32 x)))
(a64.bit_of_32 x 1)
(spec (= (extract 0 0 x) (result))))
(rule (lower (trunc.i64.i1 (value.i64 x)))
(a64.bit_of_64 x 1)
(spec (= (extract 0 0 x) (result))))
;; Reading memory. Two addressing modes, a register and a register plus a constant. The constant is
;; held to the nine signed bits every load can take, which is the unscaled form; a larger one that
;; the scaled form could take is left to the plain rule for now.
;; A `_Bool` object is one byte holding a zero or a one, and a truth value in a register is the
;; same zero or one, so reading one is the byte load and writing one is the byte store. Nothing
;; above bit zero is ever anything but zero on either side, which is the invariant x86-64 keeps.
(rule (lower (load.i1 (value.i64 a)))
(a64.ldr_bit (amode_base a))
(spec (= (extract 0 0 (select (mem) a)) (result))))
(rule (lower (load.i1 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.ldr_bit (amode_base_offset a k))
(spec (= (extract 0 0 (select (mem) (bvadd a k))) (result))))
(rule (lower (store.i1 (value.i1 v) (value.i64 a)))
(a64.str_bit (amode_base a) v)
(spec (= (store (mem) a (zero_extend 1 8 v)) (result))))
(rule (lower (store.i1 (value.i1 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.str_bit (amode_base_offset a k) v)
(spec (= (store (mem) (bvadd a k) (zero_extend 1 8 v)) (result))))
(rule (lower (load.i8 (value.i64 a)))
(a64.ldr_8 (amode_base a))
(spec (= (select (mem) a) (result))))
(rule (lower (load.i16 (value.i64 a)))
(a64.ldr_16 (amode_base a))
(spec (= (concat (select (mem) (bvadd a 1)) (select (mem) a)) (result))))
(rule (lower (load.i32 (value.i64 a)))
(a64.ldr_32 (amode_base a))
(spec (= (concat (select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a)) (result))))
(rule (lower (load.i64 (value.i64 a)))
(a64.ldr_64 (amode_base a))
(spec (= (concat (select (mem) (bvadd a 7)) (select (mem) (bvadd a 6))
(select (mem) (bvadd a 5)) (select (mem) (bvadd a 4))
(select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a)) (result))))
(rule (lower (load.i8 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.ldr_8 (amode_base_offset a k))
(spec (= (select (mem) (bvadd a k)) (result))))
(rule (lower (load.i16 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.ldr_16 (amode_base_offset a k))
(spec (= (concat (select (mem) (bvadd (bvadd a k) 1)) (select (mem) (bvadd a k))) (result))))
(rule (lower (load.i32 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.ldr_32 (amode_base_offset a k))
(spec (= (concat (select (mem) (bvadd (bvadd a k) 3)) (select (mem) (bvadd (bvadd a k) 2))
(select (mem) (bvadd (bvadd a k) 1)) (select (mem) (bvadd a k))) (result))))
(rule (lower (load.i64 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.ldr_64 (amode_base_offset a k))
(spec (= (concat (select (mem) (bvadd (bvadd a k) 7)) (select (mem) (bvadd (bvadd a k) 6))
(select (mem) (bvadd (bvadd a k) 5)) (select (mem) (bvadd (bvadd a k) 4))
(select (mem) (bvadd (bvadd a k) 3)) (select (mem) (bvadd (bvadd a k) 2))
(select (mem) (bvadd (bvadd a k) 1)) (select (mem) (bvadd a k))) (result))))
;; Writing memory. The value comes first in the IR and last in the machine term, as it does in the
;; x86-64 file.
(rule (lower (store.i8 (value.i8 v) (value.i64 a)))
(a64.str_8 (amode_base a) v)
(spec (= (store (mem) a v) (result))))
(rule (lower (store.i16 (value.i16 v) (value.i64 a)))
(a64.str_16 (amode_base a) v)
(spec (= (store (store (mem)
a (extract 7 0 v))
(bvadd a 1) (extract 15 8 v)) (result))))
(rule (lower (store.i32 (value.i32 v) (value.i64 a)))
(a64.str_32 (amode_base a) v)
(spec (= (store (store (store (store (mem)
a (extract 7 0 v))
(bvadd a 1) (extract 15 8 v))
(bvadd a 2) (extract 23 16 v))
(bvadd a 3) (extract 31 24 v)) (result))))
(rule (lower (store.i64 (value.i64 v) (value.i64 a)))
(a64.str_64 (amode_base a) v)
(spec (= (store (store (store (store (store (store (store (store (mem)
a (extract 7 0 v))
(bvadd a 1) (extract 15 8 v))
(bvadd a 2) (extract 23 16 v))
(bvadd a 3) (extract 31 24 v))
(bvadd a 4) (extract 39 32 v))
(bvadd a 5) (extract 47 40 v))
(bvadd a 6) (extract 55 48 v))
(bvadd a 7) (extract 63 56 v)) (result))))
(rule (lower (store.i8 (value.i8 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.str_8 (amode_base_offset a k) v)
(spec (= (store (mem) (bvadd a k) v) (result))))
(rule (lower (store.i16 (value.i16 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.str_16 (amode_base_offset a k) v)
(spec (= (store (store (mem)
(bvadd a k) (extract 7 0 v))
(bvadd (bvadd a k) 1) (extract 15 8 v)) (result))))
(rule (lower (store.i32 (value.i32 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.str_32 (amode_base_offset a k) v)
(spec (= (store (store (store (store (mem)
(bvadd a k) (extract 7 0 v))
(bvadd (bvadd a k) 1) (extract 15 8 v))
(bvadd (bvadd a k) 2) (extract 23 16 v))
(bvadd (bvadd a k) 3) (extract 31 24 v)) (result))))
(rule (lower (store.i64 (value.i64 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.str_64 (amode_base_offset a k) v)
(spec (= (store (store (store (store (store (store (store (store (mem)
(bvadd a k) (extract 7 0 v))
(bvadd (bvadd a k) 1) (extract 15 8 v))
(bvadd (bvadd a k) 2) (extract 23 16 v))
(bvadd (bvadd a k) 3) (extract 31 24 v))
(bvadd (bvadd a k) 4) (extract 39 32 v))
(bvadd (bvadd a k) 5) (extract 47 40 v))
(bvadd (bvadd a k) 6) (extract 55 48 v))
(bvadd (bvadd a k) 7) (extract 63 56 v)) (result))))
;; Giving a value back. What is below thirty two bits comes back in the low end of `w0`, and the
;; convention says the caller extends it, so all four of those are the thirty two bit pseudo.
(rule (lower (ret.i1 (value.i1 v)))
(a64.ret_val_32 v)
(spec (= v (result))))
(rule (lower (ret.i8 (value.i8 v)))
(a64.ret_val_32 v)
(spec (= v (result))))
(rule (lower (ret.i16 (value.i16 v)))
(a64.ret_val_32 v)
(spec (= v (result))))
(rule (lower (ret.i32 (value.i32 v)))
(a64.ret_val_32 v)
(spec (= v (result))))
(rule (lower (ret.i64 (value.i64 v)))
(a64.ret_val_64 v)
(spec (= v (result))))
;; Branching on a truth value, which the layout turns into a compare and a `b.ne` or a `b.eq`.
(rule (lower (brif.i1 (value.i1 c)))
(a64.br_cond_32 c)
(spec (= c (result))))
;; Floats, at the two formats C has registers for. A `long double` is a quad here, and every
;; operation on one is a call into the runtime rather than an instruction.
(rule (lower (fadd.f32 (value.f32 x) (value.f32 y)))
(a64.fadd_f32 x y)
(spec (= (fp.add x y) (result))))
(rule (lower (fadd.f64 (value.f64 x) (value.f64 y)))
(a64.fadd_f64 x y)
(spec (= (fp.add x y) (result))))
(rule (lower (fsub.f32 (value.f32 x) (value.f32 y)))
(a64.fsub_f32 x y)
(spec (= (fp.sub x y) (result))))
(rule (lower (fsub.f64 (value.f64 x) (value.f64 y)))
(a64.fsub_f64 x y)
(spec (= (fp.sub x y) (result))))
(rule (lower (fmul.f32 (value.f32 x) (value.f32 y)))
(a64.fmul_f32 x y)
(spec (= (fp.mul x y) (result))))
(rule (lower (fmul.f64 (value.f64 x) (value.f64 y)))
(a64.fmul_f64 x y)
(spec (= (fp.mul x y) (result))))
(rule (lower (fdiv.f32 (value.f32 x) (value.f32 y)))
(a64.fdiv_f32 x y)
(spec (= (fp.div x y) (result))))
(rule (lower (fdiv.f64 (value.f64 x) (value.f64 y)))
(a64.fdiv_f64 x y)
(spec (= (fp.div x y) (result))))
(rule (lower (ret.f32 (value.f32 v)))
(a64.ret_val_f32 v)
(spec (= v (result))))
(rule (lower (ret.f64 (value.f64 v)))
(a64.ret_val_f64 v)
(spec (= v (result))))
(rule (lower (ret.f128 (value.f128 v)))
(a64.ret_val_f128 v)
(spec (= v (result))))
;; Comparing two floats, which is an `fcmp` and the `cset` behind it as one term, for the reason the
;; integer comparisons are. The machine has a condition for each of the IR's fourteen predicates but
;; two, and those two take a second instruction, so no rule needs its operands the other way round.
(rule (lower (fcmp_ogt.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_gt_f32 x y)
(spec (= (ite (fp.gt x y) 1 0) (result))))
(rule (lower (fcmp_oge.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_ge_f32 x y)
(spec (= (ite (fp.geq x y) 1 0) (result))))
(rule (lower (fcmp_olt.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_lt_f32 x y)
(spec (= (ite (fp.lt x y) 1 0) (result))))
(rule (lower (fcmp_ole.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_le_f32 x y)
(spec (= (ite (fp.leq x y) 1 0) (result))))
(rule (lower (fcmp_one.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_one_f32 x y)
(spec (= (ite (or (fp.lt x y) (fp.gt x y)) 1 0) (result))))
(rule (lower (fcmp_ord.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_ord_f32 x y)
(spec (= (ite (and (not (fp.isNaN x)) (not (fp.isNaN y))) 1 0) (result))))
(rule (lower (fcmp_uno.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_uno_f32 x y)
(spec (= (ite (or (fp.isNaN x) (fp.isNaN y)) 1 0) (result))))
(rule (lower (fcmp_ueq.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_ueq_f32 x y)
(spec (= (ite (not (or (fp.lt x y) (fp.gt x y))) 1 0) (result))))
(rule (lower (fcmp_ult.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_ult_f32 x y)
(spec (= (ite (not (fp.geq x y)) 1 0) (result))))
(rule (lower (fcmp_ule.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_ule_f32 x y)
(spec (= (ite (not (fp.gt x y)) 1 0) (result))))
(rule (lower (fcmp_ugt.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_ugt_f32 x y)
(spec (= (ite (not (fp.leq x y)) 1 0) (result))))
(rule (lower (fcmp_uge.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_uge_f32 x y)
(spec (= (ite (not (fp.lt x y)) 1 0) (result))))
(rule (lower (fcmp_oeq.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_eq_f32 x y)
(spec (= (ite (fp.eq x y) 1 0) (result))))
(rule (lower (fcmp_une.f32.i1 (value.f32 x) (value.f32 y)))
(a64.fcmp_set_ne_f32 x y)
(spec (= (ite (not (fp.eq x y)) 1 0) (result))))
(rule (lower (fcmp_ogt.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_gt_f64 x y)
(spec (= (ite (fp.gt x y) 1 0) (result))))
(rule (lower (fcmp_oge.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_ge_f64 x y)
(spec (= (ite (fp.geq x y) 1 0) (result))))
(rule (lower (fcmp_olt.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_lt_f64 x y)
(spec (= (ite (fp.lt x y) 1 0) (result))))
(rule (lower (fcmp_ole.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_le_f64 x y)
(spec (= (ite (fp.leq x y) 1 0) (result))))
(rule (lower (fcmp_one.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_one_f64 x y)
(spec (= (ite (or (fp.lt x y) (fp.gt x y)) 1 0) (result))))
(rule (lower (fcmp_ord.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_ord_f64 x y)
(spec (= (ite (and (not (fp.isNaN x)) (not (fp.isNaN y))) 1 0) (result))))
(rule (lower (fcmp_uno.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_uno_f64 x y)
(spec (= (ite (or (fp.isNaN x) (fp.isNaN y)) 1 0) (result))))
(rule (lower (fcmp_ueq.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_ueq_f64 x y)
(spec (= (ite (not (or (fp.lt x y) (fp.gt x y))) 1 0) (result))))
(rule (lower (fcmp_ult.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_ult_f64 x y)
(spec (= (ite (not (fp.geq x y)) 1 0) (result))))
(rule (lower (fcmp_ule.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_ule_f64 x y)
(spec (= (ite (not (fp.gt x y)) 1 0) (result))))
(rule (lower (fcmp_ugt.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_ugt_f64 x y)
(spec (= (ite (not (fp.leq x y)) 1 0) (result))))
(rule (lower (fcmp_uge.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_uge_f64 x y)
(spec (= (ite (not (fp.lt x y)) 1 0) (result))))
(rule (lower (fcmp_oeq.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_eq_f64 x y)
(spec (= (ite (fp.eq x y) 1 0) (result))))
(rule (lower (fcmp_une.f64.i1 (value.f64 x) (value.f64 y)))
(a64.fcmp_set_ne_f64 x y)
(spec (= (ite (not (fp.eq x y)) 1 0) (result))))
;; Reading a float out of memory and writing one back, with the same two addressing modes.
(rule (lower (load.f32 (value.i64 a)))
(a64.ldr_f32 (amode_base a))
(spec (= (float_from_bits 32 (concat (select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a))) (result))))
(rule (lower (load.f32 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.ldr_f32 (amode_base_offset a k))
(spec (= (float_from_bits 32 (concat (select (mem) (bvadd (bvadd a k) 3)) (select (mem) (bvadd (bvadd a k) 2))
(select (mem) (bvadd (bvadd a k) 1)) (select (mem) (bvadd a k)))) (result))))
(rule (lower (load.f64 (value.i64 a)))
(a64.ldr_f64 (amode_base a))
(spec (= (float_from_bits 64 (concat (select (mem) (bvadd a 7)) (select (mem) (bvadd a 6))
(select (mem) (bvadd a 5)) (select (mem) (bvadd a 4))
(select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a))) (result))))
(rule (lower (load.f64 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.ldr_f64 (amode_base_offset a k))
(spec (= (float_from_bits 64 (concat (select (mem) (bvadd (bvadd a k) 7)) (select (mem) (bvadd (bvadd a k) 6))
(select (mem) (bvadd (bvadd a k) 5)) (select (mem) (bvadd (bvadd a k) 4))
(select (mem) (bvadd (bvadd a k) 3)) (select (mem) (bvadd (bvadd a k) 2))
(select (mem) (bvadd (bvadd a k) 1)) (select (mem) (bvadd a k)))) (result))))
(rule (lower (store.f32 (value.f32 v) (value.i64 a)))
(a64.str_f32 (amode_base a) v)
(spec (= (store (store (store (store (mem)
a (extract 7 0 (bits_from_float 32 v)))
(bvadd a 1) (extract 15 8 (bits_from_float 32 v)))
(bvadd a 2) (extract 23 16 (bits_from_float 32 v)))
(bvadd a 3) (extract 31 24 (bits_from_float 32 v))) (result))))
(rule (lower (store.f32 (value.f32 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.str_f32 (amode_base_offset a k) v)
(spec (= (store (store (store (store (mem)
(bvadd a k) (extract 7 0 (bits_from_float 32 v)))
(bvadd (bvadd a k) 1) (extract 15 8 (bits_from_float 32 v)))
(bvadd (bvadd a k) 2) (extract 23 16 (bits_from_float 32 v)))
(bvadd (bvadd a k) 3) (extract 31 24 (bits_from_float 32 v))) (result))))
(rule (lower (store.f64 (value.f64 v) (value.i64 a)))
(a64.str_f64 (amode_base a) v)
(spec (= (store (store (store (store (store (store (store (store (mem)
a (extract 7 0 (bits_from_float 64 v)))
(bvadd a 1) (extract 15 8 (bits_from_float 64 v)))
(bvadd a 2) (extract 23 16 (bits_from_float 64 v)))
(bvadd a 3) (extract 31 24 (bits_from_float 64 v)))
(bvadd a 4) (extract 39 32 (bits_from_float 64 v)))
(bvadd a 5) (extract 47 40 (bits_from_float 64 v)))
(bvadd a 6) (extract 55 48 (bits_from_float 64 v)))
(bvadd a 7) (extract 63 56 (bits_from_float 64 v))) (result))))
(rule (lower (store.f64 (value.f64 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.str_f64 (amode_base_offset a k) v)
(spec (= (store (store (store (store (store (store (store (store (mem)
(bvadd a k) (extract 7 0 (bits_from_float 64 v)))
(bvadd (bvadd a k) 1) (extract 15 8 (bits_from_float 64 v)))
(bvadd (bvadd a k) 2) (extract 23 16 (bits_from_float 64 v)))
(bvadd (bvadd a k) 3) (extract 31 24 (bits_from_float 64 v)))
(bvadd (bvadd a k) 4) (extract 39 32 (bits_from_float 64 v)))
(bvadd (bvadd a k) 5) (extract 47 40 (bits_from_float 64 v)))
(bvadd (bvadd a k) 6) (extract 55 48 (bits_from_float 64 v)))
(bvadd (bvadd a k) 7) (extract 63 56 (bits_from_float 64 v))) (result))))
;; A quad is sixteen bytes in one vector register, and `ldr q` and `str q` move all of it.
(rule (lower (load.f128 (value.i64 a)))
(a64.ldr_f128 (amode_base a))
(spec (= (float_from_bits 128 (concat (select (mem) (bvadd a 15)) (select (mem) (bvadd a 14))
(select (mem) (bvadd a 13)) (select (mem) (bvadd a 12))
(select (mem) (bvadd a 11)) (select (mem) (bvadd a 10))
(select (mem) (bvadd a 9)) (select (mem) (bvadd a 8))
(select (mem) (bvadd a 7)) (select (mem) (bvadd a 6))
(select (mem) (bvadd a 5)) (select (mem) (bvadd a 4))
(select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a))) (result))))
(rule (lower (load.f128 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.ldr_f128 (amode_base_offset a k))
(spec (= (float_from_bits 128 (concat (select (mem) (bvadd (bvadd a k) 15)) (select (mem) (bvadd (bvadd a k) 14))
(select (mem) (bvadd (bvadd a k) 13)) (select (mem) (bvadd (bvadd a k) 12))
(select (mem) (bvadd (bvadd a k) 11)) (select (mem) (bvadd (bvadd a k) 10))
(select (mem) (bvadd (bvadd a k) 9)) (select (mem) (bvadd (bvadd a k) 8))
(select (mem) (bvadd (bvadd a k) 7)) (select (mem) (bvadd (bvadd a k) 6))
(select (mem) (bvadd (bvadd a k) 5)) (select (mem) (bvadd (bvadd a k) 4))
(select (mem) (bvadd (bvadd a k) 3)) (select (mem) (bvadd (bvadd a k) 2))
(select (mem) (bvadd (bvadd a k) 1)) (select (mem) (bvadd a k)))) (result))))
(rule (lower (store.f128 (value.f128 v) (value.i64 a)))
(a64.str_f128 (amode_base a) v)
(spec (= (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (mem)
a (extract 7 0 (bits_from_float 128 v)))
(bvadd a 1) (extract 15 8 (bits_from_float 128 v)))
(bvadd a 2) (extract 23 16 (bits_from_float 128 v)))
(bvadd a 3) (extract 31 24 (bits_from_float 128 v)))
(bvadd a 4) (extract 39 32 (bits_from_float 128 v)))
(bvadd a 5) (extract 47 40 (bits_from_float 128 v)))
(bvadd a 6) (extract 55 48 (bits_from_float 128 v)))
(bvadd a 7) (extract 63 56 (bits_from_float 128 v)))
(bvadd a 8) (extract 71 64 (bits_from_float 128 v)))
(bvadd a 9) (extract 79 72 (bits_from_float 128 v)))
(bvadd a 10) (extract 87 80 (bits_from_float 128 v)))
(bvadd a 11) (extract 95 88 (bits_from_float 128 v)))
(bvadd a 12) (extract 103 96 (bits_from_float 128 v)))
(bvadd a 13) (extract 111 104 (bits_from_float 128 v)))
(bvadd a 14) (extract 119 112 (bits_from_float 128 v)))
(bvadd a 15) (extract 127 120 (bits_from_float 128 v))) (result))))
(rule (lower (store.f128 (value.f128 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (and (>= k -256) (< k 256)))
(a64.str_f128 (amode_base_offset a k) v)
(spec (= (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (mem)
(bvadd a k) (extract 7 0 (bits_from_float 128 v)))
(bvadd (bvadd a k) 1) (extract 15 8 (bits_from_float 128 v)))
(bvadd (bvadd a k) 2) (extract 23 16 (bits_from_float 128 v)))
(bvadd (bvadd a k) 3) (extract 31 24 (bits_from_float 128 v)))
(bvadd (bvadd a k) 4) (extract 39 32 (bits_from_float 128 v)))
(bvadd (bvadd a k) 5) (extract 47 40 (bits_from_float 128 v)))
(bvadd (bvadd a k) 6) (extract 55 48 (bits_from_float 128 v)))
(bvadd (bvadd a k) 7) (extract 63 56 (bits_from_float 128 v)))
(bvadd (bvadd a k) 8) (extract 71 64 (bits_from_float 128 v)))
(bvadd (bvadd a k) 9) (extract 79 72 (bits_from_float 128 v)))
(bvadd (bvadd a k) 10) (extract 87 80 (bits_from_float 128 v)))
(bvadd (bvadd a k) 11) (extract 95 88 (bits_from_float 128 v)))
(bvadd (bvadd a k) 12) (extract 103 96 (bits_from_float 128 v)))
(bvadd (bvadd a k) 13) (extract 111 104 (bits_from_float 128 v)))
(bvadd (bvadd a k) 14) (extract 119 112 (bits_from_float 128 v)))
(bvadd (bvadd a k) 15) (extract 127 120 (bits_from_float 128 v))) (result))))
;; Conversions with a float on one side. The instruction names put the destination format second
;; for `fcvt` and the source first for the rest, which is how `rucc_target::aarch64` spells them.
(rule (lower (fpext.f32.f64 (value.f32 x)))
(a64.fcvt_f32_f64 x)
(spec (= (float_from_float 32 64 x) (result))))
(rule (lower (fptrunc.f64.f32 (value.f64 x)))
(a64.fcvt_f64_f32 x)
(spec (= (float_from_float 64 32 x) (result))))
(rule (lower (fptosi.f32.i32 (value.f32 x)))
(a64.fcvtzs_f32_32 x)
(spec (= (signed_from_float 32 32 x) (result))))
(rule (lower (fptosi.f32.i64 (value.f32 x)))
(a64.fcvtzs_f32_64 x)
(spec (= (signed_from_float 32 64 x) (result))))
(rule (lower (fptosi.f64.i32 (value.f64 x)))
(a64.fcvtzs_f64_32 x)
(spec (= (signed_from_float 64 32 x) (result))))
(rule (lower (fptosi.f64.i64 (value.f64 x)))
(a64.fcvtzs_f64_64 x)
(spec (= (signed_from_float 64 64 x) (result))))
(rule (lower (sitofp.i32.f32 (value.i32 x)))
(a64.scvtf_32_f32 x)
(spec (= (float_from_signed 32 32 x) (result))))
(rule (lower (sitofp.i32.f64 (value.i32 x)))
(a64.scvtf_32_f64 x)
(spec (= (float_from_signed 32 64 x) (result))))
(rule (lower (sitofp.i64.f32 (value.i64 x)))
(a64.scvtf_64_f32 x)
(spec (= (float_from_signed 64 32 x) (result))))
(rule (lower (sitofp.i64.f64 (value.i64 x)))
(a64.scvtf_64_f64 x)
(spec (= (float_from_signed 64 64 x) (result))))
;; Moving a register from one file to the other, which is what a bitcast is.
(rule (lower (bitcast.f32.i32 (value.f32 x)))
(a64.fmov_from_f32 x)
(spec (= (bits_from_float 32 x) (result))))
(rule (lower (bitcast.i32.f32 (value.i32 x)))
(a64.fmov_to_f32 x)
(spec (= (float_from_bits 32 x) (result))))
(rule (lower (bitcast.f64.i64 (value.f64 x)))
(a64.fmov_from_f64 x)
(spec (= (bits_from_float 64 x) (result))))
(rule (lower (bitcast.i64.f64 (value.i64 x)))
(a64.fmov_to_f64 x)
(spec (= (float_from_bits 64 x) (result))))