Module Jasmin.Armv8a_instr_decl

type __ = Obj.t
module E : sig ... end
type armv8a_options = {
  1. has_shift : Shift_kind.shift_kind option;
  2. opts_size : Wsize.wsize;
}
val has_shift : armv8a_options -> Shift_kind.shift_kind option
val opts_size : armv8a_options -> Wsize.wsize
type is_armv8a_options =
  1. | Coq_is_Build_armv8a_options of Shift_kind.shift_kind option * (Shift_kind.shift_kind, Shift_kind.is_shift_kind) Std.Prelude.is_option * Wsize.wsize * Wsize.is_wsize
val armv8a_options_tag : armv8a_options -> BinNums.positive
val is_armv8a_options_inhab : armv8a_options -> is_armv8a_options
val is_armv8a_options_functor : armv8a_options -> is_armv8a_options -> is_armv8a_options
type box_armv8a_options_Build_armv8a_options = {
  1. coq_Box_armv8a_options_Build_armv8a_options_0 : Shift_kind.shift_kind option;
  2. coq_Box_armv8a_options_Build_armv8a_options_1 : Wsize.wsize;
}
val coq_Box_armv8a_options_Build_armv8a_options_0 : box_armv8a_options_Build_armv8a_options -> Shift_kind.shift_kind option
val coq_Box_armv8a_options_Build_armv8a_options_1 : box_armv8a_options_Build_armv8a_options -> Wsize.wsize
type armv8a_options_fields_t = box_armv8a_options_Build_armv8a_options
val armv8a_options_fields : armv8a_options -> armv8a_options_fields_t
val armv8a_options_construct : BinNums.positive -> box_armv8a_options_Build_armv8a_options -> armv8a_options option
val armv8a_options_eqb : armv8a_options -> armv8a_options -> bool
val armv8a_options_eqb_OK : armv8a_options -> armv8a_options -> Datatypes.reflect
val armv8a_options_eqb_OK_sumbool : armv8a_options -> armv8a_options -> bool
val eqTC_armv8a_options : armv8a_options Utils0.eqTypeC
val armv8a_options_eqType : Eqtype.Equality.coq_type
val default_opts : armv8a_options
val opts_at : Wsize.wsize -> armv8a_options
type armv8a_mnemonic =
  1. | ADD
  2. | ADDS
  3. | ADC
  4. | ADCS
  5. | SUB
  6. | SUBS
  7. | NEG
  8. | MUL
  9. | MADD
  10. | MSUB
  11. | SDIV
  12. | UDIV
  13. | AND
  14. | ORR
  15. | EOR
  16. | MVN
  17. | ASR
  18. | LSL
  19. | LSR
  20. | ROR
  21. | MOV
  22. | MOVN
  23. | MOVZ
  24. | MOVK
  25. | ADR
  26. | SXTB
  27. | SXTH
  28. | SXTW
  29. | UXTB
  30. | UXTH
  31. | UXTW
  32. | CMP
  33. | TST
  34. | CSEL
  35. | LDR
  36. | LDRB
  37. | LDRH
  38. | LDRSB
  39. | LDRSH
  40. | LDRSW
  41. | STR
  42. | STRB
  43. | STRH
val armv8a_mnemonic_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> armv8a_mnemonic -> 'a1
val armv8a_mnemonic_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> armv8a_mnemonic -> 'a1
type is_armv8a_mnemonic =
  1. | Coq_is_ADD
  2. | Coq_is_ADDS
  3. | Coq_is_ADC
  4. | Coq_is_ADCS
  5. | Coq_is_SUB
  6. | Coq_is_SUBS
  7. | Coq_is_NEG
  8. | Coq_is_MUL
  9. | Coq_is_MADD
  10. | Coq_is_MSUB
  11. | Coq_is_SDIV
  12. | Coq_is_UDIV
  13. | Coq_is_AND
  14. | Coq_is_ORR
  15. | Coq_is_EOR
  16. | Coq_is_MVN
  17. | Coq_is_ASR
  18. | Coq_is_LSL
  19. | Coq_is_LSR
  20. | Coq_is_ROR
  21. | Coq_is_MOV
  22. | Coq_is_MOVN
  23. | Coq_is_MOVZ
  24. | Coq_is_MOVK
  25. | Coq_is_ADR
  26. | Coq_is_SXTB
  27. | Coq_is_SXTH
  28. | Coq_is_SXTW
  29. | Coq_is_UXTB
  30. | Coq_is_UXTH
  31. | Coq_is_UXTW
  32. | Coq_is_CMP
  33. | Coq_is_TST
  34. | Coq_is_CSEL
  35. | Coq_is_LDR
  36. | Coq_is_LDRB
  37. | Coq_is_LDRH
  38. | Coq_is_LDRSB
  39. | Coq_is_LDRSH
  40. | Coq_is_LDRSW
  41. | Coq_is_STR
  42. | Coq_is_STRB
  43. | Coq_is_STRH
val is_armv8a_mnemonic_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> armv8a_mnemonic -> is_armv8a_mnemonic -> 'a1
val is_armv8a_mnemonic_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> armv8a_mnemonic -> is_armv8a_mnemonic -> 'a1
val armv8a_mnemonic_tag : armv8a_mnemonic -> BinNums.positive
val is_armv8a_mnemonic_inhab : armv8a_mnemonic -> is_armv8a_mnemonic
val is_armv8a_mnemonic_functor : armv8a_mnemonic -> is_armv8a_mnemonic -> is_armv8a_mnemonic
type box_armv8a_mnemonic_ADD =
  1. | Box_armv8a_mnemonic_ADD
type armv8a_mnemonic_fields_t = __
val armv8a_mnemonic_fields : armv8a_mnemonic -> armv8a_mnemonic_fields_t
val armv8a_mnemonic_construct : BinNums.positive -> armv8a_mnemonic_fields_t -> armv8a_mnemonic option
val armv8a_mnemonic_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> armv8a_mnemonic -> is_armv8a_mnemonic -> 'a1
val armv8a_mnemonic_eqb_fields : (armv8a_mnemonic -> armv8a_mnemonic -> bool) -> BinNums.positive -> armv8a_mnemonic_fields_t -> armv8a_mnemonic_fields_t -> bool
val armv8a_mnemonic_eqb : armv8a_mnemonic -> armv8a_mnemonic -> bool
val armv8a_mnemonic_eqb_OK : armv8a_mnemonic -> armv8a_mnemonic -> Datatypes.reflect
val armv8a_mnemonic_eqb_OK_sumbool : armv8a_mnemonic -> armv8a_mnemonic -> bool
val eqTC_armv8a_mnemonic : armv8a_mnemonic Utils0.eqTypeC
val armv8a_mnemonic_eqType : Eqtype.Equality.coq_type
val armv8a_mnemonics : armv8a_mnemonic list
val finTC_armv8a_mnemonic : armv8a_mnemonic Utils0.finTypeC
val armv8a_mnemonic_finType : Fintype.Finite.coq_type
val has_shift_mnemonics : armv8a_mnemonic list
val ror_shift_mnemonics : armv8a_mnemonic list
val shift_allowed : armv8a_mnemonic -> Shift_kind.shift_kind -> bool
val sized_mnemonics : armv8a_mnemonic list
val wsize_uload_mn : (Wsize.wsize * armv8a_mnemonic) list
val uload_mn_of_wsize : Wsize.wsize -> armv8a_mnemonic option
val wsize_sload_mn : (Wsize.wsize * armv8a_mnemonic) list
val sload_mn_of_wsize : Wsize.wsize -> armv8a_mnemonic option
val wsize_of_sload_mn : armv8a_mnemonic -> Wsize.wsize option
val wsize_of_narrow_load_mn : armv8a_mnemonic -> Wsize.wsize option
val wsize_store_mn : (Wsize.wsize * armv8a_mnemonic) list
val store_mn_of_wsize : Wsize.wsize -> armv8a_mnemonic option
val wsize_of_narrow_store_mn : armv8a_mnemonic -> Wsize.wsize option
val string_of_armv8a_mnemonic : armv8a_mnemonic -> string
type armv8a_asm_op =
  1. | ARMv8A_op of armv8a_mnemonic * armv8a_options
val armv8a_asm_op_rect : (armv8a_mnemonic -> armv8a_options -> 'a1) -> armv8a_asm_op -> 'a1
val armv8a_asm_op_rec : (armv8a_mnemonic -> armv8a_options -> 'a1) -> armv8a_asm_op -> 'a1
type is_armv8a_asm_op =
  1. | Coq_is_ARMv8A_op of armv8a_mnemonic * is_armv8a_mnemonic * armv8a_options * is_armv8a_options
val is_armv8a_asm_op_rect : (armv8a_mnemonic -> is_armv8a_mnemonic -> armv8a_options -> is_armv8a_options -> 'a1) -> armv8a_asm_op -> is_armv8a_asm_op -> 'a1
val is_armv8a_asm_op_rec : (armv8a_mnemonic -> is_armv8a_mnemonic -> armv8a_options -> is_armv8a_options -> 'a1) -> armv8a_asm_op -> is_armv8a_asm_op -> 'a1
val armv8a_asm_op_tag : armv8a_asm_op -> BinNums.positive
val is_armv8a_asm_op_inhab : armv8a_asm_op -> is_armv8a_asm_op
val is_armv8a_asm_op_functor : armv8a_asm_op -> is_armv8a_asm_op -> is_armv8a_asm_op
type box_armv8a_asm_op_ARMv8A_op = {
  1. coq_Box_armv8a_asm_op_ARMv8A_op_0 : armv8a_mnemonic;
  2. coq_Box_armv8a_asm_op_ARMv8A_op_1 : armv8a_options;
}
val coq_Box_armv8a_asm_op_ARMv8A_op_0 : box_armv8a_asm_op_ARMv8A_op -> armv8a_mnemonic
val coq_Box_armv8a_asm_op_ARMv8A_op_1 : box_armv8a_asm_op_ARMv8A_op -> armv8a_options
type armv8a_asm_op_fields_t = box_armv8a_asm_op_ARMv8A_op
val armv8a_asm_op_fields : armv8a_asm_op -> armv8a_asm_op_fields_t
val armv8a_asm_op_construct : BinNums.positive -> box_armv8a_asm_op_ARMv8A_op -> armv8a_asm_op option
val armv8a_asm_op_induction : (armv8a_mnemonic -> is_armv8a_mnemonic -> armv8a_options -> is_armv8a_options -> 'a1) -> armv8a_asm_op -> is_armv8a_asm_op -> 'a1
val armv8a_asm_op_eqb_fields : (armv8a_asm_op -> armv8a_asm_op -> bool) -> BinNums.positive -> box_armv8a_asm_op_ARMv8A_op -> box_armv8a_asm_op_ARMv8A_op -> bool
val armv8a_asm_op_eqb : armv8a_asm_op -> armv8a_asm_op -> bool
val armv8a_asm_op_eqb_OK : armv8a_asm_op -> armv8a_asm_op -> Datatypes.reflect
val armv8a_asm_op_eqb_OK_sumbool : armv8a_asm_op -> armv8a_asm_op -> bool
val eqTC_armv8a_asm_op : armv8a_asm_op Utils0.eqTypeC
val armv8a_asm_op_eqType : Eqtype.Equality.coq_type
val coq_NF_of_word : Wsize.wsize -> Word0.word -> bool
val coq_ZF_of_word : Wsize.wsize -> Word0.word -> bool
val nzcv_of_logop : Wsize.wsize -> Word0.word -> Sem_type.sem_tuple
val nzcv_w_of_logop : Wsize.wsize -> Word0.word -> Utils0.ltuple
val armv8a_ADD_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_ADDS_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_SUB_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_SUBS_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_ADC_semi : Wsize.wsize -> Word0.word -> Word0.word -> bool -> Sem_type.sem_tuple
val armv8a_ADCS_semi : Wsize.wsize -> Word0.word -> Word0.word -> bool -> Sem_type.sem_tuple
val armv8a_NEG_semi : Wsize.wsize -> Word0.word -> Sem_type.sem_tuple
val armv8a_MUL_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_SDIV_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_UDIV_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_MVN_semi : Wsize.wsize -> Word0.word -> Sem_type.sem_tuple
val armv8a_MOV_semi : Wsize.wsize -> Word0.word -> Sem_type.sem_tuple
val armv8a_MOVZ_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_MOVN_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_extend_semi : Wsize.wsize -> bool -> Wsize.wsize -> Word0.word -> Word0.word
val armv8a_ADR_semi : Word0.word -> Sem_type.sem_tuple
val armv8a_CMP_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_TST_semi : Wsize.wsize -> Word0.word -> Word0.word -> Sem_type.sem_tuple
val armv8a_CSEL_semi : Wsize.wsize -> Word0.word -> Word0.word -> bool -> Sem_type.sem_tuple
val armv8a_prim_string : (string * armv8a_asm_op Sopn.prim_constructor) list