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/X86_params/index.html
Module Jasmin.X86_params
val x86_op_align :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Wsize.wsize ->
Wsize.wsize ->
(Fexpr.lexpr list
* (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
Sopn.sopn)
* Fexpr.rexpr listval lea_ptr :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.lval ->
Expr.pexpr ->
Expr.assgn_tag ->
Expr.pexpr ->
(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
Expr.instr_rval x86_mov_ofs :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.lval ->
Expr.assgn_tag ->
Stack_alloc_params.mov_kind ->
Expr.pexpr ->
Expr.pexpr ->
(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
Expr.instr_r
optionval x86_immediate :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
X86_extra.x86_extended_op Expr.instr_rval x86_swap :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.assgn_tag ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
X86_extra.x86_extended_op Expr.instr_rval x86_saparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(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
Stack_alloc_params.stack_alloc_paramsval x86_allocate_stack_frame :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i option ->
BinNums.coq_Z ->
((Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr list)
listval x86_free_stack_frame :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i option ->
BinNums.coq_Z ->
((Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr list)
listval is_regx_e : Fexpr.rexpr -> boolval is_regx_l : Fexpr.lexpr -> boolval x86_lassign :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Fexpr.lexpr ->
Wsize.wsize ->
Fexpr.rexpr ->
(Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr listval x86_set_up_sp_register :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
Wsize.wsize ->
Expr.var_i ->
Expr.var_i ->
((Fexpr.lexpr list
* (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
Sopn.sopn)
* Fexpr.rexpr list)
listval x86_lmove :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Wsize.wsize ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr listval x86_check_ws : Wsize.wsize -> boolval x86_lstore :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Wsize.wsize ->
Expr.var_i ->
BinNums.coq_Z ->
Expr.var_i ->
(Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr listval x86_lload :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Wsize.wsize ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr listval x86_liparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(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
Linearization.linearization_paramsval x86_loparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(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
Arch_params.lowering_paramsval lflags : Expr.lval listval is_mmx_protect : Wsize.wsize -> Expr.lval list -> boolval x86_sh_lower :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.lval list ->
Slh_ops.slh_op ->
Expr.pexpr list ->
((Expr.lval list
* (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
Sopn.sopn)
* Expr.pexpr list)
optionval x86_shparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(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
Slh_lowering.sh_paramsval not_condt : X86_decl.condt -> X86_decl.condtval or_condt :
Expr.instr_info ->
Fexpr.fexpr ->
X86_decl.condt ->
X86_decl.condt ->
X86_decl.condt Compiler_util.cexecval and_condt :
Expr.instr_info ->
Fexpr.fexpr ->
X86_decl.condt ->
X86_decl.condt ->
(Compiler_util.pp_error_loc, X86_decl.condt) Utils0.resultval of_var_e_bool :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.instr_info ->
Expr.var_i ->
X86_decl.rflag Compiler_util.cexecval assemble_cond_r :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.instr_info ->
Fexpr.fexpr ->
X86_decl.condt Compiler_util.cexecval assemble_cond :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.instr_info ->
Fexpr.fexpr ->
X86_decl.condt Compiler_util.cexecval is_valid_address :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_decl.reg_address ->
boolval x86_agparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(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)
Asm_gen.asm_gen_paramsval x86_szparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(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
Stack_zeroization.stack_zeroization_paramsval x86_is_move_op :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(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
Sopn.asm_op_t ->
boolval x86_params :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(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_params.architecture_params