Module Jasmin.X86_stack_zeroization
val loop_small_cmd :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.ident ->
Label.label ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linear.lcmdval loop_large_cmd :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.ident ->
Label.label ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linear.lcmdval x86_stack_zero_loop :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.ident ->
Label.label ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linear.lcmd
* Var0.SvExtra.Sv.tval x86_stack_zero_loopSCT :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.ident ->
Label.label ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linear.linstr
list
* Var0.SvExtra.Sv.tval unrolled_small_cmd :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.ident ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linear.lcmdval unrolled_large_cmd :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.ident ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linear.lcmdval x86_stack_zero_unrolled :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.ident ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linear.lcmd
* Var0.SvExtra.Sv.tval x86_stack_zero_cmd :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Stack_zero_strategy.stack_zero_strategy ->
Ident.Ident.ident ->
Label.label ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
((X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linear.lcmd
* Var0.SvExtra.Sv.t)
Compiler_util.cexec