diff options
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 339 |
1 files changed, 289 insertions, 50 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index e1f89fad..72113425 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -83,24 +83,9 @@ open Pre_env (* On conserve la fct de cofix pour la conversion *) -type vm_env = { - size : int; (* longueur de la liste [n] *) - fv_rev : fv_elem list (* [fvn; ... ;fv1] *) - } - + let empty_fv = { size= 0; fv_rev = [] } - -type comp_env = { - nb_stack : int; (* nbre de variables sur la pile *) - in_stack : int list; (* position dans la pile *) - nb_rec : int; (* nbre de fonctions mutuellement *) - (* recursives = nbr *) - pos_rec : instruction list; (* instruction d'acces pour les variables *) - (* de point fix ou de cofix *) - offset : int; - in_env : vm_env ref - } - + let fv r = !(r.in_env) let empty_comp_env ()= @@ -231,17 +216,40 @@ let rec discard_dead_code cont = cont 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 *) @@ -315,52 +323,105 @@ let code_construct tag nparams arity cont = fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; Kclosure(lbl,0) :: cont -type block = - | Bconstr of constr - | Bstrconst of structured_constant - | Bmakeblock of int * block array - | Bconstruct_app of int * int * int * block array - (* tag , nparams, arity *) - let get_strcst = function | Bstrconst sc -> sc | _ -> raise Not_found -let rec str_const c = + +let rec str_const c = match kind_of_term c with | Sort s -> Bstrconst (Const_sorts s) | Cast(c,_,_) -> str_const c | App(f,args) -> begin match kind_of_term f with - | Construct((kn,j),i) -> + | Construct((kn,j),i) -> (* arnaud: Construct(((kn,j),i) as cstr) -> *) + begin let oib = lookup_mind kn !global_env in let oip = oib.mind_packets.(j) in let num,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in if nparams + arity = Array.length args then - if arity = 0 then Bstrconst(Const_b0 num) - else - let rargs = Array.sub args nparams arity in - let b_args = Array.map str_const rargs in - try - let sc_args = Array.map get_strcst b_args in - Bstrconst(Const_bn(num, sc_args)) - with Not_found -> - Bmakeblock(num,b_args) + (* spiwack: *) + (* 1/ tries to compile the constructor in an optimal way, + it is supposed to work only if the arguments are + all fully constructed, fails with Cbytecodes.NotClosed. + it can also raise Not_found when there is no special + treatment for this constructor + for instance: tries to to compile an integer of the + form I31 D1 D2 ... D31 to [D1D2...D31] as + a processor number (a caml number actually) *) + try + try + Bstrconst (Retroknowledge.get_vm_constant_static_info + (!global_env).retroknowledge + (kind_of_term f) args) + with NotClosed -> + (* 2/ if the arguments are not all closed (this is + expectingly (and it is currently the case) the only + reason why this exception is raised) tries to + give a clever, run-time behavior to the constructor. + Raises Not_found if there is no special treatment + for this integer. + this is done in a lazy fashion, using the constructor + Bspecial because it needs to know the continuation + and such, which can't be done at this time. + for instance, for int31: if one of the digit is + not closed, it's not impossible that the number + gets fully instanciated at run-time, thus to ensure + uniqueness of the representation in the vm + it is necessary to try and build a caml integer + during the execution *) + let rargs = Array.sub args nparams arity in + let b_args = Array.map str_const rargs in + Bspecial ((Retroknowledge.get_vm_constant_dynamic_info + (!global_env).retroknowledge + (kind_of_term f)), + b_args) + with Not_found -> + (* 3/ if no special behavior is available, then the compiler + falls back to the normal behavior *) + if arity = 0 then Bstrconst(Const_b0 num) + else + let rargs = Array.sub args nparams arity in + let b_args = Array.map str_const rargs in + try + let sc_args = Array.map get_strcst b_args in + Bstrconst(Const_bn(num, sc_args)) + with Not_found -> + Bmakeblock(num,b_args) else - let b_args = Array.map str_const args in - Bconstruct_app(num, nparams, arity, b_args) + let b_args = Array.map str_const args in + (* spiwack: tries first to apply the run-time compilation + behavior of the constructor, as in 2/ above *) + try + Bspecial ((Retroknowledge.get_vm_constant_dynamic_info + (!global_env).retroknowledge + (kind_of_term f)), + b_args) + with Not_found -> + Bconstruct_app(num, nparams, arity, b_args) + end | _ -> Bconstr c end | Ind ind -> Bstrconst (Const_ind ind) - | Construct ((kn,j),i) -> - let oib = lookup_mind kn !global_env in - let oip = oib.mind_packets.(j) in - let num,arity = oip.mind_reloc_tbl.(i-1) in - let nparams = oib.mind_nparams in - if nparams + arity = 0 then Bstrconst(Const_b0 num) - else Bconstruct_app(num,nparams,arity,[||]) + | Construct ((kn,j),i) -> (*arnaud: Construct ((kn,j),i as cstr) -> *) + begin + (* spiwack: tries first to apply the run-time compilation + behavior of the constructor, as in 2/ above *) + try + Bspecial ((Retroknowledge.get_vm_constant_dynamic_info + (!global_env).retroknowledge + (kind_of_term c)), + [| |]) + with Not_found -> + let oib = lookup_mind kn !global_env in + let oip = oib.mind_packets.(j) in + let num,arity = oip.mind_reloc_tbl.(i-1) in + let nparams = oib.mind_nparams in + if nparams + arity = 0 then Bstrconst(Const_b0 num) + else Bconstruct_app(num,nparams,arity,[||]) + end | _ -> Bconstr c (* compilation des applications *) @@ -413,6 +474,7 @@ let rec get_allias env kn = | BCallias kn' -> get_allias env kn' | _ -> kn + (* compilation des expressions *) let rec compile_constr reloc c sz cont = @@ -424,8 +486,7 @@ let rec compile_constr reloc c sz cont = | Rel i -> pos_rel i reloc sz :: cont | Var id -> pos_named id reloc :: cont - | Const kn -> Kgetglobal (get_allias !global_env kn) :: cont - + | Const kn -> compile_const reloc kn [||] sz cont | Sort _ | Ind _ | Construct _ -> compile_str_cst reloc (str_const c) sz cont @@ -452,6 +513,7 @@ let rec compile_constr reloc c sz cont = begin match kind_of_term f with | Construct _ -> compile_str_cst reloc (str_const c) sz cont + | Const kn -> compile_const reloc kn args sz cont | _ -> comp_app compile_constr compile_constr reloc f args sz cont end | Fix ((rec_args,init),(_,type_bodies,rec_bodies)) -> @@ -569,11 +631,19 @@ let rec compile_constr reloc c sz cont = done; c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; let code_sw = - match branch1 with - | Klabel lbl -> Kpush_retaddr lbl :: !c + 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_constr reloc a sz code_sw + compile_constr reloc a sz + (try + let entry = Term.Ind ind in + Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge + entry code_sw + with Not_found -> + code_sw) and compile_str_cst reloc sc sz cont = match sc with @@ -588,6 +658,40 @@ and compile_str_cst reloc sc sz cont = comp_app (fun _ _ _ cont -> code_construct tag nparams arity cont) compile_str_cst reloc () args sz cont + | Bspecial (comp_fx, args) -> comp_fx reloc args sz cont + + +(* spiwack : compilation of constants with their arguments. + Makes a special treatment with 31-bit integer addition *) +and compile_const = +(*arnaud: let code_construct kn cont = + let f_cont = + let else_lbl = Label.create () in + Kareconst(2, else_lbl):: Kacc 0:: Kpop 1:: + Kaddint31:: Kreturn 0:: Klabel else_lbl:: + (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*) + Kgetglobal (get_allias !global_env kn):: + Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *) + in + let lbl = Label.create () in + fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)]; + Kclosure(lbl, 0)::cont + in *) + fun reloc-> fun kn -> fun args -> fun sz -> fun cont -> + let nargs = Array.length args in + (* spiwack: checks if there is a specific way to compile the constant + if there is not, Not_found is raised, and the function + falls back on its normal behavior *) + try + Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge + (kind_of_term (mkConst kn)) reloc args sz cont + with Not_found -> + if nargs = 0 then + Kgetglobal (get_allias !global_env kn) :: cont + else + comp_app (fun _ _ _ cont -> + Kgetglobal (get_allias !global_env kn) :: cont) + compile_constr reloc () args sz cont let compile env c = set_global_env env; @@ -625,3 +729,138 @@ let compile_constant_body env body opaque boxed = let to_patch = to_memory res in BCdefined (false, to_patch) + +(* spiwack: additional function which allow different part of compilation of the + 31-bit integers *) + +let make_areconst n else_lbl cont = + if n <=0 then + cont + else + Kareconst (n, else_lbl)::cont + + +(* try to compile int31 as a const_b0. Succeed if all the arguments are closed + fails otherwise by raising NotClosed*) +let compile_structured_int31 fc args = + if not fc then raise Not_found else + Const_b0 + (Array.fold_left + (fun temp_i -> fun t -> match kind_of_term t with + | Construct (_,d) -> 2*temp_i+d-1 + | _ -> raise NotClosed) + 0 args + ) + +(* this function is used for the compilation of the constructor of + the int31, it is used when it appears not fully applied, or + applied to at least one non-closed digit *) +let dynamic_int31_compilation fc reloc args sz cont = + if not fc then raise Not_found else + let nargs = Array.length args in + if nargs = 31 then + let (escape,labeled_cont) = make_branch cont in + let else_lbl = Label.create() in + comp_args compile_str_cst reloc args sz + ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont) + else + let code_construct cont = (* spiwack: variant of the global code_construct + which handles dynamic compilation of + integers *) + let f_cont = + let else_lbl = Label.create () in + [Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl); + Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0] + in + let lbl = Label.create() in + fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)]; + Kclosure(lbl,0) :: cont + in + if nargs = 0 then + code_construct cont + else + comp_app (fun _ _ _ cont -> code_construct cont) + compile_str_cst reloc () args sz cont + +(*(* template compilation for 2ary operation, it probably possible + to make a generic such function with arity abstracted *) +let op2_compilation op = + let code_construct normal cont = (*kn cont =*) + let f_cont = + let else_lbl = Label.create () in + Kareconst(2, else_lbl):: Kacc 0:: Kpop 1:: + op:: Kreturn 0:: Klabel else_lbl:: + (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*) + (*Kgetglobal (get_allias !global_env kn):: *) + normal:: + Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *) + in + let lbl = Label.create () in + fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)]; + Kclosure(lbl, 0)::cont + in + fun normal fc _ reloc args sz cont -> + if not fc then raise Not_found else + let nargs = Array.length args in + if nargs=2 then (*if it is a fully applied addition*) + let (escape, labeled_cont) = make_branch cont in + let else_lbl = Label.create () in + comp_args compile_constr reloc args sz + (Kisconst else_lbl::(make_areconst 1 else_lbl + (*Kaddint31::escape::Klabel else_lbl::Kpush::*) + (op::escape::Klabel else_lbl::Kpush:: + (* works as comp_app with nargs = 2 and non-tailcall cont*) + (*Kgetglobal (get_allias !global_env kn):: *) + normal:: + Kapply 2::labeled_cont))) + else if nargs=0 then + code_construct normal cont + else + comp_app (fun _ _ _ cont -> code_construct normal cont) + compile_constr reloc () args sz cont *) + +(*template for n-ary operation, invariant: n>=1, + the operations does the following : + 1/ checks if all the arguments are constants (i.e. non-block values) + 2/ if they are, uses the "op" instruction to execute + 3/ if at least one is not, branches to the normal behavior: + Kgetglobal (get_allias !global_env kn) *) +let op_compilation n op = + let code_construct kn cont = + let f_cont = + let else_lbl = Label.create () in + Kareconst(n, else_lbl):: Kacc 0:: Kpop 1:: + op:: Kreturn 0:: Klabel else_lbl:: + (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*) + Kgetglobal (get_allias !global_env kn):: + Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *) + in + let lbl = Label.create () in + fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)]; + Kclosure(lbl, 0)::cont + in + fun kn fc reloc args sz cont -> + if not fc then raise Not_found else + let nargs = Array.length args in + if nargs=n then (*if it is a fully applied addition*) + let (escape, labeled_cont) = make_branch cont in + let else_lbl = Label.create () in + comp_args compile_constr reloc args sz + (Kisconst else_lbl::(make_areconst (n-1) else_lbl + (*Kaddint31::escape::Klabel else_lbl::Kpush::*) + (op::escape::Klabel else_lbl::Kpush:: + (* works as comp_app with nargs = n and non-tailcall cont*) + Kgetglobal (get_allias !global_env kn):: + Kapply n::labeled_cont))) + else if nargs=0 then + code_construct kn cont + else + comp_app (fun _ _ _ cont -> code_construct kn cont) + compile_constr reloc () args sz cont + +let int31_escape_before_match fc cont = + if not fc then + raise Not_found + else + let escape_lbl, labeled_cont = label_code cont in + (Kisconst escape_lbl)::Kdecompint31::labeled_cont |