;; What the terms in the x86-64 rule set mean, in bitvectors.
;;
;; This is the file a reviewer reads to find out what the compiler believes an instruction
;; does. Every head the rules use has an entry, which is the tax `spec/10-backend.md` says
;; to pay from the first rule rather than to retrofit, and a head with no entry here is an
;; error rather than an unchecked assumption.
;;
;; A machine head is one instruction at one operand size, because `addl` and `addq` are two
;; instructions with two encodings and a model whose entries do not stand one to one with
;; instructions is a model nobody can check against a manual.
;;
;; The IR half of this file is not about x86-64 and will move out of it when a second target
;; arrives. It is here because a model belongs beside the rules it is read with.
;; The values a rule matches. A `value` is something already computed and sitting in a
;; register, and an `iconst` is a constant the selector has in hand.
(semantics (value.i8 v) v)
(semantics (value.i16 v) v)
(semantics (value.i32 v) v)
(semantics (value.i64 v) v)
(semantics (iconst.i8 c) c)
(semantics (iconst.i16 c) c)
(semantics (iconst.i32 c) c)
(semantics (iconst.i64 c) c)
;; Integer arithmetic. Two's complement in every case, which is what a bitvector is.
(semantics (add.i8 l r) (bvadd l r))
(semantics (add.i16 l r) (bvadd l r))
(semantics (add.i32 l r) (bvadd l r))
(semantics (add.i64 l r) (bvadd l r))
(semantics (sub.i8 l r) (bvsub l r))
(semantics (sub.i16 l r) (bvsub l r))
(semantics (sub.i32 l r) (bvsub l r))
(semantics (sub.i64 l r) (bvsub l r))
(semantics (and.i8 l r) (bvand l r))
(semantics (and.i16 l r) (bvand l r))
(semantics (and.i32 l r) (bvand l r))
(semantics (and.i64 l r) (bvand l r))
(semantics (or.i8 l r) (bvor l r))
(semantics (or.i16 l r) (bvor l r))
(semantics (or.i32 l r) (bvor l r))
(semantics (or.i64 l r) (bvor l r))
(semantics (xor.i8 l r) (bvxor l r))
(semantics (xor.i16 l r) (bvxor l r))
(semantics (xor.i32 l r) (bvxor l r))
(semantics (xor.i64 l r) (bvxor l r))
(semantics (mul.i8 l r) (bvmul l r))
(semantics (mul.i16 l r) (bvmul l r))
(semantics (mul.i32 l r) (bvmul l r))
(semantics (mul.i64 l r) (bvmul l r))
;; Division and remainder. The IR only ever carries a division whose divisor the language
;; says is not zero, so nothing here says what a division by zero means: on this machine it
;; is a trap rather than a value, and a model that gave it one would be describing an
;; instruction that does not exist.
(semantics (sdiv.i8 l r) (bvsdiv l r))
(semantics (sdiv.i16 l r) (bvsdiv l r))
(semantics (sdiv.i32 l r) (bvsdiv l r))
(semantics (sdiv.i64 l r) (bvsdiv l r))
(semantics (srem.i8 l r) (bvsrem l r))
(semantics (srem.i16 l r) (bvsrem l r))
(semantics (srem.i32 l r) (bvsrem l r))
(semantics (srem.i64 l r) (bvsrem l r))
(semantics (udiv.i8 l r) (bvudiv l r))
(semantics (udiv.i16 l r) (bvudiv l r))
(semantics (udiv.i32 l r) (bvudiv l r))
(semantics (udiv.i64 l r) (bvudiv l r))
(semantics (urem.i8 l r) (bvurem l r))
(semantics (urem.i16 l r) (bvurem l r))
(semantics (urem.i32 l r) (bvurem l r))
(semantics (urem.i64 l r) (bvurem l r))
;; Shifts. The IR takes the count modulo the width it is shifting, which is a decision
;; rather than an accident: C leaves a wider count undefined, `spec/08-ir.md` has no poison
;; to hand back, and a value that is unspecified but stable is what a machine gives anyway.
;; The machine takes its count modulo thirty two below the widest size and modulo sixty four
;; at it, so the two agree at thirty two bits and sixty four and do not below them, which is
;; why the narrow rules mask before they shift.
(semantics (shl.i8 l r) (bvshl l (bvand r 7)))
(semantics (shl.i16 l r) (bvshl l (bvand r 15)))
(semantics (shl.i32 l r) (bvshl l (bvand r 31)))
(semantics (shl.i64 l r) (bvshl l (bvand r 63)))
(semantics (lshr.i8 l r) (bvlshr l (bvand r 7)))
(semantics (lshr.i16 l r) (bvlshr l (bvand r 15)))
(semantics (lshr.i32 l r) (bvlshr l (bvand r 31)))
(semantics (lshr.i64 l r) (bvlshr l (bvand r 63)))
(semantics (ashr.i8 l r) (bvashr l (bvand r 7)))
(semantics (ashr.i16 l r) (bvashr l (bvand r 15)))
(semantics (ashr.i32 l r) (bvashr l (bvand r 31)))
(semantics (ashr.i64 l r) (bvashr l (bvand r 63)))
;; Comparisons. One entry each rather than one per operand size, because what a comparison
;; means does not depend on how wide the things it compares are. The answer is one bit.
(semantics (icmp_eq.i1 l r) (ite (= l r) 1 0))
(semantics (icmp_ne.i1 l r) (ite (not (= l r)) 1 0))
(semantics (icmp_slt.i1 l r) (ite (bvslt l r) 1 0))
(semantics (icmp_sle.i1 l r) (ite (bvsle l r) 1 0))
(semantics (icmp_sgt.i1 l r) (ite (bvsgt l r) 1 0))
(semantics (icmp_sge.i1 l r) (ite (bvsge l r) 1 0))
(semantics (icmp_ult.i1 l r) (ite (bvult l r) 1 0))
(semantics (icmp_ule.i1 l r) (ite (bvule l r) 1 0))
(semantics (icmp_ugt.i1 l r) (ite (bvugt l r) 1 0))
(semantics (icmp_uge.i1 l r) (ite (bvuge l r) 1 0))
;; Conversions between widths. A head names both, since sign extending from eight bits and
;; from thirty two are two different instructions and so are two different terms.
(semantics (sext.i8.i16 v) (sign_extend 8 16 v))
(semantics (sext.i8.i32 v) (sign_extend 8 32 v))
(semantics (sext.i8.i64 v) (sign_extend 8 64 v))
(semantics (sext.i16.i32 v) (sign_extend 16 32 v))
(semantics (sext.i16.i64 v) (sign_extend 16 64 v))
(semantics (sext.i32.i64 v) (sign_extend 32 64 v))
(semantics (zext.i8.i16 v) (zero_extend 8 16 v))
(semantics (zext.i8.i32 v) (zero_extend 8 32 v))
(semantics (zext.i8.i64 v) (zero_extend 8 64 v))
(semantics (zext.i16.i32 v) (zero_extend 16 32 v))
(semantics (zext.i16.i64 v) (zero_extend 16 64 v))
(semantics (zext.i32.i64 v) (zero_extend 32 64 v))
(semantics (trunc.i16.i8 v) (extract 7 0 v))
(semantics (trunc.i32.i8 v) (extract 7 0 v))
(semantics (trunc.i32.i16 v) (extract 15 0 v))
(semantics (trunc.i64.i8 v) (extract 7 0 v))
(semantics (trunc.i64.i16 v) (extract 15 0 v))
(semantics (trunc.i64.i32 v) (extract 31 0 v))
;; The machine. Everything below this line is x86-64 and nothing above it is.
;; Loading a constant into a register. The sixty four bit form is the one that takes a full
;; width immediate, which is why it needs no guard where the arithmetic does.
(semantics (x64.mov_ri_8 c) c)
(semantics (x64.mov_ri_16 c) c)
(semantics (x64.mov_ri_32 c) c)
(semantics (x64.mov_ri_64 c) c)
;; Arithmetic, register with register and register with immediate. At sixty four bits the
;; immediate is thirty two bits sign extended, and saying so here is what makes the guard on
;; those rules load bearing rather than decorative.
(semantics (x64.add_rr_8 l r) (bvadd l r))
(semantics (x64.add_rr_16 l r) (bvadd l r))
(semantics (x64.add_rr_32 l r) (bvadd l r))
(semantics (x64.add_rr_64 l r) (bvadd l r))
(semantics (x64.sub_rr_8 l r) (bvsub l r))
(semantics (x64.sub_rr_16 l r) (bvsub l r))
(semantics (x64.sub_rr_32 l r) (bvsub l r))
(semantics (x64.sub_rr_64 l r) (bvsub l r))
(semantics (x64.and_rr_8 l r) (bvand l r))
(semantics (x64.and_rr_16 l r) (bvand l r))
(semantics (x64.and_rr_32 l r) (bvand l r))
(semantics (x64.and_rr_64 l r) (bvand l r))
(semantics (x64.or_rr_8 l r) (bvor l r))
(semantics (x64.or_rr_16 l r) (bvor l r))
(semantics (x64.or_rr_32 l r) (bvor l r))
(semantics (x64.or_rr_64 l r) (bvor l r))
(semantics (x64.xor_rr_8 l r) (bvxor l r))
(semantics (x64.xor_rr_16 l r) (bvxor l r))
(semantics (x64.xor_rr_32 l r) (bvxor l r))
(semantics (x64.xor_rr_64 l r) (bvxor l r))
(semantics (x64.imul_rr_8 l r) (bvmul l r))
(semantics (x64.imul_rr_16 l r) (bvmul l r))
(semantics (x64.imul_rr_32 l r) (bvmul l r))
(semantics (x64.imul_rr_64 l r) (bvmul l r))
(semantics (x64.add_ri_8 l r) (bvadd l r))
(semantics (x64.add_ri_16 l r) (bvadd l r))
(semantics (x64.add_ri_32 l r) (bvadd l r))
(semantics (x64.add_ri_64 l r) (bvadd l (sign_extend 32 64 (extract 31 0 r))))
(semantics (x64.sub_ri_8 l r) (bvsub l r))
(semantics (x64.sub_ri_16 l r) (bvsub l r))
(semantics (x64.sub_ri_32 l r) (bvsub l r))
(semantics (x64.sub_ri_64 l r) (bvsub l (sign_extend 32 64 (extract 31 0 r))))
(semantics (x64.and_ri_8 l r) (bvand l r))
(semantics (x64.and_ri_16 l r) (bvand l r))
(semantics (x64.and_ri_32 l r) (bvand l r))
(semantics (x64.and_ri_64 l r) (bvand l (sign_extend 32 64 (extract 31 0 r))))
(semantics (x64.or_ri_8 l r) (bvor l r))
(semantics (x64.or_ri_16 l r) (bvor l r))
(semantics (x64.or_ri_32 l r) (bvor l r))
(semantics (x64.or_ri_64 l r) (bvor l (sign_extend 32 64 (extract 31 0 r))))
(semantics (x64.xor_ri_8 l r) (bvxor l r))
(semantics (x64.xor_ri_16 l r) (bvxor l r))
(semantics (x64.xor_ri_32 l r) (bvxor l r))
(semantics (x64.xor_ri_64 l r) (bvxor l (sign_extend 32 64 (extract 31 0 r))))
(semantics (x64.imul_ri_8 l r) (bvmul l r))
(semantics (x64.imul_ri_16 l r) (bvmul l r))
(semantics (x64.imul_ri_32 l r) (bvmul l r))
(semantics (x64.imul_ri_64 l r) (bvmul l (sign_extend 32 64 (extract 31 0 r))))
;; Negation and complement, which are one instruction each and not the subtract and the
;; exclusive or the IR writes them as.
(semantics (x64.neg_r_8 v) (bvneg v))
(semantics (x64.neg_r_16 v) (bvneg v))
(semantics (x64.neg_r_32 v) (bvneg v))
(semantics (x64.neg_r_64 v) (bvneg v))
(semantics (x64.not_r_8 v) (bvnot v))
(semantics (x64.not_r_16 v) (bvnot v))
(semantics (x64.not_r_32 v) (bvnot v))
(semantics (x64.not_r_64 v) (bvnot v))
;; Division. Both quotient and remainder come out of one instruction, and which of the two
;; a rule wants is which register it reads afterwards, so they are two heads here.
(semantics (x64.idiv_quo_8 l r) (bvsdiv l r))
(semantics (x64.idiv_quo_16 l r) (bvsdiv l r))
(semantics (x64.idiv_quo_32 l r) (bvsdiv l r))
(semantics (x64.idiv_quo_64 l r) (bvsdiv l r))
(semantics (x64.idiv_rem_8 l r) (bvsrem l r))
(semantics (x64.idiv_rem_16 l r) (bvsrem l r))
(semantics (x64.idiv_rem_32 l r) (bvsrem l r))
(semantics (x64.idiv_rem_64 l r) (bvsrem l r))
(semantics (x64.div_quo_8 l r) (bvudiv l r))
(semantics (x64.div_quo_16 l r) (bvudiv l r))
(semantics (x64.div_quo_32 l r) (bvudiv l r))
(semantics (x64.div_quo_64 l r) (bvudiv l r))
(semantics (x64.div_rem_8 l r) (bvurem l r))
(semantics (x64.div_rem_16 l r) (bvurem l r))
(semantics (x64.div_rem_32 l r) (bvurem l r))
(semantics (x64.div_rem_64 l r) (bvurem l r))
;; Shifts, by an immediate and by cl. The mask is the machine's own and is the reason a
;; narrow shift by a register is not one instruction.
(semantics (x64.shl_ri_8 l r) (bvshl l (bvand r 31)))
(semantics (x64.shl_ri_16 l r) (bvshl l (bvand r 31)))
(semantics (x64.shl_ri_32 l r) (bvshl l (bvand r 31)))
(semantics (x64.shl_ri_64 l r) (bvshl l (bvand r 63)))
(semantics (x64.shr_ri_8 l r) (bvlshr l (bvand r 31)))
(semantics (x64.shr_ri_16 l r) (bvlshr l (bvand r 31)))
(semantics (x64.shr_ri_32 l r) (bvlshr l (bvand r 31)))
(semantics (x64.shr_ri_64 l r) (bvlshr l (bvand r 63)))
(semantics (x64.sar_ri_8 l r) (bvashr l (bvand r 31)))
(semantics (x64.sar_ri_16 l r) (bvashr l (bvand r 31)))
(semantics (x64.sar_ri_32 l r) (bvashr l (bvand r 31)))
(semantics (x64.sar_ri_64 l r) (bvashr l (bvand r 63)))
(semantics (x64.shl_rcl_8 l r) (bvshl l (bvand r 31)))
(semantics (x64.shl_rcl_16 l r) (bvshl l (bvand r 31)))
(semantics (x64.shl_rcl_32 l r) (bvshl l (bvand r 31)))
(semantics (x64.shl_rcl_64 l r) (bvshl l (bvand r 63)))
(semantics (x64.shr_rcl_8 l r) (bvlshr l (bvand r 31)))
(semantics (x64.shr_rcl_16 l r) (bvlshr l (bvand r 31)))
(semantics (x64.shr_rcl_32 l r) (bvlshr l (bvand r 31)))
(semantics (x64.shr_rcl_64 l r) (bvlshr l (bvand r 63)))
(semantics (x64.sar_rcl_8 l r) (bvashr l (bvand r 31)))
(semantics (x64.sar_rcl_16 l r) (bvashr l (bvand r 31)))
(semantics (x64.sar_rcl_32 l r) (bvashr l (bvand r 31)))
(semantics (x64.sar_rcl_64 l r) (bvashr l (bvand r 63)))
;; A comparison and the byte it sets. The two are one head because the flags between them
;; are not a value: a term is something a solver can be asked about and the flags register
;; is not one, so the unit a rule names is the pair that produces the bit.
(semantics (x64.cmp_set_e_8 l r) (ite (= l r) 1 0))
(semantics (x64.cmp_set_e_16 l r) (ite (= l r) 1 0))
(semantics (x64.cmp_set_e_32 l r) (ite (= l r) 1 0))
(semantics (x64.cmp_set_e_64 l r) (ite (= l r) 1 0))
(semantics (x64.cmp_set_ne_8 l r) (ite (not (= l r)) 1 0))
(semantics (x64.cmp_set_ne_16 l r) (ite (not (= l r)) 1 0))
(semantics (x64.cmp_set_ne_32 l r) (ite (not (= l r)) 1 0))
(semantics (x64.cmp_set_ne_64 l r) (ite (not (= l r)) 1 0))
(semantics (x64.cmp_set_l_8 l r) (ite (bvslt l r) 1 0))
(semantics (x64.cmp_set_l_16 l r) (ite (bvslt l r) 1 0))
(semantics (x64.cmp_set_l_32 l r) (ite (bvslt l r) 1 0))
(semantics (x64.cmp_set_l_64 l r) (ite (bvslt l r) 1 0))
(semantics (x64.cmp_set_le_8 l r) (ite (bvsle l r) 1 0))
(semantics (x64.cmp_set_le_16 l r) (ite (bvsle l r) 1 0))
(semantics (x64.cmp_set_le_32 l r) (ite (bvsle l r) 1 0))
(semantics (x64.cmp_set_le_64 l r) (ite (bvsle l r) 1 0))
(semantics (x64.cmp_set_g_8 l r) (ite (bvsgt l r) 1 0))
(semantics (x64.cmp_set_g_16 l r) (ite (bvsgt l r) 1 0))
(semantics (x64.cmp_set_g_32 l r) (ite (bvsgt l r) 1 0))
(semantics (x64.cmp_set_g_64 l r) (ite (bvsgt l r) 1 0))
(semantics (x64.cmp_set_ge_8 l r) (ite (bvsge l r) 1 0))
(semantics (x64.cmp_set_ge_16 l r) (ite (bvsge l r) 1 0))
(semantics (x64.cmp_set_ge_32 l r) (ite (bvsge l r) 1 0))
(semantics (x64.cmp_set_ge_64 l r) (ite (bvsge l r) 1 0))
(semantics (x64.cmp_set_b_8 l r) (ite (bvult l r) 1 0))
(semantics (x64.cmp_set_b_16 l r) (ite (bvult l r) 1 0))
(semantics (x64.cmp_set_b_32 l r) (ite (bvult l r) 1 0))
(semantics (x64.cmp_set_b_64 l r) (ite (bvult l r) 1 0))
(semantics (x64.cmp_set_be_8 l r) (ite (bvule l r) 1 0))
(semantics (x64.cmp_set_be_16 l r) (ite (bvule l r) 1 0))
(semantics (x64.cmp_set_be_32 l r) (ite (bvule l r) 1 0))
(semantics (x64.cmp_set_be_64 l r) (ite (bvule l r) 1 0))
(semantics (x64.cmp_set_a_8 l r) (ite (bvugt l r) 1 0))
(semantics (x64.cmp_set_a_16 l r) (ite (bvugt l r) 1 0))
(semantics (x64.cmp_set_a_32 l r) (ite (bvugt l r) 1 0))
(semantics (x64.cmp_set_a_64 l r) (ite (bvugt l r) 1 0))
(semantics (x64.cmp_set_ae_8 l r) (ite (bvuge l r) 1 0))
(semantics (x64.cmp_set_ae_16 l r) (ite (bvuge l r) 1 0))
(semantics (x64.cmp_set_ae_32 l r) (ite (bvuge l r) 1 0))
(semantics (x64.cmp_set_ae_64 l r) (ite (bvuge l r) 1 0))
;; The conversions. Truncation is not an instruction at all: the low half of a register is
;; a register, so what these heads say is which part of it the next instruction reads.
(semantics (x64.movzx_8_16 v) (zero_extend 8 16 v))
(semantics (x64.movzx_8_32 v) (zero_extend 8 32 v))
(semantics (x64.movzx_8_64 v) (zero_extend 8 64 v))
(semantics (x64.movzx_16_32 v) (zero_extend 16 32 v))
(semantics (x64.movzx_16_64 v) (zero_extend 16 64 v))
(semantics (x64.mov_32_to_64 v) (zero_extend 32 64 v))
(semantics (x64.movsx_8_16 v) (sign_extend 8 16 v))
(semantics (x64.movsx_8_32 v) (sign_extend 8 32 v))
(semantics (x64.movsx_8_64 v) (sign_extend 8 64 v))
(semantics (x64.movsx_16_32 v) (sign_extend 16 32 v))
(semantics (x64.movsx_16_64 v) (sign_extend 16 64 v))
(semantics (x64.movsxd_32_64 v) (sign_extend 32 64 v))
(semantics (x64.low_8 v) (extract 7 0 v))
(semantics (x64.low_16 v) (extract 15 0 v))
(semantics (x64.low_32 v) (extract 31 0 v))
;; The addressing mode, and the instruction that computes one rather than loading from it.
;; This is where the arithmetic that x86-64 does for free lands.
(semantics (amode_base_index_scale base index scale) (bvadd base (bvmul index scale)))
(semantics (amode_index_scale index scale) (bvmul index scale))
(semantics (x64.lea_64 address) address)
;; Two more addressing modes, which are the ones a load and a store reach through. A `mov`
;; can use every mode `lea` can, so nothing here is about memory: an addressing mode is an
;; addition and the instruction that reads it is what makes it an access.
(semantics (amode_base base) base)
(semantics (amode_base_offset base offset) (bvadd base offset))
;; Reading memory.
;;
;; Memory is a map from an address to a byte and there is nothing wider than a byte in it, so
;; a load of more than one byte is written out. The first argument of `concat` is the high
;; end, and the byte at the highest address is the high end on a little endian machine, so
;; these count down. Anybody checking this file against a manual should read exactly that.
(semantics (load.i8 a) (select (mem) a))
(semantics (load.i16 a)
(concat (select (mem) (bvadd a 1)) (select (mem) a)))
(semantics (load.i32 a)
(concat (select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a)))
(semantics (load.i64 a)
(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)))
;; Writing memory.
;;
;; The same access the other way round, and written the other way round: a `store` puts one
;; byte into a memory and gives back the memory it made, so these nest, and the innermost one
;; runs first. The byte at the lowest address is the low end of the value.
;;
;; The value comes before the address in the IR head and after it in the machine one, and both
;; of those are somebody else's decision rather than this file's. A pattern is matched against
;; an IR instruction's operand list by position, so an IR head whose arguments are in a
;; different order from the instruction it names is a rule that binds the address to the value.
;; Nothing in a proof would catch that, because a proof is about this file agreeing with itself.
(semantics (store.i8 v a) (store (mem) a v))
(semantics (store.i16 v a)
(store (store (mem) a (extract 7 0 v))
(bvadd a 1) (extract 15 8 v)))
(semantics (store.i32 v a)
(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)))
(semantics (store.i64 v a)
(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)))
;; The instructions that do it. Written out again rather than in terms of the IR heads above,
;; for the reason `x64.add_rr_32` is written out rather than in terms of `add.i32`: the two
;; halves of a rule are two statements that have to agree, and two statements that share a
;; definition agree about nothing.
(semantics (x64.mov_rm_8 a) (select (mem) a))
(semantics (x64.mov_rm_16 a)
(concat (select (mem) (bvadd a 1)) (select (mem) a)))
(semantics (x64.mov_rm_32 a)
(concat (select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a)))
(semantics (x64.mov_rm_64 a)
(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)))
(semantics (x64.mov_mr_8 a v) (store (mem) a v))
(semantics (x64.mov_mr_16 a v)
(store (store (mem) a (extract 7 0 v))
(bvadd a 1) (extract 15 8 v)))
(semantics (x64.mov_mr_32 a v)
(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)))
(semantics (x64.mov_mr_64 a v)
(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)))
;; Giving a value back.
;;
;; A return is the first term here that is not about computing anything. What a rule for one
;; can claim is that the value the function returns is the value the machine leaves for the
;; caller, unchanged, and that is what these two lines say and all they say. That the register
;; it is left in is the right one is a fact about the target rather than about arithmetic, and
;; a solver that has no notion of a register cannot check it, so `rucc_target::x86_64` says
;; which register it is and a test there checks that against both conventions.
;;
;; A return of nothing has no entry, because a rule that put nothing anywhere would have
;; nothing to prove. The selector writes no instruction for one at all.
(semantics (ret.i8 v) v)
(semantics (ret.i16 v) v)
(semantics (ret.i32 v) v)
(semantics (ret.i64 v) v)
(semantics (x64.ret_val_8 v) v)
(semantics (x64.ret_val_16 v) v)
(semantics (x64.ret_val_32 v) v)
(semantics (x64.ret_val_64 v) v)
;; Branching on a condition.
;;
;; The same kind of claim as a return, and for the same reason. What a rule for a conditional
;; branch can say is that the machine branches on the value the IR branched on, unchanged, and
;; where the two arms go is a fact about the block rather than about the term: a machine IR
;; block holds its own successors, so no pattern and no replacement ever names one.
;;
;; The condition is one bit here and a whole byte register on the machine, which is the same
;; abstraction every comparison above already makes: a `setcc` writes a byte whose other seven
;; bits are zero, and what the model is about is the bit.
;;
;; An unconditional jump has no entry, because it reads nothing and computes nothing, and the
;; block it goes to is on the block. The selector writes no instruction for one at all.
(semantics (value.i1 v) v)
(semantics (brif.i1 v) v)
(semantics (x64.br_cond_8 v) v)