package jasmin
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa
doc/jasmin.jasmin/Jasmin/X86_lowering/index.html
Module Jasmin.X86_lowering
val is_regx_e : Expr.pexpr -> boolval is_regx_l : Expr.lval -> boolval vword : Wsize.wsize -> Ident.Ident.ident -> Var0.Var.varval fv_of : Lowering.fresh_vars -> Var0.Var.varval fv_cf : Lowering.fresh_vars -> Var0.Var.varval fv_sf : Lowering.fresh_vars -> Var0.Var.varval fv_zf : Lowering.fresh_vars -> Var0.Var.varval fvars : Lowering.fresh_vars -> Var0.SvExtra.Sv.tval disj_fvars : Lowering.fresh_vars -> Var0.SvExtra.Sv.t -> boolval fvars_correct :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Expr.progT ->
(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.fun_decl
list ->
boolval stype_of_lval : Expr.lval -> Type.stypeval wsize_of_stype : Type.stype -> Wsize.wsizeval wsize_of_lval : Expr.lval -> Wsize.wsizeval lower_cond_classify :
Lowering.fresh_vars ->
Expr.var_info ->
Expr.pexpr ->
((((Expr.lval list * Wsize.wsize) * Expr.pexpr) * Expr.pexpr) * Expr.pexpr)
optionval lower_condition :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Expr.var_info ->
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
list
* Expr.pexprval add_inc_dec_classify :
Wsize.wsize ->
Expr.pexpr ->
Expr.pexpr ->
add_inc_decval sub_inc_dec_classify : Eqtype.Equality.sort -> Expr.pexpr -> sub_inc_dectype lower_cassgn_t = | LowerMov of bool| LowerCopn of (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| LowerInc of (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| LowerLea of Wsize.wsize * Lea.lea| LowerFopn of Wsize.wsize * (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 * Wsize.wsize option| LowerDiscardFlags of Datatypes.nat * (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| LowerCond| LowerIf of Type.stype * Expr.pexpr * Expr.pexpr * Expr.pexpr| LowerDivMod of divmod_pos * Wsize.signedness * Wsize.wsize * (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 * Expr.pexpr| LowerConcat of Expr.pexpr * Expr.pexpr| LowerAssgn
val is_lea : Wsize.wsize -> Expr.lval -> Expr.pexpr -> Lea.lea optionval is_lnot : Expr.pexpr -> Expr.pexpr optionval is_andn : Expr.pexpr -> Expr.pexpr -> (Expr.pexpr * Expr.pexpr) optionval mulr :
Wsize.wsize ->
Expr.pexpr ->
Expr.pexpr ->
X86_instr_decl.x86_op * Expr.pexpr listval check_shift_amount : Wsize.wsize -> Expr.pexpr -> Expr.pexpr optionval check_signed_range :
Wsize.wsize option ->
Wsize.wsize ->
BinNums.coq_Z ->
boolval lower_cassgn_classify :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Eqtype.Equality.sort ->
Expr.pexpr ->
Expr.lval ->
lower_cassgn_ttype opn_5flags_cases_t = | Opn5f_large_immed of Expr.pexpr * Expr.pexpr * Expr.pexpr list| Opn5f_other
val opn_5flags_cases :
Expr.pexpr list ->
Wsize.wsize option ->
Wsize.wsize ->
opn_5flags_cases_tval opn_no_imm :
(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.sopn ->
(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.sopnval opn_5flags :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Wsize.wsize option ->
Wsize.wsize ->
Expr.var_info ->
Expr.lval ->
Expr.lval ->
Expr.assgn_tag ->
(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 ->
(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
listval reduce_wconst : Wsize.wsize -> Expr.pexpr -> Expr.pexprval lower_cassgn :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
lowering_options ->
(Expr.instr_info -> Compiler_util.warning_msg -> Expr.instr_info) ->
Lowering.fresh_vars ->
Expr.instr_info ->
Expr.lval ->
Expr.assgn_tag ->
Type.stype ->
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
listval lower_addcarry_classify :
bool ->
Expr.lval list ->
Expr.pexpr list ->
((((Expr.var_info * (Wsize.wsize -> X86_instr_decl.x86_op)) * Expr.pexpr list)
* Expr.lval)
* Expr.lval)
optionval lower_addcarry :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Wsize.wsize ->
bool ->
Expr.lval list ->
Expr.assgn_tag ->
Expr.pexpr 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
Expr.instr_r
listval lower_mulu :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Wsize.wsize ->
Expr.lval list ->
Expr.assgn_tag ->
Expr.pexpr 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
Expr.instr_r
listval lower_swap :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Type.stype ->
Expr.lval list ->
Expr.assgn_tag ->
Expr.pexpr 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
Expr.instr_r
listval lower_pseudo_operator :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Expr.lval list ->
Expr.assgn_tag ->
Pseudo_operator.pseudo_operator ->
Expr.pexpr 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
Expr.instr_r
listval lower_copn :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Lowering.fresh_vars ->
Expr.lval list ->
Expr.assgn_tag ->
(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 ->
(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
listval lower_i :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
lowering_options ->
(Expr.instr_info -> Compiler_util.warning_msg -> Expr.instr_info) ->
Lowering.fresh_vars ->
(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 ->
(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
list sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>