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 = {

r_slot : slot;
r_align : Wsize.wsize;
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 =

| Sconst of BinNums.coq_Z
| Svar of Var0.Var.var
| Sof_int of Wsize.wsize * sexpr
| Sto_int of Wsize.signedness * Wsize.wsize * sexpr
| Sneg of Expr.op_kind * sexpr
| Sadd of Expr.op_kind * sexpr * sexpr
| Smul of Expr.op_kind * sexpr * sexpr
| 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 = {

ss_ofs : sexpr;
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 = {

sr_region : region;
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 =

| Valid
| Unknown
| Borrowed of intervals

type status_map = status Var0.Mvar.t

type region_map = {

var_region : sub_region Var0.Mvar.t;
region_var : status_map Mr.t;

}

val empty_status_map : status Var0.Mvar.t

val empty : region_map

val get_sub_region : 
  region_map ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, sub_region) Utils0.result

val get_status_map : status Var0.Mvar.t Mr.t -> region -> status_map

val get_status : status_map -> Eqtype.Equality.sort -> status

val get_var_status : 
  status Var0.Mvar.t Mr.t ->
  region ->
  Eqtype.Equality.sort ->
  status

type concrete_slice = {

cs_ofs : BinNums.coq_Z;
cs_len : BinNums.coq_Z;

}

type ptr_kind_init =

| PIdirect of Var0.Var.var * concrete_slice * Expr.v_scope
| PIregptr of Var0.Var.var
| PIstkptr of Var0.Var.var * concrete_slice * Var0.Var.var

type ptr_kind =

| Pdirect of Var0.Var.var * BinNums.coq_Z * Wsize.wsize * concrete_slice * Expr.v_scope
| Pregptr of Var0.Var.var
| Pstkptr of Var0.Var.var * BinNums.coq_Z * Wsize.wsize * concrete_slice * Var0.Var.var

type vptr_kind =

| VKglob of BinNums.coq_Z * Wsize.wsize
| VKptr of ptr_kind

type pos_map = {

vrip : Var0.Var.var;
vrsp : Var0.Var.var;
vxlen : Var0.Var.var;
globals : (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t;
locals : ptr_kind Var0.Mvar.t;
vnew : Var0.SvExtra.Sv.t;

}

type param_info = {

pp_ptr : Var0.Var.var;
pp_writable : bool;
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_align : 
  Eqtype.Equality.sort ->
  Expr.var_i ->
  sub_region ->
  Wsize.wsize ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val check_writable : 
  Expr.var_i ->
  region ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val is_valid : status -> bool

val check_valid : 
  Expr.var_i ->
  status ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

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 sub_region_status_at_ofs : 
  Expr.var_i ->
  sub_region ->
  status ->
  Eqtype.Equality.sort ->
  Eqtype.Equality.sort ->
  sub_region * status

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 set_clear : 
  region_map ->
  Expr.var_i ->
  sub_region ->
  (Compiler_util.pp_error_loc, region_map) Utils0.result

val is_unknown : status -> bool

val set_status : 
  status Var0.Mvar.t ->
  Eqtype.Equality.sort ->
  status ->
  status Var0.Mvar.Map.t

val set_word_status : 
  region_map ->
  sub_region ->
  Eqtype.Equality.sort ->
  status ->
  status_map Mr.Map.t

val set_word_pure : 
  region_map ->
  sub_region ->
  Eqtype.Equality.sort ->
  status ->
  region_map

val set_word : 
  region_map ->
  Eqtype.Equality.sort ->
  sub_region ->
  Expr.var_i ->
  status ->
  Wsize.wsize ->
  (Compiler_util.pp_error_loc, region_map) Utils0.result

val set_move_status : 
  status Var0.Mvar.t Mr.t ->
  Eqtype.Equality.sort ->
  region ->
  status ->
  status Var0.Mvar.t Mr.Map.t

val set_move : 
  region_map ->
  Eqtype.Equality.sort ->
  sub_region ->
  status ->
  region_map

val insert_status : 
  Var0.Var.var ->
  status ->
  Eqtype.Equality.sort ->
  Eqtype.Equality.sort ->
  status ->
  status

val set_move_sub : 
  region_map ->
  region ->
  Eqtype.Equality.sort ->
  status ->
  Eqtype.Equality.sort ->
  Eqtype.Equality.sort ->
  status ->
  region_map

val zone_of_cs : concrete_slice -> symbolic_zone

val sub_region_stkptr : slot -> Wsize.wsize -> concrete_slice -> sub_region

val set_stack_ptr : 
  region_map ->
  slot ->
  Wsize.wsize ->
  concrete_slice ->
  Var0.Var.var ->
  region_map

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

val get_sub_region_status : 
  region_map ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, sub_region * status) Utils0.result

val get_gsub_region_status : 
  region_map ->
  Expr.var_i ->
  vptr_kind ->
  (Compiler_util.pp_error_loc, sub_region * status) Utils0.result

type table = {

bindings : sexpr Var0.Mvar.t;
counter : Uint63.t;
vars : Var0.SvExtra.Sv.t;

}

val table_fresh_var : 
  (Var0.Var.var -> Uint63.t -> Var0.Var.var) ->
  table ->
  Var0.Var.var ->
  (Compiler_util.pp_error_loc, table * sexpr) Utils0.result

val table_get_var : 
  (Var0.Var.var -> Uint63.t -> Var0.Var.var) ->
  table ->
  Eqtype.Equality.sort ->
  (Compiler_util.pp_error_loc, table * sexpr) Utils0.result

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 get_symbolic_of_pexpr : 
  (Var0.Var.var -> Uint63.t -> Var0.Var.var) ->
  table ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, table * sexpr) Utils0.result

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 clone : 
  (Wsize.v_kind -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident) ->
  Var0.Var.var ->
  Uint63.t ->
  Var0.Var.var

val mul : Wsize.coq_PointerData -> Expr.pexpr -> Expr.pexpr -> Expr.pexpr

val mk_ofs : 
  Wsize.coq_PointerData ->
  Warray_.arr_access ->
  Wsize.wsize ->
  Expr.pexpr ->
  BinNums.coq_Z ->
  Expr.pexpr

val mk_ofs_int : Warray_.arr_access -> Wsize.wsize -> sexpr -> sexpr

val get_global : 
  pos_map ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, BinNums.coq_Z * Wsize.wsize) Utils0.result

val get_local : pos_map -> Var0.Var.var -> ptr_kind option

val get_var_kind : 
  pos_map ->
  Expr.gvar ->
  (Compiler_util.pp_error_loc, vptr_kind option) Utils0.result

val check_diff : 
  pos_map ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val check_var : 
  pos_map ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val with_var : Expr.var_i -> Var0.Var.var -> Expr.var_i

val base_ptr : pos_map -> Expr.v_scope -> Var0.Var.var

val addr_from_pk : 
  pos_map ->
  Expr.var_i ->
  ptr_kind ->
  (Compiler_util.pp_error_loc, Expr.var_i * BinNums.coq_Z) Utils0.result

val addr_from_vpk : 
  pos_map ->
  Expr.var_i ->
  vptr_kind ->
  (Compiler_util.pp_error_loc, Expr.var_i * BinNums.coq_Z) Utils0.result

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 alloc_e : 
  Wsize.coq_PointerData ->
  pos_map ->
  region_map ->
  Expr.pexpr ->
  Type.stype ->
  (Compiler_util.pp_error_loc, Expr.pexpr) Utils0.result

val alloc_es : 
  Wsize.coq_PointerData ->
  pos_map ->
  region_map ->
  Expr.pexpr list ->
  Type.stype list ->
  (Compiler_util.pp_error_loc, Expr.pexpr list) Utils0.result

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 alloc_lval : 
  Wsize.coq_PointerData ->
  pos_map ->
  region_map ->
  Expr.lval ->
  Type.stype ->
  (Compiler_util.pp_error_loc, region_map * Expr.lval) Utils0.result

val nop : 'a1 Sopn.asmOp -> 'a1 Expr.instr_r

val is_nop : 
  region_map ->
  Eqtype.Equality.sort ->
  sub_region ->
  slot ->
  Wsize.wsize ->
  concrete_slice ->
  Eqtype.Equality.sort ->
  bool

val get_addr : 
  'a1 Sopn.asmOp ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  Expr.var_i ->
  Expr.lval ->
  Expr.assgn_tag ->
  Stack_alloc_params.mov_kind ->
  Expr.pexpr ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, 'a1 Expr.instr_r) Utils0.result

val is_stack_ptr : 
  vptr_kind ->
  ((((Var0.Var.var * BinNums.coq_Z) * Wsize.wsize) * concrete_slice)
   * Var0.Var.var)
    option

val addr_from_vpk_pexpr : 
  Wsize.coq_PointerData ->
  pos_map ->
  status Var0.Mvar.t Mr.t ->
  Expr.var_i ->
  vptr_kind ->
  (Compiler_util.pp_error_loc, Expr.pexpr * BinNums.coq_Z) Utils0.result

val mk_mov : vptr_kind -> Stack_alloc_params.mov_kind

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 alloc_array_move : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  (Wsize.v_kind -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident) ->
  (sub_region -> Compiler_util.pp_error) ->
  pos_map ->
  table ->
  region_map ->
  Expr.lval ->
  Expr.assgn_tag ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, (table * region_map) * 'a1 Expr.instr_r)
    Utils0.result

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 lower_protect_ptr_fail : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 Slh_lowering.sh_params ->
  Expr.instr_info ->
  Expr.lval list ->
  Expr.assgn_tag ->
  Expr.pexpr list ->
  'a1 Expr.instr_r Compiler_util.cexec

val alloc_protect_ptr : 
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  'a1 Sopn.asmOp ->
  'a1 Slh_lowering.sh_params ->
  pos_map ->
  region_map ->
  Expr.instr_info ->
  Expr.lval ->
  Expr.assgn_tag ->
  Expr.pexpr ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, region_map * 'a1 Expr.instr_r) Utils0.result

val alloc_array_move_init : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  (Wsize.v_kind -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident) ->
  (sub_region -> Compiler_util.pp_error) ->
  pos_map ->
  table ->
  region_map ->
  Expr.lval ->
  Expr.assgn_tag ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, (table * region_map) * 'a1 Expr.instr_r)
    Utils0.result

val bad_lval_number : Compiler_util.pp_error_loc

val alloc_lvals : 
  Wsize.coq_PointerData ->
  pos_map ->
  region_map ->
  Expr.lval list ->
  Type.stype list ->
  (Compiler_util.pp_error_loc, region_map * Expr.lval list) Utils0.result

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 : sexpr -> (Compiler_util.pp_error_loc, Type.stype) Utils0.result

val typecheck_slice : symbolic_slice -> bool

val merge_interval : intervals -> intervals -> intervals option

val read_e_rec : Var0.SvExtra.Sv.t -> sexpr -> Var0.SvExtra.Sv.t

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 merge : Var0.SvExtra.Sv.t -> region_map -> region_map -> region_map

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 = {

sao_align : Wsize.wsize;
sao_size : BinNums.coq_Z;
sao_ioff : BinNums.coq_Z;
sao_extra_size : BinNums.coq_Z;
sao_max_size : BinNums.coq_Z;
sao_max_call_depth : BinNums.coq_Z;
sao_params : param_info option list;
sao_return : Datatypes.nat option list;
sao_slots : ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list;
sao_alloc : (Var0.Var.var * ptr_kind_init) list;
sao_to_save : (Var0.Var.var * BinNums.coq_Z) list;
sao_rsp : Expr.saved_stack;
sao_return_address : Expr.return_address_location;

}

val sao_frame_size : stk_alloc_oracle_t -> BinNums.coq_Z

val get_Pvar : 
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, Expr.gvar) Utils0.result

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 get_regptr : 
  pos_map ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, Expr.var_i) Utils0.result

val alloc_lval_call : 
  Wsize.coq_PointerData ->
  pos_map ->
  ((bool * sub_region) option * Expr.pexpr) list ->
  region_map ->
  Expr.lval ->
  Datatypes.nat option ->
  (Compiler_util.pp_error_loc, region_map * Expr.lval) 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 alloc_call : 
  bool ->
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  pos_map ->
  (Var0.funname -> stk_alloc_oracle_t) ->
  stk_alloc_oracle_t ->
  region_map ->
  Expr.lval list ->
  Var0.funname ->
  Expr.pexpr list ->
  (Compiler_util.pp_error_loc, region_map * 'a1 Expr.instr_r) Utils0.result

val alloc_syscall : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  pos_map ->
  Expr.instr_info ->
  region_map ->
  Expr.lval list ->
  BinNums.positive Syscall_t.syscall_t ->
  Expr.pexpr list ->
  (Compiler_util.pp_error_loc, region_map * 'a1 Expr.instr list) Utils0.result

val is_swap_array : 'a1 Sopn.asmOp -> 'a1 Sopn.sopn -> bool

val alloc_array_swap : 
  'a1 Sopn.asmOp ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  pos_map ->
  region_map ->
  Expr.lval list ->
  Expr.assgn_tag ->
  Expr.pexpr list ->
  (Compiler_util.pp_error_loc, region_map * 'a1 Expr.instr_r) Utils0.result

val alloc_i : 
  bool ->
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  'a1 Sopn.asmOp ->
  'a1 Slh_lowering.sh_params ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  ('a1 Sopn.asm_op_t -> bool) ->
  (Wsize.v_kind -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident) ->
  (sub_region -> Compiler_util.pp_error) ->
  pos_map ->
  (Var0.funname -> stk_alloc_oracle_t) ->
  'a1 Expr._uprog ->
  stk_alloc_oracle_t ->
  (table * region_map) ->
  'a1 Expr.instr ->
  ((table * region_map) * 'a1 Expr.instr list) Compiler_util.cexec

val init_stack_layout : 
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  stk_alloc_oracle_t ->
  (Compiler_util.pp_error_loc, (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t)
    Utils0.result

val add_alloc : 
  Wsize.coq_PointerData ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  (Var0.Var.var * ptr_kind_init) ->
  ((ptr_kind Var0.Mvar.t * region_map) * Var0.SvExtra.Sv.t) ->
  (Compiler_util.pp_error_loc,
    (ptr_kind Var0.Mvar.Map.t * region_map) * Var0.SvExtra.Sv.t)
    Utils0.result

val init_local_map : 
  Wsize.coq_PointerData ->
  Var0.SvExtra.Sv.elt ->
  Var0.SvExtra.Sv.elt ->
  Var0.SvExtra.Sv.elt ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  stk_alloc_oracle_t ->
  (Compiler_util.pp_error_loc,
    (ptr_kind Var0.Mvar.t * region_map) * Var0.SvExtra.Sv.t)
    Utils0.result

val check_result : 
  pos_map ->
  region_map ->
  Eqtype.Equality.sort option list ->
  Expr.var_i list ->
  Datatypes.nat option ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, Expr.var_i) Utils0.result

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 init_param : 
  Wsize.coq_PointerData ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  ((Var0.SvExtra.Sv.t * ptr_kind Var0.Mvar.t) * region_map) ->
  param_info option ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc,
    ((Var0.SvExtra.Sv.t * ptr_kind Var0.Mvar.Map.t) * region_map)
    * (sub_region option * Expr.var_i))
    Utils0.result

val init_params : 
  Wsize.coq_PointerData ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  Var0.SvExtra.Sv.t ->
  ptr_kind Var0.Mvar.t ->
  region_map ->
  param_info option list ->
  Expr.var_i list ->
  (Compiler_util.pp_error_loc,
    ((Var0.SvExtra.Sv.t * ptr_kind Var0.Mvar.t) * region_map)
    * (sub_region option * 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 alloc_fd_aux : 
  bool ->
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  'a1 Sopn.asmOp ->
  'a1 Slh_lowering.sh_params ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  ('a1 Sopn.asm_op_t -> bool) ->
  (Wsize.v_kind -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident) ->
  (sub_region -> Compiler_util.pp_error) ->
  'a1 Expr._uprog ->
  Expr.sprog_extra ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  (Var0.funname -> stk_alloc_oracle_t) ->
  stk_alloc_oracle_t ->
  ('a1, unit) Expr._fundef ->
  'a1 Expr._ufundef Compiler_util.cexec

val alloc_fd : 
  bool ->
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  'a1 Sopn.asmOp ->
  'a1 Slh_lowering.sh_params ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  ('a1 Sopn.asm_op_t -> bool) ->
  (Wsize.v_kind -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident) ->
  (sub_region -> Compiler_util.pp_error) ->
  'a1 Expr._uprog ->
  Expr.sprog_extra ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t ->
  (Var0.funname -> stk_alloc_oracle_t) ->
  Var0.funname ->
  ('a1, unit) Expr._fundef ->
  (Compiler_util.pp_error_loc, 'a1 Expr.sfundef) Utils0.result

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 check_glob : 
  Ssralg.GRing.ComRing.sort list ->
  Global.glob_value ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val size_glob : Global.glob_value -> BinNums.coq_Z

val init_map : 
  ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list ->
  Ssralg.GRing.ComRing.sort list ->
  Global.glob_decl list ->
  (BinNums.coq_Z * Wsize.wsize) Var0.Mvar.t Compiler_util.cexec

val alloc_prog : 
  bool ->
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  'a1 Sopn.asmOp ->
  'a1 Slh_lowering.sh_params ->
  'a1 Stack_alloc_params.stack_alloc_params ->
  ('a1 Sopn.asm_op_t -> bool) ->
  (Wsize.v_kind -> Uint63.t -> string -> Type.stype -> Ident.Ident.ident) ->
  (sub_region -> Compiler_util.pp_error) ->
  Ident.Ident.ident ->
  Ident.Ident.ident ->
  Ssralg.GRing.ComRing.sort list ->
  ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list ->
  (Var0.funname -> stk_alloc_oracle_t) ->
  'a1 Expr._uprog ->
  'a1 Expr._sprog Compiler_util.cexec

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Stack_alloc/index.html

Module `Jasmin.Stack_alloc`

package jasmin

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Stack_alloc/index.html

Module Jasmin.Stack_alloc

dune-project
Dependency

Module `Jasmin.Stack_alloc`