Ast.Instruction_nameThe intention is that none of these are aliases. Expansions of instructions that are aliases are done by the "ins_*" functions below.
Names such as "ADD_immediate" are intended to correspond to the titles such as "ADD (immediate)" in the ARM Architecture Reference Manual.
type (_, _) t = | ABS_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| ADDP_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
tNote: It is claimed that a W-form of ADDS exists but is not modelled here.
*)| ADDS : (quad,
[ `Reg of [ `GP of [< `X | `XZR ] ] ]
* [ `Reg of [ `GP of [< `X | `SP ] ] ]
* [ `Imm of [< `Twelve ] ]
* [ `Optional of [ `Fixed_shift of [ `Lsl_by_twelve ] ] option ])
t| ADDV : (pair,
[ `Reg of [ `Neon of [< `Scalar of [< `B | `H | `S ] as 'w ] ] ]
* [ `Reg of
[ `Neon of
[ `Vector of
[< `V8B | `V16B | `V4H | `V8H | `V2S | `V4S ] * 'w ] ] ])
tNote: It is claimed that a W-form of ADD_immediate exists but is not modelled here.
*)| ADD_immediate : (quad,
[ `Reg of [ `GP of [< `X | `SP | `FP ] ] ]
* [ `Reg of [ `GP of [< `X | `SP | `FP ] ] ]
* [ `Imm of [< `Twelve | `Sym of [ `Twelve ] ] ]
* [ `Optional of
[ `Fixed_shift of [ `Lsl_by_twelve ] ] option ])
t| ADD_shifted_register : (quad,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Optional of
[ `Shift of [< `Lsl | `Lsr | `Asr ] * [ `Six ] ]
option ])
t| ADD_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| ADR : (pair,
[ `Reg of [ `GP of [ `X ] ] ] * [ `Imm of [ `Sym of [ `Nineteen ] ] ])
t| ADRP : (pair,
[ `Reg of [ `GP of [ `X ] ] ]
* [ `Imm of [ `Sym of [ `Twenty_one ] ] ])
tNote: A W-form of AND_immediate exists but is not modelled here. W-form logical immediates use a different bitmask encoding (N=0, 6-bit immr/imms) than X-form (N can be 0 or 1, different valid patterns).
*)| AND_immediate : (triple,
[ `Reg of [ `GP of [< `X ] ] ]
* [ `Reg of [ `GP of [< `X ] ] ]
* [< `Bitmask ])
t| AND_shifted_register : (quad,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Optional of
[ `Shift of [< `Lsl | `Lsr | `Asr ] * [ `Six ] ]
option ])
t| AND_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| ASRV : (triple,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ])
t| B : (singleton, [ `Imm of [ `Sym of _ ] ]) t| BL : (singleton, [ `Imm of [ `Sym of _ ] ]) t| BLR : (singleton, [ `Reg of [ `GP of [ `X ] ] ]) t| BR : (singleton, [ `Reg of [ `GP of [ `X ] ] ]) t| B_cond : Branch_cond.t -> (singleton, [ `Imm of [ `Sym of _ ] ]) t| CBNZ : (pair, [ `Reg of [ `GP of [< `X | `W ] ] ] * [ `Imm of [ `Sym of _ ] ])
t| CBZ : (pair, [ `Reg of [ `GP of [< `X | `W ] ] ] * [ `Imm of [ `Sym of _ ] ]) t| CLZ : (pair,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ])
t| CM_register : Simd_int_cmp.t -> (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v)
* ([< any_width ] as 'w) ] ] ]
* [ `Reg of
[ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of
[ `Neon of [ `Vector of 'v * 'w ] ] ])
t| CM_zero : Simd_int_cmp.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v)
* ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| CNT : (pair,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ])
t| CNT_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| CSEL : (quad,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Cond ])
t| CSINC : (quad,
[ `Reg of [ `GP of [< `X | `W | `XZR | `WZR ] ] ]
* [ `Reg of [ `GP of [< `X | `W | `XZR | `WZR ] ] ]
* [ `Reg of [ `GP of [< `X | `W | `XZR | `WZR ] ] ]
* [ `Cond ])
t| CTZ : (pair,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ])
t| DMB : Memory_barrier.t -> (singleton, unit) t| DSB : Memory_barrier.t -> (singleton, unit) t| DUP : Neon_reg_name.Lane_index.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v)
* ([< any_width ] as 'w) ] ] ]
* [ `Reg of
[ `Neon of [ `Vector of 'v * 'w ] ] ])
tNote: A W-form of EOR_immediate exists but is not modelled here. W-form logical immediates use a different bitmask encoding (N=0, 6-bit immr/imms) than X-form (N can be 0 or 1, different valid patterns).
*)| EOR_immediate : (triple,
[ `Reg of [ `GP of [< `X ] ] ]
* [ `Reg of [ `GP of [< `X ] ] ]
* [< `Bitmask ])
t| EOR_shifted_register : (quad,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Optional of
[ `Shift of [< `Lsl | `Lsr | `Asr ] * [ `Six ] ]
option ])
t| EOR_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| EXT : (quad,
[ `Reg of [ `Neon of [ `Vector of [ `V16B ] * [ `B ] ] ] ]
* [ `Reg of [ `Neon of [ `Vector of [ `V16B ] * [ `B ] ] ] ]
* [ `Reg of [ `Neon of [ `Vector of [ `V16B ] * [ `B ] ] ] ]
* [ `Imm of [ `Six ] ])
t| FABS : (pair,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FADD : (triple,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FADDP_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FADD_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FCMP : (pair,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FCM_register : Float_cond.t -> (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of
[ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of
[ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FCM_zero : Float_cond.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FCSEL : (quad,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Cond ])
t| FCVT : (pair,
[ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ]
* [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ])
t| FCVTL_vector : (pair,
[ `Reg of [ `Neon of [ `Vector of [ `V2D ] * [ `D ] ] ] ]
* [ `Reg of
[ `Neon of [ `Vector of [< `V2S | `V4S ] * [ `S ] ] ] ])
tNote: It is claimed that a W destination form of FCVTNS exists but is not modelled here.
*)| FCVTNS : (pair,
[ `Reg of [ `GP of [< `X ] ] ]
* [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ])
t| FCVTNS_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FCVTN_vector : (pair,
[ `Reg of
[ `Neon of [ `Vector of [< `V2S | `V4S ] * [ `S ] ] ] ]
* [ `Reg of [ `Neon of [ `Vector of [ `V2D ] * [ `D ] ] ] ])
tNote: It is claimed that a W destination form of FCVTZS exists but is not modelled here.
*)| FCVTZS : (pair,
[ `Reg of [ `GP of [< `X ] ] ]
* [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ])
t| FCVTZS_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FDIV : (triple,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FDIV_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FMADD : (quad,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FMAX : (triple,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FMAX_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FMIN : (triple,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FMIN_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FMOV_fp : (pair,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FMOV_gp_to_fp_32 : (pair,
[ `Reg of [ `Neon of [ `Scalar of [ `S ] ] ] ]
* [ `Reg of [ `GP of [< `W | `WZR ] ] ])
t| FMOV_gp_to_fp_64 : (pair,
[ `Reg of [ `Neon of [ `Scalar of [ `D ] ] ] ]
* [ `Reg of [ `GP of [< `X | `XZR ] ] ])
t| FMOV_fp_to_gp_32 : (pair,
[ `Reg of [ `GP of [ `W ] ] ]
* [ `Reg of [ `Neon of [< `Scalar of [< `S ] ] ] ])
t| FMOV_fp_to_gp_64 : (pair,
[ `Reg of [ `GP of [ `X ] ] ]
* [ `Reg of [ `Neon of [< `Scalar of [< `D ] ] ] ])
t| FMOV_scalar_immediate : (pair,
[ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ]
* [ `Imm of [ `Sixty_four ] ])
t| FMSUB : (quad,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FMUL : (triple,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FMUL_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FNEG : (pair,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FNEG_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FNMADD : (quad,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FNMSUB : (quad,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FNMUL : (triple,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FRECPE_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FRINT : Rounding_mode.t -> (pair,
[ `Reg of
[ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FRINT_vector : Rounding_mode.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of
[ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FRSQRTE_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FSQRT : (pair,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FSQRT_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| FSUB : (triple,
[ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]
* [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ])
t| FSUB_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V2S | `V4S | `V2D ] as 'v)
* ([< `S | `D ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| INS : ('elem, 'gp) Element_to_GP.t
* Neon_reg_name.Lane_index.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
[< any_vector ] * 'elem ] ] ]
* [ `Reg of [ `GP of 'gp ] ])
t| INS_V : Neon_reg_name.Lane_index.Src_and_dest.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
[< any_vector ]
* [<
any_width ] ] ] ]
* [ `Reg of
[ `Neon of
[ `Vector of
[<
any_vector ]
*
[<
any_width ] ] ] ])
t| LDAR : (pair, [ `Reg of [ `GP of [< `X | `W ] ] ] * [ `Mem of [ `Base_reg ] ])
t| LDP : ('w1, 'w2) LDP_STP_width.t -> (triple,
[ `Reg of [ `GP of 'w1 ] ]
* [ `Reg of [ `GP of 'w2 ] ]
* [ `Mem of
[ `Offset_pair
| `Pre_pair
| `Post_pair ] ])
t| LDR : (pair,
[ `Reg of [ `GP of [< `X | `W | `LR ] ] ]
* [ `Mem of Addressing_mode.single ])
t| LDRB : (pair,
[ `Reg of [ `GP of [< `W ] ] ] * [ `Mem of Addressing_mode.single ])
t| LDRH : (pair,
[ `Reg of [ `GP of [< `W ] ] ] * [ `Mem of Addressing_mode.single ])
t| LDRSB : (pair,
[ `Reg of [ `GP of [< `X ] ] ] * [ `Mem of Addressing_mode.single ])
t| LDRSH : (pair,
[ `Reg of [ `GP of [< `X ] ] ] * [ `Mem of Addressing_mode.single ])
t| LDRSW : (pair,
[ `Reg of [ `GP of [< `X ] ] ] * [ `Mem of Addressing_mode.single ])
t| LDR_simd_and_fp : (pair,
[ `Reg of [ `Neon of [< `Scalar of [< `D | `S | `Q ] ] ] ]
* [ `Mem of Addressing_mode.single ])
t| LSLV : (triple,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ])
t| LSRV : (triple,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ])
t| MADD : (quad,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of [< `X | `W | `XZR | `WZR ] ] ])
t| MOVI : (pair,
[ `Reg of
[ `Neon of
[< `Scalar of _
| `Vector of [< any_vector ] * [< any_width ] ] ] ]
* [ `Imm of [< `Twelve ] ])
t| MOVK : (triple,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Imm of [ `Sixteen_unsigned ] ]
* [ `Lsl_by_multiple_of_16_bits of 'w ])
t| MOVN : (triple,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Imm of [ `Sixteen_unsigned ] ]
* [ `Optional of [ `Lsl_by_multiple_of_16_bits of 'w ] option ])
t| MOVZ : (triple,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Imm of [ `Sixteen_unsigned ] ]
* [ `Optional of [ `Lsl_by_multiple_of_16_bits of 'w ] option ])
t| MSUB : (quad,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of [< `X | `W | `XZR | `WZR ] ] ])
t| MUL_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V8B | `V16B | `V4H | `V8H | `V2S | `V4S ] as 'v)
* ([< `B | `H | `S ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| MVN_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| NEG_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| NOP : (singleton, unit) tNote: A W-form of ORR_immediate exists but is not modelled here. W-form logical immediates use a different bitmask encoding (N=0, 6-bit immr/imms) than X-form (N can be 0 or 1, different valid patterns).
*)| ORR_immediate : (triple,
[ `Reg of [ `GP of [< `X ] ] ]
* [ `Reg of [ `GP of [< `X | `XZR ] ] ]
* [< `Bitmask ])
t| ORR_shifted_register : (quad,
[ `Reg of [ `GP of [< `X | `W | `XZR | `WZR ] ] ]
* [ `Reg of [ `GP of [< `X | `W | `XZR | `WZR ] ] ]
* [ `Reg of [ `GP of [< `X | `W | `XZR | `WZR ] ] ]
* [ `Optional of
[ `Shift of [< `Lsl | `Lsr | `Asr ] * [ `Six ] ]
option ])
t| ORR_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| RBIT : (pair,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ])
t| RET : (singleton, unit) t| REV : (pair,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ])
t| REV16 : (pair,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ])
t| SBFM : (quad,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Imm of [ `Six ] ]
* [ `Imm of [ `Six ] ])
tNote: It is claimed that a W source form of SCVTF exists but is not modelled here.
*)| SCVTF : (pair,
[ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ]
* [ `Reg of [ `GP of [< `X ] ] ])
t| SCVTF_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| SDIV : (triple,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ])
t| SHL : (triple,
[ `Reg of
[ `Neon of
[ `Vector of ([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Shift_by_element_width of 'w ])
t| SMAX_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V8B | `V16B | `V4H | `V8H | `V2S | `V4S ] as 'v)
* ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| SMIN_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V8B | `V16B | `V4H | `V8H | `V2S | `V4S ] as 'v)
* ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| SMOV : ('elem, 'gp) Smov_element_to_GP.t
* Neon_reg_name.Lane_index.t -> (pair,
[ `Reg of [ `GP of 'gp ] ]
* [ `Reg of
[ `Neon of
[ `Vector of
[< any_vector ] * 'elem ] ] ])
t| SMULH : (triple,
[ `Reg of [ `GP of [ `X ] ] ]
* [ `Reg of [ `GP of [ `X ] ] ]
* [ `Reg of [ `GP of [ `X ] ] ])
t| SMULL2_vector : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Widen_mul2.t ->
(triple,
[ `Reg of [ `Neon of [ `Vector of 'dst_arr * 'dst_w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'src_arr * 'src_w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'src_arr * 'src_w ] ] ])
t| SMULL_vector : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Widen_mul.t -> (triple,
[
`Reg of
[
`Neon of
[
`Vector of
'dst_arr
* 'dst_w ] ] ]
*
[
`Reg of
[
`Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ]
*
[
`Reg of
[
`Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| SQADD_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| SQSUB_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| SQXTN : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Narrow.t -> (pair,
[ `Reg of
[ `Neon of
[
`Vector of
'dst_arr
* 'dst_w ] ] ]
* [ `Reg of
[ `Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| SQXTN2 : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Narrow2.t -> (pair,
[ `Reg of
[ `Neon of
[
`Vector of
'dst_arr
* 'dst_w ] ] ]
* [ `Reg of
[
`Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| SSHL_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| SSHR : (triple,
[ `Reg of
[ `Neon of
[ `Vector of ([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Shift_by_element_width of 'w ])
t| STP : ('w1, 'w2) LDP_STP_width.t -> (triple,
[ `Reg of [ `GP of 'w1 ] ]
* [ `Reg of [ `GP of 'w2 ] ]
* [ `Mem of
[ `Offset_pair
| `Pre_pair
| `Post_pair ] ])
t| STR : (pair,
[ `Reg of [ `GP of [< `X | `W | `LR ] ] ]
* [ `Mem of Addressing_mode.single ])
t| STRB : (pair,
[ `Reg of [ `GP of [< `W ] ] ] * [ `Mem of Addressing_mode.single ])
t| STRH : (pair,
[ `Reg of [ `GP of [< `W ] ] ] * [ `Mem of Addressing_mode.single ])
t| STR_simd_and_fp : (pair,
[ `Reg of [ `Neon of [< `Scalar of [< `D | `S | `Q ] ] ] ]
* [ `Mem of Addressing_mode.single ])
t| SUBS_immediate : (quad,
[ `Reg of [ `GP of [< `W | `WZR | `X | `XZR ] ] ]
* [ `Reg of [ `GP of [< `W | `X | `SP ] ] ]
* [ `Imm of [< `Twelve ] ]
* [ `Optional of
[ `Fixed_shift of [ `Lsl_by_twelve ] ] option ])
tNote: It is claimed that a W-form of SUBS_shifted_register exists but is not modelled here.
*)| SUBS_shifted_register : (quad,
[ `Reg of [ `GP of [< `X | `XZR ] ] ]
* [ `Reg of [ `GP of [< `X | `SP ] ] ]
* [ `Reg of [ `GP of [< `X ] ] ]
* [ `Optional of
[ `Shift of [< `Lsl | `Lsr | `Asr ] * [ `Six ] ]
option ])
tNote: It is claimed that a W-form of SUB_immediate exists but is not modelled here.
*)| SUB_immediate : (quad,
[ `Reg of [ `GP of [< `X | `SP ] ] ]
* [ `Reg of [ `GP of [< `X | `SP ] ] ]
* [ `Imm of [< `Twelve ] ]
* [ `Optional of
[ `Fixed_shift of [ `Lsl_by_twelve ] ] option ])
t| SUB_shifted_register : (quad,
[ `Reg of [ `GP of [< `X | `W ] as 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Reg of [ `GP of 'w ] ]
* [ `Optional of
[ `Shift of [< `Lsl | `Lsr | `Asr ] * [ `Six ] ]
option ])
t| SUB_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| SXTL : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Widen.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
'dst_arr
* 'dst_w ] ] ]
* [ `Reg of
[ `Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
tNote: A W-form of TBNZ exists (with bit positions 0-31) but is not modelled here. Currently uses generic 6-bit immediate; when W-form is added, the bit position should be width-dependent (0-31 for W, 0-63 for X).
*)| TBNZ : (triple,
[ `Reg of [ `GP of [ `X ] ] ]
* [ `Imm of [ `Six ] ]
* [ `Imm of [ `Sym of _ ] ])
tNote: A W-form of TBZ exists (with bit positions 0-31) but is not modelled here. Currently uses generic 6-bit immediate; when W-form is added, the bit position should be width-dependent (0-31 for W, 0-63 for X).
*)| TBZ : (triple,
[ `Reg of [ `GP of [ `X ] ] ]
* [ `Imm of [ `Six ] ]
* [ `Imm of [ `Sym of _ ] ])
t| TST : (pair, [ `Reg of [ `GP of [< `X ] ] ] * [< `Bitmask ]) t| UADDLP_vector : (pair,
[ `Reg of
[ `Neon of
[ `Vector of
[< `V4H | `V8H | `V2S | `V4S | `V1D | `V2D ]
* [< any_width ] ] ] ]
* [ `Reg of
[ `Neon of
[ `Vector of
[< `V8B | `V16B | `V4H | `V8H | `V2S | `V4S ]
* [< any_width ] ] ] ])
t| UBFM : (quad,
[ `Reg of [ `GP of [< `X | `W ] ] ]
* [ `Reg of [ `GP of [< `X | `W ] ] ]
* [ `Imm of [ `Six ] ]
* [ `Imm of [ `Six ] ])
t| UMAX_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V8B | `V16B | `V4H | `V8H | `V2S | `V4S ] as 'v)
* ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| UMIN_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< `V8B | `V16B | `V4H | `V8H | `V2S | `V4S ] as 'v)
* ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| UMOV : ('elem, 'gp) Element_to_GP.t
* Neon_reg_name.Lane_index.t -> (pair,
[ `Reg of [ `GP of 'gp ] ]
* [ `Reg of
[ `Neon of
[ `Vector of
[< any_vector ] * 'elem ] ] ])
t| UMULH : (triple,
[ `Reg of [ `GP of [ `X ] ] ]
* [ `Reg of [ `GP of [ `X ] ] ]
* [ `Reg of [ `GP of [ `X ] ] ])
t| UMULL2_vector : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Widen_mul2.t ->
(triple,
[ `Reg of [ `Neon of [ `Vector of 'dst_arr * 'dst_w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'src_arr * 'src_w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'src_arr * 'src_w ] ] ])
t| UMULL_vector : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Widen_mul.t -> (triple,
[
`Reg of
[
`Neon of
[
`Vector of
'dst_arr
* 'dst_w ] ] ]
*
[
`Reg of
[
`Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ]
*
[
`Reg of
[
`Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| UQADD_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| UQSUB_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| UQXTN : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Narrow.t -> (pair,
[ `Reg of
[ `Neon of
[
`Vector of
'dst_arr
* 'dst_w ] ] ]
* [ `Reg of
[ `Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| UQXTN2 : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Narrow2.t -> (pair,
[ `Reg of
[ `Neon of
[
`Vector of
'dst_arr
* 'dst_w ] ] ]
* [ `Reg of
[
`Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| USHL_vector : (triple,
[ `Reg of
[ `Neon of
[ `Vector of
([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| USHR : (triple,
[ `Reg of
[ `Neon of
[ `Vector of ([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Shift_by_element_width of 'w ])
t| UXTL : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Widen.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
'dst_arr
* 'dst_w ] ] ]
* [ `Reg of
[ `Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| XTN : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Narrow.t -> (pair,
[ `Reg of
[ `Neon of
[ `Vector of
'dst_arr
* 'dst_w ] ] ]
* [ `Reg of
[ `Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| XTN2 : ('src_arr, 'src_w, 'dst_arr, 'dst_w) Narrow2.t -> (pair,
[ `Reg of
[ `Neon of
[
`Vector of
'dst_arr
* 'dst_w ] ] ]
* [ `Reg of
[ `Neon of
[
`Vector of
'src_arr
* 'src_w ] ] ])
t| YIELD : (singleton, unit) t| ZIP1 : (triple,
[ `Reg of
[ `Neon of
[ `Vector of ([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t| ZIP2 : (triple,
[ `Reg of
[ `Neon of
[ `Vector of ([< any_vector ] as 'v) * ([< any_width ] as 'w) ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ]
* [ `Reg of [ `Neon of [ `Vector of 'v * 'w ] ] ])
t