From 4ee0cedff7726a56ebd53125995a7ae131660b4a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 18 Aug 2020 13:07:54 +0200 Subject: Rename VM-related kernel/cfoo files to kernel/vmfoo --- kernel/vmbytegen.ml | 934 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 934 insertions(+) create mode 100644 kernel/vmbytegen.ml (limited to 'kernel/vmbytegen.ml') diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml new file mode 100644 index 0000000000..1274e3a867 --- /dev/null +++ b/kernel/vmbytegen.ml @@ -0,0 +1,934 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* *) +(* type = [Ct1 | .... | Ctn] *) +(* Ci is the code pointer of the i-th body *) +(* At runtime, a fixpoint environment (which is the same as the fixpoint *) +(* itself) is a pointer to the field holding its code pointer. *) +(* In each fixpoint body, de Bruijn [nbr] represents the first fixpoint *) +(* and de Bruijn [1] the last one. *) +(* Access to these variables is performed by the [Koffsetclosure n] *) +(* instruction that shifts the environment pointer of [n] fields. *) + +(* This allows representing mutual fixpoints in just one block. *) +(* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint *) +(* types. They are used in conversion tests (which requires that *) +(* fixpoint types must be convertible). Their environment is the one of *) +(* the last fixpoint : *) +(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) +(* ^ *) + +(* Representation of mutual cofix : *) +(* a1 = [A_t | accumulate | [Cfx_t | fcofix1 ] ] *) +(* ... *) +(* anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ] *) +(* *) +(* fcofix1 = [clos_t | code1 | a1 |...| anbr | fv1 |...| fvn | type] *) +(* ^ *) +(* ... *) +(* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *) +(* ^ *) +(* The [ai] blocks are functions that accumulate their arguments: *) +(* ai arg1 argp ---> *) +(* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) +(* If such a block is matched against, we have to force evaluation, *) +(* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *) +(* (note that [ai'] is a pointer to the closure, passed as argument) *) +(* Once evaluation is completed [ai'] is updated with the result: *) +(* ai' <-- *) +(* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) +(* This representation is nice because the application of the cofix is *) +(* evaluated only once (it simulates a lazy evaluation) *) +(* Moreover, when cofix don't have arguments, it is possible to create *) +(* a cycle, e.g.: *) +(* cofix one := cons 1 one *) +(* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *) +(* fcofix1 = [clos_t | code | a1] *) +(* The result of evaluating [a1] is [cons_t | 1 | a1]. *) +(* When [a1] is updated : *) +(* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *) +(* The cycle is created ... *) +(* *) +(* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) +(* conversion of cofixpoints (which is intentional). *) + +module Fv_elem = +struct +type t = fv_elem + +let compare e1 e2 = match e1, e2 with +| FVnamed id1, FVnamed id2 -> Id.compare id1 id2 +| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1 +| FVrel _, FVnamed _ -> 1 +| FVrel r1, FVrel r2 -> Int.compare r1 r2 +| FVrel _, (FVuniv_var _ | FVevar _) -> -1 +| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 +| FVuniv_var _, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var _, FVevar _ -> -1 +| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 +| FVevar e1, FVevar e2 -> Evar.compare e1 e2 + +end + +module FvMap = Map.Make(Fv_elem) + +(*spiwack: both type have been moved from Vmbytegen because I needed then + for the retroknowledge *) +type vm_env = { + size : int; (* longueur de la liste [n] *) + fv_rev : fv_elem list; (* [fvn; ... ;fv1] *) + fv_fwd : int FvMap.t; (* reverse mapping *) + } + + +type comp_env = { + arity : int; (* arity of the current function, 0 if none *) + nb_uni_stack : int ; (* number of universes on the stack, *) + (* universes are always at the bottom. *) + nb_stack : int; (* number of variables on the stack *) + in_stack : int Range.t; (* position in the stack *) + nb_rec : int; (* number of mutually recursive functions *) + pos_rec : instruction list; (* instruction d'acces pour les variables *) + (* de point fix ou de cofix *) + offset : int; + in_env : vm_env ref (* The free variables of the expression *) + } + +module Config = struct + let stack_threshold = 256 (* see byterun/coq_memory.h *) + let stack_safety_margin = 15 +end + +type argument = ArgLambda of lambda | ArgUniv of Univ.Level.t + +let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty } +let push_fv d e = { + size = e.size + 1; + fv_rev = d :: e.fv_rev; + fv_fwd = FvMap.add d e.size e.fv_fwd; +} + +let fv r = !(r.in_env) + +let empty_comp_env ()= + { arity = 0; + nb_uni_stack = 0; + nb_stack = 0; + in_stack = Range.empty; + nb_rec = 0; + pos_rec = []; + offset = 0; + in_env = ref empty_fv + } + +(* Maximal stack size reached during the current function body. Used to + reallocate the stack if we lack space. *) +let max_stack_size = ref 0 + +let set_max_stack_size stack_size = + if stack_size > !max_stack_size then + max_stack_size := stack_size + +let ensure_stack_capacity f x = + let old = !max_stack_size in + max_stack_size := 0; + let code = f x in + let used_safe = + !max_stack_size + Config.stack_safety_margin + in + max_stack_size := old; + if used_safe > Config.stack_threshold then + Kensurestackcapacity used_safe :: code + else code + +(*i Creation functions for comp_env *) + +let rec add_param n sz l = + if Int.equal n 0 then l else add_param (n - 1) sz (Range.cons (n+sz) l) + +let comp_env_fun ?(univs=0) arity = + { arity; + nb_uni_stack = univs ; + nb_stack = arity; + in_stack = add_param arity 0 Range.empty; + nb_rec = 0; + pos_rec = []; + offset = 1; + in_env = ref empty_fv + } + + +let comp_env_fix_type rfv = + { arity = 0; + nb_uni_stack = 0; + nb_stack = 0; + in_stack = Range.empty; + nb_rec = 0; + pos_rec = []; + offset = 1; + in_env = rfv + } + +let comp_env_fix ndef curr_pos arity rfv = + let prec = ref [] in + for i = ndef downto 1 do + prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec + done; + { arity; + nb_uni_stack = 0; + nb_stack = arity; + in_stack = add_param arity 0 Range.empty; + nb_rec = ndef; + pos_rec = !prec; + offset = 2 * (ndef - curr_pos - 1)+1; + in_env = rfv + } + +let comp_env_cofix_type ndef rfv = + { arity = 0; + nb_uni_stack = 0; + nb_stack = 0; + in_stack = Range.empty; + nb_rec = 0; + pos_rec = []; + offset = 1+ndef; + in_env = rfv + } + +let comp_env_cofix ndef arity rfv = + let prec = ref [] in + for i = 1 to ndef do + prec := Kenvacc i :: !prec + done; + { arity; + nb_uni_stack = 0; + nb_stack = arity; + in_stack = add_param arity 0 Range.empty; + nb_rec = ndef; + pos_rec = !prec; + offset = ndef+1; + in_env = rfv + } + +(* [push_param ] add function parameters on the stack *) +let push_param n sz r = + { r with + nb_stack = r.nb_stack + n; + in_stack = add_param n sz r.in_stack } + +(* [push_local sz r] add a new variable on the stack at position [sz] *) +let push_local sz r = + { r with + nb_stack = r.nb_stack + 1; + in_stack = Range.cons (sz + 1) r.in_stack } + +(*i Compilation of variables *) +let find_at fv env = FvMap.find fv env.fv_fwd + +let pos_named id r = + let env = !(r.in_env) in + let cid = FVnamed id in + try Kenvacc(r.offset + find_at cid env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv cid env; + Kenvacc (r.offset + pos) + +let pos_rel i r sz = + if i <= r.nb_stack then + Kacc(sz - (Range.get r.in_stack (i-1))) + else + let i = i - r.nb_stack in + if i <= r.nb_rec then + try List.nth r.pos_rec (i-1) + with (Failure _|Invalid_argument _) -> assert false + else + let i = i - r.nb_rec in + let db = FVrel(i) in + let env = !(r.in_env) in + try Kenvacc(r.offset + find_at db env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv db env; + Kenvacc(r.offset + pos) + +let pos_universe_var i r sz = + (* Compilation of a universe variable can happen either at toplevel (the + current closure correspond to a constant and has local universes) or in a + local closure (which has no local universes). *) + if r.nb_uni_stack != 0 then + (* Universe variables are represented by De Bruijn levels (not indices), + starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] + with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access + the last universe. *) + Kacc (sz - r.arity - (r.nb_uni_stack - i)) + else + let env = !(r.in_env) in + let db = FVuniv_var i in + try Kenvacc (r.offset + find_at db env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv db env; + Kenvacc(r.offset + pos) + +let pos_evar evk r = + let env = !(r.in_env) in + let cid = FVevar evk in + try Kenvacc(r.offset + find_at cid env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv cid env; + Kenvacc (r.offset + pos) + +(*i Examination of the continuation *) + +(* Discard all instructions up to the next label. *) +(* This function is to be applied to the continuation before adding a *) +(* non-terminating instruction (branch, raise, return, appterm) *) +(* in front of it. *) + +let discard_dead_code cont = cont +(*function + [] -> [] + | (Klabel _ | Krestart ) :: _ as cont -> cont + | _ :: cont -> discard_dead_code cont +*) + +(* Return a label to the beginning of the given continuation. *) +(* If the sequence starts with a branch, use the target of that branch *) +(* as the label, thus avoiding a jump to a jump. *) + +let label_code = function + | Klabel lbl :: _ as cont -> (lbl, cont) + | Kbranch lbl :: _ as cont -> (lbl, cont) + | cont -> let lbl = Label.create() in (lbl, Klabel lbl :: cont) + +(* Return a branch to the continuation. That is, an instruction that, + when executed, branches to the continuation or performs what the + continuation performs. We avoid generating branches to returns. *) +(* spiwack: make_branch was only used once. Changed it back to the ZAM + one to match the appropriate semantics (old one avoided the + introduction of an unconditional branch operation, which seemed + appropriate for the 31-bit integers' code). As a memory, I leave + the former version in this comment. +let make_branch cont = + match cont with + | (Kreturn _ as return) :: cont' -> return, cont' + | Klabel lbl as b :: _ -> b, cont + | _ -> let b = Klabel(Label.create()) in b,b::cont +*) + +let rec make_branch_2 lbl n cont = + function + Kreturn m :: _ -> (Kreturn (n + m), cont) + | Klabel _ :: c -> make_branch_2 lbl n cont c + | Kpop m :: c -> make_branch_2 lbl (n + m) cont c + | _ -> + match lbl with + Some lbl -> (Kbranch lbl, cont) + | None -> let lbl = Label.create() in (Kbranch lbl, Klabel lbl :: cont) + +let make_branch cont = + match cont with + (Kbranch _ as branch) :: _ -> (branch, cont) + | (Kreturn _ as return) :: _ -> (return, cont) + | Klabel lbl :: _ -> make_branch_2 (Some lbl) 0 cont cont + | _ -> make_branch_2 (None) 0 cont cont + +(* Check if we're in tailcall position *) + +let rec is_tailcall = function + | Kreturn k :: _ -> Some k + | Klabel _ :: c -> is_tailcall c + | _ -> None + +(* Extension of the continuation *) + +(* Add a Kpop n instruction in front of a continuation *) +let rec add_pop n = function + | Kpop m :: cont -> add_pop (n+m) cont + | Kreturn m:: cont -> Kreturn (n+m) ::cont + | cont -> if Int.equal n 0 then cont else Kpop n :: cont + +let add_grab arity lbl cont = + if Int.equal arity 1 then Klabel lbl :: cont + else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont + +let add_grabrec rec_arg arity lbl cont = + if Int.equal arity 1 && rec_arg < arity then + Klabel lbl :: Kgrabrec 0 :: Krestart :: cont + else + Krestart :: Klabel lbl :: Kgrabrec rec_arg :: + Krestart :: Kgrab (arity - 1) :: cont + +(* continuation of a cofix *) + +let cont_cofix arity = + (* accu = res *) + (* stk = ai::args::ra::... *) + (* ai = [At|accumulate|[Cfx_t|fcofix]|args] *) + [ Kpush; + Kpush; (* stk = res::res::ai::args::ra::... *) + Kacc 2; + Kfield 1; + Kfield 0; + Kmakeblock(2, cofix_evaluated_tag); + Kpush; (* stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*) + Kacc 2; + Ksetfield 1; (* ai = [At|accumulate|[Cfxe_t|fcofix|res]|args] *) + (* stk = res::ai::args::ra::... *) + Kacc 0; (* accu = res *) + Kreturn (arity+2) ] + + +(* Code of closures *) +let fun_code = ref [] + +let init_fun_code () = fun_code := [] + +(* Compilation of constructors and inductive types *) + + +(* +If [tag] hits the OCaml limitation for non constant constructors, we switch to +another representation for the remaining constructors: +[last_variant_tag|tag - Obj.last_non_constant_constructor_tag|args] + +We subtract Obj.last_non_constant_constructor_tag for efficiency of match interpretation. + *) + +let nest_block tag arity cont = + Kconst (Const_b0 (tag - Obj.last_non_constant_constructor_tag)) :: + Kmakeblock(arity+1, Obj.last_non_constant_constructor_tag) :: cont + +let code_makeblock ~stack_size ~arity ~tag cont = + if tag < Obj.last_non_constant_constructor_tag then + Kmakeblock(arity, tag) :: cont + else begin + set_max_stack_size (stack_size + 1); + Kpush :: nest_block tag arity cont + end + +let compile_structured_constant _cenv sc sz cont = + set_max_stack_size sz; + Kconst sc :: cont + +(* compiling application *) +let comp_args comp_expr cenv args sz cont = + let nargs_m_1 = Array.length args - 1 in + let c = ref (comp_expr cenv args.(0) (sz + nargs_m_1) cont) in + for i = 1 to nargs_m_1 do + c := comp_expr cenv args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) + done; + !c + +let comp_app comp_fun comp_arg cenv f args sz cont = + let nargs = Array.length args in + if Int.equal nargs 0 then comp_fun cenv f sz cont + else + match is_tailcall cont with + | Some k -> + comp_args comp_arg cenv args sz + (Kpush :: + comp_fun cenv f (sz + nargs) + (Kappterm(nargs, k + nargs) :: (discard_dead_code cont))) + | None -> + if nargs <= 4 then + comp_args comp_arg cenv args sz + (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) + else + let lbl,cont1 = label_code cont in + Kpush_retaddr lbl :: + (comp_args comp_arg cenv args (sz + 3) + (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1)))) + +(* Compiling free variables *) + +let compile_fv_elem cenv fv sz cont = + match fv with + | FVrel i -> pos_rel i cenv sz :: cont + | FVnamed id -> pos_named id cenv :: cont + | FVuniv_var i -> pos_universe_var i cenv sz :: cont + | FVevar evk -> pos_evar evk cenv :: cont + +let rec compile_fv cenv l sz cont = + match l with + | [] -> cont + | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem cenv fvn sz cont + | fvn :: tl -> + compile_fv_elem cenv fvn sz + (Kpush :: compile_fv cenv tl (sz + 1) cont) + + +(* Compiling constants *) + +let rec get_alias env kn = + let cb = lookup_constant kn env in + let tps = cb.const_body_code in + match tps with + | None -> kn + | Some tps -> + (match Vmemitcodes.force tps with + | BCalias kn' -> get_alias env kn' + | _ -> kn) + +(* Some primitives are not implemented natively by the VM, but calling OCaml + code instead *) +let is_caml_prim = let open CPrimitives in function + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength -> true + | _ -> false + +(* sz is the size of the local stack *) +let rec compile_lam env cenv lam sz cont = + set_max_stack_size sz; + match lam with + | Lrel(_, i) -> pos_rel i cenv sz :: cont + + | Lint i -> compile_structured_constant cenv (Const_b0 i) sz cont + + | Lval v -> compile_structured_constant cenv (Const_val v) sz cont + + | Luint i -> compile_structured_constant cenv (Const_uint i) sz cont + + | Lfloat f -> compile_structured_constant cenv (Const_float f) sz cont + + | Lproj (p,arg) -> + compile_lam env cenv arg sz (Kproj p :: cont) + + | Lvar id -> pos_named id cenv :: cont + + | Levar (evk, args) -> + if Array.is_empty args then + compile_fv_elem cenv (FVevar evk) sz cont + else + (** Arguments are reversed in evar instances *) + let args = Array.copy args in + let () = Array.rev args in + comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont + + | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont + + | Lind (ind,u) -> + if Univ.Instance.is_empty u then + compile_structured_constant cenv (Const_ind ind) sz cont + else comp_app compile_structured_constant compile_universe cenv + (Const_ind ind) (Univ.Instance.to_array u) sz cont + + | Lsort (Sorts.SProp | Sorts.Prop | Sorts.Set as s) -> + compile_structured_constant cenv (Const_sort s) sz cont + | Lsort (Sorts.Type u) -> + (* We represent universes as a global constant with local universes + "compacted", i.e. as [u arg0 ... argn] where we will substitute (after + evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *) + let u,s = Univ.compact_univ u in + let compile_get_univ cenv idx sz cont = + set_max_stack_size sz; + compile_fv_elem cenv (FVuniv_var idx) sz cont + in + if List.is_empty s then + compile_structured_constant cenv (Const_sort (Sorts.sort_of_univ u)) sz cont + else + comp_app compile_structured_constant compile_get_univ cenv + (Const_sort (Sorts.sort_of_univ u)) (Array.of_list s) sz cont + + | Llet (_id,def,body) -> + compile_lam env cenv def sz + (Kpush :: + compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) + + | Lprod (dom,codom) -> + let cont1 = + Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in + compile_lam env cenv codom sz cont1 + + | Llam (ids,body) -> + let arity = Array.length ids in + let r_fun = comp_env_fun arity in + let lbl_fun = Label.create() in + let cont_fun = + ensure_stack_capacity (compile_lam env r_fun body arity) [Kreturn arity] + in + fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; + let fv = fv r_fun in + compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) + + | Lapp (f, args) -> + begin match f with + | Lconst (kn,u) -> compile_constant env cenv kn u args sz cont + | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont + end + + | Lfix ((rec_args, init), (_decl, types, bodies)) -> + let ndef = Array.length types in + let rfv = ref empty_fv in + let lbl_types = Array.make ndef Label.no in + let lbl_bodies = Array.make ndef Label.no in + (* Compiling types *) + let env_type = comp_env_fix_type rfv in + for i = 0 to ndef - 1 do + let fcode = + ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop] + in + let lbl,fcode = label_code fcode in + lbl_types.(i) <- lbl; + fun_code := [Ksequence(fcode,!fun_code)] + done; + (* Compiling bodies *) + for i = 0 to ndef - 1 do + let params,body = decompose_Llam bodies.(i) in + let arity = Array.length params in + let env_body = comp_env_fix ndef i arity rfv in + let cont1 = + ensure_stack_capacity (compile_lam env env_body body arity) [Kreturn arity] + in + let lbl = Label.create () in + lbl_bodies.(i) <- lbl; + let fcode = add_grabrec rec_args.(i) arity lbl cont1 in + fun_code := [Ksequence(fcode,!fun_code)] + done; + let fv = !rfv in + compile_fv cenv fv.fv_rev sz + (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) + + + | Lcofix(init, (_decl,types,bodies)) -> + let ndef = Array.length types in + let lbl_types = Array.make ndef Label.no in + let lbl_bodies = Array.make ndef Label.no in + (* Compiling types *) + let rfv = ref empty_fv in + let env_type = comp_env_cofix_type ndef rfv in + for i = 0 to ndef - 1 do + let fcode = + ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop] + in + let lbl,fcode = label_code fcode in + lbl_types.(i) <- lbl; + fun_code := [Ksequence(fcode,!fun_code)] + done; + (* Compiling bodies *) + for i = 0 to ndef - 1 do + let params,body = decompose_Llam bodies.(i) in + let arity = Array.length params in + let env_body = comp_env_cofix ndef arity rfv in + let lbl = Label.create () in + let comp arity = + (* 4 stack slots are needed to update the cofix when forced *) + set_max_stack_size (arity + 4); + compile_lam env env_body body (arity+1) (cont_cofix arity) + in + let cont = ensure_stack_capacity comp arity in + lbl_bodies.(i) <- lbl; + fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)]; + done; + let fv = !rfv in + set_max_stack_size (sz + fv.size + ndef + 2); + compile_fv cenv fv.fv_rev sz + (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) + + | Lif(t, bt, bf) -> + let branch, cont = make_branch cont in + let lbl_true = Label.create() in + let lbl_false = Label.create() in + compile_lam env cenv t sz + (Kswitch([|lbl_true;lbl_false|],[||]) :: + Klabel lbl_false :: + compile_lam env cenv bf sz + (branch :: + Klabel lbl_true :: + compile_lam env cenv bt sz cont)) + + | Lcase(ci,rtbl,t,a,branches) -> + let ind = ci.ci_ind in + let mib = lookup_mind (fst ind) env in + let oib = mib.mind_packets.(snd ind) in + let lbl_consts = Array.make oib.mind_nb_constant Label.no in + let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *) + let nconst = Array.length branches.constant_branches in + let nblock = min nallblock (Obj.last_non_constant_constructor_tag + 1) in + let lbl_blocks = Array.make nblock Label.no in + let neblock = max 0 (nallblock - Obj.last_non_constant_constructor_tag) in + let lbl_eblocks = Array.make neblock Label.no in + let branch1, cont = make_branch cont in + (* Compilation of the return type *) + let fcode = + ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop] + in + let lbl_typ,fcode = label_code fcode in + fun_code := [Ksequence(fcode,!fun_code)]; + (* Compilation of the branches *) + let lbl_sw = Label.create () in + let sz_b,branch,is_tailcall = + match branch1 with + | Kreturn k -> + assert (Int.equal k sz) ; + sz, branch1, true + | Kbranch _ -> sz+3, Kjump, false + | _ -> assert false + in + + let c = ref cont in + (* Perform the extra match if needed (too many block constructors) *) + if neblock <> 0 then begin + let lbl_b, code_b = + label_code ( + Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in + lbl_blocks.(Obj.last_non_constant_constructor_tag) <- lbl_b; + c := code_b + end; + + (* Compilation of constant branches *) + for i = nconst - 1 downto 0 do + let aux = + compile_lam env cenv branches.constant_branches.(i) sz_b (branch::!c) + in + let lbl_b,code_b = label_code aux in + lbl_consts.(i) <- lbl_b; + c := code_b + done; + (* -1 for accu branch *) + for i = nallblock - 2 downto 0 do + let tag = i + 1 in + let (ids, body) = branches.nonconstant_branches.(i) in + let arity = Array.length ids in + let code_b = + compile_lam env (push_param arity sz_b cenv) + body (sz_b+arity) (add_pop arity (branch::!c)) in + let code_b = + if tag < Obj.last_non_constant_constructor_tag then begin + set_max_stack_size (sz_b + arity); + Kpushfields arity :: code_b + end + else begin + set_max_stack_size (sz_b + arity + 1); + Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b + end + in + let lbl_b, code_b = label_code code_b in + if tag < Obj.last_non_constant_constructor_tag then lbl_blocks.(tag) <- lbl_b + else lbl_eblocks.(tag - Obj.last_non_constant_constructor_tag) <- lbl_b; + c := code_b + done; + + let annot = + {rtbl = rtbl; tailcall = is_tailcall; + max_stack_size = !max_stack_size - sz} + in + + (* Compiling branch for accumulators *) + let lbl_accu, code_accu = + set_max_stack_size (sz+3); + label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch :: !c) + in + lbl_blocks.(0) <- lbl_accu; + + c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: code_accu; + let code_sw = + match branch1 with + (* spiwack : branch1 can't be a lbl anymore it's a Branch instead + | Klabel lbl -> Kpush_retaddr lbl :: !c *) + | Kbranch lbl -> Kpush_retaddr lbl :: !c + | _ -> !c + in + compile_lam env cenv a sz code_sw + + | Lmakeblock (tag,args) -> + let arity = Array.length args in + let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in + comp_args (compile_lam env) cenv args sz cont + + | Lprim (Some (kn,u), op, args) when is_caml_prim op -> + let arity = CPrimitives.arity op in + let nparams = CPrimitives.nparams op in + let nargs = arity - nparams in + assert (arity = Array.length args && arity <= 4); + let (jump, cont) = make_branch cont in + let lbl_default = Label.create () in + let default = + let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in + let cont = + if Univ.Instance.is_empty u then cont + else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) + in + Klabel lbl_default :: + Kpush :: + if Int.equal nparams 0 then cont + else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) + in + fun_code := [Ksequence(default, !fun_code)]; + comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) + + | Lprim (kn, op, args) -> + comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont) + +and compile_get_global cenv (kn,u) sz cont = + set_max_stack_size sz; + if Univ.Instance.is_empty u then + Kgetglobal kn :: cont + else + comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) + compile_universe cenv () (Univ.Instance.to_array u) sz cont + +and compile_universe cenv uni sz cont = + set_max_stack_size sz; + match Univ.Level.var_index uni with + | None -> compile_structured_constant cenv (Const_univ_level uni) sz cont + | Some idx -> pos_universe_var idx cenv sz :: cont + +and compile_constant env cenv kn u args sz cont = + set_max_stack_size sz; + if Univ.Instance.is_empty u then + (* normal compilation *) + comp_app (fun _ _ sz cont -> + compile_get_global cenv (kn,u) sz cont) + (compile_lam env) cenv () args sz cont + else + let compile_arg cenv constr_or_uni sz cont = + match constr_or_uni with + | ArgLambda t -> compile_lam env cenv t sz cont + | ArgUniv uni -> compile_universe cenv uni sz cont + in + let u = Univ.Instance.to_array u in + let lu = Array.length u in + let all = + Array.init (lu + Array.length args) + (fun i -> if i < lu then ArgUniv u.(i) else ArgLambda args.(i-lu)) + in + comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) + compile_arg cenv () all sz cont + +let is_univ_copy max u = + let u = Univ.Instance.to_array u in + if Array.length u = max then + Array.fold_left_i (fun i acc u -> + if acc then + match Univ.Level.var_index u with + | None -> false + | Some l -> l = i + else false) true u + else + false + +let dump_bytecode = ref false + +let dump_bytecodes init code fvs = + let open Pp in + (str "code =" ++ fnl () ++ + pp_bytecodes init ++ fnl () ++ + pp_bytecodes code ++ fnl () ++ + str "fv = " ++ + prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++ + fnl ()) + +let compile ~fail_on_error ?universes:(universes=0) env c = + init_fun_code (); + Label.reset_label_counter (); + let cont = [Kstop] in + try + let cenv, init_code = + if Int.equal universes 0 then + let lam = lambda_of_constr ~optimize:true env c in + let cenv = empty_comp_env () in + cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont + else + (* We are going to generate a lambda, but merge the universe closure + * with the function closure if it exists. + *) + let lam = lambda_of_constr ~optimize:true env c in + let params, body = decompose_Llam lam in + let arity = Array.length params in + let cenv = empty_comp_env () in + let full_arity = arity + universes in + let r_fun = comp_env_fun ~univs:universes arity in + let lbl_fun = Label.create () in + let cont_fun = + ensure_stack_capacity (compile_lam env r_fun body full_arity) + [Kreturn full_arity] + in + fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; + let fv = fv r_fun in + let init_code = + ensure_stack_capacity (compile_fv cenv fv.fv_rev 0) + (Kclosure(lbl_fun,fv.size) :: cont) + in + cenv, init_code + in + let fv = List.rev (!(cenv.in_env).fv_rev) in + (if !dump_bytecode then + Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; + Some (init_code,!fun_code, Array.of_list fv) + with TooLargeInductive msg as exn -> + let _, info = Exninfo.capture exn in + let fn = if fail_on_error then + CErrors.user_err ?loc:None ~info ~hdr:"compile" + else + (fun x -> Feedback.msg_warning x) in + fn msg; None + +let compile_constant_body ~fail_on_error env univs = function + | Undef _ | OpaqueDef _ | Primitive _ -> Some BCconstant + | Def sb -> + let body = Mod_subst.force_constr sb in + let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in + match kind body with + | Const (kn',u) when is_univ_copy instance_size u -> + (* we use the canonical name of the constant*) + let con= Constant.make1 (Constant.canonical kn') in + Some (BCalias (get_alias env con)) + | _ -> + let res = compile ~fail_on_error ~universes:instance_size env body in + Option.map (fun x -> BCdefined (to_memory x)) res + +(* Shortcut of the previous function used during module strengthening *) + +let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn)) -- cgit v1.2.3