;; 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)