package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.2.tar.bz2
sha256=aa0d21f532c1560a0939244cfd1c8414ba2b42c9d1403960f458500446cb1ebb
doc/jasmin.jasmin/Jasmin/Arm_params/index.html
Module Jasmin.Arm_params
val arm_mov_ofs :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.lval ->
Expr.assgn_tag ->
Stack_alloc_params.mov_kind ->
Expr.pexpr ->
Expr.pexpr ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Expr.instr_r
optionval arm_immediate :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
Arm_extra.arm_extended_op Expr.instr_rval arm_swap :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.assgn_tag ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Expr.instr_rval arm_saparams :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Stack_alloc_params.stack_alloc_paramsval arm_allocate_stack_frame :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i option ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list)
listval arm_free_stack_frame :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i option ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list)
listval arm_set_up_sp_register :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
Wsize.wsize ->
Expr.var_i ->
Expr.var_i ->
((Fexpr.lexpr list
* (Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Sopn.sopn)
* Fexpr.rexpr list)
listval arm_tmp2 :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.identval arm_lmove :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval arm_check_ws : Eqtype.Equality.sort -> boolval arm_lstore :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
Expr.var_i ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval arm_lload :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval arm_liparams :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Linearization.linearization_paramsval arm_fvars_correct :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Expr.progT ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Expr.fun_decl
list ->
boolval arm_loparams :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
((Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op,
Arm_lowering.lowering_options)
Arch_params.lowering_paramsval arm_shparams :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Slh_lowering.sh_paramsval condt_of_rflag : Arm_decl.rflag -> Arm_decl.condtval condt_not : Arm_decl.condt -> Arm_decl.condtval condt_and : Arm_decl.condt -> Arm_decl.condt -> Arm_decl.condt optionval condt_or : Arm_decl.condt -> Arm_decl.condt -> Arm_decl.condt optionval is_rflags_GE : Arm_decl.rflag -> Arm_decl.rflag -> boolval assemble_cond :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.instr_info ->
Fexpr.fexpr ->
Arm_decl.condt Compiler_util.cexecval is_valid_address :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_decl.reg_address ->
boolval arm_szparams :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Stack_zeroization.stack_zeroization_paramsval arm_is_move_op :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Sopn.asm_op_t ->
boolval arm_params :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op,
Arm_lowering.lowering_options)
Arch_params.architecture_params