Module Jasmin.X86_lowering

val is_regx_e : Expr.pexpr -> bool
val is_regx_l : Expr.lval -> bool
type lowering_options = {
  1. use_lea : bool;
  2. use_set0 : bool;
}
val disj_fvars : Lowering.fresh_vars -> Var0.SvExtra.Sv.t -> 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
type add_inc_dec =
  1. | AddInc of Expr.pexpr
  2. | AddDec of Expr.pexpr
  3. | AddNone
val add_inc_dec_classify : Wsize.wsize -> Expr.pexpr -> Expr.pexpr -> add_inc_dec
type sub_inc_dec =
  1. | SubInc
  2. | SubDec
  3. | SubNone
val sub_inc_dec_classify : Eqtype.Equality.sort -> Expr.pexpr -> sub_inc_dec
type divmod_pos =
  1. | DM_Fst
  2. | DM_Snd
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 check_shift_amount : Wsize.wsize -> Expr.pexpr -> Expr.pexpr option
val check_signed_range : Wsize.wsize option -> Wsize.wsize -> BinNums.coq_Z -> bool
type opn_5flags_cases_t =
  1. | Opn5f_large_immed of Expr.pexpr * Expr.pexpr * Expr.pexpr list
  2. | Opn5f_other
val opn_5flags_cases : Expr.pexpr list -> Wsize.wsize option -> Wsize.wsize -> opn_5flags_cases_t
val reduce_wconst : Wsize.wsize -> Expr.pexpr -> Expr.pexpr
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