bc0de464bc
In [this comment](https://github.com/bytecodealliance/wasmtime/pull/3545#discussion_r756284757) I noted a potential subtle issue with the way that a few rules were written that is fine now but could cause some unexpected pain when we get around to verification. Specifically, a set of rules of the form ``` (rule (A (B _)) (C)) (rule (A _) (D)) ``` should, under any reasonable "default" rule ordering scheme, fire the more specific rule `(A (B _))` when applicable, in preference to the second "fallback" rule. However, for future verification-specific applications of ISLE, we want to ensure the property that a rule's meaning/validity is not dependent on being overridden by more specific rules. In other words, if a rule specifies a rewrite, that rewrite should always be correct; and choosing a more specific rule can give a *better* compilation (better generated code) but should not be necessary for correctness. This is an admittedly under-documented part of the language, though in the pending #3560 I added a note about rule ordering being a heuristic that should hopefully make this slightly clearer. Ultimately I want to have tests that choose non-default rule orderings and differentially fuzz in order to be sure that we're following this principle; and of course once we're actually doing verification, we'll catch issues like this upfront. Apologies for the subtle footgun here and hopefully the reasoning is clear enough :-)
182 lines
7.6 KiB
Common Lisp
182 lines
7.6 KiB
Common Lisp
;; aarch64 instruction selection and CLIF-to-MachInst lowering.
|
|
|
|
;; The main lowering constructor term: takes a clif `Inst` and returns the
|
|
;; register(s) within which the lowered instruction's result values live.
|
|
(decl lower (Inst) ValueRegs)
|
|
|
|
;;;; Rules for `iconst` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(rule (lower (has_type ty (iconst (u64_from_imm64 n))))
|
|
(value_reg (imm ty n)))
|
|
|
|
;;;; Rules for `bconst` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(rule (lower (has_type ty (bconst $false)))
|
|
(value_reg (imm ty 0)))
|
|
|
|
(rule (lower (has_type ty (bconst $true)))
|
|
(value_reg (imm ty 1)))
|
|
|
|
;;;; Rules for `null` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(rule (lower (has_type ty (null)))
|
|
(value_reg (imm ty 0)))
|
|
|
|
;;;; Rules for `iadd` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
;; `i64` and smaller
|
|
|
|
;; Base case, simply adding things in registers.
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd x y)))
|
|
(value_reg (alu_rrr (iadd_op ty) (put_in_reg x) (put_in_reg y))))
|
|
|
|
;; Special cases for when one operand is an immediate that fits in 12 bits.
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd x (imm12_from_value y))))
|
|
(value_reg (alu_rr_imm12 (iadd_op ty) (put_in_reg x) y)))
|
|
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd (imm12_from_value x) y)))
|
|
(value_reg (alu_rr_imm12 (iadd_op ty) (put_in_reg y) x)))
|
|
|
|
;; Same as the previous special cases, except we can switch the addition to a
|
|
;; subtraction if the negated immediate fits in 12 bits.
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd x (imm12_from_negated_value y))))
|
|
(value_reg (alu_rr_imm12 (isub_op ty) (put_in_reg x) y)))
|
|
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd (imm12_from_negated_value x) y)))
|
|
(value_reg (alu_rr_imm12 (isub_op ty) (put_in_reg y) x)))
|
|
|
|
;; Special cases for when we're adding an extended register where the extending
|
|
;; operation can get folded into the add itself.
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd x (extended_value_from_value y))))
|
|
(value_reg (alu_rr_extend_reg (iadd_op ty) (put_in_reg x) y)))
|
|
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd (extended_value_from_value x) y)))
|
|
(value_reg (alu_rr_extend_reg (iadd_op ty) (put_in_reg y) x)))
|
|
|
|
;; Special cases for when we're adding the shift of a different
|
|
;; register by a constant amount and the shift can get folded into the add.
|
|
(rule (lower (has_type (fits_in_64 ty)
|
|
(iadd x (def_inst (ishl y (def_inst (iconst (lshl_from_imm64 <ty amt))))))))
|
|
(value_reg (alu_rrr_shift (iadd_op ty) (put_in_reg x) (put_in_reg y) amt)))
|
|
|
|
(rule (lower (has_type (fits_in_64 ty)
|
|
(iadd (def_inst (ishl x (def_inst (iconst (lshl_from_imm64 <ty amt))))) y)))
|
|
(value_reg (alu_rrr_shift (iadd_op ty) (put_in_reg y) (put_in_reg x) amt)))
|
|
|
|
;; Fold an `iadd` and `imul` combination into a `madd` instruction.
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd x (def_inst (imul y z)))))
|
|
(value_reg (alu_rrrr (madd_op ty) (put_in_reg y) (put_in_reg z) (put_in_reg x))))
|
|
|
|
(rule (lower (has_type (fits_in_64 ty) (iadd (def_inst (imul x y)) z)))
|
|
(value_reg (alu_rrrr (madd_op ty) (put_in_reg x) (put_in_reg y) (put_in_reg z))))
|
|
|
|
;; Helper to use either a 32 or 64-bit add depending on the input type.
|
|
(decl iadd_op (Type) ALUOp)
|
|
(rule (iadd_op (fits_in_32 _ty)) (ALUOp.Add32))
|
|
(rule (iadd_op $I64) (ALUOp.Add64))
|
|
|
|
;; Helper to use either a 32 or 64-bit sub depending on the input type.
|
|
(decl isub_op (Type) ALUOp)
|
|
(rule (isub_op (fits_in_32 _ty)) (ALUOp.Sub32))
|
|
(rule (isub_op $I64) (ALUOp.Sub64))
|
|
|
|
;; Helper to use either a 32 or 64-bit madd depending on the input type.
|
|
(decl madd_op (Type) ALUOp3)
|
|
(rule (madd_op (fits_in_32 _ty)) (ALUOp3.MAdd32))
|
|
(rule (madd_op $I64) (ALUOp3.MAdd64))
|
|
|
|
;; vectors
|
|
|
|
(rule (lower (has_type ty @ (multi_lane _ _) (iadd x y)))
|
|
(value_reg (vec_rrr (VecALUOp.Add) (put_in_reg x) (put_in_reg y) (vector_size ty))))
|
|
|
|
;; `i128`
|
|
(rule (lower (has_type $I128 (iadd x y)))
|
|
(let (
|
|
;; Get the high/low registers for `x`.
|
|
(x_regs ValueRegs (put_in_regs x))
|
|
(x_lo Reg (value_regs_get x_regs 0))
|
|
(x_hi Reg (value_regs_get x_regs 1))
|
|
|
|
;; Get the high/low registers for `y`.
|
|
(y_regs ValueRegs (put_in_regs y))
|
|
(y_lo Reg (value_regs_get y_regs 0))
|
|
(y_hi Reg (value_regs_get y_regs 1))
|
|
)
|
|
;; the actual addition is `adds` followed by `adc` which comprises the
|
|
;; low/high bits of the result
|
|
(with_flags
|
|
(add64_with_flags x_lo y_lo)
|
|
(adc64 x_hi y_hi))))
|
|
|
|
;;;; Rules for `isub` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
;; `i64` and smaller
|
|
|
|
;; Base case, simply subtracting things in registers.
|
|
(rule (lower (has_type (fits_in_64 ty) (isub x y)))
|
|
(value_reg (alu_rrr (isub_op ty) (put_in_reg x) (put_in_reg y))))
|
|
|
|
;; Special case for when one operand is an immediate that fits in 12 bits.
|
|
(rule (lower (has_type (fits_in_64 ty) (isub x (imm12_from_value y))))
|
|
(value_reg (alu_rr_imm12 (isub_op ty) (put_in_reg x) y)))
|
|
|
|
;; Same as the previous special case, except we can switch the subtraction to an
|
|
;; addition if the negated immediate fits in 12 bits.
|
|
(rule (lower (has_type (fits_in_64 ty) (isub x (imm12_from_negated_value y))))
|
|
(value_reg (alu_rr_imm12 (iadd_op ty) (put_in_reg x) y)))
|
|
|
|
;; Special cases for when we're subtracting an extended register where the
|
|
;; extending operation can get folded into the sub itself.
|
|
(rule (lower (has_type (fits_in_64 ty) (isub x (extended_value_from_value y))))
|
|
(value_reg (alu_rr_extend_reg (isub_op ty) (put_in_reg x) y)))
|
|
|
|
;; Finally a special case for when we're subtracting the shift of a different
|
|
;; register by a constant amount and the shift can get folded into the sub.
|
|
(rule (lower (has_type (fits_in_64 ty)
|
|
(isub x (def_inst (ishl y (def_inst (iconst (lshl_from_imm64 <ty amt))))))))
|
|
(value_reg (alu_rrr_shift (isub_op ty) (put_in_reg x) (put_in_reg y) amt)))
|
|
|
|
;; vectors
|
|
(rule (lower (has_type ty @ (multi_lane _ _) (isub x y)))
|
|
(value_reg (vec_rrr (VecALUOp.Sub) (put_in_reg x) (put_in_reg y) (vector_size ty))))
|
|
|
|
;; `i128`
|
|
(rule (lower (has_type $I128 (isub x y)))
|
|
(let (
|
|
;; Get the high/low registers for `x`.
|
|
(x_regs ValueRegs (put_in_regs x))
|
|
(x_lo Reg (value_regs_get x_regs 0))
|
|
(x_hi Reg (value_regs_get x_regs 1))
|
|
|
|
;; Get the high/low registers for `y`.
|
|
(y_regs ValueRegs (put_in_regs y))
|
|
(y_lo Reg (value_regs_get y_regs 0))
|
|
(y_hi Reg (value_regs_get y_regs 1))
|
|
)
|
|
;; the actual subtraction is `subs` followed by `sbc` which comprises
|
|
;; the low/high bits of the result
|
|
(with_flags
|
|
(sub64_with_flags x_lo y_lo)
|
|
(sbc64 x_hi y_hi))))
|
|
|
|
;;;; Rules for `uadd_sat` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(rule (lower (has_type (vec128 ty) (uadd_sat x y)))
|
|
(value_reg (vec_rrr (VecALUOp.Uqadd) (put_in_reg x) (put_in_reg y) (vector_size ty))))
|
|
|
|
;;;; Rules for `sadd_sat` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(rule (lower (has_type (vec128 ty) (sadd_sat x y)))
|
|
(value_reg (vec_rrr (VecALUOp.Sqadd) (put_in_reg x) (put_in_reg y) (vector_size ty))))
|
|
|
|
;;;; Rules for `usub_sat` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(rule (lower (has_type (vec128 ty) (usub_sat x y)))
|
|
(value_reg (vec_rrr (VecALUOp.Uqsub) (put_in_reg x) (put_in_reg y) (vector_size ty))))
|
|
|
|
;;;; Rules for `ssub_sat` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(rule (lower (has_type (vec128 ty) (ssub_sat x y)))
|
|
(value_reg (vec_rrr (VecALUOp.Sqsub) (put_in_reg x) (put_in_reg y) (vector_size ty))))
|