package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Sopn

type arg_constrained_register =
  1. | ACR_any
  2. | ACR_exact of Var0.Var.var
  3. | ACR_subset of Var0.Var.var list
type arg_desc =
  1. | ADImplicit of Var0.Var.var
  2. | ADExplicit of Datatypes.nat * arg_constrained_register
type arg_position =
  1. | APout of Datatypes.nat
  2. | APin of Datatypes.nat
type instruction_desc = {
  1. str : unit -> string;
  2. tin : Type.stype list;
  3. i_in : arg_desc list;
  4. tout : Type.stype list;
  5. i_out : arg_desc list;
  6. conflicts : (arg_position * arg_position) list;
  7. semi : Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod;
  8. i_valid : bool;
  9. i_safe : Wsize.safe_cond list;
}
val str : instruction_desc -> unit -> string
val tin : instruction_desc -> Type.stype list
val i_in : instruction_desc -> arg_desc list
val tout : instruction_desc -> Type.stype list
val i_out : instruction_desc -> arg_desc list
val conflicts : instruction_desc -> (arg_position * arg_position) list
val i_valid : instruction_desc -> bool
val i_safe : instruction_desc -> Wsize.safe_cond list
type 'asm_op prim_constructor =
  1. | PrimX86 of prim_x86_suffix list * prim_x86_suffix -> 'asm_op option
  2. | PrimARM of bool -> bool -> (string, 'asm_op) Utils0.result
type 'asm_op asmOp = {
  1. _eqT : 'asm_op Utils0.eqTypeC;
  2. asm_op_instr : 'asm_op -> instruction_desc;
  3. prim_string : (string * 'asm_op prim_constructor) list;
}
val _eqT : 'a1 asmOp -> 'a1 Utils0.eqTypeC
val asm_op_instr : 'a1 asmOp -> 'a1 -> instruction_desc
val prim_string : 'a1 asmOp -> (string * 'a1 prim_constructor) list
type 'asm_op asm_op_t = 'asm_op
type 'asm_op sopn =
  1. | Opseudo_op of Pseudo_operator.pseudo_operator
  2. | Oslh of Slh_ops.slh_op
  3. | Oasm of 'asm_op asm_op_t
val sopn_beq : 'a1 asmOp -> 'a1 sopn -> 'a1 sopn -> bool
val sopn_eq_axiom : 'a1 asmOp -> 'a1 sopn Eqtype.eq_axiom
val coq_HB_unnamed_factory_1 : 'a1 asmOp -> 'a1 sopn Eqtype.Coq_hasDecEq.axioms_
val sopn_sopn__canonical__eqtype_Equality : 'a1 asmOp -> Eqtype.Equality.coq_type
val sopn_copy : 'a1 asmOp -> Wsize.wsize -> BinNums.positive -> 'a1 sopn
val sopn_nop : 'a1 asmOp -> 'a1 sopn
val sopn_mulu : 'a1 asmOp -> Wsize.wsize -> 'a1 sopn
val sopn_addcarry : 'a1 asmOp -> Wsize.wsize -> 'a1 sopn
val sopn_subcarry : 'a1 asmOp -> Wsize.wsize -> 'a1 sopn
val is_Oslh : 'a1 asmOp -> 'a1 sopn -> Slh_ops.slh_op option
val coq_Ocopy_instr : Wsize.wsize -> BinNums.positive -> instruction_desc
val coq_Onop_instr : instruction_desc
val coq_Omulu_instr : Wsize.wsize -> instruction_desc
val coq_Oaddcarry_instr : Wsize.wsize -> instruction_desc
val coq_Osubcarry_instr : Wsize.wsize -> instruction_desc
val coq_Ospill_instr : Pseudo_operator.spill_op -> Type.stype list -> instruction_desc
val coq_Oswap_instr : Type.stype -> instruction_desc
val pseudo_op_get_instr_desc : Pseudo_operator.pseudo_operator -> instruction_desc
val coq_SLHinit_str : string
val coq_SLHinit_instr : Wsize.coq_MSFsize -> instruction_desc
val coq_SLHupdate_str : string
val coq_SLHupdate_instr : Wsize.coq_MSFsize -> instruction_desc
val coq_SLHmove_str : string
val coq_SLHmove_instr : Wsize.coq_MSFsize -> instruction_desc
val coq_SLHprotect_str : string
val coq_SLHprotect_instr : Wsize.coq_MSFsize -> Wsize.wsize -> instruction_desc
val coq_SLHprotect_ptr_str : string
val coq_SLHprotect_ptr_instr : Wsize.coq_MSFsize -> BinNums.positive -> instruction_desc
val coq_SLHprotect_ptr_fail_str : string
val coq_SLHprotect_ptr_fail_instr : Wsize.coq_MSFsize -> BinNums.positive -> instruction_desc
val slh_op_instruction_desc : Wsize.coq_MSFsize -> Slh_ops.slh_op -> instruction_desc
val get_instr_desc : Wsize.coq_MSFsize -> 'a1 asmOp -> 'a1 sopn -> instruction_desc
val string_of_sopn : Wsize.coq_MSFsize -> 'a1 asmOp -> 'a1 sopn -> string
val sopn_tin : Wsize.coq_MSFsize -> 'a1 asmOp -> 'a1 sopn -> Type.stype list
val sopn_tout : Wsize.coq_MSFsize -> 'a1 asmOp -> 'a1 sopn -> Type.stype list
val sopn_sem_ : Wsize.coq_MSFsize -> 'a1 asmOp -> 'a1 sopn -> Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod
val eqC_sopn : 'a1 asmOp -> 'a1 sopn Utils0.eqTypeC
val map_prim_constructor : ('a1 -> 'a2) -> 'a1 prim_constructor -> 'a2 prim_constructor
val primM : 'a1 -> 'a1 prim_constructor
val primP : Wsize.coq_PointerData -> (Wsize.wsize -> 'a1) -> 'a1 prim_constructor
val sopn_prim_string : Wsize.coq_PointerData -> 'a1 asmOp -> (string * 'a1 sopn prim_constructor) list
val asmOp_sopn : Wsize.coq_PointerData -> Wsize.coq_MSFsize -> 'a1 asmOp -> 'a1 sopn asmOp