Module Jasmin.Compiler

type __ = Obj.t
val pp_s : string -> Compiler_util.pp_error
type compiler_step =
  1. | Typing
  2. | ParamsExpansion
  3. | WintWord
  4. | ArrayCopy
  5. | AddArrInit
  6. | LowerSpill
  7. | Inlining
  8. | RemoveUnusedFunction
  9. | Unrolling
  10. | Splitting
  11. | Renaming
  12. | RemovePhiNodes
  13. | DeadCode_Renaming
  14. | RemoveArrInit
  15. | MakeRefArguments
  16. | RegArrayExpansion
  17. | RemoveGlobal
  18. | LoadConstantsInCond
  19. | LowerInstruction
  20. | PropagateInline
  21. | SLHLowering
  22. | LowerAddressing
  23. | StackAllocation
  24. | RemoveReturn
  25. | RegAllocation
  26. | DeadCode_RegAllocation
  27. | Linearization
  28. | StackZeroization
  29. | Tunneling
  30. | Assembly
val compiler_step_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> compiler_step -> 'a1
val compiler_step_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> compiler_step -> 'a1
type is_compiler_step =
  1. | Coq_is_Typing
  2. | Coq_is_ParamsExpansion
  3. | Coq_is_WintWord
  4. | Coq_is_ArrayCopy
  5. | Coq_is_AddArrInit
  6. | Coq_is_LowerSpill
  7. | Coq_is_Inlining
  8. | Coq_is_RemoveUnusedFunction
  9. | Coq_is_Unrolling
  10. | Coq_is_Splitting
  11. | Coq_is_Renaming
  12. | Coq_is_RemovePhiNodes
  13. | Coq_is_DeadCode_Renaming
  14. | Coq_is_RemoveArrInit
  15. | Coq_is_MakeRefArguments
  16. | Coq_is_RegArrayExpansion
  17. | Coq_is_RemoveGlobal
  18. | Coq_is_LoadConstantsInCond
  19. | Coq_is_LowerInstruction
  20. | Coq_is_PropagateInline
  21. | Coq_is_SLHLowering
  22. | Coq_is_LowerAddressing
  23. | Coq_is_StackAllocation
  24. | Coq_is_RemoveReturn
  25. | Coq_is_RegAllocation
  26. | Coq_is_DeadCode_RegAllocation
  27. | Coq_is_Linearization
  28. | Coq_is_StackZeroization
  29. | Coq_is_Tunneling
  30. | Coq_is_Assembly
val is_compiler_step_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> compiler_step -> is_compiler_step -> 'a1
val is_compiler_step_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> compiler_step -> is_compiler_step -> 'a1
val compiler_step_tag : compiler_step -> BinNums.positive
val is_compiler_step_inhab : compiler_step -> is_compiler_step
val is_compiler_step_functor : compiler_step -> is_compiler_step -> is_compiler_step
type box_compiler_step_Typing =
  1. | Box_compiler_step_Typing
type compiler_step_fields_t = __
val compiler_step_fields : compiler_step -> compiler_step_fields_t
val compiler_step_construct : BinNums.positive -> compiler_step_fields_t -> compiler_step option
val compiler_step_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> compiler_step -> is_compiler_step -> 'a1
val compiler_step_eqb_fields : (compiler_step -> compiler_step -> bool) -> BinNums.positive -> compiler_step_fields_t -> compiler_step_fields_t -> bool
val compiler_step_eqb : compiler_step -> compiler_step -> bool
val compiler_step_eqb_OK : compiler_step -> compiler_step -> Bool.reflect
val compiler_step_eqb_OK_sumbool : compiler_step -> compiler_step -> bool
val compiler_step_list : compiler_step list
val coq_HB_unnamed_factory_1 : compiler_step Eqtype.Coq_hasDecEq.axioms_
val compiler_compiler_step__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type stack_alloc_oracles = {
  1. ao_globals : Ssralg.GRing.ComRing.sort list;
  2. ao_global_alloc : ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list;
  3. ao_stack_alloc : Var0.funname -> Stack_alloc.stk_alloc_oracle_t;
}
val ao_global_alloc : stack_alloc_oracles -> ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list
type ('asm_op, 'lowering_options) compiler_params = {
  1. rename_fd : Expr.instr_info -> Var0.funname -> 'asm_op Expr._ufundef -> 'asm_op Expr._ufundef;
  2. expand_fd : Var0.funname -> 'asm_op Expr._ufundef -> Array_expansion.expand_info;
  3. split_live_ranges_fd : Var0.funname -> 'asm_op Expr._ufundef -> 'asm_op Expr._ufundef;
  4. renaming_fd : Var0.funname -> 'asm_op Expr._ufundef -> 'asm_op Expr._ufundef;
  5. remove_phi_nodes_fd : Var0.funname -> 'asm_op Expr._ufundef -> 'asm_op Expr._ufundef;
  6. stack_register_symbol : Ident.Ident.ident;
  7. global_static_data_symbol : Ident.Ident.ident;
  8. stackalloc : 'asm_op Expr._uprog -> stack_alloc_oracles;
  9. removereturn : 'asm_op Expr._sprog -> Var0.funname -> bool list option;
  10. regalloc : 'asm_op Expr._sfun_decl list -> 'asm_op Expr._sfun_decl list;
  11. remove_wint_annot : Var0.funname -> 'asm_op Expr._ufundef -> 'asm_op Expr._ufundef;
  12. print_uprog : compiler_step -> 'asm_op Expr._uprog -> 'asm_op Expr._uprog;
  13. print_sprog : compiler_step -> 'asm_op Expr._sprog -> 'asm_op Expr._sprog;
  14. print_linear : compiler_step -> 'asm_op Linear.lprog -> 'asm_op Linear.lprog;
  15. refresh_instr_info : Var0.funname -> 'asm_op Expr._ufundef -> 'asm_op Expr._ufundef;
  16. warning : Expr.instr_info -> Compiler_util.warning_msg -> Expr.instr_info;
  17. lowering_opt : 'lowering_options;
  18. fresh_id : Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident;
  19. fresh_var_ident : Wsize.v_kind -> Expr.instr_info -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident;
  20. slh_info : 'asm_op Expr._uprog -> Var0.funname -> Slh_lowering.slh_t list * Slh_lowering.slh_t list;
  21. stack_zero_info : Var0.funname -> (Stack_zero_strategy.stack_zero_strategy * Wsize.wsize option) option;
  22. dead_vars_ufd : 'asm_op Expr._ufun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t;
  23. dead_vars_sfd : 'asm_op Expr._sfun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t;
  24. pp_sr : Stack_alloc.sub_region -> Compiler_util.pp_error;
}
val rename_fd : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Expr.instr_info -> Var0.funname -> 'a1 Expr._ufundef -> 'a1 Expr._ufundef
val split_live_ranges_fd : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Var0.funname -> 'a1 Expr._ufundef -> 'a1 Expr._ufundef
val renaming_fd : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Var0.funname -> 'a1 Expr._ufundef -> 'a1 Expr._ufundef
val remove_phi_nodes_fd : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Var0.funname -> 'a1 Expr._ufundef -> 'a1 Expr._ufundef
val stack_register_symbol : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Ident.Ident.ident
val global_static_data_symbol : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Ident.Ident.ident
val stackalloc : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> 'a1 Expr._uprog -> stack_alloc_oracles
val removereturn : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> 'a1 Expr._sprog -> Var0.funname -> bool list option
val regalloc : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> 'a1 Expr._sfun_decl list -> 'a1 Expr._sfun_decl list
val remove_wint_annot : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Var0.funname -> 'a1 Expr._ufundef -> 'a1 Expr._ufundef
val print_uprog : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> compiler_step -> 'a1 Expr._uprog -> 'a1 Expr._uprog
val print_sprog : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> compiler_step -> 'a1 Expr._sprog -> 'a1 Expr._sprog
val print_linear : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> compiler_step -> 'a1 Linear.lprog -> 'a1 Linear.lprog
val refresh_instr_info : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Var0.funname -> 'a1 Expr._ufundef -> 'a1 Expr._ufundef
val lowering_opt : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> 'a2
val fresh_id : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident
val fresh_var_ident : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Wsize.v_kind -> Expr.instr_info -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident
val slh_info : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> 'a1 Expr._uprog -> Var0.funname -> Slh_lowering.slh_t list * Slh_lowering.slh_t list
val stack_zero_info : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> Var0.funname -> (Stack_zero_strategy.stack_zero_strategy * Wsize.wsize option) option
val dead_vars_ufd : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> 'a1 Expr._ufun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t
val dead_vars_sfd : 'a1 Sopn.asmOp -> ('a1, 'a2) compiler_params -> 'a1 Expr._sfun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t
val split_live_ranges_prog : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr._uprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr._uprog
val renaming_prog : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr._uprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr._uprog
val remove_phi_nodes_prog : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr._uprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr._uprog
val var_tmp : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> Var0.Var.var
val var_tmp2 : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> Var0.Var.var
val var_tmps : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> Var0.SvExtra.Sv.t
val live_range_splitting : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog Compiler_util.cexec
val inlining : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> Var0.funname list -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog Compiler_util.cexec
val compiler_first_part : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> Var0.funname list -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog Compiler_util.cexec
val compiler_third_part : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> (Var0.funname -> Datatypes.nat option list option) -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.sprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.sprog Compiler_util.cexec
val wptr_status : Expr.var_i -> bool option
val allNone : 'a1 option list -> bool
val check_wf_ptr : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> Var0.funname list -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog -> (Var0.funname -> Stack_alloc.stk_alloc_oracle_t) -> unit Compiler_util.cexec
val compiler_front_end : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> Var0.funname list -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.sprog Compiler_util.cexec
val check_export : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> Var0.funname list -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.sprog -> unit Compiler_util.cexec
val compiler_back_end : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> Var0.funname list -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.sprog -> (Compiler_util.pp_error_loc, ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Linear.lprog) Utils0.result
val compiler_back_end_to_asm : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> Var0.funname list -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.sprog -> (Compiler_util.pp_error_loc, ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) Arch_decl.asm_prog) Utils0.result
val compile_prog_to_asm : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.calling_convention -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7, 'a8) Arch_params.architecture_params -> (('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op, 'a8) compiler_params -> Var0.funname list -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) Arch_extra.extended_op Expr.uprog -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) Arch_decl.asm_prog Compiler_util.cexec