;; What the terms in the AArch64 rule set mean, in bitvectors.
;;
;; The x86-64 model is the one to read first. This one says the same things about a different
;; machine and follows the same rules: a machine head is one instruction at one operand size, and
;; every head the rules use has an entry here or in the file this one includes.
(include crates/rucc-ir/rules/ir.model)
;; The machine. Everything from here down is AArch64 and nothing above it is.
;; Loading a constant into a register. What one `mov` can build is a question for the rule's guard,
;; and this says only that the register ends up holding the constant.
(semantics (a64.mov_ri_32 c) c)
(semantics (a64.mov_ri_64 c) c)
;; Writing sixteen bits of a constant into a register and leaving the rest of it alone, which is how
;; a constant too wide for one `mov` is built a piece at a time. The number is the piece, and the
;; head says which sixteen bits it goes in.
(semantics (a64.movk_ri_16_32 d c) (concat (extract 15 0 c) (extract 15 0 d)))
(semantics (a64.movk_ri_16_64 d c) (concat (extract 63 32 d) (concat (extract 15 0 c) (extract 15 0 d))))
(semantics (a64.movk_ri_32_64 d c) (concat (extract 63 48 d) (concat (extract 15 0 c) (extract 31 0 d))))
(semantics (a64.movk_ri_48_64 d c) (concat (extract 15 0 c) (extract 47 0 d)))
;; Arithmetic. The same operation at the two sizes the machine has, and with a constant in place of
;; the second register where the instruction takes one.
(semantics (a64.add_rr_32 l r) (bvadd l r))
(semantics (a64.add_rr_64 l r) (bvadd l r))
(semantics (a64.sub_rr_32 l r) (bvsub l r))
(semantics (a64.sub_rr_64 l r) (bvsub l r))
(semantics (a64.and_rr_32 l r) (bvand l r))
(semantics (a64.and_rr_64 l r) (bvand l r))
(semantics (a64.orr_rr_32 l r) (bvor l r))
(semantics (a64.orr_rr_64 l r) (bvor l r))
(semantics (a64.eor_rr_32 l r) (bvxor l r))
(semantics (a64.eor_rr_64 l r) (bvxor l r))
(semantics (a64.mul_rr_32 l r) (bvmul l r))
(semantics (a64.mul_rr_64 l r) (bvmul l r))
(semantics (a64.add_ri_32 l r) (bvadd l r))
(semantics (a64.add_ri_64 l r) (bvadd l r))
(semantics (a64.sub_ri_32 l r) (bvsub l r))
(semantics (a64.sub_ri_64 l r) (bvsub l r))
(semantics (a64.neg_r_32 v) (bvsub 0 v))
(semantics (a64.neg_r_64 v) (bvsub 0 v))
(semantics (a64.mvn_r_32 v) (bvnot v))
(semantics (a64.mvn_r_64 v) (bvnot v))
;; Division. The machine gives back zero for a divisor of zero where the IR has no such division at
;; all, so the entries say what the two agree on and nothing about the case neither side reaches.
(semantics (a64.sdiv_rr_32 l r) (bvsdiv l r))
(semantics (a64.sdiv_rr_64 l r) (bvsdiv l r))
(semantics (a64.udiv_rr_32 l r) (bvudiv l r))
(semantics (a64.udiv_rr_64 l r) (bvudiv l r))
;; A multiply with an add or a subtract on the end, in the order the instruction takes its operands:
;; the two to multiply, then the one the product is added to or taken from.
(semantics (a64.madd_rrr_32 n m a) (bvadd a (bvmul n m)))
(semantics (a64.madd_rrr_64 n m a) (bvadd a (bvmul n m)))
(semantics (a64.msub_rrr_32 n m a) (bvsub a (bvmul n m)))
(semantics (a64.msub_rrr_64 n m a) (bvsub a (bvmul n m)))
;; Shifts. By a constant the count is whatever the rule's guard let through, and by a register the
;; machine takes it modulo the size of the register.
(semantics (a64.lsl_ri_32 l r) (bvshl l r))
(semantics (a64.lsl_ri_64 l r) (bvshl l r))
(semantics (a64.lsr_ri_32 l r) (bvlshr l r))
(semantics (a64.lsr_ri_64 l r) (bvlshr l r))
(semantics (a64.asr_ri_32 l r) (bvashr l r))
(semantics (a64.asr_ri_64 l r) (bvashr l r))
(semantics (a64.lsl_rr_32 l r) (bvshl l (bvand r 31)))
(semantics (a64.lsl_rr_64 l r) (bvshl l (bvand r 63)))
(semantics (a64.lsr_rr_32 l r) (bvlshr l (bvand r 31)))
(semantics (a64.lsr_rr_64 l r) (bvlshr l (bvand r 63)))
(semantics (a64.asr_rr_32 l r) (bvashr l (bvand r 31)))
(semantics (a64.asr_rr_64 l r) (bvashr l (bvand r 63)))
;; A compare and the `cset` behind it, which leaves a one or a zero in the whole register. The
;; condition codes are the architecture's names: `lo`, `ls`, `hi` and `hs` are the unsigned ones.
(semantics (a64.cmp_set_eq_32 l r) (ite (= l r) 1 0))
(semantics (a64.cmp_set_eq_ri_32 l r) (ite (= l r) 1 0))
(semantics (a64.cmp_set_eq_64 l r) (ite (= l r) 1 0))
(semantics (a64.cmp_set_eq_ri_64 l r) (ite (= l r) 1 0))
(semantics (a64.cmp_set_ne_32 l r) (ite (not (= l r)) 1 0))
(semantics (a64.cmp_set_ne_ri_32 l r) (ite (not (= l r)) 1 0))
(semantics (a64.cmp_set_ne_64 l r) (ite (not (= l r)) 1 0))
(semantics (a64.cmp_set_ne_ri_64 l r) (ite (not (= l r)) 1 0))
(semantics (a64.cmp_set_lt_32 l r) (ite (bvslt l r) 1 0))
(semantics (a64.cmp_set_lt_ri_32 l r) (ite (bvslt l r) 1 0))
(semantics (a64.cmp_set_lt_64 l r) (ite (bvslt l r) 1 0))
(semantics (a64.cmp_set_lt_ri_64 l r) (ite (bvslt l r) 1 0))
(semantics (a64.cmp_set_le_32 l r) (ite (bvsle l r) 1 0))
(semantics (a64.cmp_set_le_ri_32 l r) (ite (bvsle l r) 1 0))
(semantics (a64.cmp_set_le_64 l r) (ite (bvsle l r) 1 0))
(semantics (a64.cmp_set_le_ri_64 l r) (ite (bvsle l r) 1 0))
(semantics (a64.cmp_set_gt_32 l r) (ite (bvsgt l r) 1 0))
(semantics (a64.cmp_set_gt_ri_32 l r) (ite (bvsgt l r) 1 0))
(semantics (a64.cmp_set_gt_64 l r) (ite (bvsgt l r) 1 0))
(semantics (a64.cmp_set_gt_ri_64 l r) (ite (bvsgt l r) 1 0))
(semantics (a64.cmp_set_ge_32 l r) (ite (bvsge l r) 1 0))
(semantics (a64.cmp_set_ge_ri_32 l r) (ite (bvsge l r) 1 0))
(semantics (a64.cmp_set_ge_64 l r) (ite (bvsge l r) 1 0))
(semantics (a64.cmp_set_ge_ri_64 l r) (ite (bvsge l r) 1 0))
(semantics (a64.cmp_set_lo_32 l r) (ite (bvult l r) 1 0))
(semantics (a64.cmp_set_lo_ri_32 l r) (ite (bvult l r) 1 0))
(semantics (a64.cmp_set_lo_64 l r) (ite (bvult l r) 1 0))
(semantics (a64.cmp_set_lo_ri_64 l r) (ite (bvult l r) 1 0))
(semantics (a64.cmp_set_ls_32 l r) (ite (bvule l r) 1 0))
(semantics (a64.cmp_set_ls_ri_32 l r) (ite (bvule l r) 1 0))
(semantics (a64.cmp_set_ls_64 l r) (ite (bvule l r) 1 0))
(semantics (a64.cmp_set_ls_ri_64 l r) (ite (bvule l r) 1 0))
(semantics (a64.cmp_set_hi_32 l r) (ite (bvugt l r) 1 0))
(semantics (a64.cmp_set_hi_ri_32 l r) (ite (bvugt l r) 1 0))
(semantics (a64.cmp_set_hi_64 l r) (ite (bvugt l r) 1 0))
(semantics (a64.cmp_set_hi_ri_64 l r) (ite (bvugt l r) 1 0))
(semantics (a64.cmp_set_hs_32 l r) (ite (bvuge l r) 1 0))
(semantics (a64.cmp_set_hs_ri_32 l r) (ite (bvuge l r) 1 0))
(semantics (a64.cmp_set_hs_64 l r) (ite (bvuge l r) 1 0))
(semantics (a64.cmp_set_hs_ri_64 l r) (ite (bvuge l r) 1 0))
;; A compare of the condition with zero and a `csel` on `ne`, which picks the second operand when
;; the condition is set.
(semantics (a64.sel_32 f t c) (ite (not (= c 0)) t f))
(semantics (a64.sel_64 f t c) (ite (not (= c 0)) t f))
;; Widening. `uxtw_64` is a `mov` of one W register to another, which clears the top half of the X
;; register it writes, and that is the whole of a zero extension from thirty two bits.
(semantics (a64.sxtb_16 v) (sign_extend 8 16 v))
(semantics (a64.sxtb_32 v) (sign_extend 8 32 v))
(semantics (a64.sxtb_64 v) (sign_extend 8 64 v))
(semantics (a64.sxth_32 v) (sign_extend 16 32 v))
(semantics (a64.sxth_64 v) (sign_extend 16 64 v))
(semantics (a64.sxtw_64 v) (sign_extend 32 64 v))
(semantics (a64.uxtb_16 v) (zero_extend 8 16 v))
(semantics (a64.uxtb_32 v) (zero_extend 8 32 v))
(semantics (a64.uxth_32 v) (zero_extend 16 32 v))
(semantics (a64.uxtw_64 v) (zero_extend 32 64 v))
(semantics (a64.uxtb_64 v) (zero_extend 8 64 v))
(semantics (a64.uxth_64 v) (zero_extend 16 64 v))
;; Widening one bit is an `and` with one, which keeps the bit and clears the rest, so it does not
;; matter what was above the bit in the register it came from.
(semantics (a64.bit_to_8 v) (zero_extend 1 8 v))
(semantics (a64.bit_to_16 v) (zero_extend 1 16 v))
(semantics (a64.bit_to_32 v) (zero_extend 1 32 v))
(semantics (a64.bit_to_64 v) (zero_extend 1 64 v))
;; Narrowing. A value narrower than its register lives in the low end of it and what is above means
;; nothing, so a narrowing is a `mov` of the W register. Narrowing to one bit is an `and` that keeps
;; the bit and clears the rest, which is what every reader of a one bit value on this machine wants.
(semantics (a64.low_8 v) (extract 7 0 v))
(semantics (a64.low_16 v) (extract 15 0 v))
(semantics (a64.low_32 v) (extract 31 0 v))
(semantics (a64.bit_of_32 l r) (bvand (extract 0 0 l) r))
(semantics (a64.bit_of_64 l r) (bvand (extract 0 0 l) r))
;; The two addressing modes a load and a store reach through, which are an addition and nothing
;; about memory.
(semantics (amode_base base) base)
(semantics (amode_base_offset base offset) (bvadd base offset))
;; Reading memory, on the IR side. A load and a store are about which end of a value sits at the
;; lowest address, which is a fact about the target, so they are given a meaning here. AArch64 is
;; little endian as Linux, the BSDs, macOS and Windows run it, so these are the x86-64 entries.
(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)))
(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))))
(semantics (load.f128 a)
(float_from_bits 128 (concat (select (mem) (bvadd a 15)) (select (mem) (bvadd a 14))
(select (mem) (bvadd a 13)) (select (mem) (bvadd a 12))
(select (mem) (bvadd a 11)) (select (mem) (bvadd a 10))
(select (mem) (bvadd a 9)) (select (mem) (bvadd a 8))
(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, on the IR side. A `store` puts one byte into a memory and gives back the memory it
;; made, so these nest and the innermost runs first.
(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)))
(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))))
(semantics (store.f128 v a)
(store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (mem)
a (extract 7 0 (bits_from_float 128 v)))
(bvadd a 1) (extract 15 8 (bits_from_float 128 v)))
(bvadd a 2) (extract 23 16 (bits_from_float 128 v)))
(bvadd a 3) (extract 31 24 (bits_from_float 128 v)))
(bvadd a 4) (extract 39 32 (bits_from_float 128 v)))
(bvadd a 5) (extract 47 40 (bits_from_float 128 v)))
(bvadd a 6) (extract 55 48 (bits_from_float 128 v)))
(bvadd a 7) (extract 63 56 (bits_from_float 128 v)))
(bvadd a 8) (extract 71 64 (bits_from_float 128 v)))
(bvadd a 9) (extract 79 72 (bits_from_float 128 v)))
(bvadd a 10) (extract 87 80 (bits_from_float 128 v)))
(bvadd a 11) (extract 95 88 (bits_from_float 128 v)))
(bvadd a 12) (extract 103 96 (bits_from_float 128 v)))
(bvadd a 13) (extract 111 104 (bits_from_float 128 v)))
(bvadd a 14) (extract 119 112 (bits_from_float 128 v)))
(bvadd a 15) (extract 127 120 (bits_from_float 128 v))))
;; The instructions that do it, written out again rather than in terms of the IR heads above, so
;; that the two halves of a rule are two statements.
(semantics (a64.ldr_8 a)
(select (mem) a))
(semantics (a64.ldr_16 a)
(concat (select (mem) (bvadd a 1)) (select (mem) a)))
(semantics (a64.ldr_32 a)
(concat (select (mem) (bvadd a 3)) (select (mem) (bvadd a 2))
(select (mem) (bvadd a 1)) (select (mem) a)))
(semantics (a64.ldr_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 (a64.ldr_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 (a64.ldr_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))))
(semantics (a64.ldr_f128 a)
(float_from_bits 128 (concat (select (mem) (bvadd a 15)) (select (mem) (bvadd a 14))
(select (mem) (bvadd a 13)) (select (mem) (bvadd a 12))
(select (mem) (bvadd a 11)) (select (mem) (bvadd a 10))
(select (mem) (bvadd a 9)) (select (mem) (bvadd a 8))
(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 (a64.str_8 a v)
(store (mem) a v))
(semantics (a64.str_16 a v)
(store (store (mem)
a (extract 7 0 v))
(bvadd a 1) (extract 15 8 v)))
(semantics (a64.str_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 (a64.str_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 (a64.str_f32 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 (a64.str_f64 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))))
(semantics (a64.str_f128 a v)
(store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (mem)
a (extract 7 0 (bits_from_float 128 v)))
(bvadd a 1) (extract 15 8 (bits_from_float 128 v)))
(bvadd a 2) (extract 23 16 (bits_from_float 128 v)))
(bvadd a 3) (extract 31 24 (bits_from_float 128 v)))
(bvadd a 4) (extract 39 32 (bits_from_float 128 v)))
(bvadd a 5) (extract 47 40 (bits_from_float 128 v)))
(bvadd a 6) (extract 55 48 (bits_from_float 128 v)))
(bvadd a 7) (extract 63 56 (bits_from_float 128 v)))
(bvadd a 8) (extract 71 64 (bits_from_float 128 v)))
(bvadd a 9) (extract 79 72 (bits_from_float 128 v)))
(bvadd a 10) (extract 87 80 (bits_from_float 128 v)))
(bvadd a 11) (extract 95 88 (bits_from_float 128 v)))
(bvadd a 12) (extract 103 96 (bits_from_float 128 v)))
(bvadd a 13) (extract 111 104 (bits_from_float 128 v)))
(bvadd a 14) (extract 119 112 (bits_from_float 128 v)))
(bvadd a 15) (extract 127 120 (bits_from_float 128 v))))
;; Giving a value back and branching on one, which compute nothing: the value arrives unchanged in
;; the register the convention names, and `rucc_target::aarch64` says which register that is.
(semantics (a64.ret_val_32 v) v)
(semantics (a64.ret_val_64 v) v)
(semantics (a64.ret_val_f32 v) v)
(semantics (a64.ret_val_f64 v) v)
(semantics (a64.ret_val_f128 v) v)
(semantics (a64.br_cond_32 v) v)
;; Floats, one entry per instruction and format.
(semantics (a64.fadd_f32 l r) (fp.add l r))
(semantics (a64.fadd_f64 l r) (fp.add l r))
(semantics (a64.fsub_f32 l r) (fp.sub l r))
(semantics (a64.fsub_f64 l r) (fp.sub l r))
(semantics (a64.fmul_f32 l r) (fp.mul l r))
(semantics (a64.fmul_f64 l r) (fp.mul l r))
(semantics (a64.fdiv_f32 l r) (fp.div l r))
(semantics (a64.fdiv_f64 l r) (fp.div l r))
;; A float compare and the `cset` behind it. The head is named after the condition C's operator
;; asks for where the machine has one, and after the IR's predicate for the rest.
(semantics (a64.fcmp_set_gt_f32 l r) (ite (fp.gt l r) 1 0))
(semantics (a64.fcmp_set_gt_f64 l r) (ite (fp.gt l r) 1 0))
(semantics (a64.fcmp_set_ge_f32 l r) (ite (fp.geq l r) 1 0))
(semantics (a64.fcmp_set_ge_f64 l r) (ite (fp.geq l r) 1 0))
(semantics (a64.fcmp_set_lt_f32 l r) (ite (fp.lt l r) 1 0))
(semantics (a64.fcmp_set_lt_f64 l r) (ite (fp.lt l r) 1 0))
(semantics (a64.fcmp_set_le_f32 l r) (ite (fp.leq l r) 1 0))
(semantics (a64.fcmp_set_le_f64 l r) (ite (fp.leq l r) 1 0))
(semantics (a64.fcmp_set_one_f32 l r) (ite (or (fp.lt l r) (fp.gt l r)) 1 0))
(semantics (a64.fcmp_set_one_f64 l r) (ite (or (fp.lt l r) (fp.gt l r)) 1 0))
(semantics (a64.fcmp_set_ord_f32 l r) (ite (and (not (fp.isNaN l)) (not (fp.isNaN r))) 1 0))
(semantics (a64.fcmp_set_ord_f64 l r) (ite (and (not (fp.isNaN l)) (not (fp.isNaN r))) 1 0))
(semantics (a64.fcmp_set_uno_f32 l r) (ite (or (fp.isNaN l) (fp.isNaN r)) 1 0))
(semantics (a64.fcmp_set_uno_f64 l r) (ite (or (fp.isNaN l) (fp.isNaN r)) 1 0))
(semantics (a64.fcmp_set_ueq_f32 l r) (ite (not (or (fp.lt l r) (fp.gt l r))) 1 0))
(semantics (a64.fcmp_set_ueq_f64 l r) (ite (not (or (fp.lt l r) (fp.gt l r))) 1 0))
(semantics (a64.fcmp_set_ult_f32 l r) (ite (not (fp.geq l r)) 1 0))
(semantics (a64.fcmp_set_ult_f64 l r) (ite (not (fp.geq l r)) 1 0))
(semantics (a64.fcmp_set_ule_f32 l r) (ite (not (fp.gt l r)) 1 0))
(semantics (a64.fcmp_set_ule_f64 l r) (ite (not (fp.gt l r)) 1 0))
(semantics (a64.fcmp_set_ugt_f32 l r) (ite (not (fp.leq l r)) 1 0))
(semantics (a64.fcmp_set_ugt_f64 l r) (ite (not (fp.leq l r)) 1 0))
(semantics (a64.fcmp_set_uge_f32 l r) (ite (not (fp.lt l r)) 1 0))
(semantics (a64.fcmp_set_uge_f64 l r) (ite (not (fp.lt l r)) 1 0))
(semantics (a64.fcmp_set_eq_f32 l r) (ite (fp.eq l r) 1 0))
(semantics (a64.fcmp_set_eq_f64 l r) (ite (fp.eq l r) 1 0))
(semantics (a64.fcmp_set_ne_f32 l r) (ite (not (fp.eq l r)) 1 0))
(semantics (a64.fcmp_set_ne_f64 l r) (ite (not (fp.eq l r)) 1 0))
;; Conversions. `fcvt_f32_f64` widens a float to a double and `fcvt_f64_f32` narrows the other way,
;; `fcvtzs` rounds toward zero into a signed integer, `scvtf` goes back, and the two `fmov` pairs
;; move the bits between the register files without looking at them.
(semantics (a64.fcvt_f32_f64 v) (float_from_float 32 64 v))
(semantics (a64.fcvt_f64_f32 v) (float_from_float 64 32 v))
(semantics (a64.fcvtzs_f32_32 v) (signed_from_float 32 32 v))
(semantics (a64.fcvtzs_f32_64 v) (signed_from_float 32 64 v))
(semantics (a64.fcvtzs_f64_32 v) (signed_from_float 64 32 v))
(semantics (a64.fcvtzs_f64_64 v) (signed_from_float 64 64 v))
(semantics (a64.scvtf_32_f32 v) (float_from_signed 32 32 v))
(semantics (a64.scvtf_32_f64 v) (float_from_signed 32 64 v))
(semantics (a64.scvtf_64_f32 v) (float_from_signed 64 32 v))
(semantics (a64.scvtf_64_f64 v) (float_from_signed 64 64 v))
(semantics (a64.fmov_to_f32 v) (float_from_bits 32 v))
(semantics (a64.fmov_from_f32 v) (bits_from_float 32 v))
(semantics (a64.fmov_to_f64 v) (float_from_bits 64 v))
(semantics (a64.fmov_from_f64 v) (bits_from_float 64 v))