Module `Jasmin.Sopn`

type arg_constrained_register =

| ACR_any
| ACR_exact of Var0.Var.var
| ACR_subset of Var0.Var.var list

type arg_desc =

| ADImplicit of Var0.Var.var
| ADExplicit of Datatypes.nat * arg_constrained_register

type arg_position =

| APout of Datatypes.nat
| APin of Datatypes.nat

type instruction_desc = {

str : unit -> string;
tin : Type.stype list;
i_in : arg_desc list;
tout : Type.stype list;
i_out : arg_desc list;
conflicts : (arg_position * arg_position) list;
semi : Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod;
i_valid : bool;
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 semi : instruction_desc -> Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod

val i_valid : instruction_desc -> bool

val i_safe : instruction_desc -> Wsize.safe_cond list

type prim_x86_suffix =

| PVp of Wsize.wsize
| PVs of Wsize.signedness * Wsize.wsize
| PVv of Wsize.velem * Wsize.wsize
| PVsv of Wsize.signedness * Wsize.velem * Wsize.wsize
| PVx of Wsize.wsize * Wsize.wsize
| PVvv of Wsize.velem * Wsize.wsize * Wsize.velem * Wsize.wsize

type 'asm_op prim_constructor =

| PrimX86 of prim_x86_suffix list * prim_x86_suffix -> 'asm_op option
| PrimARM of bool -> bool -> (string, 'asm_op) Utils0.result

type 'asm_op asmOp = {

_eqT : 'asm_op Utils0.eqTypeC;
asm_op_instr : 'asm_op -> instruction_desc;
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 =

| Opseudo_op of Pseudo_operator.pseudo_operator
| Oslh of Slh_ops.slh_op
| 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 spill_semi : Type.stype list -> Sem_type.sem_tuple Sem_type.sem_prod

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 se_init_sem : Wsize.coq_MSFsize -> Ssralg.GRing.ComRing.sort

val se_update_sem : 
  Wsize.coq_MSFsize ->
  bool ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val se_move_sem : 
  Wsize.coq_MSFsize ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val se_protect_sem : 
  Wsize.coq_MSFsize ->
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val se_protect_ptr_sem : 
  Wsize.coq_MSFsize ->
  BinNums.positive ->
  Warray_.WArray.array ->
  Ssralg.GRing.ComRing.sort ->
  Warray_.WArray.array

val se_protect_ptr_fail_sem : 
  Wsize.coq_MSFsize ->
  BinNums.positive ->
  Warray_.WArray.array ->
  Ssralg.GRing.ComRing.sort ->
  Warray_.WArray.array Utils0.exec

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 sopn_sem : 
  Wsize.coq_MSFsize ->
  'a1 asmOp ->
  'a1 sopn ->
  Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod Utils0.exec

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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Sopn/index.html

Module `Jasmin.Sopn`

package jasmin

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Sopn/index.html

Module Jasmin.Sopn

dune-project
Dependency

Module `Jasmin.Sopn`