Module `Jasmin.X86_extra`

type __ = Obj.t

module E : sig ... end

type x86_extra_op =

| Oset0 of Wsize.wsize
| Oconcat128
| Ox86MOVZX32
| Ox86MULX of Wsize.wsize
| Ox86MULX_hi of Wsize.wsize
| Ox86SLHinit
| Ox86SLHupdate
| Ox86SLHmove
| Ox86SLHprotect of Wsize.reg_kind * Wsize.wsize

val x86_extra_op_rect : 
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  (Wsize.wsize -> 'a1) ->
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.reg_kind -> Wsize.wsize -> 'a1) ->
  x86_extra_op ->
  'a1

val x86_extra_op_rec : 
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  (Wsize.wsize -> 'a1) ->
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.reg_kind -> Wsize.wsize -> 'a1) ->
  x86_extra_op ->
  'a1

type is_x86_extra_op =

| Coq_is_Oset0 of Wsize.wsize * Wsize.is_wsize
| Coq_is_Oconcat128
| Coq_is_Ox86MOVZX32
| Coq_is_Ox86MULX of Wsize.wsize * Wsize.is_wsize
| Coq_is_Ox86MULX_hi of Wsize.wsize * Wsize.is_wsize
| Coq_is_Ox86SLHinit
| Coq_is_Ox86SLHupdate
| Coq_is_Ox86SLHmove
| Coq_is_Ox86SLHprotect of Wsize.reg_kind * Wsize.is_reg_kind * Wsize.wsize * Wsize.is_wsize

val is_x86_extra_op_rect : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.reg_kind -> Wsize.is_reg_kind -> Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  x86_extra_op ->
  is_x86_extra_op ->
  'a1

val is_x86_extra_op_rec : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.reg_kind -> Wsize.is_reg_kind -> Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  x86_extra_op ->
  is_x86_extra_op ->
  'a1

val x86_extra_op_tag : x86_extra_op -> BinNums.positive

val is_x86_extra_op_inhab : x86_extra_op -> is_x86_extra_op

val is_x86_extra_op_functor : 
  x86_extra_op ->
  is_x86_extra_op ->
  is_x86_extra_op

type box_x86_extra_op_Oset0 = Wsize.wsize

val coq_Box_x86_extra_op_Oset0_0 : box_x86_extra_op_Oset0 -> Wsize.wsize

type box_x86_extra_op_Oconcat128 =

| Box_x86_extra_op_Oconcat128

type box_x86_extra_op_Ox86SLHprotect = {

coq_Box_x86_extra_op_Ox86SLHprotect_0 : Wsize.reg_kind;
coq_Box_x86_extra_op_Ox86SLHprotect_1 : Wsize.wsize;

}

val coq_Box_x86_extra_op_Ox86SLHprotect_0 : 
  box_x86_extra_op_Ox86SLHprotect ->
  Wsize.reg_kind

val coq_Box_x86_extra_op_Ox86SLHprotect_1 : 
  box_x86_extra_op_Ox86SLHprotect ->
  Wsize.wsize

type x86_extra_op_fields_t = __

val x86_extra_op_fields : x86_extra_op -> x86_extra_op_fields_t

val x86_extra_op_construct : 
  BinNums.positive ->
  x86_extra_op_fields_t ->
  x86_extra_op option

val x86_extra_op_induction : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.reg_kind -> Wsize.is_reg_kind -> Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  x86_extra_op ->
  is_x86_extra_op ->
  'a1

val x86_extra_op_eqb_fields : 
  (x86_extra_op -> x86_extra_op -> bool) ->
  BinNums.positive ->
  x86_extra_op_fields_t ->
  x86_extra_op_fields_t ->
  bool

val x86_extra_op_eqb : x86_extra_op -> x86_extra_op -> bool

val x86_extra_op_eqb_OK : x86_extra_op -> x86_extra_op -> Bool.reflect

val x86_extra_op_eqb_OK_sumbool : x86_extra_op -> x86_extra_op -> bool

val coq_HB_unnamed_factory_1 : x86_extra_op Eqtype.Coq_hasDecEq.axioms_

val x86_extra_x86_extra_op__canonical__eqtype_Equality : 
  Eqtype.Equality.coq_type

val coq_Oset0_instr : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Sopn.instruction_desc

val coq_Oconcat128_instr : Sopn.instruction_desc

val coq_Ox86MOVZX32_instr : Sopn.instruction_desc

val x86_MULX : 
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Sem_type.sem_tuple

val coq_Ox86MULX_instr : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Sopn.instruction_desc

val x86_MULX_hi : 
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Sem_type.sem_tuple

val coq_Ox86MULX_hi_instr : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Sopn.instruction_desc

val coq_Ox86SLHinit_str : string

val coq_Ox86SLHinit_instr : Sopn.instruction_desc

val x86_se_update_sem : 
  bool ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort * Ssralg.GRing.ComRing.sort

val coq_Ox86SLHupdate_str : string

val coq_Ox86SLHupdate_instr : Sopn.instruction_desc

val coq_Ox86SLHmove_str : string

val coq_Ox86SLHmove_instr : Sopn.instruction_desc

val se_protect_small_sem : 
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Sem_type.sem_tuple

val se_protect_mmx_sem : 
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val se_protect_large_sem : 
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort * Ssralg.GRing.ComRing.sort

val coq_Ox86SLHprotect_str : string

val coq_Ox86SLHprotect_instr : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.reg_kind ->
  Wsize.wsize ->
  Sopn.instruction_desc

val get_instr_desc : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  x86_extra_op ->
  Sopn.instruction_desc

val prim_string : (string * x86_extra_op Sopn.prim_constructor) list

val re_i : Wsize.wsize -> BinNums.coq_Z -> Fexpr.rexpr

val re8_0 : Fexpr.rexpr

val re8_1 : Fexpr.rexpr

val assemble_slh_init : 
  Fexpr.lexpr list ->
  (((X86_decl.register,
      X86_decl.register_ext,
      X86_decl.xmm_register,
      X86_decl.rflag,
      X86_decl.condt,
      X86_instr_decl.x86_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

val assemble_slh_update : 
  Expr.instr_info ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (((X86_decl.register,
      X86_decl.register_ext,
      X86_decl.xmm_register,
      X86_decl.rflag,
      X86_decl.condt,
      X86_instr_decl.x86_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

val assemble_slh_protect : 
  Expr.instr_info ->
  Wsize.reg_kind ->
  Wsize.wsize ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (((X86_decl.register,
      X86_decl.register_ext,
      X86_decl.xmm_register,
      X86_decl.rflag,
      X86_decl.condt,
      X86_instr_decl.x86_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

val assemble_slh_move : 
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (((X86_decl.register,
      X86_decl.register_ext,
      X86_decl.xmm_register,
      X86_decl.rflag,
      X86_decl.condt,
      X86_instr_decl.x86_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

val assemble_extra : 
  Expr.instr_info ->
  x86_extra_op ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (((X86_decl.register,
      X86_decl.register_ext,
      X86_decl.xmm_register,
      X86_decl.rflag,
      X86_decl.condt,
      X86_instr_decl.x86_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

val eqC_x86_extra_op : x86_extra_op Utils0.eqTypeC

val x86_extra_op_decl : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  x86_extra_op Sopn.asmOp

val x86_extra : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    x86_extra_op)
    Arch_extra.asm_extra

type x86_extended_op =
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    x86_extra_op)
    Arch_extra.extended_op

val coq_Ox86 : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  X86_instr_decl.x86_op ->
  x86_extended_op Sopn.sopn

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/X86_extra/index.html

Module `Jasmin.X86_extra`

package jasmin

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/X86_extra/index.html

Module Jasmin.X86_extra

dune-project
Dependency

Module `Jasmin.X86_extra`