Module Jasmin.Riscv_stack_zeroization
val sz_init :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Wsize.wsize ->
BinNums.coq_Z ->
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extended_op
Linear.lcmdval store_zero :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Wsize.wsize ->
Expr.var_i ->
BinNums.coq_Z ->
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extended_op
Linear.linstr_rval sz_loop :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Label.label ->
Wsize.wsize ->
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extended_op
Linear.lcmdval restore_sp :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extended_op
Linear.linstr
listval stack_zero_loop :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Label.label ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extended_op
Linear.lcmdval sz_unrolled :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Wsize.wsize ->
BinNums.coq_Z ->
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extended_op
Linear.lcmdval stack_zero_unrolled :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extended_op
Linear.lcmdval stack_zeroization_cmd :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Stack_zero_strategy.stack_zero_strategy ->
Ident.Ident.ident ->
Label.label ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extended_op
Linear.lcmd
* Var0.SvExtra.Sv.t)
Compiler_util.cexec