package jasmin

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

Module Jasmin.Arch_decl

type __ = Obj.t
type 't coq_ToString = {
  1. category : string;
  2. _finC : 't Utils0.finTypeC;
  3. to_string : 't -> string;
}
val category : Type.ltype -> 'a1 coq_ToString -> string
val _finC : Type.ltype -> 'a1 coq_ToString -> 'a1 Utils0.finTypeC
val to_string : Type.ltype -> 'a1 coq_ToString -> 'a1 -> string
val rtype : Type.ltype -> 'a1 coq_ToString -> Type.ltype
type ('reg, 'regx, 'xreg, 'rflag, 'cond) arch_decl = {
  1. reg_size : Wsize.wsize;
  2. xreg_size : Wsize.wsize;
  3. cond_eqC : 'cond Utils0.eqTypeC;
  4. toS_r : 'reg coq_ToString;
  5. toS_rx : 'regx coq_ToString;
  6. toS_x : 'xreg coq_ToString;
  7. toS_f : 'rflag coq_ToString;
  8. ad_rsp : 'reg;
  9. ad_fcp : Flag_combination.coq_FlagCombinationParams;
  10. caimm_cond_eqC : __ Utils0.eqTypeC;
  11. caimm_cond_pp : __ -> string;
  12. check_CAimm : __ -> Wsize.wsize -> Word0.word -> bool;
}
val reg_size : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Wsize.wsize
val xreg_size : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Wsize.wsize
val cond_eqC : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a5 Utils0.eqTypeC
val toS_r : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a1 coq_ToString
val toS_rx : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a2 coq_ToString
val toS_x : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a3 coq_ToString
val toS_f : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a4 coq_ToString
val ad_rsp : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a1
val ad_fcp : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Flag_combination.coq_FlagCombinationParams
type ('reg, 'regx, 'xreg, 'rflag, 'cond) caimm_cond = __
val caimm_cond_eqC : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) caimm_cond Utils0.eqTypeC
val caimm_cond_pp : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) caimm_cond -> string
val check_CAimm : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) caimm_cond -> Wsize.wsize -> Word0.word -> bool
val arch_pd : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Wsize.coq_PointerData
val arch_msfsz : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Wsize.coq_MSFsize
val mk_ptr : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Ident.Ident.ident -> Var0.Var.var
type ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t = 'reg
type ('reg, 'regx, 'xreg, 'rflag, 'cond) regx_t = 'regx
type ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t = 'xreg
type ('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t = 'rflag
type ('reg, 'regx, 'xreg, 'rflag, 'cond) cond_t = 'cond
val lreg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Type.ltype
type ('reg, 'regx, 'xreg, 'rflag, 'cond) wreg = Sem_type.sem_t
val lxreg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Type.ltype
type ('reg, 'regx, 'xreg, 'rflag, 'cond) wxreg = Sem_type.sem_t
type ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_address = {
  1. ad_disp : Word0.word;
  2. ad_base : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t option;
  3. ad_scale : Datatypes.nat;
  4. ad_offset : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t option;
}
val ad_disp : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_address -> Word0.word
val ad_base : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_address -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option
val ad_scale : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_address -> Datatypes.nat
val ad_offset : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_address -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option
type ('reg, 'regx, 'xreg, 'rflag, 'cond) address =
  1. | Areg of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_address
  2. | Arip of Word0.word
val oeq_reg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option -> bool
val reg_address_beq : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_address -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_address -> bool
val reg_address_eq_axiom : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_address Eqtype.eq_axiom
val coq_HB_unnamed_factory_1 : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_address Eqtype.Coq_hasDecEq.axioms_
val arch_decl_reg_address__canonical__eqtype_Equality : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Eqtype.Equality.coq_type
val address_beq : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) address -> ('a1, 'a2, 'a3, 'a4, 'a5) address -> bool
val address_eq_axiom : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) address Eqtype.eq_axiom
val coq_HB_unnamed_factory_3 : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) address Eqtype.Coq_hasDecEq.axioms_
val arch_decl_address__canonical__eqtype_Equality : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Eqtype.Equality.coq_type
type ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg =
  1. | Condt of ('reg, 'regx, 'xreg, 'rflag, 'cond) cond_t
  2. | Imm of Wsize.wsize * Word0.word
  3. | Reg of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t
  4. | Regx of ('reg, 'regx, 'xreg, 'rflag, 'cond) regx_t
  5. | Addr of ('reg, 'regx, 'xreg, 'rflag, 'cond) address
  6. | XReg of ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t
type ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_args = ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg list
val is_Condt : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg -> ('a1, 'a2, 'a3, 'a4, 'a5) cond_t option
val asm_arg_beq : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg -> bool
val asm_arg_eq_axiom : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg Eqtype.eq_axiom
val coq_HB_unnamed_factory_5 : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg Eqtype.Coq_hasDecEq.axioms_
val arch_decl_asm_arg__canonical__eqtype_Equality : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Eqtype.Equality.coq_type
type msb_flag =
  1. | MSB_CLEAR
  2. | MSB_MERGE
val msb_flag_rect : 'a1 -> 'a1 -> msb_flag -> 'a1
val msb_flag_rec : 'a1 -> 'a1 -> msb_flag -> 'a1
type is_msb_flag =
  1. | Coq_is_MSB_CLEAR
  2. | Coq_is_MSB_MERGE
val is_msb_flag_rect : 'a1 -> 'a1 -> msb_flag -> is_msb_flag -> 'a1
val is_msb_flag_rec : 'a1 -> 'a1 -> msb_flag -> is_msb_flag -> 'a1
val msb_flag_tag : msb_flag -> BinNums.positive
val is_msb_flag_inhab : msb_flag -> is_msb_flag
val is_msb_flag_functor : msb_flag -> is_msb_flag -> is_msb_flag
type box_msb_flag_MSB_CLEAR =
  1. | Box_msb_flag_MSB_CLEAR
type msb_flag_fields_t = __
val msb_flag_fields : msb_flag -> msb_flag_fields_t
val msb_flag_construct : BinNums.positive -> msb_flag_fields_t -> msb_flag option
val msb_flag_induction : 'a1 -> 'a1 -> msb_flag -> is_msb_flag -> 'a1
val msb_flag_eqb_fields : (msb_flag -> msb_flag -> bool) -> BinNums.positive -> msb_flag_fields_t -> msb_flag_fields_t -> bool
val msb_flag_eqb : msb_flag -> msb_flag -> bool
val msb_flag_eqb_OK : msb_flag -> msb_flag -> Datatypes.reflect
val msb_flag_eqb_OK_sumbool : msb_flag -> msb_flag -> bool
val coq_HB_unnamed_factory_7 : msb_flag Eqtype.Coq_hasDecEq.axioms_
val arch_decl_msb_flag__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type ('reg, 'regx, 'xreg, 'rflag, 'cond) implicit_arg =
  1. | IArflag of ('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t
  2. | IAreg of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t
val implicit_arg_beq : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) implicit_arg -> ('a1, 'a2, 'a3, 'a4, 'a5) implicit_arg -> bool
val implicit_arg_eq_axiom : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) implicit_arg Eqtype.eq_axiom
val coq_HB_unnamed_factory_9 : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) implicit_arg Eqtype.Coq_hasDecEq.axioms_
val arch_decl_implicit_arg__canonical__eqtype_Equality : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Eqtype.Equality.coq_type
type addr_kind =
  1. | AK_compute
  2. | AK_mem of Memory_model.aligned
type ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_constrained_register =
  1. | ACR_any
  2. | ACR_exact of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t
  3. | ACR_vector of ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t
  4. | ACR_subset of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t list
type ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_desc =
  1. | ADImplicit of ('reg, 'regx, 'xreg, 'rflag, 'cond) implicit_arg
  2. | ADExplicit of addr_kind * Datatypes.nat * ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_constrained_register
val coq_F : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) rflag_t -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc
val coq_R : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc
val coq_Ea : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Datatypes.nat -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc
val coq_Eu : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Datatypes.nat -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc
val coq_Ec : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Datatypes.nat -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc
val coq_Ef : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Datatypes.nat -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc
val check_oreg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_constrained_register -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg -> bool
type ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_kind =
  1. | CAcond
  2. | CAreg
  3. | CAregx
  4. | CAxmm
  5. | CAmem of bool
  6. | CAimm of ('reg, 'regx, 'xreg, 'rflag, 'cond) caimm_cond option * Wsize.wsize
val arg_kind_eqb : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind -> bool
val arg_kind_eqb_OK : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind -> Datatypes.reflect
val coq_HB_unnamed_factory_11 : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind Eqtype.Coq_hasDecEq.axioms_
val arch_decl_arg_kind__canonical__eqtype_Equality : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Eqtype.Equality.coq_type
type ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_kinds = ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_kind list
type ('reg, 'regx, 'xreg, 'rflag, 'cond) args_kinds = ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_kinds list
type ('reg, 'regx, 'xreg, 'rflag, 'cond) i_args_kinds = ('reg, 'regx, 'xreg, 'rflag, 'cond) args_kinds list
val check_arg_kind : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind -> bool
val check_arg_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_kinds -> bool
val check_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_args -> ('a1, 'a2, 'a3, 'a4, 'a5) args_kinds -> bool
val check_i_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_args -> bool
val check_arg_dest : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc -> Type.ltype -> bool
type ('reg, 'regx, 'xreg, 'rflag, 'cond) pp_asm_op_ext =
  1. | PP_error
  2. | PP_name
  3. | PP_iname of Wsize.wsize
  4. | PP_iname2 of string * Wsize.wsize * Wsize.wsize
  5. | PP_viname of Wsize.velem * bool
  6. | PP_viname2 of Wsize.velem * Wsize.velem
  7. | PP_ct of ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg
type ('reg, 'regx, 'xreg, 'rflag, 'cond) pp_asm_op = {
  1. pp_aop_name : string;
  2. pp_aop_ext : ('reg, 'regx, 'xreg, 'rflag, 'cond) pp_asm_op_ext;
  3. pp_aop_args : (Wsize.wsize * ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg) list;
}
val pp_aop_name : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op -> string
val pp_aop_ext : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op -> ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op_ext
val pp_aop_args : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op -> (Wsize.wsize * ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg) list
type ('reg, 'regx, 'xreg, 'rflag, 'cond) instr_desc_t = {
  1. id_valid : bool;
  2. id_msb_flag : msb_flag;
  3. id_tin : Type.ltype list;
  4. id_in : ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_desc list;
  5. id_tout : Type.ltype list;
  6. id_out : ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_desc list;
  7. id_semi : Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod;
  8. id_args_kinds : ('reg, 'regx, 'xreg, 'rflag, 'cond) i_args_kinds;
  9. id_nargs : Datatypes.nat;
  10. id_str_jas : unit -> string;
  11. id_safe : Wsize.safe_cond list;
  12. id_doit : Sopn.doit_t;
  13. id_pp_asm : ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_args -> ('reg, 'regx, 'xreg, 'rflag, 'cond) pp_asm_op;
}
val id_valid : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> bool
val id_msb_flag : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> msb_flag
val id_tin : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> Type.ltype list
val id_in : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list
val id_tout : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> Type.ltype list
val id_out : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list
val id_semi : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> Sem_type.sem_tuple Utils0.exec Sem_type.sem_prod
val id_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds
val id_nargs : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> Datatypes.nat
val id_str_jas : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> unit -> string
val id_safe : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> Wsize.safe_cond list
val id_doit : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> Sopn.doit_t
val id_pp_asm : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_args -> ('a1, 'a2, 'a3, 'a4, 'a5) pp_asm_op
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_decl = {
  1. _eqT : 'asm_op Utils0.eqTypeC;
  2. instr_desc_op : 'asm_op -> ('reg, 'regx, 'xreg, 'rflag, 'cond) instr_desc_t;
  3. prim_string : (string * 'asm_op Sopn.prim_constructor) list;
}
val _eqT : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> 'a6 Utils0.eqTypeC
val instr_desc_op : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> 'a6 -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t
val prim_string : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> (string * 'a6 Sopn.prim_constructor) list
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_t' = 'asm_op
type 'asm_op asm_op_msb_t_gen = Wsize.wsize option * 'asm_op
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_msb_t = 'asm_op asm_op_msb_t_gen
val extend_size : Wsize.wsize -> Type.ltype -> Type.ltype
val apply_lprod : ('a1 -> 'a2) -> __ list -> 'a1 Utils0.lprod -> 'a2 Utils0.lprod
val is_not_CAmem : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_kind -> bool
val exclude_mem_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc -> ('a1, 'a2, 'a3, 'a4, 'a5) args_kinds -> ('a1, 'a2, 'a3, 'a4, 'a5) args_kinds
val exclude_mem_i_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc -> ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds -> ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds
val exclude_mem_aux : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list -> ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds
val is_nil : 'a1 list -> bool
val exclude_mem : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list -> ('a1, 'a2, 'a3, 'a4, 'a5) i_args_kinds
val can_zeroextend : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t -> bool
val instr_desc : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_msb_t -> ('a1, 'a2, 'a3, 'a4, 'a5) instr_desc_t
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_i_r =
  1. | ALIGN
  2. | LABEL of Label.label_kind * Label.label
  3. | STORELABEL of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t * Label.label
  4. | JMP of Label.remote_label
  5. | JMPI of ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg
  6. | Jcc of Label.label * ('reg, 'regx, 'xreg, 'rflag, 'cond) cond_t
  7. | JAL of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t * Label.remote_label
  8. | CALL of Label.remote_label
  9. | POPPC
  10. | AsmOp of ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_t' * ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_args
  11. | SysCall of (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t
  12. | Declassify_val of Type.ltype * ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_arg
  13. | Declassify_mem of BinNums.coq_Z * ('reg, 'regx, 'xreg, 'rflag, 'cond) address
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_i = {
  1. asmi_ii : Expr.instr_info;
  2. asmi_i : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_i_r;
}
val asmi_ii : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_i -> Expr.instr_info
val asmi_i : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_i -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_i_r
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_code = ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_i list
type ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_typed_reg =
  1. | ARReg of ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t
  2. | ARegX of ('reg, 'regx, 'xreg, 'rflag, 'cond) regx_t
  3. | AXReg of ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t
  4. | ABReg of ('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t
val asm_typed_reg_beq : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg -> bool
val asm_typed_reg_eq_axiom : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg Eqtype.eq_axiom
val coq_HB_unnamed_factory_13 : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg Eqtype.Coq_hasDecEq.axioms_
val arch_decl_asm_typed_reg__canonical__eqtype_Equality : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Eqtype.Equality.coq_type
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_fundef = {
  1. asm_fd_align : Wsize.wsize;
  2. asm_fd_arg : ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_typed_reg list;
  3. asm_fd_body : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_code;
  4. asm_fd_res : ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_typed_reg list;
  5. asm_fd_export : bool;
  6. asm_fd_total_stack : BinNums.coq_Z;
  7. asm_fd_align_args : Wsize.wsize list;
}
val asm_fd_align : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef -> Wsize.wsize
val asm_fd_arg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg list
val asm_fd_body : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_code
val asm_fd_res : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg list
val asm_fd_export : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef -> bool
val asm_fd_total_stack : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef -> BinNums.coq_Z
val asm_fd_align_args : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef -> Wsize.wsize list
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_prog = {
  1. asm_globs : Word0.word list;
  2. asm_glob_names : ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list;
  3. asm_funcs : (Var0.funname * ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_fundef) list;
}
val asm_globs : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_prog -> Word0.word list
val asm_glob_names : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_prog -> ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list
val asm_funcs : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_prog -> (Var0.funname * ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef) list
val is_ABReg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg -> bool
type ('reg, 'regx, 'xreg, 'rflag, 'cond) calling_convention = {
  1. callee_saved : ('reg, 'regx, 'xreg, 'rflag, 'cond) asm_typed_reg list;
  2. call_reg_args : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t list;
  3. call_xreg_args : ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t list;
  4. call_reg_ret : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t list;
  5. call_xreg_ret : ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t list;
}
val callee_saved : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg list
val call_reg_args : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t list
val call_xreg_args : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t list
val call_reg_ret : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t list
val call_xreg_ret : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t list
val get_ARReg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t option
val get_ARegX : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg -> ('a1, 'a2, 'a3, 'a4, 'a5) regx_t option
val get_AXReg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg -> ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t option
val check_list : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 'a6 Utils0.eqTypeC -> (('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg -> 'a6 option) -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_typed_reg list -> 'a6 list -> bool
val check_call_conv : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_fundef -> bool
type ('reg, 'regx, 'xreg, 'rflag, 'cond) internal_calling_convention = {
  1. icall_reg : ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t list;
  2. icall_regx : ('reg, 'regx, 'xreg, 'rflag, 'cond) regx_t list;
  3. icall_xreg : ('reg, 'regx, 'xreg, 'rflag, 'cond) xreg_t list;
  4. icall_rflag : ('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t list;
}
val icall_reg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) internal_calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t list
val icall_regx : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) internal_calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) regx_t list
val icall_xreg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) internal_calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t list
val icall_rflag : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) internal_calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5) rflag_t list
val registers : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) reg_t list
val registerxs : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) regx_t list
val xregisters : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) xreg_t list
val rflags : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) rflag_t list
type rflagv =
  1. | Def of bool
  2. | Undef
val rflagv_rect : (bool -> 'a1) -> 'a1 -> rflagv -> 'a1
val rflagv_rec : (bool -> 'a1) -> 'a1 -> rflagv -> 'a1
type is_rflagv =
  1. | Coq_is_Def of bool * Param1.Coq_exports.is_bool
  2. | Coq_is_Undef
val is_rflagv_rect : (bool -> Param1.Coq_exports.is_bool -> 'a1) -> 'a1 -> rflagv -> is_rflagv -> 'a1
val is_rflagv_rec : (bool -> Param1.Coq_exports.is_bool -> 'a1) -> 'a1 -> rflagv -> is_rflagv -> 'a1
val rflagv_tag : rflagv -> BinNums.positive
val is_rflagv_inhab : rflagv -> is_rflagv
val is_rflagv_functor : rflagv -> is_rflagv -> is_rflagv
type box_rflagv_Def = bool
val coq_Box_rflagv_Def_0 : box_rflagv_Def -> bool
type box_rflagv_Undef =
  1. | Box_rflagv_Undef
type rflagv_fields_t = __
val rflagv_fields : rflagv -> rflagv_fields_t
val rflagv_construct : BinNums.positive -> rflagv_fields_t -> rflagv option
val rflagv_induction : (bool -> Param1.Coq_exports.is_bool -> 'a1) -> 'a1 -> rflagv -> is_rflagv -> 'a1
val rflagv_eqb_fields : (rflagv -> rflagv -> bool) -> BinNums.positive -> rflagv_fields_t -> rflagv_fields_t -> bool
val rflagv_eqb : rflagv -> rflagv -> bool
val rflagv_eqb_OK : rflagv -> rflagv -> Datatypes.reflect
val rflagv_eqb_OK_sumbool : rflagv -> rflagv -> bool
val coq_HB_unnamed_factory_15 : rflagv Eqtype.Coq_hasDecEq.axioms_
val arch_decl_rflagv__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm = {
  1. _arch_decl : ('reg, 'regx, 'xreg, 'rflag, 'cond) arch_decl;
  2. _asm_op_decl : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_decl;
  3. eval_cond : (('reg, 'regx, 'xreg, 'rflag, 'cond) reg_t -> Word0.word) -> (('reg, 'regx, 'xreg, 'rflag, 'cond) rflag_t -> bool Utils0.exec) -> ('reg, 'regx, 'xreg, 'rflag, 'cond) cond_t -> bool Utils0.exec;
}
val _arch_decl : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl
val _asm_op_decl : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm_op_decl
val eval_cond : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) asm -> (('a1, 'a2, 'a3, 'a4, 'a5) reg_t -> Word0.word) -> (('a1, 'a2, 'a3, 'a4, 'a5) rflag_t -> bool Utils0.exec) -> ('a1, 'a2, 'a3, 'a4, 'a5) cond_t -> bool Utils0.exec