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.stype -> 'a1 coq_ToString -> string
val _finC : Type.stype -> 'a1 coq_ToString -> 'a1 Utils0.finTypeC
val to_string : Type.stype -> 'a1 coq_ToString -> 'a1 -> string
val rtype : Type.stype -> 'a1 coq_ToString -> Type.stype
type caimm_checker_s =
  1. | CAimmC_none
  2. | CAimmC_arm_shift_amout of Shift_kind.shift_kind
  3. | CAimmC_arm_wencoding of Arm_expand_imm.expected_wencoding
  4. | CAimmC_arm_0_8_16_24
  5. | CAimmC_riscv_12bits_signed
  6. | CAimmC_riscv_5bits_unsigned
val caimm_checker_s_rect : 'a1 -> (Shift_kind.shift_kind -> 'a1) -> (Arm_expand_imm.expected_wencoding -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> caimm_checker_s -> 'a1
val caimm_checker_s_rec : 'a1 -> (Shift_kind.shift_kind -> 'a1) -> (Arm_expand_imm.expected_wencoding -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> caimm_checker_s -> 'a1
type is_caimm_checker_s =
  1. | Coq_is_CAimmC_none
  2. | Coq_is_CAimmC_arm_shift_amout of Shift_kind.shift_kind * Shift_kind.is_shift_kind
  3. | Coq_is_CAimmC_arm_wencoding of Arm_expand_imm.expected_wencoding * Arm_expand_imm.is_expected_wencoding
  4. | Coq_is_CAimmC_arm_0_8_16_24
  5. | Coq_is_CAimmC_riscv_12bits_signed
  6. | Coq_is_CAimmC_riscv_5bits_unsigned
val is_caimm_checker_s_rect : 'a1 -> (Shift_kind.shift_kind -> Shift_kind.is_shift_kind -> 'a1) -> (Arm_expand_imm.expected_wencoding -> Arm_expand_imm.is_expected_wencoding -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> caimm_checker_s -> is_caimm_checker_s -> 'a1
val is_caimm_checker_s_rec : 'a1 -> (Shift_kind.shift_kind -> Shift_kind.is_shift_kind -> 'a1) -> (Arm_expand_imm.expected_wencoding -> Arm_expand_imm.is_expected_wencoding -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> caimm_checker_s -> is_caimm_checker_s -> 'a1
val caimm_checker_s_tag : caimm_checker_s -> BinNums.positive
val is_caimm_checker_s_inhab : caimm_checker_s -> is_caimm_checker_s
val is_caimm_checker_s_functor : caimm_checker_s -> is_caimm_checker_s -> is_caimm_checker_s
type box_caimm_checker_s_CAimmC_none =
  1. | Box_caimm_checker_s_CAimmC_none
type box_caimm_checker_s_CAimmC_arm_shift_amout = Shift_kind.shift_kind
val coq_Box_caimm_checker_s_CAimmC_arm_shift_amout_0 : box_caimm_checker_s_CAimmC_arm_shift_amout -> Shift_kind.shift_kind
type box_caimm_checker_s_CAimmC_arm_wencoding = Arm_expand_imm.expected_wencoding
val coq_Box_caimm_checker_s_CAimmC_arm_wencoding_0 : box_caimm_checker_s_CAimmC_arm_wencoding -> Arm_expand_imm.expected_wencoding
type caimm_checker_s_fields_t = __
val caimm_checker_s_fields : caimm_checker_s -> caimm_checker_s_fields_t
val caimm_checker_s_construct : BinNums.positive -> caimm_checker_s_fields_t -> caimm_checker_s option
val caimm_checker_s_induction : 'a1 -> (Shift_kind.shift_kind -> Shift_kind.is_shift_kind -> 'a1) -> (Arm_expand_imm.expected_wencoding -> Arm_expand_imm.is_expected_wencoding -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> caimm_checker_s -> is_caimm_checker_s -> 'a1
val caimm_checker_s_eqb_fields : (caimm_checker_s -> caimm_checker_s -> bool) -> BinNums.positive -> caimm_checker_s_fields_t -> caimm_checker_s_fields_t -> bool
val caimm_checker_s_eqb : caimm_checker_s -> caimm_checker_s -> bool
val caimm_checker_s_eqb_OK : caimm_checker_s -> caimm_checker_s -> Bool.reflect
val caimm_checker_s_eqb_OK_sumbool : caimm_checker_s -> caimm_checker_s -> bool
val coq_HB_unnamed_factory_1 : caimm_checker_s Eqtype.Coq_hasDecEq.axioms_
val arch_decl_caimm_checker_s__canonical__eqtype_Equality : Eqtype.Equality.coq_type
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. check_CAimm : caimm_checker_s -> Wsize.wsize -> Ssralg.GRing.ComRing.sort -> 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
val check_CAimm : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> caimm_checker_s -> Wsize.wsize -> Ssralg.GRing.ComRing.sort -> 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 sreg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Type.stype
type ('reg, 'regx, 'xreg, 'rflag, 'cond) wreg = Sem_type.sem_t
val sxreg : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> Type.stype
type ('reg, 'regx, 'xreg, 'rflag, 'cond) wxreg = Sem_type.sem_t
type ('reg, 'regx, 'xreg, 'rflag, 'cond) reg_address = {
  1. ad_disp : Ssralg.GRing.ComRing.sort;
  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 -> Ssralg.GRing.ComRing.sort
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 Ssralg.GRing.ComRing.sort
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_3 : ('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_5 : ('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 * Ssralg.GRing.ComRing.sort
  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_7 : ('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 -> Bool.reflect
val msb_flag_eqb_OK_sumbool : msb_flag -> msb_flag -> bool
val coq_HB_unnamed_factory_9 : 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_11 : ('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 arg_kind =
  1. | CAcond
  2. | CAreg
  3. | CAregx
  4. | CAxmm
  5. | CAmem of bool
  6. | CAimm of caimm_checker_s * Wsize.wsize
val arg_kind_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> (bool -> 'a1) -> (caimm_checker_s -> Wsize.wsize -> 'a1) -> arg_kind -> 'a1
val arg_kind_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> (bool -> 'a1) -> (caimm_checker_s -> Wsize.wsize -> 'a1) -> arg_kind -> 'a1
type is_arg_kind =
  1. | Coq_is_CAcond
  2. | Coq_is_CAreg
  3. | Coq_is_CAregx
  4. | Coq_is_CAxmm
  5. | Coq_is_CAmem of bool * Param1.Coq_exports.is_bool
  6. | Coq_is_CAimm of caimm_checker_s * is_caimm_checker_s * Wsize.wsize * Wsize.is_wsize
val is_arg_kind_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> (bool -> Param1.Coq_exports.is_bool -> 'a1) -> (caimm_checker_s -> is_caimm_checker_s -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> arg_kind -> is_arg_kind -> 'a1
val is_arg_kind_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> (bool -> Param1.Coq_exports.is_bool -> 'a1) -> (caimm_checker_s -> is_caimm_checker_s -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> arg_kind -> is_arg_kind -> 'a1
val arg_kind_tag : arg_kind -> BinNums.positive
val is_arg_kind_inhab : arg_kind -> is_arg_kind
val is_arg_kind_functor : arg_kind -> is_arg_kind -> is_arg_kind
type box_arg_kind_CAcond =
  1. | Box_arg_kind_CAcond
type box_arg_kind_CAmem = bool
val coq_Box_arg_kind_CAmem_0 : box_arg_kind_CAmem -> bool
type box_arg_kind_CAimm = {
  1. coq_Box_arg_kind_CAimm_0 : caimm_checker_s;
  2. coq_Box_arg_kind_CAimm_1 : Wsize.wsize;
}
val coq_Box_arg_kind_CAimm_0 : box_arg_kind_CAimm -> caimm_checker_s
val coq_Box_arg_kind_CAimm_1 : box_arg_kind_CAimm -> Wsize.wsize
type arg_kind_fields_t = __
val arg_kind_fields : arg_kind -> arg_kind_fields_t
val arg_kind_construct : BinNums.positive -> arg_kind_fields_t -> arg_kind option
val arg_kind_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> (bool -> Param1.Coq_exports.is_bool -> 'a1) -> (caimm_checker_s -> is_caimm_checker_s -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> arg_kind -> is_arg_kind -> 'a1
val arg_kind_eqb_fields : (arg_kind -> arg_kind -> bool) -> BinNums.positive -> arg_kind_fields_t -> arg_kind_fields_t -> bool
val arg_kind_eqb : arg_kind -> arg_kind -> bool
val arg_kind_eqb_OK : arg_kind -> arg_kind -> Bool.reflect
val arg_kind_eqb_OK_sumbool : arg_kind -> arg_kind -> bool
val coq_HB_unnamed_factory_13 : arg_kind Eqtype.Coq_hasDecEq.axioms_
val arch_decl_arg_kind__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type arg_kinds = arg_kind list
type args_kinds = arg_kinds list
type i_args_kinds = args_kinds list
val check_arg_kind : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg -> arg_kind -> bool
val check_arg_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_arg -> arg_kinds -> bool
val check_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) asm_args -> args_kinds -> bool
val check_i_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> 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.stype -> 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.stype list;
  4. id_in : ('reg, 'regx, 'xreg, 'rflag, 'cond) arg_desc list;
  5. id_tout : Type.stype 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 : i_args_kinds;
  9. id_nargs : Datatypes.nat;
  10. id_str_jas : unit -> string;
  11. id_safe : Wsize.safe_cond list;
  12. 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.stype 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.stype 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 -> 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_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 ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) asm_op_msb_t = Wsize.wsize option * 'asm_op
val extend_size : Wsize.wsize -> Type.stype -> Type.stype
val apply_lprod : ('a1 -> 'a2) -> __ list -> 'a1 Utils0.lprod -> 'a2 Utils0.lprod
val is_not_CAmem : arg_kind -> bool
val exclude_mem_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc -> args_kinds -> args_kinds
val exclude_mem_i_args_kinds : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc -> i_args_kinds -> i_args_kinds
val exclude_mem_aux : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> i_args_kinds -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list -> i_args_kinds
val is_nil : 'a1 list -> bool
val exclude_mem : ('a1, 'a2, 'a3, 'a4, 'a5) arch_decl -> i_args_kinds -> ('a1, 'a2, 'a3, 'a4, 'a5) arg_desc list -> i_args_kinds
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 BinNums.positive Syscall_t.syscall_t
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_15 : ('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 : Ssralg.GRing.ComRing.sort 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 -> Ssralg.GRing.ComRing.sort 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
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 -> Bool.reflect
val rflagv_eqb_OK_sumbool : rflagv -> rflagv -> bool
val coq_HB_unnamed_factory_17 : 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 -> Ssralg.GRing.ComRing.sort) -> (('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 -> Ssralg.GRing.ComRing.sort) -> (('a1, 'a2, 'a3, 'a4, 'a5) rflag_t -> bool Utils0.exec) -> ('a1, 'a2, 'a3, 'a4, 'a5) cond_t -> bool Utils0.exec