package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Stack_alloc

type __ = Obj.t
module E : sig ... end
val size_of : Type.stype -> BinNums.coq_Z
type slot = Var0.Var.var
type region = {
  1. r_slot : slot;
  2. r_align : Wsize.wsize;
  3. r_writable : bool;
}
val region_beq : region -> region -> bool
val region_same : region -> region -> bool
val region_axiom : region Eqtype.eq_axiom
val coq_HB_unnamed_factory_1 : region Eqtype.Coq_hasDecEq.axioms_
val stack_alloc_region__canonical__eqtype_Equality : Eqtype.Equality.coq_type
module CmpR : sig ... end
module Mr : sig ... end
type sexpr =
  1. | Sconst of BinNums.coq_Z
  2. | Svar of Var0.Var.var
  3. | Sof_int of Wsize.wsize * sexpr
  4. | Sto_int of Wsize.signedness * Wsize.wsize * sexpr
  5. | Sneg of Expr.op_kind * sexpr
  6. | Sadd of Expr.op_kind * sexpr * sexpr
  7. | Smul of Expr.op_kind * sexpr * sexpr
  8. | Ssub of Expr.op_kind * sexpr * sexpr
val sexpr_beq : sexpr -> sexpr -> bool
val sexpr_eq_axiom : sexpr Eqtype.eq_axiom
val coq_HB_unnamed_factory_3 : sexpr Eqtype.Coq_hasDecEq.axioms_
val stack_alloc_sexpr__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val is_const : sexpr -> BinNums.coq_Z option
type symbolic_slice = {
  1. ss_ofs : sexpr;
  2. ss_len : sexpr;
}
val symbolic_slice_beq : symbolic_slice -> symbolic_slice -> bool
val symbolic_slice_eq_axiom : symbolic_slice Eqtype.eq_axiom
val coq_HB_unnamed_factory_5 : symbolic_slice Eqtype.Coq_hasDecEq.axioms_
val stack_alloc_symbolic_slice__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type symbolic_zone = symbolic_slice list
type sub_region = {
  1. sr_region : region;
  2. sr_zone : symbolic_zone;
}
val sub_region_beq : sub_region -> sub_region -> bool
val sub_region_eq_axiom : sub_region Eqtype.eq_axiom
val coq_HB_unnamed_factory_7 : sub_region Eqtype.Coq_hasDecEq.axioms_
val stack_alloc_sub_region__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type intervals = symbolic_slice list
val symbolic_slice_ble : symbolic_slice -> symbolic_slice -> bool option
val disjoint_slices : symbolic_slice -> symbolic_slice -> bool
val get_sub_interval : intervals -> Eqtype.Equality.sort -> bool
val add_sub_interval : intervals -> symbolic_slice -> intervals option
val remove_sub_interval : intervals -> Eqtype.Equality.sort -> intervals
type status =
  1. | Valid
  2. | Unknown
  3. | Borrowed of intervals
type status_map = status Var0.Mvar.t
type region_map = {
  1. var_region : sub_region Var0.Mvar.t;
  2. region_var : status_map Mr.t;
}
val empty_status_map : status Var0.Mvar.t
val empty : region_map
val get_status_map : status Var0.Mvar.t Mr.t -> region -> status_map
val get_status : status_map -> Eqtype.Equality.sort -> status
type concrete_slice = {
  1. cs_ofs : BinNums.coq_Z;
  2. cs_len : BinNums.coq_Z;
}
type ptr_kind_init =
  1. | PIdirect of Var0.Var.var * concrete_slice * Expr.v_scope
  2. | PIregptr of Var0.Var.var
  3. | PIstkptr of Var0.Var.var * concrete_slice * Var0.Var.var
type vptr_kind =
  1. | VKglob of BinNums.coq_Z * Wsize.wsize
  2. | VKptr of ptr_kind
type pos_map = {
  1. vrip : Var0.Var.var;
  2. vrsp : Var0.Var.var;
  3. vxlen : Var0.Var.var;
  4. globals : (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t;
  5. locals : ptr_kind Var0.Mvar.t;
  6. vnew : Var0.SvExtra.Sv.t;
}
type param_info = {
  1. pp_ptr : Var0.Var.var;
  2. pp_writable : bool;
  3. pp_align : Wsize.wsize;
}
val divide_z : BinNums.coq_Z -> Wsize.wsize -> bool
val divide : sexpr -> Wsize.wsize -> bool
val divide_zone : symbolic_slice list -> Wsize.wsize -> bool
val check_writable : Expr.var_i -> region -> (Compiler_util.pp_error_loc, unit) Utils0.result
val is_valid : status -> bool
val split_last : symbolic_slice list -> symbolic_slice list * symbolic_slice
val sub_zone_at_ofs : symbolic_zone -> sexpr -> sexpr -> symbolic_slice list
val sub_region_at_ofs : sub_region -> sexpr -> sexpr -> sub_region
val get_sub_status : status -> Eqtype.Equality.sort -> bool
val get_suffix : symbolic_zone -> symbolic_zone -> symbolic_zone option option
val fill_status : status -> symbolic_slice -> status
val clear_status : status -> symbolic_zone -> status option
val clear_status_map_aux : region_map -> symbolic_zone -> Eqtype.Equality.sort -> status -> status option
val clear_status_map : region_map -> symbolic_zone -> status_map -> status Var0.Mvar.t
val set_clear_status : region_map -> sub_region -> status_map Mr.Map.t
val set_clear_pure : region_map -> sub_region -> region_map
val is_unknown : status -> bool
val zone_of_cs : concrete_slice -> symbolic_zone
val sub_region_stkptr : slot -> Wsize.wsize -> concrete_slice -> sub_region
val check_stack_ptr : status Var0.Mvar.t Mr.t -> slot -> Wsize.wsize -> concrete_slice -> Eqtype.Equality.sort -> bool
val sub_region_full : Var0.Var.var -> region -> sub_region
val sub_region_glob : slot -> Wsize.wsize -> sub_region
type table = {
  1. bindings : sexpr Var0.Mvar.t;
  2. counter : Uint63.t;
  3. vars : Var0.SvExtra.Sv.t;
}
val merge_table : table -> table -> table
val symbolic_of_pexpr : (Var0.Var.var -> Uint63.t -> Var0.Var.var) -> table -> Expr.pexpr -> (table * sexpr) option Compiler_util.cexec
val remove_binding : table -> Eqtype.Equality.sort -> table
val remove_binding_lval : table -> Expr.lval -> table
val remove_binding_lvals : table -> Expr.lval list -> table
val table_set_var : table -> Eqtype.Equality.sort -> sexpr -> table
val update_table : table -> Expr.lval -> sexpr option -> table
val assert_check : bool -> bool -> 'a1 -> ('a1, unit) Utils0.result
val mk_ofs_int : Warray_.arr_access -> Wsize.wsize -> sexpr -> sexpr
val get_local : pos_map -> Var0.Var.var -> ptr_kind option
val with_var : Expr.var_i -> Var0.Var.var -> Expr.var_i
val base_ptr : pos_map -> Expr.v_scope -> Var0.Var.var
val bad_arg_number : Compiler_util.pp_error_loc
val not_trivially_incorrect : Warray_.arr_access -> Wsize.wsize -> Expr.pexpr -> BinNums.coq_Z -> bool
val sub_region_direct : slot -> Wsize.wsize -> concrete_slice -> Eqtype.Equality.sort -> sub_region
val sub_region_stack : slot -> Wsize.wsize -> concrete_slice -> sub_region
val nop : 'a1 Sopn.asmOp -> 'a1 Expr.instr_r
val is_stack_ptr : vptr_kind -> ((((Var0.Var.var * BinNums.coq_Z) * Wsize.wsize) * concrete_slice) * Var0.Var.var) option
val regions_are_not_equal : (sub_region -> Compiler_util.pp_error) -> string -> Expr.var_i -> sub_region -> sub_region -> Compiler_util.pp_error_loc
val is_protect_ptr_fail : 'a1 Sopn.asmOp -> Expr.lval list -> 'a1 Sopn.sopn -> Expr.pexpr list -> ((Expr.lval * Expr.pexpr) * Expr.pexpr) option
val bad_lval_number : Compiler_util.pp_error_loc
val incl_interval : intervals -> intervals -> bool
val incl_status : status -> status -> bool
val incl_status_map : status_map -> status_map -> bool
val incl : region_map -> region_map -> bool
val type_of_op_kind : Expr.op_kind -> Type.stype
val typecheck_slice : symbolic_slice -> bool
val merge_interval : intervals -> intervals -> intervals option
val read_e : sexpr -> Var0.SvExtra.Sv.t
val read_slice : symbolic_slice -> Var0.SvExtra.Sv.t
val merge_status : Var0.SvExtra.Sv.t -> Var0.Var.var -> status option -> status option -> status option
val merge_status_map : Var0.SvExtra.Sv.t -> region -> status_map option -> status_map option -> status Var0.Mvar.t option
val incl_table : table -> table -> bool
val loop2 : 'a1 Sopn.asmOp -> Expr.instr_info -> (table -> region_map -> (((table * region_map) * (table * region_map)) * ((Expr.pexpr * 'a1 Expr.instr list list) * 'a1 Expr.instr list list)) Compiler_util.cexec) -> Datatypes.nat -> table -> region_map -> (Compiler_util.pp_error_loc, (table * region_map) * ((Expr.pexpr * 'a1 Expr.instr list list) * 'a1 Expr.instr list list)) Utils0.result
type stk_alloc_oracle_t = {
  1. sao_align : Wsize.wsize;
  2. sao_size : BinNums.coq_Z;
  3. sao_ioff : BinNums.coq_Z;
  4. sao_extra_size : BinNums.coq_Z;
  5. sao_max_size : BinNums.coq_Z;
  6. sao_max_call_depth : BinNums.coq_Z;
  7. sao_params : param_info option list;
  8. sao_return : Datatypes.nat option list;
  9. sao_slots : ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list;
  10. sao_alloc : (Var0.Var.var * ptr_kind_init) list;
  11. sao_to_save : (Var0.Var.var * BinNums.coq_Z) list;
  12. sao_rsp : Expr.saved_stack;
  13. sao_return_address : Expr.return_address_location;
}
val sao_frame_size : stk_alloc_oracle_t -> BinNums.coq_Z
val alloc_call_arg_aux : pos_map -> region_map -> region_map -> param_info option -> Expr.pexpr -> (Compiler_util.pp_error_loc, region_map * ((bool * sub_region) option * Expr.pexpr)) Utils0.result
val alloc_call_args_aux : pos_map -> region_map -> param_info option list -> Expr.pexpr list -> (Compiler_util.pp_error_loc, region_map * ((bool * sub_region) option * Expr.pexpr) list) Utils0.result
val disjoint_zones : Eqtype.Equality.sort list -> Eqtype.Equality.sort list -> bool
val disj_sub_regions : sub_region -> sub_region -> bool
val check_all_disj : sub_region list -> sub_region list -> ((bool * sub_region) option * Expr.pexpr) list -> bool
val alloc_call_args : pos_map -> region_map -> Var0.funname -> param_info option list -> Expr.pexpr list -> (Compiler_util.pp_error_loc, region_map * ((bool * sub_region) option * Expr.pexpr) list) Utils0.result
val check_lval_reg_call : pos_map -> Expr.lval -> (Compiler_util.pp_error_loc, unit) Utils0.result
val alloc_call_res : Wsize.coq_PointerData -> pos_map -> region_map -> ((bool * sub_region) option * Expr.pexpr) list -> Datatypes.nat option list -> Expr.lval list -> (Compiler_util.pp_error_loc, region_map * Expr.lval list) Utils0.result
val is_swap_array : 'a1 Sopn.asmOp -> 'a1 Sopn.sopn -> bool
val check_all_writable_regions_returned : sub_region option list -> Datatypes.nat option list -> bool
val check_results : pos_map -> region_map -> Eqtype.Equality.sort option list -> Expr.var_i list -> Datatypes.nat option list -> Expr.var_i list -> (Compiler_util.pp_error_loc, Expr.var_i list) Utils0.result
val fresh_reg : (Wsize.v_kind -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident) -> string -> Type.stype -> Ident.Ident.ident
val ptake : BinNums.positive -> 'a1 list -> 'a1 list -> ('a1 list * 'a1 list) option
val ztake : BinNums.coq_Z -> 'a1 list -> ('a1 list * 'a1 list) option
val size_glob : Global.glob_value -> BinNums.coq_Z