;; Lowering x86-64.
;;
;; 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. A leaf that says `f32` rather than `i32` is a float, which is a
;; different kind of thing from the thirty two bits it occupies and lives in a different
;; register file.
;;
;; 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))))
;; A truth value written down, which is a zero or a one and is put in a byte because there is no
;; narrower register to put it in. The seven bits above it are zero, which is the same shape a
;; `setcc` leaves behind and is what every rule below written at this width relies on.
(rule (lower (iconst.i1 k))
(x64.mov_ri_8 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))))
;; The same three at one bit, which is a byte instruction on two bytes that are a zero or a one.
;; Each of them gives back a zero or a one for the same reason it gives back the right answer, so
;; the shape a truth value comes in survives them and there is nothing to mask afterwards. These
;; are the only arithmetic at this width: an `!=` between two truth values is the `xor`, a `&&`
;; and a `||` the front end did not turn into branches are the other two, and nothing writes an
;; add or a shift of one bit.
(rule (lower (and.i1 (value.i1 x) (value.i1 y)))
(x64.and_rr_8 x y)
(spec (= (bvand x y) (result))))
(rule (lower (or.i1 (value.i1 x) (value.i1 y)))
(x64.or_rr_8 x y)
(spec (= (bvor x y) (result))))
(rule (lower (xor.i1 (value.i1 x) (value.i1 y)))
(x64.xor_rr_8 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))))
;; Widening a truth value, which is what a comparison used as a number goes through and is by
;; some way the commonest conversion a C program writes. The machine has no widening from one
;; bit, so what runs is the widening from the byte the bit is in, and these four heads are named
;; apart from that widening so the model can say what they do to the one bit rather than what
;; they do to the byte. That is the same abstraction the model already makes for `setcc`, which
;; writes a whole byte and is given a meaning one bit wide, and it is sound for the same reason:
;; the seven bits above are zero, so widening the byte and widening the bit give the same answer.
(rule (lower (zext.i1.i8 (value.i1 x)))
(x64.bit_to_8 x)
(spec (= (zero_extend 1 8 x) (result))))
(rule (lower (zext.i1.i16 (value.i1 x)))
(x64.bit_to_16 x)
(spec (= (zero_extend 1 16 x) (result))))
(rule (lower (zext.i1.i32 (value.i1 x)))
(x64.bit_to_32 x)
(spec (= (zero_extend 1 32 x) (result))))
(rule (lower (zext.i1.i64 (value.i1 x)))
(x64.bit_to_64 x)
(spec (= (zero_extend 1 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))))
;; Floats.
;;
;; The first rules here whose terms are not bitvectors. What they claim is what the integer
;; arithmetic above claims, in the arithmetic the floating point standard defines rather than in
;; two's complement: `addss` computes the sum that `fadd` computes, rounded to nearest with ties
;; to even, which is the rounding a C program gets unless it asks for another.
;;
;; That is a stronger claim than it looks. It is not that the two agree on the numbers that
;; behave, it is that they agree on every bit pattern either can be handed, so a not a number
;; going in one side and the same not a number coming out the other is part of what was proved.
;;
;; Each of these is one instruction and one format, the same way `addl` and `addq` are two
;; instructions. The `ss` ones work in one float and the `sd` ones in one double, which is what
;; the names have always meant and is why no rule here needs a width on the machine term.
;;
;; A `long double` has no rules. It is eighty bits on the x87 stack, which is a third register
;; file nothing here allocates in, and `crates/rucc-codegen/src/abi.rs` refuses one by name
;; rather than lowering it into a register that cannot hold it.
(rule (lower (fadd.f32 (value.f32 x) (value.f32 y)))
(x64.addss_rr x y)
(spec (= (fp.add x y) (result))))
(rule (lower (fadd.f64 (value.f64 x) (value.f64 y)))
(x64.addsd_rr x y)
(spec (= (fp.add x y) (result))))
(rule (lower (fsub.f32 (value.f32 x) (value.f32 y)))
(x64.subss_rr x y)
(spec (= (fp.sub x y) (result))))
(rule (lower (fsub.f64 (value.f64 x) (value.f64 y)))
(x64.subsd_rr x y)
(spec (= (fp.sub x y) (result))))
(rule (lower (fmul.f32 (value.f32 x) (value.f32 y)))
(x64.mulss_rr x y)
(spec (= (fp.mul x y) (result))))
(rule (lower (fmul.f64 (value.f64 x) (value.f64 y)))
(x64.mulsd_rr x y)
(spec (= (fp.mul x y) (result))))
(rule (lower (fdiv.f32 (value.f32 x) (value.f32 y)))
(x64.divss_rr x y)
(spec (= (fp.div x y) (result))))
(rule (lower (fdiv.f64 (value.f64 x) (value.f64 y)))
(x64.divsd_rr x y)
(spec (= (fp.div x y) (result))))
;; Giving a float back. The same claim the integer returns make, and the register it is left in
;; is a fact about the target in the same way: it is `xmm0` on both conventions, and the test
;; that says so is in `rucc_target::x86_64` where the conventions are.
(rule (lower (ret.f32 (value.f32 v)))
(x64.ret_val_f32 v)
(spec (= v (result))))
(rule (lower (ret.f64 (value.f64 v)))
(x64.ret_val_f64 v)
(spec (= v (result))))
;; Reading a float out of memory and writing one back.
;;
;; The two addressing modes the integer accesses have, at the two formats, which is the same
;; eight rules over again with one thing different: the bytes are read as a float at the end
;; rather than left as a number. That one thing is what the register file turns on. `movss` and
;; `mov` move the same four bytes and neither looks at them, so a rule that lowered this to a
;; `mov` would be right about the memory and would still put the value where no float
;; instruction can reach it, and the model is written to make that an error rather than a proof.
;;
;; Neither of these is the instruction a spill uses. A spill moves a whole register because a
;; slot holds whatever was in it, and these move the width of the value because that is all the
;; program asked for. `crates/rucc-codegen/src/finish.rs` writes the first and a rule writes the
;; second, and they are different opcodes so that neither can be mistaken for the other.
(rule (lower (load.f32 (value.i64 a)))
(x64.movss_rm (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.f64 (value.i64 a)))
(x64.movsd_rm (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.f32 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.movss_rm (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 (add.i64 (value.i64 a) (iconst.i64 k))))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.movsd_rm (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)))
(x64.movss_mr (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.f64 (value.f64 v) (value.i64 a)))
(x64.movsd_mr (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.f32 (value.f32 v) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.movss_mr (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) (add.i64 (value.i64 a) (iconst.i64 k))))
(if (= k (sign_extend 32 64 (extract 31 0 k))))
(x64.movsd_mr (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))))
;; Conversions.
;;
;; Fourteen rules and fourteen instructions, one each, which is what makes this the part of the
;; float work that a rule can say all of. Every one of them is a single instruction that reads one
;; register and writes another, and the two registers are in different files in ten of them.
;;
;; Three different things happen here and the names keep them apart. Between the two formats and
;; from an integer to a float, the value is kept as closely as the format allows and rounded to
;; nearest, which is the mode a C program runs in. From a float to an integer, the part before the
;; point is kept and the rest is discarded, which is what C says and is why the instruction is the
;; one with two `t`s in its name: `cvttsd2si` truncates and `cvtsd2si` rounds, and only the first
;; of them is a conversion C ever asks for. A bitcast keeps every bit and no value at all.
;;
;; What a conversion does to a float too big for the integer it is asked for is not claimed. C
;; leaves it undefined, the machine writes a value of its own, and the model leaves it unspecified,
;; so these rules are proved for every float the conversion has an answer for and say nothing about
;; the rest. That is the strongest true claim about them rather than a gap in the proof.
;;
;; The unsigned conversions are not here. The machine has no instruction for either at any width a
;; rule could name, so each is several instructions and is written as a rewrite into these rather
;; than as a rule that would have to be a program.
(rule (lower (fpext.f32.f64 (value.f32 x)))
(x64.cvtss2sd x)
(spec (= (float_from_float 32 64 x) (result))))
(rule (lower (fptrunc.f64.f32 (value.f64 x)))
(x64.cvtsd2ss x)
(spec (= (float_from_float 64 32 x) (result))))
(rule (lower (fptosi.f32.i32 (value.f32 x)))
(x64.cvttss2si_32 x)
(spec (= (signed_from_float 32 32 x) (result))))
(rule (lower (fptosi.f32.i64 (value.f32 x)))
(x64.cvttss2si_64 x)
(spec (= (signed_from_float 32 64 x) (result))))
(rule (lower (fptosi.f64.i32 (value.f64 x)))
(x64.cvttsd2si_32 x)
(spec (= (signed_from_float 64 32 x) (result))))
(rule (lower (fptosi.f64.i64 (value.f64 x)))
(x64.cvttsd2si_64 x)
(spec (= (signed_from_float 64 64 x) (result))))
(rule (lower (sitofp.i32.f32 (value.i32 x)))
(x64.cvtsi2ss_32 x)
(spec (= (float_from_signed 32 32 x) (result))))
(rule (lower (sitofp.i64.f32 (value.i64 x)))
(x64.cvtsi2ss_64 x)
(spec (= (float_from_signed 64 32 x) (result))))
(rule (lower (sitofp.i32.f64 (value.i32 x)))
(x64.cvtsi2sd_32 x)
(spec (= (float_from_signed 32 64 x) (result))))
(rule (lower (sitofp.i64.f64 (value.i64 x)))
(x64.cvtsi2sd_64 x)
(spec (= (float_from_signed 64 64 x) (result))))
;; Moving a register from one file to the other, which is what a bitcast is. The bits arrive
;; unchanged, so what the value means changes and what it is made of does not, and this is the one
;; place in the rule set where a float and the number spelling it are the same thing.
(rule (lower (bitcast.i32.f32 (value.i32 x)))
(x64.movd_to_xmm x)
(spec (= (float_from_bits 32 x) (result))))
(rule (lower (bitcast.i64.f64 (value.i64 x)))
(x64.movq_to_xmm x)
(spec (= (float_from_bits 64 x) (result))))
(rule (lower (bitcast.f32.i32 (value.f32 x)))
(x64.movd_from_xmm x)
(spec (= (bits_from_float 32 x) (result))))
(rule (lower (bitcast.f64.i64 (value.f64 x)))
(x64.movq_from_xmm x)
(spec (= (bits_from_float 64 x) (result))))
;; Comparing two floats. A `ucomisd` and the byte a condition sets, which is one term for the
;; reason the integer comparisons are: what the compare writes is the flags, and the flags between
;; the two instructions are not a value anything could hold.
;;
;; The machine answers four questions and C asks fourteen, so the rules here are three shapes. Six
;; predicates are one of the machine's own conditions and are a rule with the operands in the order
;; they were written. Four more are one of those conditions with the operands the other way round,
;; which is what `x64.ucomisd_set_a y x` is doing: the instruction has no `below and ordered`
;; condition and does not need one, since less than is greater than read backwards and swapping two
;; registers costs nothing. The last two need two conditions and are the two instructions that
;; carry a spare byte to put them together in.
;;
;; What makes any of this more than a table is the NaN case, and it is the whole of why the
;; predicates come in pairs. An ordered comparison is false when either operand is a NaN and an
;; unordered one is true, and the machine says which happened in the parity flag, so every rule
;; below either uses a condition that already accounts for it or says so with the parity flag.
(rule (lower (fcmp_ogt.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_a x y)
(spec (= (ite (fp.gt x y) 1 0) (result))))
(rule (lower (fcmp_oge.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_ae x y)
(spec (= (ite (fp.geq x y) 1 0) (result))))
(rule (lower (fcmp_olt.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_a y x)
(spec (= (ite (fp.lt x y) 1 0) (result))))
(rule (lower (fcmp_ole.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_ae y x)
(spec (= (ite (fp.leq x y) 1 0) (result))))
(rule (lower (fcmp_one.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_ne 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)))
(x64.ucomiss_set_np 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)))
(x64.ucomiss_set_p 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)))
(x64.ucomiss_set_e 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)))
(x64.ucomiss_set_b x y)
(spec (= (ite (not (fp.geq x y)) 1 0) (result))))
(rule (lower (fcmp_ule.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_be x y)
(spec (= (ite (not (fp.gt x y)) 1 0) (result))))
(rule (lower (fcmp_ugt.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_b y x)
(spec (= (ite (not (fp.leq x y)) 1 0) (result))))
(rule (lower (fcmp_uge.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_be y x)
(spec (= (ite (not (fp.lt x y)) 1 0) (result))))
(rule (lower (fcmp_oeq.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_e_and_np x y)
(spec (= (ite (fp.eq x y) 1 0) (result))))
(rule (lower (fcmp_une.f32.i1 (value.f32 x) (value.f32 y)))
(x64.ucomiss_set_ne_or_p x y)
(spec (= (ite (not (fp.eq x y)) 1 0) (result))))
(rule (lower (fcmp_ogt.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_a x y)
(spec (= (ite (fp.gt x y) 1 0) (result))))
(rule (lower (fcmp_oge.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_ae x y)
(spec (= (ite (fp.geq x y) 1 0) (result))))
(rule (lower (fcmp_olt.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_a y x)
(spec (= (ite (fp.lt x y) 1 0) (result))))
(rule (lower (fcmp_ole.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_ae y x)
(spec (= (ite (fp.leq x y) 1 0) (result))))
(rule (lower (fcmp_one.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_ne 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)))
(x64.ucomisd_set_np 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)))
(x64.ucomisd_set_p 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)))
(x64.ucomisd_set_e 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)))
(x64.ucomisd_set_b x y)
(spec (= (ite (not (fp.geq x y)) 1 0) (result))))
(rule (lower (fcmp_ule.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_be x y)
(spec (= (ite (not (fp.gt x y)) 1 0) (result))))
(rule (lower (fcmp_ugt.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_b y x)
(spec (= (ite (not (fp.leq x y)) 1 0) (result))))
(rule (lower (fcmp_uge.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_be y x)
(spec (= (ite (not (fp.lt x y)) 1 0) (result))))
(rule (lower (fcmp_oeq.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_e_and_np x y)
(spec (= (ite (fp.eq x y) 1 0) (result))))
(rule (lower (fcmp_une.f64.i1 (value.f64 x) (value.f64 y)))
(x64.ucomisd_set_ne_or_p x y)
(spec (= (ite (not (fp.eq x y)) 1 0) (result))))