inst.isle

;; Instruction formats.
(type MInst
  (enum
    (Nop)

    ;; Label to output at the beginning of a block
    (Label
      (imm usize))

    (LoadConst32
      (rd WritableReg)
      (imm u32))

    (LoadConst64
      (rd WritableReg)
      (imm u64))

    ;; An ALU operation with two register sources and a register destination.
    (AluRRR
      (alu_op AluOPRRR)
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg))

    ;;Multiplication via Arith
    (MulArith
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg))

    (Shl64
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg))

    (Shru64
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg))

    ;;Division via Arith
    (DivArith
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg))

    (UDivArith
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg))

    (RemArith
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg))

    (URemArith
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg))

    (Ineg
      (rd WritableReg)
      (rs1 Reg))

    (Bnot
      (rd WritableReg)
      (rs1 Reg))

    ;; An load
    (Load
      (rd WritableReg)
      (op LoadOP)
      (flags MemFlags)
      (from AMode))
    ;; An Store
    (Store
      (to AMode)
      (op StoreOP)
      (flags MemFlags)
      (src Reg))

    ;; A pseudo-instruction that captures register arguments in vregs.
    (Args
      (args VecArgPair))

    (Ret (rets VecRetPair)
         (stack_bytes_to_pop u64))

    (Extend
      (rd WritableReg)
      (rn Reg)
      (signed bool)
      (from_bits u8)
      (to_bits u8))

    ;; Adjust the stack pointer as necessary.
    (ReserveSp
      (amount u64))
    (ReleaseSp
      (amount u64))

    (Call
      (info BoxCallInfo))

      ;; A machine indirect-call instruction.
    (CallInd
      (info BoxCallIndInfo))

    ;; A direct return-call macro instruction.
    (ReturnCall
      (callee BoxExternalName)
      (info BoxReturnCallInfo))

    ;; An indirect return-call macro instruction.
    (ReturnCallInd
      (callee Reg)
      (info BoxReturnCallInfo))

    (TrapIf
      (test Reg)
      (trap_code TrapCode))

    ;; use a simple compare to decide to cause trap or not.
    (TrapIfC
      (rs1 Reg)
      (rs2 Reg)
      (cc IntCC)
      (trap_code TrapCode))

    (Jal
      ;; (rd WritableReg) don't use
      (dest BranchTarget))

    (CondBr
      (taken BranchTarget)
      (not_taken BranchTarget)
      (kind IntegerCompare))

    ;; Load an inline symbol reference.
    (LoadExtName
      (rd WritableReg)
      (name BoxExternalName)
      (offset i64))

    ;; Load address referenced by `mem` into `rd`.
    (LoadAddr
      (rd WritableReg)
      (mem AMode))

    ;; Marker, no-op in generated code: SP "virtual offset" is adjusted. This
    ;; controls how AMode::NominalSPOffset args are lowered.
    (VirtualSPOffsetAdj
      (amount i64))

    ;; A MOV instruction. These are encoded as OrR's (AluRRR form) but we
    ;; keep them separate at the `Inst` level for better pretty-printing
    ;; and faster `is_move()` logic.
    (Mov
      (rd WritableReg)
      (rm Reg)
      (ty Type))

    ;; A MOV instruction, but where the source register is a non-allocatable
    ;; PReg. It's important that the register be non-allocatable, as regalloc2
    ;; will not see it as used.
    (MovFromPReg
      (rd WritableReg)
      (rm PReg))

    (ECall)

    (EBreak)

    ;; An instruction guaranteed to always be undefined and to trigger an illegal instruction at
    ;; runtime.
    (Udf
      (trap_code TrapCode))
    ;; a jump and link register operation
    (Jalr
      ;;Plain unconditional jumps (assembler pseudo-op J) are encoded as a JAL with rd=x0.
      (rd WritableReg)
      (base Reg)
      (offset Imm32))

    ;; select x or y base on condition
    (Select
      (dst VecWritableReg)
      (ty Type)
      (condition Reg)
      (x ValueRegs)
      (y ValueRegs))

    (BrTable
      (index Reg)
      (tmp1 WritableReg)
      (tmp2 WritableReg)
      (targets VecBranchTarget))

    ;; select x or y base on op_code
    (IntSelect
      (op IntSelectOP)
      (dst VecWritableReg)
      (x ValueRegs)
      (y ValueRegs)
      (ty Type))
    ;; an integer compare.
    (Icmp
      (cc IntCC)
      (rd WritableReg)
      (a ValueRegs)
      (b ValueRegs)
      (ty Type))
    ;; select a reg base on condition.
    ;; very useful because in lowering stage we can not have condition branch.
    (SelectReg
      (rd WritableReg)
      (rs1 Reg)
      (rs2 Reg)
      (condition IntegerCompare))

    (RawData (data VecU8))

    ;; An unwind pseudo-instruction.
       (Unwind
        (inst UnwindInst))

    ;; A dummy use, useful to keep a value alive.
       (DummyUse
        (reg Reg))

    ;; popcnt  if target doesn't support extension B
    ;; use iteration to implement.
    (Popcnt
      (sum WritableReg)
      (step WritableReg)
      (tmp WritableReg)
      (rs Reg)
      (ty Type))

    ;;; counting leading or trailing zeros.
    (Cltz
      ;; leading or trailing.
      (leading bool)
      (sum WritableReg)
      (step WritableReg)
      (tmp WritableReg)
      (rs Reg)
      (ty Type))
    ;; Byte-reverse register
    (Rev8
      (rs Reg)
      (step WritableReg)
      (tmp WritableReg)
      (rd WritableReg))
    ;;
    (Brev8
      (rs Reg)
      (ty Type)
      (step WritableReg)
      (tmp WritableReg)
      (tmp2 WritableReg)
      (rd WritableReg))
    (StackProbeLoop
      (guard_size u32)
      (probe_count u32)
      (tmp WritableReg))

    ;; An addition with 2 32-bit immediates.
    (AddImm32
      (rd WritableReg)
      (src1 Imm32)
      (src2 Imm32))

))

(type IntSelectOP (enum
  (Smax)
  (Umax)
  (Smin)
  (Umin)
))

(type AtomicOP (enum
  (LrW)
  (ScW)
  (AmoswapW)
  (AmoaddW)
  (AmoxorW)
  (AmoandW)
  (AmoorW)
  (AmominW)
  (AmomaxW)
  (AmominuW)
  (AmomaxuW)
  (LrD)
  (ScD)
  (AmoswapD)
  (AmoaddD)
  (AmoxorD)
  (AmoandD)
  (AmoorD)
  (AmominD)
  (AmomaxD)
  (AmominuD)
  (AmomaxuD)
))

(type LoadOP (enum
  (I8)
  (I16)
  (I32)
  (U8)
  (U16)
  (U32)
  (U64)
  (Flw)
  (Fld)
))

(type StoreOP (enum
  (I8)
  (I16)
  (I32)
  (I64)
  (Fsw)
  (Fsd)
))

(type ZkasmBase (enum
  (Heap)
  (Global)
  (Table)
))

(type AluOPRRR (enum
  ;; base set
  (Add)
  (Sub)
  (Sll)
  (Slt)
  (SltU)
  (Sgt)
  (Sgtu)
  (Xor)
  (Srl)
  (Sra)
  (Or)
  (And)

  ;; RV64I Base Instruction Set (in addition to RV32I)
  (Addw)
  (Subw)
  (Sllw)
  (Srlw)
  (Sraw)


  ;;RV32M Standard Extension
  (Mulh)
  (Mulhsu)
  (Mulhu)
  (DivU)
  (Rem)
  (RemU)

  ;; RV64M Standard Extension (in addition to RV32M)
  (Divuw)
  (Remw)
  (Remuw)

  ;; Zba: Address Generation Instructions
  (Adduw)
  (Sh1add)
  (Sh1adduw)
  (Sh2add)
  (Sh2adduw)
  (Sh3add)
  (Sh3adduw)

  ;; Zbb: Bit Manipulation Instructions
  (Andn)
  (Orn)
  (Xnor)
  (Max)
  (Maxu)
  (Min)
  (Minu)
  (Rol)
  (Rolw)
  (Ror)
  (Rorw)

  ;; Zbs: Single-bit instructions
  (Bclr)
  (Bext)
  (Binv)
  (Bset)

  ;; Zbc: Carry-less multiplication
  (Clmul)
  (Clmulh)
  (Clmulr)

  ;; Zbkb: Bit-manipulation for Cryptography
  (Pack)
  (Packw)
  (Packh)
))


(type AluOPRRI (enum
  ;; Base ISA
  (Addi)
  (Slti)
  (SltiU)
  (Xori)
  (Ori)
  (Andi)
  (Slli)
  (Srli)
  (Srai)
  (Addiw)
  (Slliw)
  (SrliW)
  (Sraiw)

  ;; Zba: Address Generation Instructions
  (SlliUw)

  ;; Zbb: Bit Manipulation Instructions
  (Clz)
  (Clzw)
  (Ctz)
  (Ctzw)
  (Cpop)
  (Cpopw)
  (Sextb)
  (Sexth)
  (Zexth)
  (Rori)
  (Roriw)
  (Rev8)
  (Brev8)
  (Orcb)

  ;; Zbs: Single-bit instructions
  (Bclri)
  (Bexti)
  (Binvi)
  (Bseti)
))

(type FFlagsException (enum
  ;; Invalid Operation
  (NV)
  ;; Divide by Zero
  (DZ)
  ;; Overflow
  (OF)
  ;; Underflow
  (UF)
  ;; Inexact
  (NX)
))

;;;; input output read write
;;;; SI SO SR SW
;;;; PI PO PR PW
;;;; lowest four bit are used.
(type FenceReq (primitive u8))

(type VecBranchTarget (primitive VecBranchTarget))
(type BoxCallInfo (primitive BoxCallInfo))
(type BoxCallIndInfo (primitive BoxCallIndInfo))
(type BoxReturnCallInfo (primitive BoxReturnCallInfo))
(type IntegerCompare (primitive IntegerCompare))
(type AMode (primitive AMode))
(type OptionReg (primitive OptionReg))
(type OptionImm12 (primitive OptionImm12))
(type OptionUimm5 (primitive OptionUimm5))
(type Imm12 (primitive Imm12))
(type Imm32 (primitive Imm32))
(type UImm5 (primitive UImm5))
(type Imm5 (primitive Imm5))
(type Imm20 (primitive Imm20))
(type Imm3 (primitive Imm3))
(type BranchTarget (primitive BranchTarget))
(type VecU8 (primitive VecU8))
(type AMO (primitive AMO))
(type VecMachLabel extern (enum))


;;;; Newtypes for Different Register Classes ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(type XReg (primitive XReg))
(type WritableXReg (primitive WritableXReg))
(type FReg (primitive FReg))
(type WritableFReg (primitive WritableFReg))
(type VReg (primitive VReg))
(type WritableVReg (primitive WritableVReg))

;; Construct a new `XReg` from a `Reg`.
;;
;; Asserts that the register has a Integer RegClass.
(decl xreg_new (Reg) XReg)
(extern constructor xreg_new xreg_new)
(convert Reg XReg xreg_new)

;; Construct a new `WritableXReg` from a `WritableReg`.
;;
;; Asserts that the register has a Integer RegClass.
(decl writable_xreg_new (WritableReg) WritableXReg)
(extern constructor writable_xreg_new writable_xreg_new)
(convert WritableReg WritableXReg writable_xreg_new)

;; Put a value into a XReg.
;;
;; Asserts that the value goes into a XReg.
(decl put_in_xreg (Value) XReg)
(rule (put_in_xreg val) (xreg_new (put_in_reg val)))
(convert Value XReg put_in_xreg)

;; Construct an `InstOutput` out of a single XReg register.
(decl output_xreg (XReg) InstOutput)
(rule (output_xreg x) (output_reg x))
(convert XReg InstOutput output_xreg)

;; Convert a `WritableXReg` to an `XReg`.
(decl pure writable_xreg_to_xreg (WritableXReg) XReg)
(extern constructor writable_xreg_to_xreg writable_xreg_to_xreg)
(convert WritableXReg XReg writable_xreg_to_xreg)

;; Convert a `WritableXReg` to an `WritableReg`.
(decl pure writable_xreg_to_writable_reg (WritableXReg) WritableReg)
(extern constructor writable_xreg_to_writable_reg writable_xreg_to_writable_reg)
(convert WritableXReg WritableReg writable_xreg_to_writable_reg)

;; Convert a `WritableXReg` to an `Reg`.
(decl pure writable_xreg_to_reg (WritableXReg) Reg)
(rule (writable_xreg_to_reg x) (writable_xreg_to_writable_reg x))
(convert WritableXReg Reg writable_xreg_to_reg)

;; Convert an `XReg` to a `Reg`.
(decl pure xreg_to_reg (XReg) Reg)
(extern constructor xreg_to_reg xreg_to_reg)
(convert XReg Reg xreg_to_reg)

;; Convert a `XReg` to a `ValueRegs`.
(decl xreg_to_value_regs (XReg) ValueRegs)
(rule (xreg_to_value_regs x) (value_reg x))
(convert XReg ValueRegs xreg_to_reg)

;; Convert a `WritableXReg` to a `ValueRegs`.
(decl writable_xreg_to_value_regs (WritableXReg) ValueRegs)
(rule (writable_xreg_to_value_regs x) (value_reg x))
(convert WritableXReg ValueRegs writable_xreg_to_value_regs)

;; Allocates a new `WritableXReg`.
(decl temp_writable_xreg () WritableXReg)
(rule (temp_writable_xreg) (temp_writable_reg $I64))

;; Converters

(convert u8 i32 u8_as_i32)
(decl u8_as_i32 (u8) i32)
(extern constructor u8_as_i32 u8_as_i32)

;;;; Instruction Helpers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(decl zk_add (Imm32 Imm32) XReg)
(rule (zk_add imm1 imm2)
    (let ((dst WritableXReg (temp_writable_xreg))
          (_ Unit (emit (MInst.AddImm32 dst imm1 imm2))))
     dst))

;; Helper for emitting the `add` instruction.
;; rd ← rs1 + rs2
(decl rv_add (XReg XReg) XReg)
(rule (rv_add rs1 rs2)
  (alu_rrr (AluOPRRR.Add) rs1 rs2))

;; Helper for emitting the `sub` instruction.
;; rd ← rs1 - rs2
(decl rv_sub (XReg XReg) XReg)
(rule (rv_sub rs1 rs2)
  (alu_rrr (AluOPRRR.Sub) rs1 rs2))

;; Helper for emitting the `sll` ("Shift Left Logical") instruction.
;; rd ← rs1 << rs2
(decl rv_sll (XReg XReg) XReg)
(rule (rv_sll rs1 rs2)
  (alu_rrr (AluOPRRR.Sll) rs1 rs2))

;; Helper for emitting the `srl` ("Shift Right Logical") instruction.
;; rd ← rs1 >> rs2
(decl rv_srl (XReg XReg) XReg)
(rule (rv_srl rs1 rs2)
  (alu_rrr (AluOPRRR.Srl) rs1 rs2))

;; Helper for emitting the `sra` ("Shift Right Arithmetic") instruction.
;; rd ← rs1 >> rs2
(decl rv_sra (XReg XReg) XReg)
(rule (rv_sra rs1 rs2)
  (alu_rrr (AluOPRRR.Sra) rs1 rs2))

;; Helper for emitting the `or` instruction.
;; rd ← rs1 ∨ rs2
(decl rv_or (XReg XReg) XReg)
(rule (rv_or rs1 rs2)
  (alu_rrr (AluOPRRR.Or) rs1 rs2))

;; Helper for emitting the `xor` instruction.
;; rd ← rs1 ⊕ rs2
(decl rv_xor (XReg XReg) XReg)
(rule (rv_xor rs1 rs2)
  (alu_rrr (AluOPRRR.Xor) rs1 rs2))

;; Helper for emitting the `and` instruction.
;; rd ← rs1 ∧ rs2
(decl rv_and (XReg XReg) XReg)
(rule (rv_and rs1 rs2)
  (alu_rrr (AluOPRRR.And) rs1 rs2))

;; Helper for emitting the `sltu` ("Set Less Than Unsigned") instruction.
;; rd ← rs1 < rs2
(decl rv_sltu (XReg XReg) XReg)
(rule (rv_sltu rs1 rs2)
  (alu_rrr (AluOPRRR.SltU) rs1 rs2))

;; Helper for emitting the `snez` instruction.
;; This instruction is a mnemonic for `sltu rd, zero, rs`.
(decl rv_snez (XReg) XReg)
(rule (rv_snez rs1)
  (rv_sltu (zero_reg) rs1))

;; RV64I Base Integer Instruction Set
;; Unlike RV32I instructions these are only present in the 64bit ISA

;; Helper for emitting the `addw` ("Add Word") instruction.
;; rd ← sext32(rs1) + sext32(rs2)
(decl rv_addw (XReg XReg) XReg)
(rule (rv_addw rs1 rs2)
  (alu_rrr (AluOPRRR.Addw) rs1 rs2))

;; Helper for emitting the `subw` ("Subtract Word") instruction.
;; rd ← sext32(rs1) - sext32(rs2)
(decl rv_subw (XReg XReg) XReg)
(rule (rv_subw rs1 rs2)
  (alu_rrr (AluOPRRR.Subw) rs1 rs2))

;; Helper for emitting the `sllw` ("Shift Left Logical Word") instruction.
;; rd ← sext32(uext32(rs1) << rs2)
(decl rv_sllw (XReg XReg) XReg)
(rule (rv_sllw rs1 rs2)
  (alu_rrr (AluOPRRR.Sllw) rs1 rs2))

;; Helper for emitting the `srlw` ("Shift Right Logical Word") instruction.
;; rd ← sext32(uext32(rs1) >> rs2)
(decl rv_srlw (XReg XReg) XReg)
(rule (rv_srlw rs1 rs2)
  (alu_rrr (AluOPRRR.Srlw) rs1 rs2))

;; Helper for emitting the `sraw` ("Shift Right Arithmetic Word") instruction.
;; rd ← sext32(rs1 >> rs2)
(decl rv_sraw (XReg XReg) XReg)
(rule (rv_sraw rs1 rs2)
  (alu_rrr (AluOPRRR.Sraw) rs1 rs2))



;; RV32M Extension
;; TODO: Enable these instructions only when we have the M extension

(decl zk_shr_u (XReg XReg) XReg)
(rule (zk_shr_u rs1 rs2)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.Shru64 dst rs1 rs2))))
        dst))

(decl zk_shl (XReg XReg) XReg)
(rule (zk_shl rs1 rs2)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.Shl64 dst rs1 rs2))))
        dst))

;; Helper for emitting the `mul` instruction.
;; rd ← rs1 × rs2
(decl zk_mul (XReg XReg) XReg)
(rule (zk_mul rs1 rs2)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.MulArith dst rs1 rs2))))
        dst))

(decl zk_divu (XReg XReg) XReg)
(rule (zk_divu rs1 rs2)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.UDivArith dst rs1 rs2))))
        dst))

;; Helper for emitting the `mulh` ("Multiply High Signed Signed") instruction.
;; rd ← (sext(rs1) × sext(rs2)) » xlen
(decl rv_mulh (XReg XReg) XReg)
(rule (rv_mulh rs1 rs2)
  (alu_rrr (AluOPRRR.Mulh) rs1 rs2))

;; Helper for emitting the `mulhu` ("Multiply High Unsigned Unsigned") instruction.
;; rd ← (uext(rs1) × uext(rs2)) » xlen
(decl rv_mulhu (XReg XReg) XReg)
(rule (rv_mulhu rs1 rs2)
  (alu_rrr (AluOPRRR.Mulhu) rs1 rs2))

;; Helper for emitting the `div` instruction.
;; rd ← rs1 ÷ rs2
(decl zk_div (XReg XReg) XReg)
(rule (zk_div rs1 rs2)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.DivArith dst rs1 rs2))))
        dst))

;; Helper for emitting the `rem` instruction.
;; rd ← rs1 % rs2
(decl zk_rem (XReg XReg) XReg)
(rule (zk_rem rs1 rs2)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.RemArith dst rs1 rs2))))
        dst))

(decl zk_remu (XReg XReg) XReg)
(rule (zk_remu rs1 rs2)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.URemArith dst rs1 rs2))))
        dst))

;; Helper for emitting the `divu` ("Divide Unsigned") instruction.
;; rd ← rs1 ÷ rs2
(decl rv_divu (XReg XReg) XReg)
(rule (rv_divu rs1 rs2)
  (alu_rrr (AluOPRRR.DivU) rs1 rs2))

;; Helper for emitting the `rem` instruction.
;; rd ← rs1 mod rs2
(decl rv_rem (XReg XReg) XReg)
(rule (rv_rem rs1 rs2)
  (alu_rrr (AluOPRRR.Rem) rs1 rs2))

;; Helper for emitting the `remu` ("Remainder Unsigned") instruction.
;; rd ← rs1 mod rs2
(decl rv_remu (XReg XReg) XReg)
(rule (rv_remu rs1 rs2)
  (alu_rrr (AluOPRRR.RemU) rs1 rs2))



;; RV64M Extension
;; TODO: Enable these instructions only when we have the M extension

;; Helper for emitting the `divuw` ("Divide Unsigned Word") instruction.
;; rd ← uext32(rs1) ÷ uext32(rs2)
(decl rv_divuw (XReg XReg) XReg)
(rule (rv_divuw rs1 rs2)
  (alu_rrr (AluOPRRR.Divuw) rs1 rs2))

;; Helper for emitting the `remw` ("Remainder Word") instruction.
;; rd ← sext32(rs1) mod sext32(rs2)
(decl rv_remw (XReg XReg) XReg)
(rule (rv_remw rs1 rs2)
  (alu_rrr (AluOPRRR.Remw) rs1 rs2))

;; Helper for emitting the `remuw` ("Remainder Unsigned Word") instruction.
;; rd ← uext32(rs1) mod uext32(rs2)
(decl rv_remuw (XReg XReg) XReg)
(rule (rv_remuw rs1 rs2)
  (alu_rrr (AluOPRRR.Remuw) rs1 rs2))


;; `Zba` Extension Instructions

;; Helper for emitting the `adduw` ("Add Unsigned Word") instruction.
;; rd ← uext32(rs1) + uext32(rs2)
(decl rv_adduw (XReg XReg) XReg)
(rule (rv_adduw rs1 rs2)
  (alu_rrr (AluOPRRR.Adduw) rs1 rs2))

;; Helper for emitting the `zext.w` ("Zero Extend Word") instruction.
;; This instruction is a mnemonic for `adduw rd, rs1, zero`.
;; rd ← uext32(rs1)
(decl rv_zextw (XReg) XReg)
(rule (rv_zextw rs1)
  (rv_adduw rs1 (zero_reg)))


;; `Zbb` Extension Instructions

;; Helper for emitting the `andn` ("And Negated") instruction.
;; rd ← rs1 ∧ ~(rs2)
(decl rv_andn (XReg XReg) XReg)
(rule (rv_andn rs1 rs2)
  (alu_rrr (AluOPRRR.Andn) rs1 rs2))

;; Helper for emitting the `orn` ("Or Negated") instruction.
;; rd ← rs1 ∨ ~(rs2)
(decl rv_orn (XReg XReg) XReg)
(rule (rv_orn rs1 rs2)
  (alu_rrr (AluOPRRR.Orn) rs1 rs2))

;; Helper for emitting the `max` instruction.
(decl rv_max (XReg XReg) XReg)
(rule (rv_max rs1 rs2)
  (alu_rrr (AluOPRRR.Max) rs1 rs2))

;; Helper for emitting the `rol` ("Rotate Left") instruction.
(decl rv_rol (XReg XReg) XReg)
(rule (rv_rol rs1 rs2)
  (alu_rrr (AluOPRRR.Rol) rs1 rs2))

;; Helper for emitting the `rolw` ("Rotate Left Word") instruction.
(decl rv_rolw (XReg XReg) XReg)
(rule (rv_rolw rs1 rs2)
  (alu_rrr (AluOPRRR.Rolw) rs1 rs2))

;; Helper for emitting the `ror` ("Rotate Right") instruction.
(decl rv_ror (XReg XReg) XReg)
(rule (rv_ror rs1 rs2)
  (alu_rrr (AluOPRRR.Ror) rs1 rs2))

;; Helper for emitting the `rorw` ("Rotate Right Word") instruction.
(decl rv_rorw (XReg XReg) XReg)
(rule (rv_rorw rs1 rs2)
  (alu_rrr (AluOPRRR.Rorw) rs1 rs2))

;; `Zbkb` Extension Instructions

;; Helper for emitting the `pack` ("Pack low halves of registers") instruction.
(decl rv_pack (XReg XReg) XReg)
(rule (rv_pack rs1 rs2)
  (alu_rrr (AluOPRRR.Pack) rs1 rs2))

;; Helper for emitting the `packw` ("Pack low 16-bits of registers") instruction.
(decl rv_packw (XReg XReg) XReg)
(rule (rv_packw rs1 rs2)
  (alu_rrr (AluOPRRR.Packw) rs1 rs2))




;; Generate a mask for the bit-width of the given type
(decl pure shift_mask (Type) u64)
(rule (shift_mask ty) (u64_sub (ty_bits (lane_type ty)) 1))

;; for load immediate
(decl imm (Type u64) Reg)
(extern constructor imm imm)

;; Imm12 Rules

; (decl load_imm12 (i32) Reg)
; (rule
;   (load_imm12 x)
;   (rv_addi (zero_reg) (imm12_const x)))

;; Imm12 Extractors

;; Helper to go directly from a `Value`, when it's an `iconst`, to an `Imm12`.
(decl imm32_from_value (Imm32) Value)
(extractor
  (imm32_from_value n)
  (def_inst (iconst (u64_from_imm64 (imm32_from_u64 n)))))

(decl imm32_from_u64 (Imm32) u64)
(extern extractor imm32_from_u64 imm32_from_u64)

(decl pure partial u64_to_imm32 (u64) Imm32)
(rule (u64_to_imm32 (imm32_from_u64 n)) n)


;; Imm5 Extractors

(decl imm5_from_u64 (Imm5) u64)
(extern extractor imm5_from_u64 imm5_from_u64)

;; Construct a Imm5 from an i8
(decl pure partial imm5_from_i8 (i8) Imm5)
(extern constructor imm5_from_i8 imm5_from_i8)

;; Extractor that matches a `Value` equivalent to a replicated Imm5 on all lanes.
;; TODO(#6527): Try matching vconst here as well
(decl replicated_imm5 (Imm5) Value)
(extractor (replicated_imm5 n)
  (def_inst (splat (iconst (u64_from_imm64 (imm5_from_u64 n))))))

;; UImm5 Helpers

;; Extractor that matches a `Value` equivalent to a replicated UImm5 on all lanes.
;; TODO(#6527): Try matching vconst here as well
(decl replicated_uimm5 (UImm5) Value)
(extractor (replicated_uimm5 n)
  (def_inst (splat (uimm5_from_value n))))

;; Helper to go directly from a `Value`, when it's an `iconst`, to an `UImm5`.
(decl uimm5_from_value (UImm5) Value)
(extractor (uimm5_from_value n)
  (iconst (u64_from_imm64 (uimm5_from_u64 n))))

;; Extract a `UImm5` from an `u8`.
(decl pure partial uimm5_from_u8 (UImm5) u8)
(extern extractor uimm5_from_u8 uimm5_from_u8)

;; Extract a `UImm5` from an `u64`.
(decl pure partial uimm5_from_u64 (UImm5) u64)
(extern extractor uimm5_from_u64 uimm5_from_u64)

;; Convert a `u64` into an `UImm5`
(decl pure partial u64_to_uimm5 (u64) UImm5)
(rule (u64_to_uimm5 (uimm5_from_u64 n)) n)

(decl uimm5_bitcast_to_imm5 (UImm5) Imm5)
(extern constructor uimm5_bitcast_to_imm5 uimm5_bitcast_to_imm5)

;; Float Helpers

;; Returns the bitpattern of the Canonical NaN for the given type.
(decl pure canonical_nan_u64 (Type) u64)
(rule (canonical_nan_u64 $F32) 0x7fc00000)
(rule (canonical_nan_u64 $F64) 0x7ff8000000000000)

;; Helper for emitting `MInst.AluRRR` instructions.
(decl alu_rrr (AluOPRRR Reg Reg) Reg)
(rule (alu_rrr op src1 src2)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.AluRRR op dst src1 src2))))
        dst))


(decl select_addi (Type) AluOPRRI)
(rule 1 (select_addi (fits_in_32 ty)) (AluOPRRI.Addiw))
(rule (select_addi (fits_in_64 ty)) (AluOPRRI.Addi))


(decl gen_and (Type ValueRegs ValueRegs) ValueRegs)
(rule 0 (gen_and (fits_in_64 _) x y)
  (rv_and (value_regs_get x 0) (value_regs_get y 0)))


(decl gen_andi (XReg u64) XReg)
(rule 0 (gen_andi x y)
  (rv_and x (imm $I64 y)))


(decl gen_or (Type ValueRegs ValueRegs) ValueRegs)
(rule 0 (gen_or (fits_in_64 _) x y)
  (rv_or (value_regs_get x 0) (value_regs_get y 0)))



(decl gen_bswap (Type XReg) XReg)

;; This is only here to make the rule below work. bswap.i8 isn't valid
(rule 0 (gen_bswap $I8 x) x)

; (rule 1 (gen_bswap (ty_int_ref_16_to_64 ty) x)
;   (if-let half_ty (ty_half_width ty))
;   (if-let half_size (u64_to_imm12 (ty_bits half_ty)))
;   (let (;; This swaps the top bytes and zeroes the bottom bytes, so that
;         ;; we can or it with the bottom bytes later.
;         (swap_top XReg (gen_bswap half_ty x))
;         (top XReg (rv_slli swap_top half_size))
;
;         ;; Get the top half, swap it, and zero extend it so we can `or` it
;         ;; with the bottom half.
;         (shifted XReg (rv_srli x half_size))
;         (swap_bot XReg (gen_bswap half_ty shifted))
;         (bot XReg (zext swap_bot half_ty $I64)))
;     (rv_or top bot)))

(decl lower_ctz (Type Reg) Reg)
(rule (lower_ctz ty x)
  (gen_cltz $false x ty))

(decl lower_clz (Type XReg) XReg)
(rule (lower_clz ty rs)
  (gen_cltz $true rs ty))

(decl gen_cltz (bool XReg Type) XReg)
(rule (gen_cltz leading rs ty)
  (let ((tmp WritableXReg (temp_writable_xreg))
        (step WritableXReg (temp_writable_xreg))
        (sum WritableXReg (temp_writable_xreg))
        (_ Unit (emit (MInst.Cltz leading sum step tmp rs ty))))
    sum))


;; Extends an integer if it is smaller than 64 bits.
(decl ext_int_if_need (bool ValueRegs Type) ValueRegs)
;;; For values smaller than 64 bits, we need to extend them to 64 bits
(rule 0 (ext_int_if_need $true val (fits_in_32 (ty_int ty)))
  (extend val (ExtendOp.Signed) ty $I64))
(rule 0 (ext_int_if_need $false val (fits_in_32 (ty_int ty)))
  (extend val (ExtendOp.Zero) ty $I64))
;; If the value is larger than one machine register, we don't need to do anything
(rule 1 (ext_int_if_need _ r $I64) r)


;; Performs a zero extension of the given value
(decl zext (XReg Type Type) XReg)
(rule (zext val from_ty (fits_in_64 to_ty)) (value_regs_get (extend val (ExtendOp.Zero) from_ty to_ty) 0))

;; Performs a signed extension of the given value
(decl sext (XReg Type Type) XReg)
(rule (sext val from_ty (fits_in_64 to_ty)) (value_regs_get (extend val (ExtendOp.Signed) from_ty to_ty) 0))

(type ExtendOp
  (enum
    (Zero)
    (Signed)))

;; Performs either a sign or zero extension of the given value
(decl extend (ValueRegs ExtendOp Type Type) ValueRegs)

;;; Generic Rules Extending to I64
(decl pure extend_shift_op (ExtendOp) AluOPRRI)
(rule (extend_shift_op (ExtendOp.Zero)) (AluOPRRI.Srli))
(rule (extend_shift_op (ExtendOp.Signed)) (AluOPRRI.Srai))

;; In the most generic case, we shift left and then shift right.
;; The type of right shift is determined by the extend op.
; (rule 0 (extend val extend_op (fits_in_32 from_ty) (fits_in_64 to_ty))
;   (let ((val XReg (value_regs_get val 0))
;         (shift Imm12 (imm_from_bits (u64_sub 64 (ty_bits from_ty))))
;         (left XReg (rv_slli val shift))
;         (shift_op AluOPRRI (extend_shift_op extend_op))
;         (right XReg (alu_rr_imm12 shift_op left shift)))
;     right))

;; Hacky no-op version.
(rule 0 (extend val extend_op (fits_in_32 from_ty) (fits_in_64 to_ty))
  (let ((right XReg (value_regs_get val 0)))
    right))

;;; Unsigned rules extending to I128
;; Extend the bottom register to I64 and then just zero out the top half.
(rule 3 (extend val (ExtendOp.Zero) (fits_in_64 from_ty) $I128)
  (let ((val XReg (value_regs_get val 0))
        (low XReg (zext val from_ty $I64))
        (high XReg (load_u64_constant 0)))
    (value_regs low high)))

;; Catch all rule for ignoring extensions of the same type.
(rule 4 (extend val _ ty ty) val)



(decl lower_b128_binary (AluOPRRR ValueRegs ValueRegs) ValueRegs)
(rule
  (lower_b128_binary op a b)
  (let
    ( ;; low part.
      (low XReg (alu_rrr op (value_regs_get a 0) (value_regs_get b 0)))
      ;; high part.
      (high XReg (alu_rrr op (value_regs_get a 1) (value_regs_get b 1))))
    (value_regs low high)))

(decl lower_umlhi (Type XReg XReg) XReg)
(rule 1 (lower_umlhi $I64 rs1 rs2)
  (rv_mulhu rs1 rs2))

; (rule (lower_umlhi ty rs1 rs2)
;   (let
;     ((tmp XReg (rv_mul (zext rs1 ty $I64) (zext rs2 ty $I64))))
;     (rv_srli tmp (imm12_const (ty_bits ty)))))

(decl lower_smlhi (Type XReg XReg) XReg)
(rule 1
  (lower_smlhi $I64 rs1 rs2)
  (rv_mulh rs1 rs2))

; (rule
;   (lower_smlhi ty rs1 rs2)
;   (let
;     ((tmp XReg (rv_mul rs1 rs2)))
;     (rv_srli tmp (imm12_const (ty_bits ty)))))


(decl lower_rotl (Type XReg XReg) XReg)

(rule
  (lower_rotl $I64 rs amount)
  (lower_rotl_shift $I64 rs amount))

(rule
  (lower_rotl $I32 rs amount)
  (lower_rotl_shift $I32 rs amount))

(rule -1
  (lower_rotl ty rs amount)
  (lower_rotl_shift ty rs amount))

;;; using shift to implement rotl.
(decl lower_rotl_shift (Type XReg XReg) XReg)

;;; for I8 and I16 ...
(rule
  (lower_rotl_shift ty rs amount)
  (let
    ((x ValueRegs (gen_shamt ty amount))
      (shamt Reg (value_regs_get x 0))
      (len_sub_shamt Reg (value_regs_get x 1))
      ;;
      (part1 Reg (rv_sll rs shamt))
      ;;
      (part2 Reg (rv_srl rs len_sub_shamt))
      (part3 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) part2)))
    (rv_or part1 part3)))


;;;; construct shift amount.rotl on i128 will use shift to implement. So can call this function.
;;;; this will return shift amount and (ty_bits - "shift amount")
;;;; if ty_bits is greater than 64 like i128, then shmat will fallback to 64.because We are 64 bit platform.
(decl gen_shamt (Type XReg) ValueRegs)
(extern constructor gen_shamt gen_shamt)

(decl lower_rotr (Type XReg XReg) XReg)

(rule
  (lower_rotr $I64 rs amount)
  (lower_rotr_shift $I64 rs amount))

(rule
  (lower_rotr $I32 rs amount)
  (lower_rotr_shift $I32 rs amount))

(rule -1
  (lower_rotr ty rs amount)
  (lower_rotr_shift ty rs amount))

(decl lower_rotr_shift (Type XReg XReg) XReg)

;;;
(rule
  (lower_rotr_shift ty rs amount)
  (let
    ((x ValueRegs (gen_shamt ty amount))
      (shamt XReg (value_regs_get x 0))
      (len_sub_shamt XReg (value_regs_get x 1))
      ;;
      (part1 XReg (rv_srl rs shamt))
      ;;
      (part2 XReg (rv_sll rs len_sub_shamt))
      ;;
      (part3 XReg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) part2)))
    (rv_or part1 part3)))



;; bseti: Set a single bit in a register, indexed by a constant.
(decl gen_bseti (Reg u64) Reg)
(rule (gen_bseti val bit)
  (if-let $false (u64_le bit 12))
  (let ((const XReg (load_u64_constant (u64_shl 1 bit))))
    (rv_or val const)))

(decl gen_popcnt (Reg Type) Reg)
(rule
  (gen_popcnt rs ty)
  (let
    ((tmp WritableXReg (temp_writable_xreg))
      (step WritableXReg (temp_writable_xreg))
      (sum WritableXReg (temp_writable_xreg))
      (_ Unit (emit (MInst.Popcnt sum step tmp rs ty))))
    (writable_reg_to_reg sum)))

;; Generates a AMode that points to a register plus an offset.
(decl gen_reg_offset_amode (Reg i64 Type) AMode)
(extern constructor gen_reg_offset_amode gen_reg_offset_amode)

;; Generates a AMode that an offset from the stack pointer.
(decl gen_sp_offset_amode (i64 Type) AMode)
(extern constructor gen_sp_offset_amode gen_sp_offset_amode)

;; Generates a AMode that an offset from the frame pointer.
(decl gen_fp_offset_amode (i64 Type) AMode)
(extern constructor gen_fp_offset_amode gen_fp_offset_amode)

;; Generates a AMode that an access to a global variable at given index.
(decl gen_global_amode (i64 Type) AMode)
(extern constructor gen_global_amode gen_global_amode)

;; Generates an AMode that points to a stack slot + offset.
(decl gen_stack_slot_amode (StackSlot i64 Type) AMode)
(extern constructor gen_stack_slot_amode gen_stack_slot_amode)

;; Generates a AMode that points to a constant in the constant pool.
(decl gen_const_amode (VCodeConstant) AMode)
(extern constructor gen_const_amode gen_const_amode)

;; Tries to match a Value + Offset into an AMode
(decl amode (Value i32 Type) AMode)
(rule 0 (amode addr offset ty) (amode_inner addr offset ty))

;; If we are adding a constant offset with an iadd we can instead make that
;; offset part of the amode offset.
;;
;; We can't recurse into `amode` again since that could cause stack overflows.
;; See: https://github.com/bytecodealliance/wasmtime/pull/6968
(rule 1 (amode (iadd addr (iconst (simm32 y))) offset ty)
  (if-let new_offset (s32_add_fallible y offset))
  (amode_inner addr new_offset ty))
(rule 2 (amode (iadd (iconst (simm32 x)) addr) offset ty)
  (if-let new_offset (s32_add_fallible x offset))
  (amode_inner addr new_offset ty))


;; These are the normal rules for generating an AMode.
(decl amode_inner (Value i32 Type) AMode)

;; In the simplest case we just lower into a Reg+Offset
(rule 0 (amode_inner r @ (value_type (ty_addr64 _)) offset ty)
  (gen_reg_offset_amode r offset ty))

;; If the value is a `get_frame_pointer`, we can just use the offset from that.
(rule 1 (amode_inner (get_frame_pointer) offset ty)
  (gen_fp_offset_amode offset ty))

;; If the value is a `get_stack_pointer`, we can just use the offset from that.
(rule 1 (amode_inner (get_stack_pointer) offset ty)
  (gen_sp_offset_amode offset ty))

(rule 1 (amode_inner (symbol_value (zkasm_base ZkasmBase.Global)) index ty)
  (gen_global_amode index ty))

;; Similarly if the value is a `stack_addr` we can also turn that into an sp offset.
(rule 1 (amode_inner (stack_addr ss ss_offset) amode_offset ty)
  (if-let combined_offset (s32_add_fallible ss_offset amode_offset))
  (gen_stack_slot_amode ss combined_offset ty))

;; Returns a canonical type for a LoadOP. We only return I64 or F64.
(decl load_op_reg_type (LoadOP) Type)
(rule 1 (load_op_reg_type (LoadOP.Fld)) $F64)
(rule 1 (load_op_reg_type (LoadOP.Flw)) $F64)
(rule 0 (load_op_reg_type _) $I64)

;; helper function to load from memory.
(decl gen_load (AMode LoadOP MemFlags) Reg)
(rule (gen_load amode op flags)
  (let ((dst WritableReg (temp_writable_reg (load_op_reg_type op)))
      (_ Unit (emit (MInst.Load dst op flags amode))))
    dst))

(decl default_memflags () MemFlags)
(extern constructor default_memflags default_memflags)

(decl offset32_add (Offset32 i64) Offset32)
(extern constructor offset32_add offset32_add)

;; helper function to store to memory.
(decl gen_store (AMode StoreOP MemFlags Reg) InstOutput)
(rule (gen_store amode op flags src)
  (side_effect (SideEffectNoResult.Inst (MInst.Store amode op flags src))))

(decl valid_atomic_transaction (Type) Type)
(extern extractor valid_atomic_transaction valid_atomic_transaction)

(decl gen_stack_addr (StackSlot Offset32) Reg)
(extern constructor gen_stack_addr gen_stack_addr)

;;
(decl gen_select (Type Reg ValueRegs ValueRegs) ValueRegs)
(rule
  (gen_select ty c x y)
  (let
    ((dst VecWritableReg (alloc_vec_writable ty))
      ;;
      (reuslt VecWritableReg (vec_writable_clone dst))
      (_ Unit (emit (MInst.Select dst ty c x y))))
    (vec_writable_to_regs reuslt)))

;; Parameters are "intcc compare_a compare_b rs1 rs2".
(decl gen_select_reg (IntCC XReg XReg Reg Reg) Reg)
(extern constructor gen_select_reg gen_select_reg)

;; load a constant into reg.
(decl load_u64_constant (u64) Reg)
(extern constructor load_u64_constant load_u64_constant)

;;; clone WritableReg
;;; if not rust compiler will complain about use moved value.
(decl vec_writable_clone (VecWritableReg) VecWritableReg)
(extern constructor vec_writable_clone vec_writable_clone)

(decl vec_writable_to_regs (VecWritableReg) ValueRegs)
(extern constructor vec_writable_to_regs vec_writable_to_regs)

(decl alloc_vec_writable (Type) VecWritableReg)
(extern constructor alloc_vec_writable alloc_vec_writable)

(decl gen_int_select (Type IntSelectOP ValueRegs ValueRegs) ValueRegs)
(rule
  (gen_int_select ty op x y)
  (let
    ( ;;;
      (dst VecWritableReg (alloc_vec_writable ty))
      ;;;
      (_ Unit (emit (MInst.IntSelect op (vec_writable_clone dst) x y ty))))
    (vec_writable_to_regs dst)))

(decl udf (TrapCode) InstOutput)
(rule
  (udf code)
  (side_effect (SideEffectNoResult.Inst (MInst.Udf code))))

(decl load_op (Type) LoadOP)
(extern constructor load_op load_op)

(decl store_op (Type) StoreOP)
(extern constructor store_op store_op)

(decl zkasm_base (ZkasmBase) GlobalValue)
(extern extractor zkasm_base zkasm_base)

;;;; load extern name
(decl load_ext_name (ExternalName i64) Reg)
(extern constructor load_ext_name load_ext_name)

;;; lower icmp
(decl lower_icmp (IntCC ValueRegs ValueRegs Type) Reg)
(rule 1 (lower_icmp cc x y ty)
  (if (signed_cond_code cc))
  (gen_icmp cc (ext_int_if_need $true x ty) (ext_int_if_need $true y ty) ty))
(rule (lower_icmp cc x y ty)
  (gen_icmp cc (ext_int_if_need $false x ty) (ext_int_if_need $false y ty) ty))


(decl i128_sub (ValueRegs ValueRegs) ValueRegs)
(rule
  (i128_sub x y )
  (let
    (;; low part.
      (low XReg (rv_sub (value_regs_get x 0) (value_regs_get y 0)))
      ;; compute borrow.
      (borrow XReg (rv_sltu (value_regs_get x 0) low))
      ;;
      (high_tmp XReg (rv_sub (value_regs_get x 1) (value_regs_get y 1)))
      ;;
      (high XReg (rv_sub high_tmp borrow)))
    (value_regs low high)))


;;; Returns the sum in the first register, and the overflow test in the second.
(decl lower_uadd_overflow (XReg XReg Type) ValueRegs)

(rule 1
  (lower_uadd_overflow x y $I64)
  (let ((tmp XReg (rv_add x y))
        (test XReg (gen_icmp (IntCC.UnsignedLessThan) tmp x $I64)))
    (value_regs tmp test)))

; (rule
;   (lower_uadd_overflow x y (fits_in_32 ty))
;   (let ((tmp_x XReg (zext x ty $I64))
;         (tmp_y XReg (zext y ty $I64))
;         (sum XReg (rv_add tmp_x tmp_y))
;         (test XReg (rv_srli sum (imm12_const (ty_bits ty)))))
;     (value_regs sum test)))

(decl label_to_br_target (MachLabel) BranchTarget)
(extern constructor label_to_br_target label_to_br_target)

(decl gen_jump (MachLabel) MInst)
(rule
  (gen_jump v)
  (MInst.Jal (label_to_br_target v)))

(decl vec_label_get (VecMachLabel u8) MachLabel )
(extern constructor vec_label_get vec_label_get)

(decl partial lower_branch (Inst VecMachLabel) Unit)
(rule (lower_branch (jump _) targets )
      (emit_side_effect (SideEffectNoResult.Inst (gen_jump (vec_label_get targets 0)))))

;;; cc a b targets Type
(decl lower_br_icmp (IntCC ValueRegs ValueRegs VecMachLabel Type) Unit)
(extern constructor lower_br_icmp lower_br_icmp)

;; int scalar zero regs.
(decl int_zero_reg (Type) ValueRegs)
(extern constructor int_zero_reg int_zero_reg)

(decl lower_cond_br (IntCC ValueRegs VecMachLabel Type) Unit)
(extern constructor lower_cond_br lower_cond_br)

(decl intcc_to_extend_op (IntCC) ExtendOp)
(extern constructor intcc_to_extend_op intcc_to_extend_op)

;; Normalize a value for comparision.
;;
;; This ensures that types smaller than a register don't accidentally
;; pass undefined high bits when being compared as a full register.
(decl normalize_cmp_value (Type ValueRegs ExtendOp) ValueRegs)

(rule 1 (normalize_cmp_value (fits_in_32 ity) r op)
      (extend r op ity $I64))

(rule (normalize_cmp_value $I64  r _) r)

(decl normalize_fcvt_from_int (XReg Type ExtendOp) XReg)
(rule 2 (normalize_fcvt_from_int r (fits_in_16 ty) op)
  (value_regs_get (extend r op ty $I64) 0))
(rule 1 (normalize_fcvt_from_int r _ _)
  r)

;; Convert a truthy value, possibly of more than one register (an
;; I128), to one register. If narrower than 64 bits, must have already
;; been masked (e.g. by `normalize_cmp_value`).
(decl truthy_to_reg (Type ValueRegs) XReg)
(rule 1 (truthy_to_reg (fits_in_64 _) regs)
      (value_regs_get regs 0))

;; Default behavior for branching based on an input value.
(rule
  (lower_branch (brif v @ (value_type ty) _ _) targets)
  (lower_cond_br (IntCC.NotEqual) (normalize_cmp_value ty v (ExtendOp.Zero)) targets ty))


;; Branching on the result of an icmp
(rule 1
  (lower_branch (brif (maybe_uextend (icmp cc a @ (value_type ty) b)) _ _) targets)
  (lower_br_icmp cc a b targets ty))

;;;
(decl lower_br_table (Reg VecMachLabel) Unit)
(extern constructor lower_br_table lower_br_table)

(rule
  (lower_branch (br_table index _) targets)
  (lower_br_table index targets))

(decl load_ra () Reg)
(extern constructor load_ra load_ra)


;; Generates a bitcast instruction.
;; Args are: src, src_ty, dst_ty
(decl gen_bitcast (Reg Type Type) Reg)
(rule (gen_bitcast r _ _) r)

;; Selects the greatest of two registers as signed values.
(decl max (Type XReg XReg) XReg)

(rule (max (fits_in_64 (ty_int ty)) x y)
  (gen_select_reg (IntCC.SignedGreaterThan) x y x y))


(decl gen_trapif (XReg TrapCode) InstOutput)
(rule
  (gen_trapif test trap_code)
  (side_effect (SideEffectNoResult.Inst (MInst.TrapIf test trap_code))))

(decl gen_trapifc (IntCC XReg XReg TrapCode) InstOutput)
(rule
  (gen_trapifc cc a b trap_code)
  (side_effect (SideEffectNoResult.Inst (MInst.TrapIfC a b cc trap_code))))

(decl shift_int_to_most_significant (XReg Type) XReg)
(extern constructor shift_int_to_most_significant shift_int_to_most_significant)

;;; generate div overflow.
; (decl gen_div_overflow (XReg XReg Type) InstOutput)
; (rule
;   (gen_div_overflow rs1 rs2 ty)
;   (let
;     ((r_const_neg_1 XReg (load_imm12 -1))
;       (r_const_min XReg (rv_slli (load_imm12 1) (imm12_const 63)))
;       (tmp_rs1 XReg (shift_int_to_most_significant rs1 ty))
;       (t1 XReg (gen_icmp (IntCC.Equal) r_const_neg_1 rs2 ty))
;       (t2 XReg (gen_icmp (IntCC.Equal) r_const_min tmp_rs1 ty))
;       (test XReg (rv_and t1 t2)))
;     (gen_trapif test (TrapCode.IntegerOverflow))))

(decl gen_div_by_zero (XReg) InstOutput)
(rule
  (gen_div_by_zero r)
  (gen_trapifc (IntCC.Equal) (zero_reg) r (TrapCode.IntegerDivisionByZero)))

;;;; Helpers for Emitting Calls ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(decl gen_call (SigRef ExternalName RelocDistance ValueSlice) InstOutput)
(extern constructor gen_call gen_call)

(decl gen_call_indirect (SigRef Value ValueSlice) InstOutput)
(extern constructor gen_call_indirect gen_call_indirect)

;;; this is trying to imitate aarch64 `madd` instruction.
(decl madd (XReg XReg XReg) XReg)
(rule
  (madd n m a)
  (let
    ((t XReg (zk_mul n m)))
    (rv_add t a)))

;;;; Helpers for physical registers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(decl gen_mov_from_preg (PReg) Reg)

(rule
  (gen_mov_from_preg rm)
  (let ((rd WritableXReg (temp_writable_xreg))
        (_ Unit (emit (MInst.MovFromPReg rd rm))))
    rd))

(decl fp_reg () PReg)
(extern constructor fp_reg fp_reg)

(decl sp_reg () PReg)
(extern constructor sp_reg sp_reg)

;; Helper for creating the zero register.
(decl zero_reg () Reg)
(extern constructor zero_reg zero_reg)

(decl value_regs_zero () ValueRegs)
(rule (value_regs_zero)
  (value_regs (imm $I64 0) (imm $I64 0)))

(decl writable_zero_reg () WritableReg)
(extern constructor writable_zero_reg writable_zero_reg)


;;;; Helpers for floating point comparisons ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; (decl not (XReg) XReg)
; (rule (not x) (rv_xori x (imm_from_bits 1)))

(type CmpResult (enum
                  (Result
                    (result XReg)
                    (invert bool))))

;; Wrapper for the common case when constructing comparison results. It assumes
;; that the result isn't negated.
(decl cmp_result (XReg) CmpResult)
(rule (cmp_result result) (CmpResult.Result result $false))

;; Wrapper for the case where it's more convenient to construct the negated
;; version of the comparison.
(decl cmp_result_invert (XReg) CmpResult)
(rule (cmp_result_invert result) (CmpResult.Result result $true))

;; Consume a CmpResult, producing a branch on its result.
(decl cond_br (CmpResult BranchTarget BranchTarget) SideEffectNoResult)
(rule (cond_br cmp then else)
      (SideEffectNoResult.Inst
        (MInst.CondBr then else (cmp_integer_compare cmp))))

;; Construct an IntegerCompare value.
(decl int_compare (IntCC XReg XReg) IntegerCompare)
(extern constructor int_compare int_compare)

;; Convert a comparison into a branch test.
(decl cmp_integer_compare (CmpResult) IntegerCompare)

(rule
  (cmp_integer_compare (CmpResult.Result res $false))
  (int_compare (IntCC.NotEqual) res (zero_reg)))

(rule
  (cmp_integer_compare (CmpResult.Result res $true))
  (int_compare (IntCC.Equal) res (zero_reg)))