Module `Jasmin.Arm_extra`

type __ = Obj.t

type arm_extra_op =

| Oarm_swap of Wsize.wsize
| Oarm_add_large_imm
| Osmart_li of Wsize.wsize
| Osmart_li_cc of Wsize.wsize

val arm_extra_op_rect : 
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> 'a1) ->
  (Wsize.wsize -> 'a1) ->
  arm_extra_op ->
  'a1

val arm_extra_op_rec : 
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> 'a1) ->
  (Wsize.wsize -> 'a1) ->
  arm_extra_op ->
  'a1

type is_arm_extra_op =

| Coq_is_Oarm_swap of Wsize.wsize * Wsize.is_wsize
| Coq_is_Oarm_add_large_imm
| Coq_is_Osmart_li of Wsize.wsize * Wsize.is_wsize
| Coq_is_Osmart_li_cc of Wsize.wsize * Wsize.is_wsize

val is_arm_extra_op_rect : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  arm_extra_op ->
  is_arm_extra_op ->
  'a1

val is_arm_extra_op_rec : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  arm_extra_op ->
  is_arm_extra_op ->
  'a1

val arm_extra_op_tag : arm_extra_op -> BinNums.positive

val is_arm_extra_op_inhab : arm_extra_op -> is_arm_extra_op

val is_arm_extra_op_functor : 
  arm_extra_op ->
  is_arm_extra_op ->
  is_arm_extra_op

type box_arm_extra_op_Oarm_swap = Wsize.wsize

val coq_Box_arm_extra_op_Oarm_swap_0 : 
  box_arm_extra_op_Oarm_swap ->
  Wsize.wsize

type box_arm_extra_op_Oarm_add_large_imm =

| Box_arm_extra_op_Oarm_add_large_imm

type arm_extra_op_fields_t = __

val arm_extra_op_fields : arm_extra_op -> arm_extra_op_fields_t

val arm_extra_op_construct : 
  BinNums.positive ->
  arm_extra_op_fields_t ->
  arm_extra_op option

val arm_extra_op_induction : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  arm_extra_op ->
  is_arm_extra_op ->
  'a1

val arm_extra_op_eqb_fields : 
  (arm_extra_op -> arm_extra_op -> bool) ->
  BinNums.positive ->
  arm_extra_op_fields_t ->
  arm_extra_op_fields_t ->
  bool

val arm_extra_op_eqb : arm_extra_op -> arm_extra_op -> bool

val arm_extra_op_eqb_OK : arm_extra_op -> arm_extra_op -> Bool.reflect

val arm_extra_op_eqb_OK_sumbool : arm_extra_op -> arm_extra_op -> bool

val coq_HB_unnamed_factory_1 : arm_extra_op Eqtype.Coq_hasDecEq.axioms_

val arm_extra_arm_extra_op__canonical__eqtype_Equality : 
  Eqtype.Equality.coq_type

val eqTC_arm_extra_op : arm_extra_op Utils0.eqTypeC

val coq_Oarm_add_large_imm_instr : Sopn.instruction_desc

val smart_li_instr : Wsize.wsize -> Sopn.instruction_desc

val smart_li_instr_cc : Wsize.wsize -> Sopn.instruction_desc

val get_instr_desc : arm_extra_op -> Sopn.instruction_desc

val arm_extra_op_decl : arm_extra_op Sopn.asmOp

module E : sig ... end

val asm_args_of_opn_args : 
  Arm_params_core.ARMFopn_core.opn_args list ->
  (((Arm_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_decl.rflag,
      Arm_decl.condt,
      Arm_instr_decl.arm_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list

val uncons : 
  Expr.instr_info ->
  'a1 list ->
  ('a1 * 'a1 list) Compiler_util.cexec

val uncons_LLvar : 
  Expr.instr_info ->
  Fexpr.lexpr list ->
  (Expr.var_i * Fexpr.lexpr list) Compiler_util.cexec

val uncons_rvar : 
  Expr.instr_info ->
  Fexpr.rexpr list ->
  (Expr.var_i * Fexpr.rexpr list) Compiler_util.cexec

val uncons_wconst : 
  Expr.instr_info ->
  Fexpr.rexpr list ->
  (BinNums.coq_Z * Fexpr.rexpr list) Compiler_util.cexec

val smart_li_args : 
  Expr.instr_info ->
  Wsize.wsize ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (Compiler_util.pp_error_loc, (Expr.var_i * BinNums.coq_Z) * Fexpr.rexpr list)
    Utils0.result

val assemble_smart_li : 
  Expr.instr_info ->
  Wsize.wsize ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (Compiler_util.pp_error_loc,
    (((Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op)
        Arch_decl.asm_op_msb_t
      * Fexpr.lexpr list)
     * Fexpr.rexpr list)
      list)
    Utils0.result

val assemble_smart_li_cc : 
  Expr.instr_info ->
  Wsize.wsize ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (((Arm_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_decl.rflag,
      Arm_decl.condt,
      Arm_instr_decl.arm_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

val assemble_extra : 
  Expr.instr_info ->
  arm_extra_op ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (((Arm_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_decl.rflag,
      Arm_decl.condt,
      Arm_instr_decl.arm_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

val arm_extra : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    arm_extra_op)
    Arch_extra.asm_extra

type arm_extended_op =
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    arm_extra_op)
    Arch_extra.extended_op

val coq_Oarm : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Arm_instr_decl.arm_op ->
  arm_extended_op Sopn.sopn

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Arm_extra/index.html

Module `Jasmin.Arm_extra`

package jasmin

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Arm_extra/index.html

Module Jasmin.Arm_extra

dune-project
Dependency

Module `Jasmin.Arm_extra`