Module Jasmin.Expr

type __ = Obj.t
val uint_of_word : Wsize.wsize -> Operators.sop1
val sint_of_word : Wsize.wsize -> Operators.sop1
val type_of_wiop1 : Operators.wiop1 -> Type.atype * Type.atype
val type_of_opk : Operators.op_kind -> Type.atype
val etype_of_opk : Operators.op_kind -> 'a1 Type.extended_type
val etype_of_op1 : Operators.sop1 -> 'a1 Type.extended_type * 'a1 Type.extended_type
val type_of_op1 : Operators.sop1 -> Type.atype * Type.atype
val type_of_op2 : Operators.sop2 -> (Type.atype * Type.atype) * Type.atype
val tin_combine_flags : Type.atype list
val type_of_opN : Operators.opN -> Type.atype list * Type.atype
module type TAG = sig ... end
module VarInfo : TAG
type var_info = Location.t
val dummy_var_info : var_info
type var_i = {
  1. v_var : Var0.Var.var;
  2. v_info : var_info;
}
val v_var : var_i -> Var0.Var.var
val v_info : var_i -> var_info
val mk_var_i : Var0.Var.var -> var_i
type v_scope =
  1. | Slocal
  2. | Sglob
type is_v_scope =
  1. | Coq_is_Slocal
  2. | Coq_is_Sglob
val v_scope_tag : v_scope -> BinNums.positive
val is_v_scope_inhab : v_scope -> is_v_scope
val is_v_scope_functor : v_scope -> is_v_scope -> is_v_scope
type box_v_scope_Slocal =
  1. | Box_v_scope_Slocal
type v_scope_fields_t = __
val v_scope_fields : v_scope -> v_scope_fields_t
val v_scope_construct : BinNums.positive -> v_scope_fields_t -> v_scope option
val v_scope_induction : 'a1 -> 'a1 -> v_scope -> is_v_scope -> 'a1
val v_scope_eqb_fields : (v_scope -> v_scope -> bool) -> BinNums.positive -> v_scope_fields_t -> v_scope_fields_t -> bool
val v_scope_eqb : v_scope -> v_scope -> bool
val v_scope_eqb_OK : v_scope -> v_scope -> Bool.reflect
val v_scope_eqb_OK_sumbool : v_scope -> v_scope -> bool
val coq_HB_unnamed_factory_1 : v_scope Eqtype.Coq_hasDecEq.axioms_
val expr_v_scope__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type gvar = {
  1. gv : var_i;
  2. gs : v_scope;
}
val gv : gvar -> var_i
val gs : gvar -> v_scope
val mk_gvar : var_i -> gvar
val mk_lvar : var_i -> gvar
val is_lvar : gvar -> bool
val is_glob : gvar -> bool
type pexpr =
  1. | Pconst of BinNums.coq_Z
  2. | Pbool of bool
  3. | Parr_init of Wsize.wsize * BinNums.positive
  4. | Pvar of gvar
  5. | Pget of Memory_model.aligned * Warray_.arr_access * Wsize.wsize * gvar * pexpr
  6. | Psub of Warray_.arr_access * Wsize.wsize * BinNums.positive * gvar * pexpr
  7. | Pload of Memory_model.aligned * Wsize.wsize * pexpr
  8. | Papp1 of Operators.sop1 * pexpr
  9. | Papp2 of Operators.sop2 * pexpr * pexpr
  10. | PappN of Operators.opN * pexpr list
  11. | Pif of Type.atype * pexpr * pexpr * pexpr
val coq_Plvar : var_i -> pexpr
val enot : pexpr -> pexpr
val eor : pexpr -> pexpr -> pexpr
val eand : pexpr -> pexpr -> pexpr
val eeq : pexpr -> pexpr -> pexpr
val eneq : pexpr -> pexpr -> pexpr
val eaddw : Wsize.wsize -> pexpr -> pexpr -> pexpr
val cf_of_condition : Operators.sop2 -> (Operators.combine_flags * Wsize.wsize) option
val pexpr_of_cf : Operators.combine_flags -> var_info -> Var0.Var.var list -> pexpr
val get_pvar : pexpr -> Var0.Var.var Utils0.exec
val get_lvar : lval -> Var0.Var.var Utils0.exec
val coq_Lnone_b : var_info -> lval
val var_info_of_lval : lval -> var_info
type dir =
  1. | UpTo
  2. | DownTo
type is_dir =
  1. | Coq_is_UpTo
  2. | Coq_is_DownTo
val dir_tag : dir -> BinNums.positive
val is_dir_inhab : dir -> is_dir
val is_dir_functor : dir -> is_dir -> is_dir
type box_dir_UpTo =
  1. | Box_dir_UpTo
type dir_fields_t = __
val dir_fields : dir -> dir_fields_t
val dir_construct : BinNums.positive -> dir_fields_t -> dir option
val dir_induction : 'a1 -> 'a1 -> dir -> is_dir -> 'a1
val dir_eqb_fields : (dir -> dir -> bool) -> BinNums.positive -> dir_fields_t -> dir_fields_t -> bool
val dir_eqb : dir -> dir -> bool
val dir_eqb_OK : dir -> dir -> Bool.reflect
val dir_eqb_OK_sumbool : dir -> dir -> bool
val coq_HB_unnamed_factory_3 : dir Eqtype.Coq_hasDecEq.axioms_
val expr_dir__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type range = (dir * pexpr) * pexpr
val wrange : dir -> BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z list
module type InstrInfoT = sig ... end
type instr_info = IInfo.t
val dummy_instr_info : instr_info
val ii_with_location : instr_info -> instr_info
val ii_is_inline : instr_info -> bool
val var_info_of_ii : instr_info -> var_info
type assgn_tag =
  1. | AT_none
  2. | AT_keep
  3. | AT_rename
  4. | AT_inline
  5. | AT_phinode
type is_assgn_tag =
  1. | Coq_is_AT_none
  2. | Coq_is_AT_keep
  3. | Coq_is_AT_rename
  4. | Coq_is_AT_inline
  5. | Coq_is_AT_phinode
val assgn_tag_tag : assgn_tag -> BinNums.positive
val is_assgn_tag_inhab : assgn_tag -> is_assgn_tag
val is_assgn_tag_functor : assgn_tag -> is_assgn_tag -> is_assgn_tag
type box_assgn_tag_AT_none =
  1. | Box_assgn_tag_AT_none
type assgn_tag_fields_t = __
val assgn_tag_fields : assgn_tag -> assgn_tag_fields_t
val assgn_tag_construct : BinNums.positive -> assgn_tag_fields_t -> assgn_tag option
val assgn_tag_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> assgn_tag -> is_assgn_tag -> 'a1
val assgn_tag_eqb_fields : (assgn_tag -> assgn_tag -> bool) -> BinNums.positive -> assgn_tag_fields_t -> assgn_tag_fields_t -> bool
val assgn_tag_eqb : assgn_tag -> assgn_tag -> bool
val assgn_tag_eqb_OK : assgn_tag -> assgn_tag -> Bool.reflect
val assgn_tag_eqb_OK_sumbool : assgn_tag -> assgn_tag -> bool
val coq_HB_unnamed_factory_5 : assgn_tag Eqtype.Coq_hasDecEq.axioms_
val expr_assgn_tag__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type align =
  1. | Align
  2. | NoAlign
type assertion = Utils0.assertion_label * pexpr
type assertions = assertion list
type 'asm_op instr_r =
  1. | Cassgn of lval * assgn_tag * Type.atype * pexpr
  2. | Copn of lval list * assgn_tag * 'asm_op Sopn.sopn * pexpr list
  3. | Csyscall of lval list * (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t * pexpr list
  4. | Cassert of assertion
  5. | Cif of pexpr * 'asm_op instr list * 'asm_op instr list
  6. | Cfor of var_i * range * 'asm_op instr list
  7. | Cwhile of align * 'asm_op instr list * pexpr * instr_info * 'asm_op instr list
  8. | Ccall of lval list * Var0.funname * pexpr list
and 'asm_op instr =
  1. | MkI of instr_info * 'asm_op instr_r
val cmd_rect_aux : 'a1 Sopn.asmOp -> 'a3 -> ('a1 instr -> 'a1 instr list -> 'a2 -> 'a3 -> 'a3) -> ('a1 instr -> 'a2) -> 'a1 instr list -> 'a3
val instr_Rect : 'a1 Sopn.asmOp -> ('a1 instr_r -> instr_info -> 'a2 -> 'a3) -> 'a4 -> ('a1 instr -> 'a1 instr list -> 'a3 -> 'a4 -> 'a4) -> (lval -> assgn_tag -> Type.atype -> pexpr -> 'a2) -> (lval list -> assgn_tag -> 'a1 Sopn.sopn -> pexpr list -> 'a2) -> (lval list -> (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t -> pexpr list -> 'a2) -> (assertion -> 'a2) -> (pexpr -> 'a1 instr list -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (var_i -> dir -> pexpr -> pexpr -> 'a1 instr list -> 'a4 -> 'a2) -> (align -> 'a1 instr list -> pexpr -> instr_info -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (lval list -> Var0.funname -> pexpr list -> 'a2) -> 'a1 instr -> 'a3
val instr_r_Rect : 'a1 Sopn.asmOp -> ('a1 instr_r -> instr_info -> 'a2 -> 'a3) -> 'a4 -> ('a1 instr -> 'a1 instr list -> 'a3 -> 'a4 -> 'a4) -> (lval -> assgn_tag -> Type.atype -> pexpr -> 'a2) -> (lval list -> assgn_tag -> 'a1 Sopn.sopn -> pexpr list -> 'a2) -> (lval list -> (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t -> pexpr list -> 'a2) -> (assertion -> 'a2) -> (pexpr -> 'a1 instr list -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (var_i -> dir -> pexpr -> pexpr -> 'a1 instr list -> 'a4 -> 'a2) -> (align -> 'a1 instr list -> pexpr -> instr_info -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (lval list -> Var0.funname -> pexpr list -> 'a2) -> 'a1 instr_r -> 'a2
val cmd_rect : 'a1 Sopn.asmOp -> ('a1 instr_r -> instr_info -> 'a2 -> 'a3) -> 'a4 -> ('a1 instr -> 'a1 instr list -> 'a3 -> 'a4 -> 'a4) -> (lval -> assgn_tag -> Type.atype -> pexpr -> 'a2) -> (lval list -> assgn_tag -> 'a1 Sopn.sopn -> pexpr list -> 'a2) -> (lval list -> (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t -> pexpr list -> 'a2) -> (assertion -> 'a2) -> (pexpr -> 'a1 instr list -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (var_i -> dir -> pexpr -> pexpr -> 'a1 instr list -> 'a4 -> 'a2) -> (align -> 'a1 instr list -> pexpr -> instr_info -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (lval list -> Var0.funname -> pexpr list -> 'a2) -> 'a1 instr list -> 'a4
module type FunInfoT = sig ... end
module FunInfo : FunInfoT
type fun_info = FInfo.t
val entry_info_of_fun_info : fun_info -> instr_info
val ret_info_of_fun_info : fun_info -> instr_info
type progT =
  1. | Build_progT
type extra_fun_t = __
type extra_prog_t = __
type extra_val_t = __
type ('asm_op, 'extra_fun_t) _fundef = {
  1. f_info : fun_info;
  2. f_tyin : Type.atype list;
  3. f_params : var_i list;
  4. f_body : 'asm_op instr list;
  5. f_tyout : Type.atype list;
  6. f_res : var_i list;
  7. f_extra : 'extra_fun_t;
}
val f_info : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> fun_info
val f_tyin : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> Type.atype list
val f_params : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> var_i list
val f_body : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> 'a1 instr list
val f_tyout : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> Type.atype list
val f_res : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> var_i list
val f_extra : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> 'a2
type ('asm_op, 'extra_fun_t) _fun_decl = Var0.funname * ('asm_op, 'extra_fun_t) _fundef
type ('asm_op, 'extra_fun_t, 'extra_prog_t) _prog = {
  1. p_funcs : ('asm_op, 'extra_fun_t) _fun_decl list;
  2. p_globs : Global.glob_decl list;
  3. p_extra : 'extra_prog_t;
}
val p_funcs : 'a1 Sopn.asmOp -> ('a1, 'a2, 'a3) _prog -> ('a1, 'a2) _fun_decl list
val p_globs : 'a1 Sopn.asmOp -> ('a1, 'a2, 'a3) _prog -> Global.glob_decl list
val p_extra : 'a1 Sopn.asmOp -> ('a1, 'a2, 'a3) _prog -> 'a3
type 'asm_op fundef = ('asm_op, extra_fun_t) _fundef
type function_signature = Type.atype list * Type.atype list
val signature_of_fundef : 'a1 Sopn.asmOp -> progT -> 'a1 fundef -> function_signature
type 'asm_op fun_decl = Var0.funname * 'asm_op fundef
type 'asm_op prog = ('asm_op, extra_fun_t, extra_prog_t) _prog
val coq_Build_prog : 'a1 Sopn.asmOp -> progT -> ('a1, extra_fun_t) _fun_decl list -> Global.glob_decl list -> extra_prog_t -> 'a1 prog
val progUnit : progT
type 'asm_op ufundef = 'asm_op fundef
type 'asm_op ufun_decl = 'asm_op fun_decl
type 'asm_op ufun_decls = 'asm_op fun_decl list
type 'asm_op uprog = 'asm_op prog
type 'asm_op _ufundef = ('asm_op, unit) _fundef
type 'asm_op _ufun_decl = ('asm_op, unit) _fun_decl
type 'asm_op _ufun_decls = ('asm_op, unit) _fun_decl list
type 'asm_op _uprog = ('asm_op, unit, unit) _prog
val to_uprog : 'a1 Sopn.asmOp -> 'a1 _uprog -> 'a1 uprog
type saved_stack =
  1. | SavedStackNone
  2. | SavedStackReg of Var0.Var.var
  3. | SavedStackStk of BinNums.coq_Z
val saved_stack_beq : saved_stack -> saved_stack -> bool
val saved_stack_eq_axiom : saved_stack Eqtype.eq_axiom
val coq_HB_unnamed_factory_7 : saved_stack Eqtype.Coq_hasDecEq.axioms_
val expr_saved_stack__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type return_address_location =
  1. | RAnone
  2. | RAreg of Var0.Var.var * Var0.Var.var option
  3. | RAstack of Var0.Var.var option * Var0.Var.var option * BinNums.coq_Z * Var0.Var.var option
val is_RAnone : return_address_location -> bool
val is_RAstack : return_address_location -> bool
val return_address_location_beq : return_address_location -> return_address_location -> bool
val return_address_location_eq_axiom : return_address_location Eqtype.eq_axiom
val expr_return_address_location__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type stk_fun_extra = {
  1. sf_align : Wsize.wsize;
  2. sf_stk_sz : BinNums.coq_Z;
  3. sf_stk_ioff : BinNums.coq_Z;
  4. sf_stk_extra_sz : BinNums.coq_Z;
  5. sf_stk_max : BinNums.coq_Z;
  6. sf_max_call_depth : BinNums.coq_Z;
  7. sf_to_save : (Var0.Var.var * BinNums.coq_Z) list;
  8. sf_save_stack : saved_stack;
  9. sf_return_address : return_address_location;
  10. sf_align_args : Wsize.wsize list;
}
val sf_align : stk_fun_extra -> Wsize.wsize
val sf_stk_sz : stk_fun_extra -> BinNums.coq_Z
val sf_stk_ioff : stk_fun_extra -> BinNums.coq_Z
val sf_stk_extra_sz : stk_fun_extra -> BinNums.coq_Z
val sf_stk_max : stk_fun_extra -> BinNums.coq_Z
val sf_max_call_depth : stk_fun_extra -> BinNums.coq_Z
val sf_to_save : stk_fun_extra -> (Var0.Var.var * BinNums.coq_Z) list
val sf_save_stack : stk_fun_extra -> saved_stack
val sf_return_address : stk_fun_extra -> return_address_location
val sf_align_args : stk_fun_extra -> Wsize.wsize list
type sprog_extra = {
  1. sp_rsp : Ident.Ident.ident;
  2. sp_rip : Ident.Ident.ident;
  3. sp_globs : Word0.word list;
  4. sp_glob_names : ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list;
}
val sp_globs : sprog_extra -> Word0.word list
val sp_glob_names : sprog_extra -> ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list
val progStack : Wsize.coq_PointerData -> progT
type 'asm_op sfundef = 'asm_op fundef
type 'asm_op sfun_decl = 'asm_op fun_decl
type 'asm_op sfun_decls = 'asm_op fun_decl list
type 'asm_op sprog = 'asm_op prog
type 'asm_op _sfundef = ('asm_op, stk_fun_extra) _fundef
type 'asm_op _sfun_decl = ('asm_op, stk_fun_extra) _fun_decl
type 'asm_op _sfun_decls = ('asm_op, stk_fun_extra) _fun_decl list
type 'asm_op _sprog = ('asm_op, stk_fun_extra, sprog_extra) _prog
val to_sprog : Wsize.coq_PointerData -> 'a1 Sopn.asmOp -> 'a1 _sprog -> 'a1 sprog
val with_body : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> 'a1 instr list -> ('a1, 'a2) _fundef
val is_const : pexpr -> BinNums.coq_Z option
val is_bool : pexpr -> bool option
val is_Papp2 : pexpr -> ((Operators.sop2 * pexpr) * pexpr) option
val is_Pload : pexpr -> bool
val is_load : pexpr -> bool
val is_array_init : pexpr -> bool
val cast_w : Wsize.wsize -> pexpr -> pexpr
val cast_ptr : Wsize.coq_PointerData -> pexpr -> pexpr
val eword_of_int : Wsize.wsize -> BinNums.coq_Z -> pexpr
val wconst : Wsize.wsize -> Word0.word -> pexpr
val is_wconst : Wsize.wsize -> pexpr -> Word0.word option
val is_wconst_of_size : Eqtype.Equality.sort -> pexpr -> BinNums.coq_Z option
val vrvs_rec : Var0.SvExtra.Sv.t -> lval list -> Var0.SvExtra.Sv.t
val vrv : lval -> Var0.SvExtra.Sv.t
val vrvs : lval list -> Var0.SvExtra.Sv.t
val lv_write_mem : lval -> bool
val write_i_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr_r -> Var0.SvExtra.Sv.t
val write_I_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr -> Var0.SvExtra.Sv.t
val write_i : 'a1 Sopn.asmOp -> 'a1 instr_r -> Var0.SvExtra.Sv.t
val write_I : 'a1 Sopn.asmOp -> 'a1 instr -> Var0.SvExtra.Sv.t
val write_c_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr list -> Var0.SvExtra.Sv.t
val write_c : 'a1 Sopn.asmOp -> 'a1 instr list -> Var0.SvExtra.Sv.t
val use_mem : pexpr -> bool
val read_gvar : gvar -> Var0.SvExtra.Sv.t
val read_e : pexpr -> Var0.SvExtra.Sv.t
val read_es_rec : Var0.SvExtra.Sv.t -> pexpr list -> Var0.SvExtra.Sv.t
val read_es : pexpr list -> Var0.SvExtra.Sv.t
val read_rv_rec : Var0.SvExtra.Sv.t -> lval -> Var0.SvExtra.Sv.t
val read_rv : lval -> Var0.SvExtra.Sv.t
val read_rvs_rec : Var0.SvExtra.Sv.t -> lval list -> Var0.SvExtra.Sv.t
val read_rvs : lval list -> Var0.SvExtra.Sv.t
val read_i_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr_r -> Var0.SvExtra.Sv.t
val read_I_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr -> Var0.SvExtra.Sv.t
val read_c_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr list -> Var0.SvExtra.Sv.t
val read_i : 'a1 Sopn.asmOp -> 'a1 instr_r -> Var0.SvExtra.Sv.t
val read_I : 'a1 Sopn.asmOp -> 'a1 instr -> Var0.SvExtra.Sv.t
val read_c : 'a1 Sopn.asmOp -> 'a1 instr list -> Var0.SvExtra.Sv.t
val vars_I : 'a1 Sopn.asmOp -> 'a1 instr -> Var0.SvExtra.Sv.t
val vars_c : 'a1 Sopn.asmOp -> 'a1 instr list -> Var0.SvExtra.Sv.t
val vars_lval : lval -> Var0.SvExtra.Sv.t
val vars_lvals : lval list -> Var0.SvExtra.Sv.t
val vars_l : var_i list -> Var0.SvExtra.Sv.t
val vars_fd : 'a1 Sopn.asmOp -> progT -> 'a1 fundef -> Var0.SvExtra.Sv.t
val vars_p : 'a1 Sopn.asmOp -> progT -> 'a1 fun_decl list -> Var0.SvExtra.Sv.t
val eq_gvar : gvar -> gvar -> bool
val eq_expr : pexpr -> pexpr -> bool
val to_lvals : Var0.Var.var list -> lval list
val is_false : pexpr -> bool
val is_zero : Eqtype.Equality.sort -> pexpr -> bool
val instr_of_copn_args : 'a1 Sopn.asmOp -> assgn_tag -> ((lval list * 'a1 Sopn.sopn) * pexpr list) -> 'a1 instr_r