package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.3.tar.bz2
sha256=e7aafd891eb54e89d41d9d7d1bbda9ddb1cddc5fdf0359d88c2b7b417ae4a39b
doc/jasmin.jasmin/Jasmin/Remove_globals/index.html
Module Jasmin.Remove_globals
module E : sig ... endval check_data :
Global.glob_value ->
Wsize.wsize ->
Ssralg.GRing.ComRing.sort ->
boolval find_glob :
Expr.instr_info ->
Expr.var_i ->
Global.glob_decl list ->
Wsize.wsize ->
Ssralg.GRing.ComRing.sort ->
(Compiler_util.pp_error_loc, Var0.Var.var) Utils0.resultval add_glob :
(Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
Expr.instr_info ->
Var0.Var.var ->
Global.glob_decl list ->
Wsize.wsize ->
Ssralg.GRing.ComRing.sort ->
(Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.resultval extend_glob_i :
'a1 Sopn.asmOp ->
(Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
'a1 Expr.instr ->
Global.glob_decl list ->
(Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.resultval extend_glob_prog :
'a1 Sopn.asmOp ->
(Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
'a1 Expr.uprog ->
(Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.resultval get_var_ :
Expr.instr_info ->
Var0.Var.var Var0.Mvar.t ->
Expr.gvar ->
(Compiler_util.pp_error_loc, Expr.gvar) Utils0.resultval remove_glob_e :
Expr.instr_info ->
Var0.Var.var Var0.Mvar.t ->
Expr.pexpr ->
(Compiler_util.pp_error_loc, Expr.pexpr) Utils0.resultval remove_glob_lv :
Expr.instr_info ->
Var0.Var.var Var0.Mvar.t ->
Expr.lval ->
(Compiler_util.pp_error_loc, Expr.lval) Utils0.resultval remove_glob :
'a1 Sopn.asmOp ->
(Var0.Var.var Var0.Mvar.t ->
'a1 Expr.instr ->
(Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec) ->
Var0.Var.var Var0.Mvar.t ->
'a1 Expr.instr list ->
(Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexecval merge_glob :
Var0.Var.var ->
Var0.Var.var option ->
Var0.Var.var option ->
Var0.Var.var optionval coq_Mincl : Var0.Var.var Var0.Mvar.t -> Var0.Var.var Var0.Mvar.t -> boolval merge_env :
Var0.Var.var Var0.Mvar.t ->
Var0.Var.var Var0.Mvar.t ->
Var0.Var.var Var0.Mvar.tval loop :
'a1 Sopn.asmOp ->
(Var0.Var.var Var0.Mvar.t ->
(Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec) ->
Datatypes.nat ->
Var0.Var.var Var0.Mvar.t ->
(Compiler_util.pp_error_loc, Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list)
Utils0.resulttype 'asm_op check2_r = | Check2_r of Expr.pexpr * Var0.Var.var Var0.Mvar.t * 'asm_op Expr.instr list * Var0.Var.var Var0.Mvar.t * 'asm_op Expr.instr list
type 'asm_op loop2_r = | Loop2_r of Expr.pexpr * 'asm_op Expr.instr list * 'asm_op Expr.instr list * Var0.Var.var Var0.Mvar.t
val loop2 :
'a1 Sopn.asmOp ->
(Var0.Var.var Var0.Mvar.t -> 'a1 check2_r Compiler_util.cexec) ->
Datatypes.nat ->
Var0.Var.var Var0.Mvar.t ->
(Compiler_util.pp_error_loc, 'a1 loop2_r) Utils0.resultval remove_glob_i :
'a1 Sopn.asmOp ->
Global.glob_decl list ->
Var0.Var.var Var0.Mvar.t ->
'a1 Expr.instr ->
(Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexecval remove_glob_fundef :
'a1 Sopn.asmOp ->
Global.glob_decl list ->
'a1 Expr.ufundef ->
(Compiler_util.pp_error_loc, ('a1, Expr.extra_fun_t) Expr._fundef)
Utils0.resultval remove_glob_prog :
'a1 Sopn.asmOp ->
(Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
'a1 Expr.uprog ->
(Compiler_util.pp_error_loc,
('a1, Expr.extra_fun_t, Expr.extra_prog_t) Expr._prog)
Utils0.result