package jasmin
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 -> bool
val is_regx_l : Expr.lval -> bool
val vword : Wsize.wsize -> Ident.Ident.ident -> Var0.Var.var
val fv_of : Lowering.fresh_vars -> Var0.Var.var
val fv_cf : Lowering.fresh_vars -> Var0.Var.var
val fv_sf : Lowering.fresh_vars -> Var0.Var.var
val fv_zf : Lowering.fresh_vars -> Var0.Var.var
val fvars : Lowering.fresh_vars -> Var0.SvExtra.Sv.t
val disj_fvars : Lowering.fresh_vars -> Var0.SvExtra.Sv.t -> bool
val 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 ->
bool
val stype_of_lval : Expr.lval -> Type.stype
val wsize_of_stype : Type.stype -> Wsize.wsize
val wsize_of_lval : Expr.lval -> Wsize.wsize
val lower_cond_classify :
Lowering.fresh_vars ->
Expr.var_info ->
Expr.pexpr ->
((((Expr.lval list * Wsize.wsize) * Expr.pexpr) * Expr.pexpr) * Expr.pexpr)
option
val 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.pexpr
val add_inc_dec_classify :
Wsize.wsize ->
Expr.pexpr ->
Expr.pexpr ->
add_inc_dec
val sub_inc_dec_classify : Eqtype.Equality.sort -> Expr.pexpr -> sub_inc_dec
type 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 option
val is_lnot : Expr.pexpr -> Expr.pexpr option
val is_andn : Expr.pexpr -> Expr.pexpr -> (Expr.pexpr * Expr.pexpr) option
val mulr :
Wsize.wsize ->
Expr.pexpr ->
Expr.pexpr ->
X86_instr_decl.x86_op * Expr.pexpr list
val check_shift_amount : Wsize.wsize -> Expr.pexpr -> Expr.pexpr option
val check_signed_range :
Wsize.wsize option ->
Wsize.wsize ->
BinNums.coq_Z ->
bool
val 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_t
type 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_t
val 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.sopn
val 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
list
val reduce_wconst : Wsize.wsize -> Expr.pexpr -> Expr.pexpr
val 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
list
val 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)
option
val 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
list
val 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
list
val 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
list
val 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
list
val 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
list
val 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)"
>