package jasmin

  1. Overview
  2. Docs
Compiler for High-Assurance and High-Speed Cryptography

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (17)

Authors

  1. J
    Jasmin authors and contributors

Maintainers

  1. J
    Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Sources

jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa

doc/jasmin.jasmin/Jasmin/Arm_instr_decl/index.html

Module Jasmin.Arm_instr_decl

type __ = Obj.t
module E : sig ... end
type arm_options = {
  1. set_flags : bool;
  2. is_conditional : bool;
  3. has_shift : Shift_kind.shift_kind option;
}
val set_flags : arm_options -> bool
val is_conditional : arm_options -> bool
val has_shift : arm_options -> Shift_kind.shift_kind option
val arm_options_tag : arm_options -> BinNums.positive
val is_arm_options_inhab : arm_options -> is_arm_options
val is_arm_options_functor : arm_options -> is_arm_options -> is_arm_options
type box_arm_options_Build_arm_options = {
  1. coq_Box_arm_options_Build_arm_options_0 : bool;
  2. coq_Box_arm_options_Build_arm_options_1 : bool;
  3. coq_Box_arm_options_Build_arm_options_2 : Shift_kind.shift_kind option;
}
val coq_Box_arm_options_Build_arm_options_0 : box_arm_options_Build_arm_options -> bool
val coq_Box_arm_options_Build_arm_options_1 : box_arm_options_Build_arm_options -> bool
val coq_Box_arm_options_Build_arm_options_2 : box_arm_options_Build_arm_options -> Shift_kind.shift_kind option
type arm_options_fields_t = box_arm_options_Build_arm_options
val arm_options_fields : arm_options -> arm_options_fields_t
val arm_options_construct : BinNums.positive -> box_arm_options_Build_arm_options -> arm_options option
val arm_options_eqb : arm_options -> arm_options -> bool
val arm_options_eqb_OK : arm_options -> arm_options -> Bool.reflect
val arm_options_eqb_OK_sumbool : arm_options -> arm_options -> bool
val eqTC_arm_options : arm_options Utils0.eqTypeC
val arm_options_eqType : Eqtype.Equality.coq_type
val default_opts : arm_options
val set_is_conditional : arm_options -> arm_options
val unset_is_conditional : arm_options -> arm_options
type halfword =
  1. | HWB
  2. | HWT
val halfword_rect : 'a1 -> 'a1 -> halfword -> 'a1
val halfword_rec : 'a1 -> 'a1 -> halfword -> 'a1
type is_halfword =
  1. | Coq_is_HWB
  2. | Coq_is_HWT
val is_halfword_rect : 'a1 -> 'a1 -> halfword -> is_halfword -> 'a1
val is_halfword_rec : 'a1 -> 'a1 -> halfword -> is_halfword -> 'a1
val halfword_tag : halfword -> BinNums.positive
val is_halfword_inhab : halfword -> is_halfword
val is_halfword_functor : halfword -> is_halfword -> is_halfword
type box_halfword_HWB =
  1. | Box_halfword_HWB
type halfword_fields_t = __
val halfword_fields : halfword -> halfword_fields_t
val halfword_construct : BinNums.positive -> halfword_fields_t -> halfword option
val halfword_induction : 'a1 -> 'a1 -> halfword -> is_halfword -> 'a1
val halfword_eqb_fields : (halfword -> halfword -> bool) -> BinNums.positive -> halfword_fields_t -> halfword_fields_t -> bool
val halfword_eqb : halfword -> halfword -> bool
val halfword_eqb_OK : halfword -> halfword -> Bool.reflect
val halfword_eqb_OK_sumbool : halfword -> halfword -> bool
type arm_mnemonic =
  1. | ADD
  2. | ADC
  3. | MUL
  4. | MLA
  5. | MLS
  6. | SDIV
  7. | SUB
  8. | SBC
  9. | RSB
  10. | UDIV
  11. | UMULL
  12. | UMAAL
  13. | UMLAL
  14. | SMULL
  15. | SMLAL
  16. | SMMUL
  17. | SMMULR
  18. | SMUL_hw of halfword * halfword
  19. | SMLA_hw of halfword * halfword
  20. | SMULW_hw of halfword
  21. | AND
  22. | BFC
  23. | BFI
  24. | BIC
  25. | EOR
  26. | MVN
  27. | ORR
  28. | ASR
  29. | LSL
  30. | LSR
  31. | ROR
  32. | REV
  33. | REV16
  34. | REVSH
  35. | ADR
  36. | MOV
  37. | MOVT
  38. | UBFX
  39. | UXTB
  40. | UXTH
  41. | SBFX
  42. | CLZ
  43. | CMP
  44. | TST
  45. | CMN
  46. | LDR
  47. | LDRB
  48. | LDRH
  49. | LDRSB
  50. | LDRSH
  51. | STR
  52. | STRB
  53. | STRH
val arm_mnemonic_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (halfword -> halfword -> 'a1) -> (halfword -> halfword -> 'a1) -> (halfword -> '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 -> arm_mnemonic -> 'a1
val arm_mnemonic_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (halfword -> halfword -> 'a1) -> (halfword -> halfword -> 'a1) -> (halfword -> '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 -> arm_mnemonic -> 'a1
type is_arm_mnemonic =
  1. | Coq_is_ADD
  2. | Coq_is_ADC
  3. | Coq_is_MUL
  4. | Coq_is_MLA
  5. | Coq_is_MLS
  6. | Coq_is_SDIV
  7. | Coq_is_SUB
  8. | Coq_is_SBC
  9. | Coq_is_RSB
  10. | Coq_is_UDIV
  11. | Coq_is_UMULL
  12. | Coq_is_UMAAL
  13. | Coq_is_UMLAL
  14. | Coq_is_SMULL
  15. | Coq_is_SMLAL
  16. | Coq_is_SMMUL
  17. | Coq_is_SMMULR
  18. | Coq_is_SMUL_hw of halfword * is_halfword * halfword * is_halfword
  19. | Coq_is_SMLA_hw of halfword * is_halfword * halfword * is_halfword
  20. | Coq_is_SMULW_hw of halfword * is_halfword
  21. | Coq_is_AND
  22. | Coq_is_BFC
  23. | Coq_is_BFI
  24. | Coq_is_BIC
  25. | Coq_is_EOR
  26. | Coq_is_MVN
  27. | Coq_is_ORR
  28. | Coq_is_ASR
  29. | Coq_is_LSL
  30. | Coq_is_LSR
  31. | Coq_is_ROR
  32. | Coq_is_REV
  33. | Coq_is_REV16
  34. | Coq_is_REVSH
  35. | Coq_is_ADR
  36. | Coq_is_MOV
  37. | Coq_is_MOVT
  38. | Coq_is_UBFX
  39. | Coq_is_UXTB
  40. | Coq_is_UXTH
  41. | Coq_is_SBFX
  42. | Coq_is_CLZ
  43. | Coq_is_CMP
  44. | Coq_is_TST
  45. | Coq_is_CMN
  46. | Coq_is_LDR
  47. | Coq_is_LDRB
  48. | Coq_is_LDRH
  49. | Coq_is_LDRSB
  50. | Coq_is_LDRSH
  51. | Coq_is_STR
  52. | Coq_is_STRB
  53. | Coq_is_STRH
val is_arm_mnemonic_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (halfword -> is_halfword -> halfword -> is_halfword -> 'a1) -> (halfword -> is_halfword -> halfword -> is_halfword -> 'a1) -> (halfword -> is_halfword -> '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 -> arm_mnemonic -> is_arm_mnemonic -> 'a1
val is_arm_mnemonic_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (halfword -> is_halfword -> halfword -> is_halfword -> 'a1) -> (halfword -> is_halfword -> halfword -> is_halfword -> 'a1) -> (halfword -> is_halfword -> '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 -> arm_mnemonic -> is_arm_mnemonic -> 'a1
val arm_mnemonic_tag : arm_mnemonic -> BinNums.positive
val is_arm_mnemonic_inhab : arm_mnemonic -> is_arm_mnemonic
val is_arm_mnemonic_functor : arm_mnemonic -> is_arm_mnemonic -> is_arm_mnemonic
type box_arm_mnemonic_ADD =
  1. | Box_arm_mnemonic_ADD
type box_arm_mnemonic_SMUL_hw = {
  1. coq_Box_arm_mnemonic_SMUL_hw_0 : halfword;
  2. coq_Box_arm_mnemonic_SMUL_hw_1 : halfword;
}
val coq_Box_arm_mnemonic_SMUL_hw_0 : box_arm_mnemonic_SMUL_hw -> halfword
val coq_Box_arm_mnemonic_SMUL_hw_1 : box_arm_mnemonic_SMUL_hw -> halfword
type box_arm_mnemonic_SMULW_hw = halfword
val coq_Box_arm_mnemonic_SMULW_hw_0 : box_arm_mnemonic_SMULW_hw -> halfword
type arm_mnemonic_fields_t = __
val arm_mnemonic_fields : arm_mnemonic -> arm_mnemonic_fields_t
val arm_mnemonic_construct : BinNums.positive -> arm_mnemonic_fields_t -> arm_mnemonic option
val arm_mnemonic_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (halfword -> is_halfword -> halfword -> is_halfword -> 'a1) -> (halfword -> is_halfword -> halfword -> is_halfword -> 'a1) -> (halfword -> is_halfword -> '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 -> arm_mnemonic -> is_arm_mnemonic -> 'a1
val arm_mnemonic_eqb_fields : (arm_mnemonic -> arm_mnemonic -> bool) -> BinNums.positive -> arm_mnemonic_fields_t -> arm_mnemonic_fields_t -> bool
val arm_mnemonic_eqb : arm_mnemonic -> arm_mnemonic -> bool
val arm_mnemonic_eqb_OK : arm_mnemonic -> arm_mnemonic -> Bool.reflect
val arm_mnemonic_eqb_OK_sumbool : arm_mnemonic -> arm_mnemonic -> bool
val eqTC_arm_mnemonic : arm_mnemonic Utils0.eqTypeC
val arm_mnemonic_eqType : Eqtype.Equality.coq_type
val arm_mnemonics : arm_mnemonic list
val finTC_arm_mnemonic : arm_mnemonic Utils0.finTypeC
val arm_mnemonic_finType : Fintype.Finite.coq_type
val set_flags_mnemonics : arm_mnemonic list
val has_shift_mnemonics : arm_mnemonic list
val condition_mnemonics : arm_mnemonic list
val always_has_shift_mnemonics : (arm_mnemonic * Shift_kind.shift_kind) list
val wsize_uload_mn : (Wsize.wsize * arm_mnemonic) list
val uload_mn_of_wsize : Wsize.wsize -> arm_mnemonic option
val wsize_of_uload_mn : arm_mnemonic -> Wsize.wsize option
val wsize_sload_mn : (Wsize.wsize * arm_mnemonic) list
val sload_mn_of_wsize : Wsize.wsize -> arm_mnemonic option
val wsize_of_sload_mn : arm_mnemonic -> Wsize.wsize option
val wsize_of_load_mn : arm_mnemonic -> Wsize.wsize option
val wsize_store_mn : (Wsize.wsize * arm_mnemonic) list
val store_mn_of_wsize : Wsize.wsize -> arm_mnemonic option
val wsize_of_store_mn : arm_mnemonic -> Wsize.wsize option
val string_of_hw : halfword -> string
val string_of_arm_mnemonic : arm_mnemonic -> string
type arm_op =
  1. | ARM_op of arm_mnemonic * arm_options
val arm_op_rect : (arm_mnemonic -> arm_options -> 'a1) -> arm_op -> 'a1
val arm_op_rec : (arm_mnemonic -> arm_options -> 'a1) -> arm_op -> 'a1
type is_arm_op =
  1. | Coq_is_ARM_op of arm_mnemonic * is_arm_mnemonic * arm_options * is_arm_options
val is_arm_op_rect : (arm_mnemonic -> is_arm_mnemonic -> arm_options -> is_arm_options -> 'a1) -> arm_op -> is_arm_op -> 'a1
val is_arm_op_rec : (arm_mnemonic -> is_arm_mnemonic -> arm_options -> is_arm_options -> 'a1) -> arm_op -> is_arm_op -> 'a1
val arm_op_tag : arm_op -> BinNums.positive
val is_arm_op_inhab : arm_op -> is_arm_op
val is_arm_op_functor : arm_op -> is_arm_op -> is_arm_op
type box_arm_op_ARM_op = {
  1. coq_Box_arm_op_ARM_op_0 : arm_mnemonic;
  2. coq_Box_arm_op_ARM_op_1 : arm_options;
}
val coq_Box_arm_op_ARM_op_0 : box_arm_op_ARM_op -> arm_mnemonic
val coq_Box_arm_op_ARM_op_1 : box_arm_op_ARM_op -> arm_options
type arm_op_fields_t = box_arm_op_ARM_op
val arm_op_fields : arm_op -> arm_op_fields_t
val arm_op_construct : BinNums.positive -> box_arm_op_ARM_op -> arm_op option
val arm_op_induction : (arm_mnemonic -> is_arm_mnemonic -> arm_options -> is_arm_options -> 'a1) -> arm_op -> is_arm_op -> 'a1
val arm_op_eqb_fields : (arm_op -> arm_op -> bool) -> BinNums.positive -> box_arm_op_ARM_op -> box_arm_op_ARM_op -> bool
val arm_op_eqb : arm_op -> arm_op -> bool
val arm_op_eqb_OK : arm_op -> arm_op -> Bool.reflect
val arm_op_eqb_OK_sumbool : arm_op -> arm_op -> bool
val eqTC_arm_op : arm_op Utils0.eqTypeC
val arm_op_eqType : Eqtype.Equality.coq_type
val coq_NF_of_word : Wsize.wsize -> Ssralg.GRing.ComRing.sort -> bool
val coq_ZF_of_word : Wsize.wsize -> Ssralg.GRing.ComRing.sort -> bool
val ak_reg_reg_imm_ : Arm_expand_imm.expected_wencoding -> Arch_decl.arg_kind list list list
val ak_reg_reg_imm_shift : Wsize.wsize -> Shift_kind.shift_kind -> Arch_decl.arg_kind list list list
val ak_reg_reg_reg_or_imm_ : Arm_expand_imm.expected_wencoding -> Arch_decl.args_kinds list
val ak_reg_imm_ : Arm_expand_imm.expected_wencoding -> Arch_decl.arg_kind list list list
val ak_reg_reg_or_imm_ : Arm_expand_imm.expected_wencoding -> Arch_decl.args_kinds list
val chk_imm_accept_shift : Arm_expand_imm.expected_wencoding
val chk_imm_accept_shift_w12 : arm_options -> Arm_expand_imm.expected_wencoding
val chk_imm_w16_encoding : bool -> Arm_expand_imm.expected_wencoding
val chk_imm_reject_shift : Arm_expand_imm.expected_wencoding
val arm_high_registers : Arm_decl.register list
val arm_BFC_semi_sc : Wsize.safe_cond list
val arm_BFI_semi_sc : Wsize.safe_cond list
val arm_ASR_C : Sem_type.sem_tuple -> BinNums.coq_Z -> bool
val arm_LSL_C : Sem_type.sem_tuple -> BinNums.coq_Z -> bool
val arm_LSR_C : Sem_type.sem_tuple -> BinNums.coq_Z -> bool
val arm_ROR_C : Sem_type.sem_tuple -> BinNums.coq_Z -> bool
val arm_REV16_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple
val arm_REVSH_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple
val bit_field_extract_semi_sc : Wsize.safe_cond list
val ak_reg_reg_imm_imm_extr : Arch_decl.arg_kind list list list
val ak_reg_reg_imm8_0_8_16_24 : Arch_decl.arg_kind list list list
val arm_prim_string : (string * arm_op Sopn.prim_constructor) list