;; Lowering x86-64, the integer core.
;;
;; What every rule in this file says is that some IR term and some machine term compute the
;; same thing, and `rucc-verify` makes each of them prove it against `x86-64.model` before
;; any of them may be used. Most of it computes a value and nothing else. The loads and the
;; stores at the bottom are the exception and are the first rules here with an effect: what
;; one of those claims is about memory as well as about a value, and memory is a thing the
;; model has because those rules needed it. The return at the bottom is the third kind again:
;; it computes nothing and writes nothing, and what it claims is that the value a function
;; gives back reaches the caller unchanged. Branches and calls are still to come, and each
;; will need the same question answered again for what it does.
;;
;; Every leaf says how wide it is. The reader of a file this size should never have to look
;; at the line above to find out, and the widths a rule relates are the whole content of the
;; conversions further down.
;;
;; The order rules are written in is for reading. Specificity is the shape of the pattern
;; rather than a sort, so no rule here is reached only because another one is below it.
;; Constants.
(rule (lower (iconst.i8 k))
(x64.mov_ri_8 k)
(spec (= k (result))))
(rule (lower (iconst.i16 k))
(x64.mov_ri_16 k)
(spec (= k (result))))
(rule (lower (iconst.i32 k))
(x64.mov_ri_32 k)
(spec (= k (result))))
(rule (lower (iconst.i64 k))
(x64.mov_ri_64 k)
(spec (= k (result))))
;; Arithmetic, register with register.
(rule (lower (add.i8 (value.i8 x) (value.i8 y)))
(x64.add_rr_8 x y)
(spec (= (bvadd x y) (result))))
(rule (lower (add.i16 (value.i16 x) (value.i16 y)))
(x64.add_rr_16 x y)
(spec (= (bvadd x y) (result))))
(rule (lower (add.i32 (value.i32 x) (value.i32 y)))
(x64.add_rr_32 x y)
(spec (= (bvadd x y) (result))))
(rule (lower (add.i64 (value.i64 x) (value.i64 y)))
(x64.add_rr_64 x y)
(spec (= (bvadd x y) (result))))
(rule (lower (sub.i8 (value.i8 x) (value.i8 y)))
(x64.sub_rr_8 x y)
(spec (= (bvsub x y) (result))))
(rule (lower (sub.i16 (value.i16 x) (value.i16 y)))
(x64.sub_rr_16 x y)
(spec (= (bvsub x y) (result))))
(rule (lower (sub.i32 (value.i32 x) (value.i32 y)))
(x64.sub_rr_32 x y)
(spec (= (bvsub x y) (result))))
(rule (lower (sub.i64 (value.i64 x) (value.i64 y)))
(x64.sub_rr_64 x y)
(spec (= (bvsub x y) (result))))
(rule (lower (and.i8 (value.i8 x) (value.i8 y)))
(x64.and_rr_8 x y)
(spec (= (bvand x y) (result))))
(rule (lower (and.i16 (value.i16 x) (value.i16 y)))
(x64.and_rr_16 x y)
(spec (= (bvand x y) (result))))
(rule (lower (and.i32 (value.i32 x) (value.i32 y)))
(x64.and_rr_32 x y)
(spec (= (bvand x y) (result))))
(rule (lower (and.i64 (value.i64 x) (value.i64 y)))
(x64.and_rr_64 x y)
(spec (= (bvand x y) (result))))
(rule (lower (or.i8 (value.i8 x) (value.i8 y)))
(x64.or_rr_8 x y)
(spec (= (bvor x y) (result))))
(rule (lower (or.i16 (value.i16 x) (value.i16 y)))
(x64.or_rr_16 x y)
(spec (= (bvor x y) (result))))
(rule (lower (or.i32 (value.i32 x) (value.i32 y)))
(x64.or_rr_32 x y)
(spec (= (bvor x y) (result))))
(rule (lower (or.i64 (value.i64 x) (value.i64 y)))
(x64.or_rr_64 x y)
(spec (= (bvor x y) (result))))
(rule (lower (xor.i8 (value.i8 x) (value.i8 y)))
(x64.xor_rr_8 x y)
(spec (= (bvxor x y) (result))))
(rule (lower (xor.i16 (value.i16 x) (value.i16 y)))
(x64.xor_rr_16 x y)
(spec (= (bvxor x y) (result))))
(rule (lower (xor.i32 (value.i32 x) (value.i32 y)))
(x64.xor_rr_32 x y)
(spec (= (bvxor x y) (result))))
(rule (lower (xor.i64 (value.i64 x) (value.i64 y)))
(x64.xor_rr_64 x y)
(spec (= (bvxor x y) (result))))
(rule (lower (mul.i8 (value.i8 x) (value.i8 y)))
(x64.imul_rr_8 x y)
(spec (= (bvmul x y) (result))))
(rule (lower (mul.i16 (value.i16 x) (value.i16 y)))
(x64.imul_rr_16 x y)
(spec (= (bvmul x y) (result))))
(rule (lower (mul.i32 (value.i32 x) (value.i32 y)))
(x64.imul_rr_32 x y)
(spec (= (bvmul x y) (result))))
(rule (lower (mul.i64 (value.i64 x) (value.i64 y)))
(x64.imul_rr_64 x y)
(spec (= (bvmul x y) (result))))
;; Arithmetic, register with immediate. At sixty four bits the machine holds the immediate
;; in thirty two and sign extends it, so the guard on those rules is the constant saying it
;; is one of the constants that survives that, which is a thing to test and not a range to
;; remember.
(rule (lower (add.i8 (value.i8 x) (iconst.i8 k)))
(x64.add_ri_8 x k)
(spec (= (bvadd x k) (result))))
(rule (lower (add.i16 (value.i16 x) (iconst.i16 k)))
(x64.add_ri_16 x k)
(spec (= (bvadd x k) (result))))
(rule (lower (add.i32 (value.i32 x) (iconst.i32 k)))
(x64.add_ri_32 x k)
(spec (= (bvadd x k) (result))))
(rule (lower (add.i64 (value.i64 x) (iconst.i64 k)))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.add_ri_64 x k)
(spec (= (bvadd x k) (result))))
(rule (lower (sub.i8 (value.i8 x) (iconst.i8 k)))
(x64.sub_ri_8 x k)
(spec (= (bvsub x k) (result))))
(rule (lower (sub.i16 (value.i16 x) (iconst.i16 k)))
(x64.sub_ri_16 x k)
(spec (= (bvsub x k) (result))))
(rule (lower (sub.i32 (value.i32 x) (iconst.i32 k)))
(x64.sub_ri_32 x k)
(spec (= (bvsub x k) (result))))
(rule (lower (sub.i64 (value.i64 x) (iconst.i64 k)))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.sub_ri_64 x k)
(spec (= (bvsub x k) (result))))
(rule (lower (and.i8 (value.i8 x) (iconst.i8 k)))
(x64.and_ri_8 x k)
(spec (= (bvand x k) (result))))
(rule (lower (and.i16 (value.i16 x) (iconst.i16 k)))
(x64.and_ri_16 x k)
(spec (= (bvand x k) (result))))
(rule (lower (and.i32 (value.i32 x) (iconst.i32 k)))
(x64.and_ri_32 x k)
(spec (= (bvand x k) (result))))
(rule (lower (and.i64 (value.i64 x) (iconst.i64 k)))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.and_ri_64 x k)
(spec (= (bvand x k) (result))))
(rule (lower (or.i8 (value.i8 x) (iconst.i8 k)))
(x64.or_ri_8 x k)
(spec (= (bvor x k) (result))))
(rule (lower (or.i16 (value.i16 x) (iconst.i16 k)))
(x64.or_ri_16 x k)
(spec (= (bvor x k) (result))))
(rule (lower (or.i32 (value.i32 x) (iconst.i32 k)))
(x64.or_ri_32 x k)
(spec (= (bvor x k) (result))))
(rule (lower (or.i64 (value.i64 x) (iconst.i64 k)))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.or_ri_64 x k)
(spec (= (bvor x k) (result))))
(rule (lower (xor.i8 (value.i8 x) (iconst.i8 k)))
(x64.xor_ri_8 x k)
(spec (= (bvxor x k) (result))))
(rule (lower (xor.i16 (value.i16 x) (iconst.i16 k)))
(x64.xor_ri_16 x k)
(spec (= (bvxor x k) (result))))
(rule (lower (xor.i32 (value.i32 x) (iconst.i32 k)))
(x64.xor_ri_32 x k)
(spec (= (bvxor x k) (result))))
(rule (lower (xor.i64 (value.i64 x) (iconst.i64 k)))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.xor_ri_64 x k)
(spec (= (bvxor x k) (result))))
(rule (lower (mul.i8 (value.i8 x) (iconst.i8 k)))
(x64.imul_ri_8 x k)
(spec (= (bvmul x k) (result))))
(rule (lower (mul.i16 (value.i16 x) (iconst.i16 k)))
(x64.imul_ri_16 x k)
(spec (= (bvmul x k) (result))))
(rule (lower (mul.i32 (value.i32 x) (iconst.i32 k)))
(x64.imul_ri_32 x k)
(spec (= (bvmul x k) (result))))
(rule (lower (mul.i64 (value.i64 x) (iconst.i64 k)))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.imul_ri_64 x k)
(spec (= (bvmul x k) (result)))
(bounded "a multiply of two unknowns at sixty four bits is out of reach, and what this rule turns on is the immediate rather than the multiply"))
;; The address arithmetic the machine does for free. A scaled index is part of an address
;; and `lea` is the instruction that computes an address without going to memory, which is
;; what makes it the cheapest multiply on this target.
(rule (lower (add.i64 (value.i64 x) (mul.i64 (value.i64 y) (iconst.i64 2))))
(x64.lea_64 (amode_base_index_scale x y 2))
(spec (= (bvadd x (bvmul y 2)) (result))))
(rule (lower (add.i64 (value.i64 x) (mul.i64 (value.i64 y) (iconst.i64 4))))
(x64.lea_64 (amode_base_index_scale x y 4))
(spec (= (bvadd x (bvmul y 4)) (result))))
(rule (lower (add.i64 (value.i64 x) (mul.i64 (value.i64 y) (iconst.i64 8))))
(x64.lea_64 (amode_base_index_scale x y 8))
(spec (= (bvadd x (bvmul y 8)) (result))))
(rule (lower (add.i64 (value.i64 x) (shl.i64 (value.i64 y) (iconst.i64 1))))
(x64.lea_64 (amode_base_index_scale x y 2))
(spec (= (bvadd x (bvshl y 1)) (result))))
(rule (lower (add.i64 (value.i64 x) (shl.i64 (value.i64 y) (iconst.i64 2))))
(x64.lea_64 (amode_base_index_scale x y 4))
(spec (= (bvadd x (bvshl y 2)) (result))))
(rule (lower (add.i64 (value.i64 x) (shl.i64 (value.i64 y) (iconst.i64 3))))
(x64.lea_64 (amode_base_index_scale x y 8))
(spec (= (bvadd x (bvshl y 3)) (result))))
(rule (lower (mul.i64 (value.i64 y) (iconst.i64 2)))
(x64.lea_64 (amode_index_scale y 2))
(spec (= (bvmul y 2) (result))))
(rule (lower (mul.i64 (value.i64 y) (iconst.i64 4)))
(x64.lea_64 (amode_index_scale y 4))
(spec (= (bvmul y 4) (result))))
(rule (lower (mul.i64 (value.i64 y) (iconst.i64 8)))
(x64.lea_64 (amode_index_scale y 8))
(spec (= (bvmul y 8) (result))))
;; Negation and complement. The IR writes both as arithmetic against a constant and the
;; machine has an instruction for each, which is a rule that has something to prove.
(rule (lower (sub.i8 (iconst.i8 0) (value.i8 x)))
(x64.neg_r_8 x)
(spec (= (bvsub 0 x) (result))))
(rule (lower (sub.i16 (iconst.i16 0) (value.i16 x)))
(x64.neg_r_16 x)
(spec (= (bvsub 0 x) (result))))
(rule (lower (sub.i32 (iconst.i32 0) (value.i32 x)))
(x64.neg_r_32 x)
(spec (= (bvsub 0 x) (result))))
(rule (lower (sub.i64 (iconst.i64 0) (value.i64 x)))
(x64.neg_r_64 x)
(spec (= (bvsub 0 x) (result))))
(rule (lower (xor.i8 (value.i8 x) (iconst.i8 -1)))
(x64.not_r_8 x)
(spec (= (bvxor x -1) (result))))
(rule (lower (xor.i16 (value.i16 x) (iconst.i16 -1)))
(x64.not_r_16 x)
(spec (= (bvxor x -1) (result))))
(rule (lower (xor.i32 (value.i32 x) (iconst.i32 -1)))
(x64.not_r_32 x)
(spec (= (bvxor x -1) (result))))
(rule (lower (xor.i64 (value.i64 x) (iconst.i64 -1)))
(x64.not_r_64 x)
(spec (= (bvxor x -1) (result))))
;; Division and remainder.
(rule (lower (sdiv.i8 (value.i8 x) (value.i8 y)))
(x64.idiv_quo_8 x y)
(spec (= (bvsdiv x y) (result))))
(rule (lower (sdiv.i16 (value.i16 x) (value.i16 y)))
(x64.idiv_quo_16 x y)
(spec (= (bvsdiv x y) (result))))
(rule (lower (sdiv.i32 (value.i32 x) (value.i32 y)))
(x64.idiv_quo_32 x y)
(spec (= (bvsdiv x y) (result))))
(rule (lower (sdiv.i64 (value.i64 x) (value.i64 y)))
(x64.idiv_quo_64 x y)
(spec (= (bvsdiv x y) (result))))
(rule (lower (srem.i8 (value.i8 x) (value.i8 y)))
(x64.idiv_rem_8 x y)
(spec (= (bvsrem x y) (result))))
(rule (lower (srem.i16 (value.i16 x) (value.i16 y)))
(x64.idiv_rem_16 x y)
(spec (= (bvsrem x y) (result))))
(rule (lower (srem.i32 (value.i32 x) (value.i32 y)))
(x64.idiv_rem_32 x y)
(spec (= (bvsrem x y) (result))))
(rule (lower (srem.i64 (value.i64 x) (value.i64 y)))
(x64.idiv_rem_64 x y)
(spec (= (bvsrem x y) (result))))
(rule (lower (udiv.i8 (value.i8 x) (value.i8 y)))
(x64.div_quo_8 x y)
(spec (= (bvudiv x y) (result))))
(rule (lower (udiv.i16 (value.i16 x) (value.i16 y)))
(x64.div_quo_16 x y)
(spec (= (bvudiv x y) (result))))
(rule (lower (udiv.i32 (value.i32 x) (value.i32 y)))
(x64.div_quo_32 x y)
(spec (= (bvudiv x y) (result))))
(rule (lower (udiv.i64 (value.i64 x) (value.i64 y)))
(x64.div_quo_64 x y)
(spec (= (bvudiv x y) (result))))
(rule (lower (urem.i8 (value.i8 x) (value.i8 y)))
(x64.div_rem_8 x y)
(spec (= (bvurem x y) (result))))
(rule (lower (urem.i16 (value.i16 x) (value.i16 y)))
(x64.div_rem_16 x y)
(spec (= (bvurem x y) (result))))
(rule (lower (urem.i32 (value.i32 x) (value.i32 y)))
(x64.div_rem_32 x y)
(spec (= (bvurem x y) (result))))
(rule (lower (urem.i64 (value.i64 x) (value.i64 y)))
(x64.div_rem_64 x y)
(spec (= (bvurem x y) (result))))
;; Shifts by a constant. The guard is the width, since a count the IR would take modulo the
;; width is a count this rule is not the one for.
(rule (lower (shl.i8 (value.i8 x) (iconst.i8 k)))
(if (and (>= k 0) (< k 8)))
(x64.shl_ri_8 x k)
(spec (= (bvshl x k) (result))))
(rule (lower (shl.i16 (value.i16 x) (iconst.i16 k)))
(if (and (>= k 0) (< k 16)))
(x64.shl_ri_16 x k)
(spec (= (bvshl x k) (result))))
(rule (lower (shl.i32 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 32)))
(x64.shl_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)))
(x64.shl_ri_64 x k)
(spec (= (bvshl x k) (result))))
(rule (lower (lshr.i8 (value.i8 x) (iconst.i8 k)))
(if (and (>= k 0) (< k 8)))
(x64.shr_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)))
(x64.shr_ri_16 x k)
(spec (= (bvlshr x k) (result))))
(rule (lower (lshr.i32 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 32)))
(x64.shr_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)))
(x64.shr_ri_64 x k)
(spec (= (bvlshr x k) (result))))
(rule (lower (ashr.i8 (value.i8 x) (iconst.i8 k)))
(if (and (>= k 0) (< k 8)))
(x64.sar_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)))
(x64.sar_ri_16 x k)
(spec (= (bvashr x k) (result))))
(rule (lower (ashr.i32 (value.i32 x) (iconst.i32 k)))
(if (and (>= k 0) (< k 32)))
(x64.sar_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)))
(x64.sar_ri_64 x k)
(spec (= (bvashr x k) (result))))
;; Shifts by a register. Below thirty two bits the machine masks the count by more than the
;; width of what it is shifting, so the narrow ones mask first and that extra instruction is
;; the whole reason these four rules are not one.
(rule (lower (shl.i8 (value.i8 x) (value.i8 y)))
(x64.shl_rcl_8 x (x64.and_ri_8 y 7))
(spec (= (bvshl x (bvand y 7)) (result))))
(rule (lower (shl.i16 (value.i16 x) (value.i16 y)))
(x64.shl_rcl_16 x (x64.and_ri_16 y 15))
(spec (= (bvshl x (bvand y 15)) (result))))
(rule (lower (shl.i32 (value.i32 x) (value.i32 y)))
(x64.shl_rcl_32 x y)
(spec (= (bvshl x (bvand y 31)) (result))))
(rule (lower (shl.i64 (value.i64 x) (value.i64 y)))
(x64.shl_rcl_64 x y)
(spec (= (bvshl x (bvand y 63)) (result))))
(rule (lower (lshr.i8 (value.i8 x) (value.i8 y)))
(x64.shr_rcl_8 x (x64.and_ri_8 y 7))
(spec (= (bvlshr x (bvand y 7)) (result))))
(rule (lower (lshr.i16 (value.i16 x) (value.i16 y)))
(x64.shr_rcl_16 x (x64.and_ri_16 y 15))
(spec (= (bvlshr x (bvand y 15)) (result))))
(rule (lower (lshr.i32 (value.i32 x) (value.i32 y)))
(x64.shr_rcl_32 x y)
(spec (= (bvlshr x (bvand y 31)) (result))))
(rule (lower (lshr.i64 (value.i64 x) (value.i64 y)))
(x64.shr_rcl_64 x y)
(spec (= (bvlshr x (bvand y 63)) (result))))
(rule (lower (ashr.i8 (value.i8 x) (value.i8 y)))
(x64.sar_rcl_8 x (x64.and_ri_8 y 7))
(spec (= (bvashr x (bvand y 7)) (result))))
(rule (lower (ashr.i16 (value.i16 x) (value.i16 y)))
(x64.sar_rcl_16 x (x64.and_ri_16 y 15))
(spec (= (bvashr x (bvand y 15)) (result))))
(rule (lower (ashr.i32 (value.i32 x) (value.i32 y)))
(x64.sar_rcl_32 x y)
(spec (= (bvashr x (bvand y 31)) (result))))
(rule (lower (ashr.i64 (value.i64 x) (value.i64 y)))
(x64.sar_rcl_64 x y)
(spec (= (bvashr x (bvand y 63)) (result))))
;; Comparisons. Each is a compare and the byte the condition sets, which is one term for
;; the reason the model gives: the flags between the two instructions are not a value.
(rule (lower (icmp_eq.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_e_8 x y)
(spec (= (ite (= x y) 1 0) (result))))
(rule (lower (icmp_eq.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_e_16 x y)
(spec (= (ite (= x y) 1 0) (result))))
(rule (lower (icmp_eq.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_e_32 x y)
(spec (= (ite (= x y) 1 0) (result))))
(rule (lower (icmp_eq.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_e_64 x y)
(spec (= (ite (= x y) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_ne_8 x y)
(spec (= (ite (not (= x y)) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_ne_16 x y)
(spec (= (ite (not (= x y)) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_ne_32 x y)
(spec (= (ite (not (= x y)) 1 0) (result))))
(rule (lower (icmp_ne.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_ne_64 x y)
(spec (= (ite (not (= x y)) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_l_8 x y)
(spec (= (ite (bvslt x y) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_l_16 x y)
(spec (= (ite (bvslt x y) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_l_32 x y)
(spec (= (ite (bvslt x y) 1 0) (result))))
(rule (lower (icmp_slt.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_l_64 x y)
(spec (= (ite (bvslt x y) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_le_8 x y)
(spec (= (ite (bvsle x y) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_le_16 x y)
(spec (= (ite (bvsle x y) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_le_32 x y)
(spec (= (ite (bvsle x y) 1 0) (result))))
(rule (lower (icmp_sle.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_le_64 x y)
(spec (= (ite (bvsle x y) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_g_8 x y)
(spec (= (ite (bvsgt x y) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_g_16 x y)
(spec (= (ite (bvsgt x y) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_g_32 x y)
(spec (= (ite (bvsgt x y) 1 0) (result))))
(rule (lower (icmp_sgt.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_g_64 x y)
(spec (= (ite (bvsgt x y) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_ge_8 x y)
(spec (= (ite (bvsge x y) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_ge_16 x y)
(spec (= (ite (bvsge x y) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_ge_32 x y)
(spec (= (ite (bvsge x y) 1 0) (result))))
(rule (lower (icmp_sge.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_ge_64 x y)
(spec (= (ite (bvsge x y) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_b_8 x y)
(spec (= (ite (bvult x y) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_b_16 x y)
(spec (= (ite (bvult x y) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_b_32 x y)
(spec (= (ite (bvult x y) 1 0) (result))))
(rule (lower (icmp_ult.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_b_64 x y)
(spec (= (ite (bvult x y) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_be_8 x y)
(spec (= (ite (bvule x y) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_be_16 x y)
(spec (= (ite (bvule x y) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_be_32 x y)
(spec (= (ite (bvule x y) 1 0) (result))))
(rule (lower (icmp_ule.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_be_64 x y)
(spec (= (ite (bvule x y) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_a_8 x y)
(spec (= (ite (bvugt x y) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_a_16 x y)
(spec (= (ite (bvugt x y) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_a_32 x y)
(spec (= (ite (bvugt x y) 1 0) (result))))
(rule (lower (icmp_ugt.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_a_64 x y)
(spec (= (ite (bvugt x y) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i8 x) (value.i8 y)))
(x64.cmp_set_ae_8 x y)
(spec (= (ite (bvuge x y) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i16 x) (value.i16 y)))
(x64.cmp_set_ae_16 x y)
(spec (= (ite (bvuge x y) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i32 x) (value.i32 y)))
(x64.cmp_set_ae_32 x y)
(spec (= (ite (bvuge x y) 1 0) (result))))
(rule (lower (icmp_uge.i1 (value.i64 x) (value.i64 y)))
(x64.cmp_set_ae_64 x y)
(spec (= (ite (bvuge x y) 1 0) (result))))
;; Conversions. A rule that relates two widths is what the verifier holds widths per term
;; for, and these are the rules that could not be written before it did.
(rule (lower (sext.i8.i16 (value.i8 x)))
(x64.movsx_8_16 x)
(spec (= (sign_extend 8 16 x) (result))))
(rule (lower (sext.i8.i32 (value.i8 x)))
(x64.movsx_8_32 x)
(spec (= (sign_extend 8 32 x) (result))))
(rule (lower (sext.i8.i64 (value.i8 x)))
(x64.movsx_8_64 x)
(spec (= (sign_extend 8 64 x) (result))))
(rule (lower (sext.i16.i32 (value.i16 x)))
(x64.movsx_16_32 x)
(spec (= (sign_extend 16 32 x) (result))))
(rule (lower (sext.i16.i64 (value.i16 x)))
(x64.movsx_16_64 x)
(spec (= (sign_extend 16 64 x) (result))))
(rule (lower (sext.i32.i64 (value.i32 x)))
(x64.movsxd_32_64 x)
(spec (= (sign_extend 32 64 x) (result))))
(rule (lower (zext.i8.i16 (value.i8 x)))
(x64.movzx_8_16 x)
(spec (= (zero_extend 8 16 x) (result))))
(rule (lower (zext.i8.i32 (value.i8 x)))
(x64.movzx_8_32 x)
(spec (= (zero_extend 8 32 x) (result))))
(rule (lower (zext.i8.i64 (value.i8 x)))
(x64.movzx_8_64 x)
(spec (= (zero_extend 8 64 x) (result))))
(rule (lower (zext.i16.i32 (value.i16 x)))
(x64.movzx_16_32 x)
(spec (= (zero_extend 16 32 x) (result))))
(rule (lower (zext.i16.i64 (value.i16 x)))
(x64.movzx_16_64 x)
(spec (= (zero_extend 16 64 x) (result))))
(rule (lower (zext.i32.i64 (value.i32 x)))
(x64.mov_32_to_64 x)
(spec (= (zero_extend 32 64 x) (result))))
(rule (lower (trunc.i16.i8 (value.i16 x)))
(x64.low_8 x)
(spec (= (extract 7 0 x) (result))))
(rule (lower (trunc.i32.i8 (value.i32 x)))
(x64.low_8 x)
(spec (= (extract 7 0 x) (result))))
(rule (lower (trunc.i32.i16 (value.i32 x)))
(x64.low_16 x)
(spec (= (extract 15 0 x) (result))))
(rule (lower (trunc.i64.i8 (value.i64 x)))
(x64.low_8 x)
(spec (= (extract 7 0 x) (result))))
(rule (lower (trunc.i64.i16 (value.i64 x)))
(x64.low_16 x)
(spec (= (extract 15 0 x) (result))))
(rule (lower (trunc.i64.i32 (value.i64 x)))
(x64.low_32 x)
(spec (= (extract 31 0 x) (result))))
;; Reading memory.
;;
;; These are the first rules in this file with an effect, and what one claims is settled in
;; `spec/10-backend.md` section 10.2 the same way everything else here is: by saying it in the
;; model and asking a solver. A load claims that the value it produces is the bytes that were
;; at the address, in the order this machine puts them there, and the `spec` clause writes
;; that order out rather than naming the head that also writes it out, so the two statements
;; are two statements.
;;
;; Two addressing modes, which are the two an address is: a register, and a register plus a
;; constant. The ones with an index and a scale are already here for `lea` and a `mov` reaches
;; through them equally well, but a rule for each is a rule the selector has to be able to
;; offer a term for, so they follow with the selector rather than ahead of it.
(rule (lower (load.i8 (value.i64 a)))
(x64.mov_rm_8 (amode_base a))
(spec (= (select (mem) a) (result))))
(rule (lower (load.i16 (value.i64 a)))
(x64.mov_rm_16 (amode_base a))
(spec (= (concat (select (mem) (bvadd a 1)) (select (mem) a)) (result))))
(rule (lower (load.i32 (value.i64 a)))
(x64.mov_rm_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)))
(x64.mov_rm_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))))
;; The same at an address the machine adds a constant to for free, which is every access to a
;; field of a structure and to a local through the frame pointer. The displacement is signed
;; and 32 bits, so the guard is the one the 64 bit immediates use, and a constant too wide for
;; it turns the rule down rather than reaching an instruction that cannot encode it. What
;; happens then is that the selector goes on to the way of showing the address that leaves the
;; addition where it is, and the plain rule above takes it, which is the right answer and is
;; one nobody had to write down.
(rule (lower (load.i8 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.mov_rm_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 (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.mov_rm_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 (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.mov_rm_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 (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.mov_rm_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.
;;
;; A store computes no value at all, so what `(result)` stands for in one of these is the
;; memory the instruction leaves rather than a number. That is the whole of what changed in
;; the language to let a rule have an effect: a term may compute a memory, and the two halves
;; of a rule have to agree about which one they computed as well as about what it is.
;;
;; The value comes first and the address second, because that is the order the IR holds them
;; in and a pattern is matched against an operand list by position. The machine instruction
;; takes them the other way round, which is why the replacement reads the other way round.
(rule (lower (store.i8 (value.i8 v) (value.i64 a)))
(x64.mov_mr_8 (amode_base a) v)
(spec (= (store (mem) a v) (result))))
(rule (lower (store.i16 (value.i16 v) (value.i64 a)))
(x64.mov_mr_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)))
(x64.mov_mr_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)))
(x64.mov_mr_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))))
;; And the same at an address with a constant added, for the same reason the loads have it.
(rule (lower (store.i8 (value.i8 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.mov_mr_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 (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.mov_mr_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 (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.mov_mr_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 (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.mov_mr_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.
;;
;; The whole of what one of these does is put the value where the caller looks for it. It is
;; not the `ret` instruction and it encodes to nothing: the epilogue has to give the frame
;; back before control leaves, and the epilogue is written after allocation by
;; `rucc_codegen::finish` rather than chosen by a rule. What survives selection is the
;; operand, because a read constrained to the return register is how the allocator is told
;; where the value has to end up.
;;
;; So the claim is that the value comes through unchanged, which is everything about a return
;; that arithmetic can say. Which register is the return register is in
;; `rucc_target::x86_64` and is checked against both conventions by a test there.
(rule (lower (ret.i8 (value.i8 v)))
(x64.ret_val_8 v)
(spec (= v (result))))
(rule (lower (ret.i16 (value.i16 v)))
(x64.ret_val_16 v)
(spec (= v (result))))
(rule (lower (ret.i32 (value.i32 v)))
(x64.ret_val_32 v)
(spec (= v (result))))
(rule (lower (ret.i64 (value.i64 v)))
(x64.ret_val_64 v)
(spec (= v (result))))
;; Branching. A conditional branch is the third kind of term with nothing to compute, and it is
;; the one whose replacement is smallest: where the two arms go is on the block rather than on
;; the instruction, so a rule for one never names a block and has only the condition to say
;; anything about. The instruction it becomes encodes to nothing on its own. What turns it into
;; a test and a jump, and which way round, is the block layout, since which of the two arms
;; falls through is layout's answer and not selection's.
;;
;; An unconditional jump has no rule for the same reason a return of nothing has none: there is
;; nothing left of it once the edge is on the block.
(rule (lower (brif.i1 (value.i1 c)))
(x64.br_cond_8 c)
(spec (= c (result))))