package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2026.09.0.tar.bz2
sha256=11fec571efb9f7b3a47fea324b4e2a68289e0b73b2248d237eccf139b5218190
doc/jasmin.jasmin/Jasmin/Armv8a_params/index.html
Module Jasmin.Armv8a_params
val to_opn :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
((Fexpr.lexpr list
* (Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op)
Arch_decl.asm_op_t')
* Fexpr.rexpr list) ->
(Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr listval coq_ARMv8AFopn_mov :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr listval coq_ARMv8AFopn_addi :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr listval coq_ARMv8AFopn_subi :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr listval coq_ARMv8AFopn_align :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
Wsize.wsize ->
(Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr listval coq_ARMv8AFopn_smart_addi :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr list)
listval coq_ARMv8AFopn_smart_subi :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr list)
listval coq_ARMv8AFopn_smart_addi_tmp :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr list)
listval coq_ARMv8AFopn_smart_subi_tmp :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr list)
listval armv8a_mov_ofs :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.lval ->
Expr.assgn_tag ->
Stack_alloc_params.mov_kind ->
Expr.pexpr ->
Expr.pexpr ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Expr.instr_r
optionval armv8a_immediate :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
((Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op)
Arch_decl.asm_op_t',
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op_gen
Expr.instr_rval armv8a_swap :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.assgn_tag ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
((Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op)
Arch_decl.asm_op_t',
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op_gen
Expr.instr_rval armv8a_saparams :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Stack_alloc_params.stack_alloc_paramsval armv8a_allocate_stack_frame :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i option ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr list)
listval armv8a_free_stack_frame :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i option ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr list)
listval armv8a_set_up_sp_register :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
Wsize.wsize ->
Expr.var_i ->
Expr.var_i ->
((Fexpr.lexpr list
* (Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Sopn.sopn)
* Fexpr.rexpr list)
listval armv8a_tmp :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.identval armv8a_tmp2 :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Ident.Ident.identval armv8a_lmove :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Wsize.wsize ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr listval armv8a_check_ws : Eqtype.Equality.sort -> boolval armv8a_lstore :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Wsize.wsize ->
Expr.var_i ->
BinNums.coq_Z ->
Expr.var_i ->
(Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr listval armv8a_lload :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Wsize.wsize ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
* Fexpr.rexpr listval armv8a_lloads :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
(Var0.Var.var * BinNums.coq_Z) list ->
BinNums.coq_Z ->
((Fexpr.lexpr list
* (Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Sopn.sopn)
* Fexpr.rexpr list)
listval armv8a_liparams :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Linearization.linearization_paramsval armv8a_fvars_correct :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Expr.progT ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Expr.fun_decl
list ->
boolval armv8a_loparams :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Arch_params.lowering_paramsval armv8a_shparams :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Slh_lowering.sh_paramsval condt_of_rflag : Arm_common.rflag -> Arm_common.condtval condt_not : Arm_common.condt -> Arm_common.condtval condt_and : Arm_common.condt -> Arm_common.condt -> Arm_common.condt optionval condt_or : Arm_common.condt -> Arm_common.condt -> Arm_common.condt optionval is_rflags_GE : Arm_common.rflag -> Arm_common.rflag -> boolval assemble_cond :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
Expr.instr_info ->
Fexpr.fexpr ->
Arm_common.condt Compiler_util.cexecval is_valid_address :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_decl.reg_address ->
boolval armv8a_agparams :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Asm_gen.asm_gen_paramsval armv8a_szparams :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Stack_zeroization.stack_zeroization_paramsval armv8a_is_move_op :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_extra.extended_op
Sopn.asm_op_t ->
boolval armv8a_params :
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt)
Arch_extra.arch_toIdent ->
(Armv8a_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_common.rflag,
Arm_common.condt,
Armv8a_instr_decl.armv8a_asm_op,
Armv8a_extra.armv8a_extra_op)
Arch_params.architecture_params