package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2026.03.0.tar.bz2
sha256=dec62a3cd0cd42cfe96ec64b3cd3961e0e8a09fb92ceb64175cffb54fde50e40
doc/jasmin.jasmin/Jasmin/Allocation/index.html
Module Jasmin.Allocation
module E : sig ... endmodule M : sig ... endval alloc_error : string -> Compiler_util.pp_error_locval cerr_varalloc :
Var0.Var.var ->
Var0.Var.var ->
string ->
Compiler_util.pp_error_locval check_v :
Sem_type.coq_WithSubWord ->
Expr.var_i ->
Expr.var_i ->
M.t ->
M.t Compiler_util.cexecval error_e : Compiler_util.pp_error_locval check_gv :
Sem_type.coq_WithSubWord ->
Expr.gvar ->
Expr.gvar ->
M.t ->
M.t Compiler_util.cexecval check_e :
Sem_type.coq_WithSubWord ->
Expr.pexpr ->
Expr.pexpr ->
M.t ->
M.t Compiler_util.cexecval check_var_aux :
Sem_type.coq_WithSubWord ->
Var0.Var.var ->
Var0.Var.var ->
M.t_ ->
M.t Compiler_util.cexecval check_varc :
Sem_type.coq_WithSubWord ->
Expr.var_i ->
Expr.var_i ->
M.t_ ->
M.t Compiler_util.cexecval is_Pvar :
(Type.atype * Expr.pexpr) option ->
(Type.atype * Expr.var_i) optionval error_lv : Compiler_util.pp_error_locval check_lval :
Sem_type.coq_WithSubWord ->
(Type.atype * Expr.pexpr) option ->
Expr.lval ->
Expr.lval ->
M.t ->
M.t Compiler_util.cexecval loop :
Sem_type.coq_WithSubWord ->
(M.t -> M.t Compiler_util.cexec) ->
Datatypes.nat ->
M.t ->
(Compiler_util.pp_error_loc, M.t) Utils0.resultval loop2 :
Sem_type.coq_WithSubWord ->
(M.t -> (M.t * M.t) Compiler_util.cexec) ->
Datatypes.nat ->
M.t ->
(Compiler_util.pp_error_loc, M.t) Utils0.resultval check_es :
Sem_type.coq_WithSubWord ->
Expr.pexpr list ->
Expr.pexpr list ->
M.t ->
(Compiler_util.pp_error_loc, M.t) Utils0.resultval check_lvals :
Sem_type.coq_WithSubWord ->
Expr.lval list ->
Expr.lval list ->
M.t ->
(Compiler_util.pp_error_loc, M.t) Utils0.resultval check_var :
Sem_type.coq_WithSubWord ->
Expr.var_i ->
Expr.var_i ->
M.t ->
M.t Compiler_util.cexecval check_vars :
Sem_type.coq_WithSubWord ->
Expr.var_i list ->
Expr.var_i list ->
M.t ->
(Compiler_util.pp_error_loc, M.t) Utils0.resultval check_I :
Sem_type.coq_WithSubWord ->
'a1 Sopn.asmOp ->
(Expr.instr_info -> Var0.SvExtra.Sv.t) ->
'a1 Expr.instr ->
'a1 Expr.instr ->
M.t_ ->
(Compiler_util.pp_error_loc, M.t_) Utils0.resultval check_cmd :
Sem_type.coq_WithSubWord ->
'a1 Sopn.asmOp ->
(Expr.instr_info -> Var0.SvExtra.Sv.t) ->
'a1 Expr.instr list ->
'a1 Expr.instr list ->
M.t_ ->
(Compiler_util.pp_error_loc, M.t_) Utils0.resultval check_fundef :
Sem_type.coq_WithSubWord ->
'a1 Sopn.asmOp ->
Expr.progT ->
(Expr.extra_fun_t ->
Expr.extra_prog_t ->
Expr.extra_prog_t ->
M.t Compiler_util.cexec) ->
(M.t ->
Expr.extra_fun_t ->
Expr.extra_fun_t ->
Expr.var_i list ->
Expr.var_i list ->
M.t Compiler_util.cexec) ->
('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
Expr.extra_prog_t ->
Expr.extra_prog_t ->
(Var0.funname * 'a1 Expr.fundef) ->
(Var0.funname * 'a1 Expr.fundef) ->
unit ->
unit Compiler_util.cexecval check_prog_error : Compiler_util.pp_error_locval check_prog :
Sem_type.coq_WithSubWord ->
'a1 Sopn.asmOp ->
Expr.progT ->
(Expr.extra_fun_t ->
Expr.extra_prog_t ->
Expr.extra_prog_t ->
M.t Compiler_util.cexec) ->
(M.t ->
Expr.extra_fun_t ->
Expr.extra_fun_t ->
Expr.var_i list ->
Expr.var_i list ->
M.t Compiler_util.cexec) ->
('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
Expr.extra_prog_t ->
(Var0.funname * 'a1 Expr.fundef) list ->
Expr.extra_prog_t ->
(Var0.funname * 'a1 Expr.fundef) list ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval init_alloc_uprog :
Sem_type.coq_WithSubWord ->
Expr.extra_fun_t ->
Expr.extra_prog_t ->
Expr.extra_prog_t ->
M.t Compiler_util.cexecval check_f_extra_u :
Sem_type.coq_WithSubWord ->
M.t ->
Expr.extra_fun_t ->
Expr.extra_fun_t ->
Expr.var_i list ->
Expr.var_i list ->
(Compiler_util.pp_error_loc, M.t) Utils0.resultval check_ufundef :
Sem_type.coq_WithSubWord ->
'a1 Sopn.asmOp ->
('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
Expr.extra_prog_t ->
Expr.extra_prog_t ->
(Var0.funname * 'a1 Expr.fundef) ->
(Var0.funname * 'a1 Expr.fundef) ->
unit ->
unit Compiler_util.cexecval check_uprog :
Sem_type.coq_WithSubWord ->
'a1 Sopn.asmOp ->
('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
Expr.extra_prog_t ->
(Var0.funname * 'a1 Expr.fundef) list ->
Expr.extra_prog_t ->
(Var0.funname * 'a1 Expr.fundef) list ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval init_alloc_sprog :
Sem_type.coq_WithSubWord ->
Wsize.coq_PointerData ->
Expr.extra_fun_t ->
Expr.extra_prog_t ->
Expr.extra_prog_t ->
M.t Compiler_util.cexecval check_f_extra_s :
Sem_type.coq_WithSubWord ->
Wsize.coq_PointerData ->
M.t ->
Expr.extra_fun_t ->
Expr.extra_fun_t ->
Expr.var_i list ->
Expr.var_i list ->
M.t Compiler_util.cexecval check_sprog :
Sem_type.coq_WithSubWord ->
'a1 Sopn.asmOp ->
Wsize.coq_PointerData ->
('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
Expr.extra_prog_t ->
(Var0.funname * 'a1 Expr.fundef) list ->
Expr.extra_prog_t ->
(Var0.funname * 'a1 Expr.fundef) list ->
(Compiler_util.pp_error_loc, unit) Utils0.result