Allocation (p.jasmin.2025.06.2.doc.jasmin.jasmin.Jasmin.Allocation)

module E : sig ... end

module M : sig ... end

val alloc_error : string -> Compiler_util.pp_error_loc

val cerr_varalloc : 
  Var0.Var.var ->
  Var0.Var.var ->
  string ->
  Compiler_util.pp_error_loc

val check_v : 
  Sem_type.coq_WithSubWord ->
  Expr.var_i ->
  Expr.var_i ->
  M.t ->
  M.t Compiler_util.cexec

val error_e : Compiler_util.pp_error_loc

val check_gv : 
  Sem_type.coq_WithSubWord ->
  Expr.gvar ->
  Expr.gvar ->
  M.t ->
  M.t Compiler_util.cexec

val check_e : 
  Sem_type.coq_WithSubWord ->
  Expr.pexpr ->
  Expr.pexpr ->
  M.t ->
  M.t Compiler_util.cexec

val check_var_aux : 
  Sem_type.coq_WithSubWord ->
  Var0.Var.var ->
  Var0.Var.var ->
  M.t_ ->
  M.t Compiler_util.cexec

val check_varc : 
  Sem_type.coq_WithSubWord ->
  Expr.var_i ->
  Expr.var_i ->
  M.t_ ->
  M.t Compiler_util.cexec

val is_Pvar : 
  (Type.stype * Expr.pexpr) option ->
  (Type.stype * Expr.var_i) option

val error_lv : Compiler_util.pp_error_loc

val check_lval : 
  Sem_type.coq_WithSubWord ->
  (Type.stype * Expr.pexpr) option ->
  Expr.lval ->
  Expr.lval ->
  M.t ->
  M.t Compiler_util.cexec

val loop : 
  Sem_type.coq_WithSubWord ->
  (M.t -> M.t Compiler_util.cexec) ->
  Datatypes.nat ->
  M.t ->
  (Compiler_util.pp_error_loc, M.t) Utils0.result

val loop2 : 
  Sem_type.coq_WithSubWord ->
  (M.t -> (M.t * M.t) Compiler_util.cexec) ->
  Datatypes.nat ->
  M.t ->
  (Compiler_util.pp_error_loc, M.t) Utils0.result

val check_es : 
  Sem_type.coq_WithSubWord ->
  Expr.pexpr list ->
  Expr.pexpr list ->
  M.t ->
  (Compiler_util.pp_error_loc, M.t) Utils0.result

val check_lvals : 
  Sem_type.coq_WithSubWord ->
  Expr.lval list ->
  Expr.lval list ->
  M.t ->
  (Compiler_util.pp_error_loc, M.t) Utils0.result

val check_var : 
  Sem_type.coq_WithSubWord ->
  Expr.var_i ->
  Expr.var_i ->
  M.t ->
  M.t Compiler_util.cexec

val check_vars : 
  Sem_type.coq_WithSubWord ->
  Expr.var_i list ->
  Expr.var_i list ->
  M.t ->
  (Compiler_util.pp_error_loc, M.t) Utils0.result

val check_I : 
  Sem_type.coq_WithSubWord ->
  'a1 Sopn.asmOp ->
  (Expr.instr_info -> Var0.SvExtra.Sv.t) ->
  'a1 Expr.instr ->
  'a1 Expr.instr ->
  M.t_ ->
  (Compiler_util.pp_error_loc, M.t_) Utils0.result

val check_cmd : 
  Sem_type.coq_WithSubWord ->
  'a1 Sopn.asmOp ->
  (Expr.instr_info -> Var0.SvExtra.Sv.t) ->
  'a1 Expr.instr list ->
  'a1 Expr.instr list ->
  M.t_ ->
  (Compiler_util.pp_error_loc, M.t_) Utils0.result

val check_fundef : 
  Sem_type.coq_WithSubWord ->
  'a1 Sopn.asmOp ->
  Expr.progT ->
  (Expr.extra_fun_t ->
    Expr.extra_prog_t ->
    Expr.extra_prog_t ->
    M.t Compiler_util.cexec) ->
  (M.t ->
    Expr.extra_fun_t ->
    Expr.extra_fun_t ->
    Expr.var_i list ->
    Expr.var_i list ->
    M.t Compiler_util.cexec) ->
  ('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
  Expr.extra_prog_t ->
  Expr.extra_prog_t ->
  (Var0.funname * 'a1 Expr.fundef) ->
  (Var0.funname * 'a1 Expr.fundef) ->
  unit ->
  unit Compiler_util.cexec

val check_prog_error : Compiler_util.pp_error_loc

val check_prog : 
  Sem_type.coq_WithSubWord ->
  'a1 Sopn.asmOp ->
  Expr.progT ->
  (Expr.extra_fun_t ->
    Expr.extra_prog_t ->
    Expr.extra_prog_t ->
    M.t Compiler_util.cexec) ->
  (M.t ->
    Expr.extra_fun_t ->
    Expr.extra_fun_t ->
    Expr.var_i list ->
    Expr.var_i list ->
    M.t Compiler_util.cexec) ->
  ('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
  Expr.extra_prog_t ->
  (Var0.funname * 'a1 Expr.fundef) list ->
  Expr.extra_prog_t ->
  (Var0.funname * 'a1 Expr.fundef) list ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val init_alloc_uprog : 
  Sem_type.coq_WithSubWord ->
  Expr.extra_fun_t ->
  Expr.extra_prog_t ->
  Expr.extra_prog_t ->
  M.t Compiler_util.cexec

val check_f_extra_u : 
  Sem_type.coq_WithSubWord ->
  M.t ->
  Expr.extra_fun_t ->
  Expr.extra_fun_t ->
  Expr.var_i list ->
  Expr.var_i list ->
  (Compiler_util.pp_error_loc, M.t) Utils0.result

val check_ufundef : 
  Sem_type.coq_WithSubWord ->
  'a1 Sopn.asmOp ->
  ('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
  Expr.extra_prog_t ->
  Expr.extra_prog_t ->
  (Var0.funname * 'a1 Expr.fundef) ->
  (Var0.funname * 'a1 Expr.fundef) ->
  unit ->
  unit Compiler_util.cexec

val check_uprog : 
  Sem_type.coq_WithSubWord ->
  'a1 Sopn.asmOp ->
  ('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
  Expr.extra_prog_t ->
  (Var0.funname * 'a1 Expr.fundef) list ->
  Expr.extra_prog_t ->
  (Var0.funname * 'a1 Expr.fundef) list ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val init_alloc_sprog : 
  Sem_type.coq_WithSubWord ->
  Wsize.coq_PointerData ->
  Expr.extra_fun_t ->
  Expr.extra_prog_t ->
  Expr.extra_prog_t ->
  M.t Compiler_util.cexec

val check_f_extra_s : 
  Sem_type.coq_WithSubWord ->
  Wsize.coq_PointerData ->
  M.t ->
  Expr.extra_fun_t ->
  Expr.extra_fun_t ->
  Expr.var_i list ->
  Expr.var_i list ->
  M.t Compiler_util.cexec

val check_sprog : 
  Sem_type.coq_WithSubWord ->
  'a1 Sopn.asmOp ->
  Wsize.coq_PointerData ->
  ('a1 Expr.fun_decl -> Expr.instr_info -> Var0.SvExtra.Sv.t) ->
  Expr.extra_prog_t ->
  (Var0.funname * 'a1 Expr.fundef) list ->
  Expr.extra_prog_t ->
  (Var0.funname * 'a1 Expr.fundef) list ->
  (Compiler_util.pp_error_loc, unit) Utils0.result