jon.recoil.org

Module Ast.Instruction_name

The 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 =
  1. | 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
  2. | 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 ] ] ]) t
    (*

    Note: It is claimed that a W-form of ADDS exists but is not modelled here.

    *)
  3. | 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
  4. | 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 ] ] ]) t
    (*

    Note: It is claimed that a W-form of ADD_immediate exists but is not modelled here.

    *)
  5. | 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
  6. | 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
  7. | 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
  8. | ADR : (pair, [ `Reg of [ `GP of [ `X ] ] ] * [ `Imm of [ `Sym of [ `Nineteen ] ] ]) t
  9. | ADRP : (pair, [ `Reg of [ `GP of [ `X ] ] ] * [ `Imm of [ `Sym of [ `Twenty_one ] ] ]) t
    (*

    Note: 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).

    *)
  10. | AND_immediate : (triple, [ `Reg of [ `GP of [< `X ] ] ] * [ `Reg of [ `GP of [< `X ] ] ] * [< `Bitmask ]) t
  11. | 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
  12. | 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
  13. | ASRV : (triple, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  14. | B : (singleton, [ `Imm of [ `Sym of _ ] ]) t
  15. | BL : (singleton, [ `Imm of [ `Sym of _ ] ]) t
  16. | BLR : (singleton, [ `Reg of [ `GP of [ `X ] ] ]) t
  17. | BR : (singleton, [ `Reg of [ `GP of [ `X ] ] ]) t
  18. | B_cond : Branch_cond.t -> (singleton, [ `Imm of [ `Sym of _ ] ]) t
  19. | CBNZ : (pair, [ `Reg of [ `GP of [< `X | `W ] ] ] * [ `Imm of [ `Sym of _ ] ]) t
  20. | CBZ : (pair, [ `Reg of [ `GP of [< `X | `W ] ] ] * [ `Imm of [ `Sym of _ ] ]) t
  21. | CLZ : (pair, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  22. | 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
  23. | 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
  24. | CNT : (pair, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  25. | 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
  26. | CSEL : (quad, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ] * [ `Reg of [ `GP of 'w ] ] * [ `Cond ]) t
  27. | 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
  28. | CTZ : (pair, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  29. | DMB : Memory_barrier.t -> (singleton, unit) t
  30. | DSB : Memory_barrier.t -> (singleton, unit) t
  31. | 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 ] ] ]) t
    (*

    Note: 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).

    *)
  32. | EOR_immediate : (triple, [ `Reg of [ `GP of [< `X ] ] ] * [ `Reg of [ `GP of [< `X ] ] ] * [< `Bitmask ]) t
  33. | 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
  34. | 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
  35. | 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
  36. | FABS : (pair, [ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ] * [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]) t
  37. | 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
  38. | 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
  39. | 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
  40. | FCMP : (pair, [ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ] * [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]) t
  41. | 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
  42. | 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
  43. | 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
  44. | FCVT : (pair, [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ] * [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ]) t
  45. | FCVTL_vector : (pair, [ `Reg of [ `Neon of [ `Vector of [ `V2D ] * [ `D ] ] ] ] * [ `Reg of [ `Neon of [ `Vector of [< `V2S | `V4S ] * [ `S ] ] ] ]) t
    (*

    Note: It is claimed that a W destination form of FCVTNS exists but is not modelled here.

    *)
  46. | FCVTNS : (pair, [ `Reg of [ `GP of [< `X ] ] ] * [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ]) t
  47. | 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
  48. | FCVTN_vector : (pair, [ `Reg of [ `Neon of [ `Vector of [< `V2S | `V4S ] * [ `S ] ] ] ] * [ `Reg of [ `Neon of [ `Vector of [ `V2D ] * [ `D ] ] ] ]) t
    (*

    Note: It is claimed that a W destination form of FCVTZS exists but is not modelled here.

    *)
  49. | FCVTZS : (pair, [ `Reg of [ `GP of [< `X ] ] ] * [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ]) t
  50. | 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
  51. | 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
  52. | 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
  53. | 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
  54. | 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
  55. | 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
  56. | 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
  57. | 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
  58. | FMOV_fp : (pair, [ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ] * [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]) t
  59. | FMOV_gp_to_fp_32 : (pair, [ `Reg of [ `Neon of [ `Scalar of [ `S ] ] ] ] * [ `Reg of [ `GP of [< `W | `WZR ] ] ]) t
  60. | FMOV_gp_to_fp_64 : (pair, [ `Reg of [ `Neon of [ `Scalar of [ `D ] ] ] ] * [ `Reg of [ `GP of [< `X | `XZR ] ] ]) t
  61. | FMOV_fp_to_gp_32 : (pair, [ `Reg of [ `GP of [ `W ] ] ] * [ `Reg of [ `Neon of [< `Scalar of [< `S ] ] ] ]) t
  62. | FMOV_fp_to_gp_64 : (pair, [ `Reg of [ `GP of [ `X ] ] ] * [ `Reg of [ `Neon of [< `Scalar of [< `D ] ] ] ]) t
  63. | FMOV_scalar_immediate : (pair, [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ] * [ `Imm of [ `Sixty_four ] ]) t
  64. | 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
  65. | 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
  66. | 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
  67. | FNEG : (pair, [ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ] * [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]) t
  68. | 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
  69. | 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
  70. | 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
  71. | 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
  72. | 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
  73. | FRINT : Rounding_mode.t -> (pair, [ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ] * [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]) t
  74. | 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
  75. | 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
  76. | FSQRT : (pair, [ `Reg of [ `Neon of [ `Scalar of [< `S | `D ] as 'p ] ] ] * [ `Reg of [ `Neon of [ `Scalar of 'p ] ] ]) t
  77. | 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
  78. | 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
  79. | 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
  80. | 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
  81. | 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
  82. | LDAR : (pair, [ `Reg of [ `GP of [< `X | `W ] ] ] * [ `Mem of [ `Base_reg ] ]) t
  83. | 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
  84. | LDR : (pair, [ `Reg of [ `GP of [< `X | `W | `LR ] ] ] * [ `Mem of Addressing_mode.single ]) t
  85. | LDRB : (pair, [ `Reg of [ `GP of [< `W ] ] ] * [ `Mem of Addressing_mode.single ]) t
  86. | LDRH : (pair, [ `Reg of [ `GP of [< `W ] ] ] * [ `Mem of Addressing_mode.single ]) t
  87. | LDRSB : (pair, [ `Reg of [ `GP of [< `X ] ] ] * [ `Mem of Addressing_mode.single ]) t
  88. | LDRSH : (pair, [ `Reg of [ `GP of [< `X ] ] ] * [ `Mem of Addressing_mode.single ]) t
  89. | LDRSW : (pair, [ `Reg of [ `GP of [< `X ] ] ] * [ `Mem of Addressing_mode.single ]) t
  90. | LDR_simd_and_fp : (pair, [ `Reg of [ `Neon of [< `Scalar of [< `D | `S | `Q ] ] ] ] * [ `Mem of Addressing_mode.single ]) t
  91. | LSLV : (triple, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  92. | LSRV : (triple, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  93. | 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
  94. | MOVI : (pair, [ `Reg of [ `Neon of [< `Scalar of _ | `Vector of [< any_vector ] * [< any_width ] ] ] ] * [ `Imm of [< `Twelve ] ]) t
  95. | MOVK : (triple, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Imm of [ `Sixteen_unsigned ] ] * [ `Lsl_by_multiple_of_16_bits of 'w ]) t
  96. | 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
  97. | 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
  98. | 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
  99. | 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
  100. | 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
  101. | 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
  102. | NOP : (singleton, unit) t
    (*

    Note: 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).

    *)
  103. | ORR_immediate : (triple, [ `Reg of [ `GP of [< `X ] ] ] * [ `Reg of [ `GP of [< `X | `XZR ] ] ] * [< `Bitmask ]) t
  104. | 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
  105. | 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
  106. | RBIT : (pair, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  107. | RET : (singleton, unit) t
  108. | REV : (pair, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  109. | REV16 : (pair, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  110. | SBFM : (quad, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ] * [ `Imm of [ `Six ] ] * [ `Imm of [ `Six ] ]) t
    (*

    Note: It is claimed that a W source form of SCVTF exists but is not modelled here.

    *)
  111. | SCVTF : (pair, [ `Reg of [ `Neon of [< `Scalar of [< `S | `D ] ] ] ] * [ `Reg of [ `GP of [< `X ] ] ]) t
  112. | 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
  113. | SDIV : (triple, [ `Reg of [ `GP of [< `X | `W ] as 'w ] ] * [ `Reg of [ `GP of 'w ] ] * [ `Reg of [ `GP of 'w ] ]) t
  114. | 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
  115. | 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
  116. | 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
  117. | 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
  118. | SMULH : (triple, [ `Reg of [ `GP of [ `X ] ] ] * [ `Reg of [ `GP of [ `X ] ] ] * [ `Reg of [ `GP of [ `X ] ] ]) t
  119. | 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
  120. | 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
  121. | 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
  122. | 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
  123. | 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
  124. | 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
  125. | 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
  126. | 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
  127. | 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
  128. | STR : (pair, [ `Reg of [ `GP of [< `X | `W | `LR ] ] ] * [ `Mem of Addressing_mode.single ]) t
  129. | STRB : (pair, [ `Reg of [ `GP of [< `W ] ] ] * [ `Mem of Addressing_mode.single ]) t
  130. | STRH : (pair, [ `Reg of [ `GP of [< `W ] ] ] * [ `Mem of Addressing_mode.single ]) t
  131. | STR_simd_and_fp : (pair, [ `Reg of [ `Neon of [< `Scalar of [< `D | `S | `Q ] ] ] ] * [ `Mem of Addressing_mode.single ]) t
  132. | 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 ]) t
    (*

    Note: It is claimed that a W-form of SUBS_shifted_register exists but is not modelled here.

    *)
  133. | 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 ]) t
    (*

    Note: It is claimed that a W-form of SUB_immediate exists but is not modelled here.

    *)
  134. | 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
  135. | 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
  136. | 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
  137. | 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 ] ] ]) t
    (*

    Note: 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).

    *)
  138. | TBNZ : (triple, [ `Reg of [ `GP of [ `X ] ] ] * [ `Imm of [ `Six ] ] * [ `Imm of [ `Sym of _ ] ]) t
    (*

    Note: 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).

    *)
  139. | TBZ : (triple, [ `Reg of [ `GP of [ `X ] ] ] * [ `Imm of [ `Six ] ] * [ `Imm of [ `Sym of _ ] ]) t
  140. | TST : (pair, [ `Reg of [ `GP of [< `X ] ] ] * [< `Bitmask ]) t
  141. | 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
  142. | UBFM : (quad, [ `Reg of [ `GP of [< `X | `W ] ] ] * [ `Reg of [ `GP of [< `X | `W ] ] ] * [ `Imm of [ `Six ] ] * [ `Imm of [ `Six ] ]) t
  143. | 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
  144. | 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
  145. | 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
  146. | UMULH : (triple, [ `Reg of [ `GP of [ `X ] ] ] * [ `Reg of [ `GP of [ `X ] ] ] * [ `Reg of [ `GP of [ `X ] ] ]) t
  147. | 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
  148. | 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
  149. | 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
  150. | 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
  151. | 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
  152. | 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
  153. | 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
  154. | 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
  155. | 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
  156. | 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
  157. | 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
  158. | YIELD : (singleton, unit) t
  159. | 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
  160. | 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