;; 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)
;; The same, for something already computed and sitting in a vector register. A float is not
;; the bitvector of its own width and the solver is told so, which is what makes an entry
;; below that mixes the two an error here rather than a proof of the wrong thing.
(semantics (value.f32 v) v)
(semantics (value.f64 v) v)
;; 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))
;; Float arithmetic. Not two's complement and not a bitvector: these are the operations the
;; floating point standard defines, and `fp.add` is the solver's own name for the one the
;; standard names. The rounding is nearest with ties to even, which `build-tools/rucc-verify`
;; writes in on every rule's behalf, because it is the rounding a C program is in unless it
;; asks for another and a rule that had to repeat it is a rule that can get it wrong.
;;
;; Division by zero has an entry here where the integer division below has none, and that is
;; the difference between the two rather than an oversight: a float divided by zero is an
;; infinity the standard names, and the machine computes it.
(semantics (fadd.f32 l r) (fp.add l r))
(semantics (fadd.f64 l r) (fp.add l r))
(semantics (fsub.f32 l r) (fp.sub l r))
(semantics (fsub.f64 l r) (fp.sub l r))
(semantics (fmul.f32 l r) (fp.mul l r))
(semantics (fmul.f64 l r) (fp.mul l r))
(semantics (fdiv.f32 l r) (fp.div l r))
(semantics (fdiv.f64 l r) (fp.div 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))
;; Conversions with a float on one side or both. A head names what it goes between and which
;; side each of them is on, since a float and a number of the same width are different terms
;; here and a width alone would not say which of the two is meant.
;;
;; The two that cross to an integer round differently in each direction, and that is C rather
;; than a choice: a number becoming a float is rounded to nearest, and a float becoming an
;; integer keeps the part before the point and discards the rest. `rucc-verify` writes the mode
;; for both, so no line here repeats it.
;;
;; A bitcast is neither of those. It is the same bits read the other way, which is what the two
;; reinterpretation heads are, and it is the only conversion here that keeps every bit and no
;; value where the others keep the value and no bit.
(semantics (fpext.f32.f64 v) (float_from_float 32 64 v))
(semantics (fptrunc.f64.f32 v) (float_from_float 64 32 v))
(semantics (fptosi.f32.i32 v) (signed_from_float 32 32 v))
(semantics (fptosi.f32.i64 v) (signed_from_float 32 64 v))
(semantics (fptosi.f64.i32 v) (signed_from_float 64 32 v))
(semantics (fptosi.f64.i64 v) (signed_from_float 64 64 v))
(semantics (sitofp.i32.f32 v) (float_from_signed 32 32 v))
(semantics (sitofp.i32.f64 v) (float_from_signed 32 64 v))
(semantics (sitofp.i64.f32 v) (float_from_signed 64 32 v))
(semantics (sitofp.i64.f64 v) (float_from_signed 64 64 v))
(semantics (bitcast.f32.i32 v) (bits_from_float 32 v))
(semantics (bitcast.f64.i64 v) (bits_from_float 64 v))
(semantics (bitcast.i32.f32 v) (float_from_bits 32 v))
(semantics (bitcast.i64.f64 v) (float_from_bits 64 v))
;; Comparing two floats, which is where the standard's own comparison lives rather than the
;; solver's `=`. The two disagree in exactly the two places a C program notices: `=` says a NaN
;; equals itself and says a positive zero differs from a negative zero, and `fp.eq` says neither,
;; which is what the machine does and what C means by `==`.
;;
;; Sixteen predicates, of which fourteen are here. An ordered one is false when either operand is a
;; NaN and an unordered one is true then, so each unordered predicate is the negation of the
;; ordered one that faces the other way: `ult` is not `geq`, and that is how they are written,
;; because writing out the NaN case fourteen times would be fourteen chances to write it wrong.
;;
;; `false` and `true` are the two that are not here. Neither looks at its operands, so neither is a
;; comparison, and nothing produces one.
(semantics (fcmp_oeq.f32.i1 l r) (ite (fp.eq l r) 1 0))
(semantics (fcmp_ogt.f32.i1 l r) (ite (fp.gt l r) 1 0))
(semantics (fcmp_oge.f32.i1 l r) (ite (fp.geq l r) 1 0))
(semantics (fcmp_olt.f32.i1 l r) (ite (fp.lt l r) 1 0))
(semantics (fcmp_ole.f32.i1 l r) (ite (fp.leq l r) 1 0))
(semantics (fcmp_one.f32.i1 l r) (ite (or (fp.lt l r) (fp.gt l r)) 1 0))
(semantics (fcmp_ord.f32.i1 l r) (ite (and (not (fp.isNaN l)) (not (fp.isNaN r))) 1 0))
(semantics (fcmp_uno.f32.i1 l r) (ite (or (fp.isNaN l) (fp.isNaN r)) 1 0))
(semantics (fcmp_ueq.f32.i1 l r) (ite (not (or (fp.lt l r) (fp.gt l r))) 1 0))
(semantics (fcmp_ugt.f32.i1 l r) (ite (not (fp.leq l r)) 1 0))
(semantics (fcmp_uge.f32.i1 l r) (ite (not (fp.lt l r)) 1 0))
(semantics (fcmp_ult.f32.i1 l r) (ite (not (fp.geq l r)) 1 0))
(semantics (fcmp_ule.f32.i1 l r) (ite (not (fp.gt l r)) 1 0))
(semantics (fcmp_une.f32.i1 l r) (ite (not (fp.eq l r)) 1 0))
(semantics (fcmp_oeq.f64.i1 l r) (ite (fp.eq l r) 1 0))
(semantics (fcmp_ogt.f64.i1 l r) (ite (fp.gt l r) 1 0))
(semantics (fcmp_oge.f64.i1 l r) (ite (fp.geq l r) 1 0))
(semantics (fcmp_olt.f64.i1 l r) (ite (fp.lt l r) 1 0))
(semantics (fcmp_ole.f64.i1 l r) (ite (fp.leq l r) 1 0))
(semantics (fcmp_one.f64.i1 l r) (ite (or (fp.lt l r) (fp.gt l r)) 1 0))
(semantics (fcmp_ord.f64.i1 l r) (ite (and (not (fp.isNaN l)) (not (fp.isNaN r))) 1 0))
(semantics (fcmp_uno.f64.i1 l r) (ite (or (fp.isNaN l) (fp.isNaN r)) 1 0))
(semantics (fcmp_ueq.f64.i1 l r) (ite (not (or (fp.lt l r) (fp.gt l r))) 1 0))
(semantics (fcmp_ugt.f64.i1 l r) (ite (not (fp.leq l r)) 1 0))
(semantics (fcmp_uge.f64.i1 l r) (ite (not (fp.lt l r)) 1 0))
(semantics (fcmp_ult.f64.i1 l r) (ite (not (fp.geq l r)) 1 0))
(semantics (fcmp_ule.f64.i1 l r) (ite (not (fp.gt l r)) 1 0))
(semantics (fcmp_une.f64.i1 l r) (ite (not (fp.eq l r)) 1 0))
;; 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))
;; The float arithmetic, one entry per instruction the way everything else here is. The `ss`
;; instructions work in one float and the `sd` ones in one double, so the format is in the
;; name and there is no size on the head to carry it.
(semantics (x64.addss_rr l r) (fp.add l r))
(semantics (x64.addsd_rr l r) (fp.add l r))
(semantics (x64.subss_rr l r) (fp.sub l r))
(semantics (x64.subsd_rr l r) (fp.sub l r))
(semantics (x64.mulss_rr l r) (fp.mul l r))
(semantics (x64.mulsd_rr l r) (fp.mul l r))
(semantics (x64.divss_rr l r) (fp.div l r))
(semantics (x64.divsd_rr l r) (fp.div l r))
;; The conversions. The suffix on these names is the width of the integer, since the format is
;; already in the mnemonic: `cvtsi2ss_64` reads a sixty four bit integer and writes a float, and
;; `cvttss2si_64` reads a float and writes a sixty four bit integer. The `movd` and `movq` pair
;; move a register between the two files and are the only ones here that are not a conversion at
;; all, which is why they mean a reinterpretation rather than a rounding.
(semantics (x64.cvtss2sd v) (float_from_float 32 64 v))
(semantics (x64.cvtsd2ss v) (float_from_float 64 32 v))
(semantics (x64.cvttss2si_32 v) (signed_from_float 32 32 v))
(semantics (x64.cvttss2si_64 v) (signed_from_float 32 64 v))
(semantics (x64.cvttsd2si_32 v) (signed_from_float 64 32 v))
(semantics (x64.cvttsd2si_64 v) (signed_from_float 64 64 v))
(semantics (x64.cvtsi2ss_32 v) (float_from_signed 32 32 v))
(semantics (x64.cvtsi2ss_64 v) (float_from_signed 64 32 v))
(semantics (x64.cvtsi2sd_32 v) (float_from_signed 32 64 v))
(semantics (x64.cvtsi2sd_64 v) (float_from_signed 64 64 v))
(semantics (x64.movd_to_xmm v) (float_from_bits 32 v))
(semantics (x64.movq_to_xmm v) (float_from_bits 64 v))
(semantics (x64.movd_from_xmm v) (bits_from_float 32 v))
(semantics (x64.movq_from_xmm v) (bits_from_float 64 v))
;; Comparing two floats and setting a byte, which is one term for the reason the integer
;; comparisons are: the flags between the compare and the set are not a value.
;;
;; `ucomisd` says four things in three flag bits, and what each of these means is which of the
;; four it accepts. Above is greater and ordered, below is less or unordered, equal is equal or
;; unordered, and parity on its own is unordered, so six of the eight are one of the four
;; possibilities and two of them are a pair of possibilities together. The eight are written in
;; terms of the standard's comparisons and their negations, because that is what a flag bit means
;; and not because it is shorter.
;;
;; The last two of each format are the ones that read two flags. An ordered equality is the flag
;; that means equal or unordered together with the flag that says it was ordered, which is
;; `fp.eq` and nothing else, and its negation is the other two put together the other way.
(semantics (x64.ucomiss_set_a l r) (ite (fp.gt l r) 1 0))
(semantics (x64.ucomiss_set_ae l r) (ite (fp.geq l r) 1 0))
(semantics (x64.ucomiss_set_b l r) (ite (not (fp.geq l r)) 1 0))
(semantics (x64.ucomiss_set_be l r) (ite (not (fp.gt l r)) 1 0))
(semantics (x64.ucomiss_set_e l r) (ite (not (or (fp.lt l r) (fp.gt l r))) 1 0))
(semantics (x64.ucomiss_set_ne l r) (ite (or (fp.lt l r) (fp.gt l r)) 1 0))
(semantics (x64.ucomiss_set_p l r) (ite (or (fp.isNaN l) (fp.isNaN r)) 1 0))
(semantics (x64.ucomiss_set_np l r) (ite (and (not (fp.isNaN l)) (not (fp.isNaN r))) 1 0))
(semantics (x64.ucomiss_set_e_and_np l r) (ite (fp.eq l r) 1 0))
(semantics (x64.ucomiss_set_ne_or_p l r) (ite (not (fp.eq l r)) 1 0))
(semantics (x64.ucomisd_set_a l r) (ite (fp.gt l r) 1 0))
(semantics (x64.ucomisd_set_ae l r) (ite (fp.geq l r) 1 0))
(semantics (x64.ucomisd_set_b l r) (ite (not (fp.geq l r)) 1 0))
(semantics (x64.ucomisd_set_be l r) (ite (not (fp.gt l r)) 1 0))
(semantics (x64.ucomisd_set_e l r) (ite (not (or (fp.lt l r) (fp.gt l r))) 1 0))
(semantics (x64.ucomisd_set_ne l r) (ite (or (fp.lt l r) (fp.gt l r)) 1 0))
(semantics (x64.ucomisd_set_p l r) (ite (or (fp.isNaN l) (fp.isNaN r)) 1 0))
(semantics (x64.ucomisd_set_np l r) (ite (and (not (fp.isNaN l)) (not (fp.isNaN r))) 1 0))
(semantics (x64.ucomisd_set_e_and_np l r) (ite (fp.eq l r) 1 0))
(semantics (x64.ucomisd_set_ne_or_p l r) (ite (not (fp.eq l r)) 1 0))
(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)))
;; A float is the same bytes in the same order with one thing said about them at the end: the
;; bits are read as a float rather than as a number. That is the whole of the difference, and it
;; is written down because it is the whole of the difference: `movss` moves bits and does not
;; look at them, so a rule that lowered a float load to an integer one would be right about the
;; machine, and it would still be a rule that put the value in the wrong register file.
(semantics (load.f32 a)
(float_from_bits 32
(concat (select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a))))
(semantics (load.f64 a)
(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))))
;; 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 same the other way, with the same one thing said about the value first. It is said once
;; per byte rather than once for the store, because there is nowhere in this language to name a
;; thing and then use it, and repeating it is better than a language change nothing else wants.
(semantics (store.f32 v a)
(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))))
(semantics (store.f64 v a)
(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))))
;; 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)))
(semantics (x64.movss_rm a)
(float_from_bits 32
(concat (select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a))))
(semantics (x64.movsd_rm a)
(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))))
(semantics (x64.movss_mr a v)
(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))))
(semantics (x64.movsd_mr a v)
(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))))
;; 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)
(semantics (ret.f32 v) v)
(semantics (ret.f64 v) v)
(semantics (x64.ret_val_f32 v) v)
(semantics (x64.ret_val_f64 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)
;; The rest of one bit.
;;
;; These are here rather than beside their own families because what they have in common is the
;; width and not the opcode, and the width is the only thing about them that needs an argument.
;; The argument is the one above: a value of this width is a byte whose top seven bits are zero,
;; the model is about the bit, and every machine head below is a byte instruction chosen because
;; it leaves that true.
;;
;; A constant and the three bitwise operations, which take zeros and ones to zeros and ones.
(semantics (iconst.i1 c) c)
(semantics (and.i1 l r) (bvand l r))
(semantics (or.i1 l r) (bvor l r))
(semantics (xor.i1 l r) (bvxor l r))
;; Widening one, and the machine heads that do it. There is no widening from one bit on this
;; machine, so what runs is `movzbl` and the rest, the same encodings the byte widenings above
;; use. They are named apart from those because a head has to mean one thing: `x64.movzx_8_32`
;; says what it does to a byte, these say what the same instruction does to the bit inside one,
;; and the two claims are equal exactly when the seven bits above are zero. Widening to a byte
;; is a plain register move, which is why `x64.bit_to_8` is not `zero_extend` of anything wider.
(semantics (zext.i1.i8 v) (zero_extend 1 8 v))
(semantics (zext.i1.i16 v) (zero_extend 1 16 v))
(semantics (zext.i1.i32 v) (zero_extend 1 32 v))
(semantics (zext.i1.i64 v) (zero_extend 1 64 v))
(semantics (x64.bit_to_8 v) (zero_extend 1 8 v))
(semantics (x64.bit_to_16 v) (zero_extend 1 16 v))
(semantics (x64.bit_to_32 v) (zero_extend 1 32 v))
(semantics (x64.bit_to_64 v) (zero_extend 1 64 v))