From 7061f479eaf148779d216ad6779cf153076fb005 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Mar 2015 22:40:29 +0100 Subject: Fixing wrong rel_context in checking positivity condition. Parameters were missing in the context, apparently without negative effects because the context was used only for whd normalization of types, while reduction (in closure.ml) was resistant to unbound rels. See however next commit for an indirect effect on the wrong computation of non recursively uniform parameters producing an anomaly when computing _rect schemas. --- kernel/indtypes.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 799471c68a..49bf3281fe 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -346,7 +346,7 @@ let typecheck_inductive env mie = in (id,cn,lc,(sign,arity))) inds - in (env_arities, params, inds) + in (env_arities, env_ar_par, params, inds) (************************************************************************) (************************************************************************) @@ -366,9 +366,8 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err id ntyp env0 nbpar c nargs err = +let explain_ind_err id ntyp env nbpar c nargs err = let (lpar,c') = mind_extract_params nbpar c in - let env = push_rel_context lpar env0 in match err with | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar)))) @@ -822,9 +821,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar, params, inds) = typecheck_inductive env mie in + let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar params inds in + let (nmr,recargs) = check_positivity kn env_ar_par params inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes -- cgit v1.2.3 From 72b5c9d35dddf774c1d517889cb8f48a932d7095 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Mar 2015 22:29:38 +0100 Subject: Fixing computation of non-recursively uniform arguments in the presence of let-ins. This fixes #3491. --- kernel/indtypes.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 49bf3281fe..6b909824ba 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -485,6 +485,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in + let largs = List.map (whd_betadeltaiota env) largs in let nmr1 = (match ra with Mrec _ -> compute_rec_par ienv hyps nmr largs -- cgit v1.2.3 From c1729637d4fe32ebe0268eb338fcf4d032bb5df7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Mar 2015 11:26:21 +0100 Subject: Fully fixing bug #3491 (anomaly when building _rect scheme in the presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli. --- kernel/declarations.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.mli b/kernel/declarations.mli index cef920c6a5..c68e39ce33 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -139,7 +139,7 @@ type one_inductive_body = { mind_kelim : sorts_family list; (** List of allowed elimination sorts *) - mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *) + mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) mind_consnrealargs : int array; (** Number of expected proper arguments of the constructors (w/o params) @@ -172,7 +172,7 @@ type mutual_inductive_body = { mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) - mind_nparams : int; (** Number of expected parameters *) + mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) -- cgit v1.2.3 From 5047734648d83890eb4fc4e5cff7ab77d46b48eb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 25 Mar 2015 17:04:38 +0100 Subject: More clever representation of substituted Cemitcode. Module substitution is made nodewise, allowing to drop it for opaque terms in the VM. This saves a few useless substitutions. --- kernel/cemitcodes.ml | 44 ++++++++++++++++++++++++++++++-------------- 1 file changed, 30 insertions(+), 14 deletions(-) (limited to 'kernel') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 9ecae2b36f..c5f88f6f5d 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -333,25 +333,41 @@ let subst_patch s (ri,pos) = let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv +let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u) + type body_code = | BCdefined of to_patch | BCallias of pconstant | BCconstant -let subst_body_code s = function - | BCdefined tp -> BCdefined (subst_to_patch s tp) - | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u) - | BCconstant -> BCconstant - -type to_patch_substituted = body_code substituted - -let from_val = from_val - -let force = force subst_body_code - -let subst_to_patch_subst = subst_substituted - -let repr_body_code = repr_substituted +type to_patch_substituted = +| PBCdefined of to_patch substituted +| PBCallias of pconstant substituted +| PBCconstant + +let from_val = function +| BCdefined tp -> PBCdefined (from_val tp) +| BCallias cu -> PBCallias (from_val cu) +| BCconstant -> PBCconstant + +let force = function +| PBCdefined tp -> BCdefined (force subst_to_patch tp) +| PBCallias cu -> BCallias (force subst_pconstant cu) +| PBCconstant -> BCconstant + +let subst_to_patch_subst s = function +| PBCdefined tp -> PBCdefined (subst_substituted s tp) +| PBCallias cu -> PBCallias (subst_substituted s cu) +| PBCconstant -> PBCconstant + +let repr_body_code = function +| PBCdefined tp -> + let (s, tp) = repr_substituted tp in + (s, BCdefined tp) +| PBCallias cu -> + let (s, cu) = repr_substituted cu in + (s, BCallias cu) +| PBCconstant -> (None, BCconstant) let to_memory (init_code, fun_code, fv) = init(); -- cgit v1.2.3 From 1bafb18f64ab1c929abfaf9c1b75f691914d9a46 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 25 Mar 2015 19:06:16 +0100 Subject: Fix vm compiler to refuse to compile code making use of inductives with more than 245 constructors (unsupported by OCaml's runtime). --- kernel/cbytegen.ml | 49 +++++++++++++++++++++++++++++++++++-------------- kernel/cbytegen.mli | 8 +++++--- kernel/csymtable.ml | 23 ++++++++++++++--------- kernel/declarations.mli | 2 +- kernel/declareops.ml | 2 +- kernel/environ.ml | 2 +- kernel/environ.mli | 2 +- kernel/mod_typing.ml | 2 +- kernel/modops.ml | 2 +- kernel/nativelambda.ml | 9 ++++++--- kernel/term_typing.ml | 12 +++++++----- 11 files changed, 73 insertions(+), 40 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 3b0c93b322..83f0a37214 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -329,6 +329,15 @@ let init_fun_code () = fun_code := [] (* Compilation of constructors and inductive types *) +(* Limitation due to OCaml's representation of non-constant + constructors: limited to 245 cases. *) + +exception TooLargeInductive of Id.t + +let check_compilable ib = + if ib.mind_nb_args < 245 then () + else raise (TooLargeInductive ib.mind_typename) + (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = let f_cont = @@ -357,6 +366,7 @@ let rec str_const c = begin let oib = lookup_mind kn !global_env in let oip = oib.mind_packets.(j) in + let () = check_compilable oip in let num,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in if Int.equal (nparams + arity) (Array.length args) then @@ -435,6 +445,7 @@ let rec str_const c = with Not_found -> let oib = lookup_mind kn !global_env in let oip = oib.mind_packets.(j) in + let () = check_compilable oip in let num,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num) @@ -489,9 +500,12 @@ let rec compile_fv reloc l sz cont = let rec get_allias env (kn,u as p) = let cb = lookup_constant kn env in let tps = cb.const_body_code in - (match Cemitcodes.force tps with - | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u') - | _ -> p) + match tps with + | None -> p + | Some tps -> + (match Cemitcodes.force tps with + | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u') + | _ -> p) (* Compiling expressions *) @@ -607,6 +621,7 @@ let rec compile_constr reloc c sz cont = let ind = ci.ci_ind in let mib = lookup_mind (fst ind) !global_env in let oib = mib.mind_packets.(snd ind) in + let () = check_compilable oib in let tbl = oib.mind_reloc_tbl in let lbl_consts = Array.make oib.mind_nb_constant Label.no in let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in @@ -706,13 +721,14 @@ and compile_const = Kgetglobal (get_allias !global_env (kn,u)) :: cont) compile_constr reloc () args sz cont -let compile env c = +let compile fail_on_error env c = set_global_env env; init_fun_code (); Label.reset_label_counter (); let reloc = empty_comp_env () in - let init_code = compile_constr reloc c 0 [Kstop] in - let fv = List.rev (!(reloc.in_env).fv_rev) in + try + let init_code = compile_constr reloc c 0 [Kstop] in + let fv = List.rev (!(reloc.in_env).fv_rev) in (* draw_instr init_code; draw_instr !fun_code; Format.print_string "fv = "; @@ -722,21 +738,26 @@ let compile env c = | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format .print_string "\n"; Format.print_flush(); *) - init_code,!fun_code, Array.of_list fv - -let compile_constant_body env = function - | Undef _ | OpaqueDef _ -> BCconstant + Some (init_code,!fun_code, Array.of_list fv) + with TooLargeInductive tname -> + let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in + (Pp.(fn + (str "Cannot compile code for virtual machine as it uses inductive " ++ + Id.print tname ++ str " which has more than 245 constructors")); + None) + +let compile_constant_body fail_on_error env = function + | Undef _ | OpaqueDef _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in match kind_of_term body with | Const (kn',u) -> (* we use the canonical name of the constant*) let con= constant_of_kn (canonical_con kn') in - BCallias (get_allias env (con,u)) + Some (BCallias (get_allias env (con,u))) | _ -> - let res = compile env body in - let to_patch = to_memory res in - BCdefined to_patch + let res = compile fail_on_error env body in + Option.map (fun x -> BCdefined (to_memory x)) res (* Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 8fb6601a93..1128f0d0b7 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -5,10 +5,12 @@ open Declarations open Pre_env -val compile : env -> constr -> bytecodes * bytecodes * fv - (** init, fun, fv *) +val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *) + env -> constr -> (bytecodes * bytecodes * fv) option +(** init, fun, fv *) -val compile_constant_body : env -> constant_def -> body_code +val compile_constant_body : bool -> + env -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index ed8b0a6d1d..b29f06c652 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -148,14 +148,17 @@ let rec slot_for_getglobal env (kn,u) = with NotEvaluated -> (* Pp.msgnl(str"not yet evaluated");*) let pos = - match Cemitcodes.force cb.const_body_code with - | BCdefined(code,pl,fv) -> - if Univ.Instance.is_empty u then - let v = eval_to_patch env (code,pl,fv) in - set_global v - else set_global (val_of_constant (kn,u)) - | BCallias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant (kn,u)) in + match cb.const_body_code with + | None -> set_global (val_of_constant (kn,u)) + | Some code -> + match Cemitcodes.force code with + | BCdefined(code,pl,fv) -> + if Univ.Instance.is_empty u then + let v = eval_to_patch env (code,pl,fv) in + set_global v + else set_global (val_of_constant (kn,u)) + | BCallias kn' -> slot_for_getglobal env kn' + | BCconstant -> set_global (val_of_constant (kn,u)) in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (Ephemeron.create pos); pos @@ -210,7 +213,9 @@ and eval_to_patch env (buff,pl,fv) = and val_of_constr env c = let (_,fun_code,_ as ccfv) = - try compile env c + try match compile true env c with + | Some v -> v + | None -> assert false with reraise -> let reraise = Errors.push reraise in let () = print_string "can not compile \n" in diff --git a/kernel/declarations.mli b/kernel/declarations.mli index c68e39ce33..27c1c3f3f0 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -70,7 +70,7 @@ type constant_body = { const_hyps : Context.section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; - const_body_code : Cemitcodes.to_patch_substituted; + const_body_code : Cemitcodes.to_patch_substituted option; const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 48a6098eee..a7051d5c13 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -129,7 +129,7 @@ let subst_const_body sub cb = const_type = type'; const_proj = proj'; const_body_code = - Cemitcodes.subst_to_patch_subst sub cb.const_body_code; + Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code } diff --git a/kernel/environ.ml b/kernel/environ.ml index 0ebff440a1..a79abbb7e8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -473,7 +473,7 @@ type unsafe_type_judgment = { (*s Compilation of global declaration *) -let compile_constant_body = Cbytegen.compile_constant_body +let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found diff --git a/kernel/environ.mli b/kernel/environ.mli index de960ecccf..ede356e699 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -253,7 +253,7 @@ type unsafe_type_judgment = { (** {6 Compilation of global declaration } *) -val compile_constant_body : env -> constant_def -> Cemitcodes.body_code +val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option exception Hyp_not_found diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 99d353aae6..26dd45f5f3 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -97,7 +97,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let cb' = { cb with const_body = def; - const_body_code = Cemitcodes.from_val (compile_constant_body env' def); + const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def); const_universes = ctx' } in before@(lab,SFBconst(cb'))::after, c', ctx' diff --git a/kernel/modops.ml b/kernel/modops.ml index d8f319fa79..d52fe611c0 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver = in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) } + const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 543397df53..383f810295 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -375,9 +375,12 @@ let makeblock env cn u tag args = let rec get_allias env (kn, u as p) = let tps = (lookup_constant kn env).const_body_code in - match Cemitcodes.force tps with - | Cemitcodes.BCallias kn' -> get_allias env kn' - | _ -> p + match tps with + | None -> p + | Some tps -> + match Cemitcodes.force tps with + | Cemitcodes.BCallias kn' -> get_allias env kn' + | _ -> p (*i Global environment *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b54511e402..a316b4492b 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -245,12 +245,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) let tps = (* FIXME: incompleteness of the bytecode vm: we compile polymorphic constants like opaque definitions. *) - if poly then Cemitcodes.from_val Cemitcodes.BCconstant + if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant) else - match proj with - | None -> Cemitcodes.from_val (compile_constant_body env def) - | Some pb -> - Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))) + let res = + match proj with + | None -> compile_constant_body env def + | Some pb -> + compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)) + in Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; -- cgit v1.2.3 From 5c6a50d6ec1d04bacd3e41ffbb88453fef92cd5d Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Thu, 26 Mar 2015 14:24:54 +0100 Subject: Fix bug 4157, change the representation of inductive constructor when there is too many non constant constructors in the inductive type Conflicts: kernel/cbytegen.ml --- kernel/cbytecodes.ml | 1 + kernel/cbytecodes.mli | 1 + kernel/cbytegen.ml | 78 +++++++++++++++++++++++++++++++++++++-------------- kernel/vconv.ml | 4 +-- kernel/vm.ml | 32 ++++++++++++++++----- kernel/vm.mli | 3 +- 6 files changed, 87 insertions(+), 32 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index ae679027d6..91b701e0e6 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -24,6 +24,7 @@ let fix_tag = 3 let switch_tag = 4 let cofix_tag = 5 let cofix_evaluated_tag = 6 +let max_tag = Obj.lazy_tag - 1 type structured_constant = | Const_sorts of sorts diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index b65268f722..4277b47710 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -20,6 +20,7 @@ val fix_tag : tag val switch_tag : tag val cofix_tag : tag val cofix_evaluated_tag : tag +val max_tag : tag type structured_constant = | Const_sorts of sorts diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 83f0a37214..95ce2da344 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -329,14 +329,32 @@ let init_fun_code () = fun_code := [] (* Compilation of constructors and inductive types *) + (* Limitation due to OCaml's representation of non-constant constructors: limited to 245 cases. *) exception TooLargeInductive of Id.t let check_compilable ib = - if ib.mind_nb_args < 245 then () - else raise (TooLargeInductive ib.mind_typename) + if not (ib.mind_nb_args <= 0xFFFF && ib.mind_nb_constant <= 0xFFFF) then + raise (TooLargeInductive ib.mind_typename) + +(* Inv: arity > 0 *) + +let const_bn tag args = + if tag < max_tag then Const_bn(tag, args) + else + Const_bn(max_tag, + [|Const_b0 (tag - max_tag); + Const_bn (0, args) |]) + +let code_makeblock arity tag cont = + if tag < max_tag then + Kmakeblock(arity, tag) :: cont + else + Kmakeblock(arity, 0) :: Kpush :: (* Const_bn (0, args) *) + Kconst (Const_b0 (tag - max_tag)) :: (* Const_b0 (tag - max_tag)) *) + Kmakeblock(2, max_tag) :: cont (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = @@ -344,7 +362,8 @@ let code_construct tag nparams arity cont = add_pop nparams (if Int.equal arity 0 then [Kconst (Const_b0 tag); Kreturn 0] - else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]) + else + Kacc 0:: Kpop 1 :: code_makeblock arity tag [Kreturn 0]) in let lbl = Label.create() in fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; @@ -354,7 +373,6 @@ let get_strcst = function | Bstrconst sc -> sc | _ -> raise Not_found - let rec str_const c = match kind_of_term c with | Sort s -> Bstrconst (Const_sorts s) @@ -367,7 +385,7 @@ let rec str_const c = let oib = lookup_mind kn !global_env in let oip = oib.mind_packets.(j) in let () = check_compilable oip in - let num,arity = oip.mind_reloc_tbl.(i-1) in + let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in if Int.equal (nparams + arity) (Array.length args) then (* spiwack: *) @@ -409,15 +427,15 @@ let rec str_const c = with Not_found -> (* 3/ if no special behavior is available, then the compiler falls back to the normal behavior *) - if Int.equal arity 0 then Bstrconst(Const_b0 num) + if Int.equal arity 0 then Bstrconst(Const_b0 tag) 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)) + Bstrconst(const_bn tag sc_args) with Not_found -> - Bmakeblock(num,b_args) + Bmakeblock(tag,b_args) else let b_args = Array.map str_const args in (* spiwack: tries first to apply the run-time compilation @@ -428,7 +446,7 @@ let rec str_const c = f), b_args) with Not_found -> - Bconstruct_app(num, nparams, arity, b_args) + Bconstruct_app(tag, nparams, arity, b_args) end | _ -> Bconstr c end @@ -624,7 +642,11 @@ let rec compile_constr reloc c sz cont = let () = check_compilable oib in let tbl = oib.mind_reloc_tbl in let lbl_consts = Array.make oib.mind_nb_constant Label.no in - let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in + let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *) + let nblock = min nallblock (max_tag + 1) in + let lbl_blocks = Array.make nblock Label.no in + let neblock = max 0 (nallblock - max_tag) in + let lbl_eblocks = Array.make neblock Label.no in let branch1,cont = make_branch cont in (* Compiling return type *) let lbl_typ,fcode = @@ -644,6 +666,15 @@ let rec compile_constr reloc c sz cont = in lbl_blocks.(0) <- lbl_accu; let c = ref code_accu in + (* perform the extra match if needed (to many block constructor) *) + if neblock <> 0 then begin + let lbl_b, code_b = + label_code ( + Kpushfields 2 :: Kacc 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in + lbl_blocks.(max_tag) <- lbl_b; + c := code_b + end; + (* Compiling regular constructor branches *) for i = 0 to Array.length tbl - 1 do let tag, arity = tbl.(i) in @@ -655,19 +686,22 @@ let rec compile_constr reloc c sz cont = else let args, body = decompose_lam branchs.(i) in let nargs = List.length args in - let lbl_b,code_b = - label_code( - if Int.equal nargs arity then + let code_b = + if Int.equal nargs arity then Kpushfields arity :: - compile_constr (push_param arity sz_b reloc) + compile_constr (push_param arity sz_b reloc) body (sz_b+arity) (add_pop arity (branch :: !c)) else let sz_appterm = if is_tailcall then sz_b + arity else arity in Kpushfields arity :: - compile_constr reloc branchs.(i) (sz_b+arity) - (Kappterm(arity,sz_appterm) :: !c)) - in - lbl_blocks.(tag) <- lbl_b; + compile_constr reloc branchs.(i) (sz_b+arity) + (Kappterm(arity,sz_appterm) :: !c) in + let code_b = + if tag < max_tag then code_b + else Kacc 1::Kpop 2::code_b in + let lbl_b,code_b = label_code code_b in + if tag < max_tag then lbl_blocks.(tag) <- lbl_b + else lbl_eblocks.(tag - max_tag) <- lbl_b; c := code_b done; c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; @@ -692,9 +726,10 @@ and compile_str_cst reloc sc sz cont = | Bstrconst sc -> Kconst sc :: cont | Bmakeblock(tag,args) -> let nargs = Array.length args in - comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont) + comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont) | Bconstruct_app(tag,nparams,arity,args) -> - if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont + if Int.equal (Array.length args) 0 then + code_construct tag nparams arity cont else comp_app (fun _ _ _ cont -> code_construct tag nparams arity cont) @@ -743,7 +778,8 @@ let compile fail_on_error env c = let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ - Id.print tname ++ str " which has more than 245 constructors")); + Id.print tname ++ str + " which has more than 65535 constant constructors or more than 65535 non-constant constructors")); None) let compile_constant_body fail_on_error env = function diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 29315b0a90..6044e1846b 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -63,9 +63,9 @@ and conv_whd env pb k whd1 whd2 cu = else conv_arguments env k args1 args2 (conv_cofix env k cf1 cf2 cu) | Vconstr_const i1, Vconstr_const i2 -> if Int.equal i1 i2 then cu else raise NotConvertible - | Vconstr_block b1, Vconstr_block b2 -> + | Vconstr_block (tag1, b1), Vconstr_block (tag2, b2) -> let sz = bsize b1 in - if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then + if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then let rcu = ref cu in for i = 0 to sz - 1 do rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu diff --git a/kernel/vm.ml b/kernel/vm.ml index 2cc1efe431..65d84e882d 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -79,7 +79,7 @@ type vprod type vfun type vfix type vcofix -type vblock +type vblock type arguments type vm_env @@ -161,7 +161,7 @@ type whd = | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int - | Vconstr_block of vblock + | Vconstr_block of int * vblock | Vatom_stk of atom * stack (*************************************************) @@ -224,7 +224,13 @@ let whd_val : values -> whd = | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) - else Vconstr_block(Obj.obj o) + else + if tag = max_tag then + let tag = Obj.obj (Obj.field o 0) + max_tag in + let block = Obj.obj (Obj.field o 1) in + Vconstr_block(tag, block) + else + Vconstr_block(tag, Obj.obj o) @@ -518,10 +524,22 @@ let type_of_switch sw = let branch_arg k (tag,arity) = if Int.equal arity 0 then ((Obj.magic tag):values) else - let b = Obj.new_block tag arity in - for i = 0 to arity - 1 do - Obj.set_field b i (Obj.repr (val_of_rel (k+i))) - done; + let init b = + for i = 0 to arity - 1 do + Obj.set_field b i (Obj.repr (val_of_rel (k+i))) + done in + let b = + if tag < max_tag then + let b = Obj.new_block tag arity in + init b; + b + else + let b0 = Obj.new_block 0 arity in + init b0; + let b = Obj.new_block max_tag 2 in + Obj.set_field b 0 (Obj.repr (tag - max_tag)); + Obj.set_field b 1 (Obj.repr b0); + b in val_of_obj b let apply_switch sw arg = diff --git a/kernel/vm.mli b/kernel/vm.mli index 295ea83c49..139202f090 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -46,7 +46,7 @@ type whd = | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int - | Vconstr_block of vblock + | Vconstr_block of int * vblock | Vatom_stk of atom * stack (** Constructors *) @@ -94,7 +94,6 @@ val reduce_cofix : int -> vcofix -> values array * values array (** Block *) -val btag : vblock -> int val bsize : vblock -> int val bfield : vblock -> int -> values -- cgit v1.2.3 From 00894adf6fc11f4336a3ece0c347676bbf0b4c11 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Thu, 26 Mar 2015 19:00:00 +0100 Subject: allows the vm to deal with inductive type with 8388607 constant constructors and 8388851 non-constant constructor. --- kernel/byterun/coq_fix_code.c | 4 ++-- kernel/byterun/coq_interp.c | 4 ++-- kernel/cbytegen.ml | 13 ++++++++++--- kernel/cemitcodes.ml | 2 +- 4 files changed, 15 insertions(+), 8 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 52dc49bf8e..f1f9c92153 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -150,8 +150,8 @@ value coq_tcode_of_code (value code, value size) { uint32_t i, sizes, const_size, block_size; COPY32(q,p); p++; sizes=*q++; - const_size = sizes & 0xFFFF; - block_size = sizes >> 16; + const_size = sizes & 0x7FFFFF; + block_size = sizes >> 23; sizes = const_size + block_size; for(i=0; i 0 *) @@ -778,8 +786,7 @@ let compile fail_on_error env c = let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ - Id.print tname ++ str - " which has more than 65535 constant constructors or more than 65535 non-constant constructors")); + Id.print tname ++ str str_max_constructors)); None) let compile_constant_body fail_on_error env = function diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index c5f88f6f5d..aa1bba02d7 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -223,7 +223,7 @@ let emit_instr = function slot_for_annot annot;out_int sz | Kswitch (tbl_const, tbl_block) -> out opSWITCH; - out_int (Array.length tbl_const + (Array.length tbl_block lsl 16)); + out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); let org = !out_position in Array.iter (out_label_with_orig org) tbl_const; Array.iter (out_label_with_orig org) tbl_block -- cgit v1.2.3 From 924a6e99f85aa0d70d42e753d6901b067ebf8f1d Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Fri, 27 Mar 2015 06:44:02 +0100 Subject: use a more compact representation of non-constant constructors for which there corresponding tag are greater than max_variant_tag. The code is a merge with the patch proposed by Bruno on github barras/coq commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c --- kernel/cbytecodes.ml | 4 +++- kernel/cbytecodes.mli | 2 +- kernel/cbytegen.ml | 52 +++++++++++++++++++++++++-------------------------- kernel/vconv.ml | 3 ++- kernel/vm.ml | 36 +++++++++++------------------------ kernel/vm.mli | 3 ++- 6 files changed, 45 insertions(+), 55 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 91b701e0e6..700de50200 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -24,7 +24,9 @@ let fix_tag = 3 let switch_tag = 4 let cofix_tag = 5 let cofix_evaluated_tag = 6 -let max_tag = Obj.lazy_tag - 1 +(* It could be greate if OCaml export this value, + So fixme if this occur in a new version of OCaml *) +let last_variant_tag = 245 type structured_constant = | Const_sorts of sorts diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 4277b47710..fbb40ffd1f 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -20,7 +20,7 @@ val fix_tag : tag val switch_tag : tag val cofix_tag : tag val cofix_evaluated_tag : tag -val max_tag : tag +val last_variant_tag : tag type structured_constant = | Const_sorts of sorts diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 0cd250113d..45808b0729 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -331,12 +331,12 @@ let init_fun_code () = fun_code := [] (* Limitation due to OCaml's representation of non-constant - constructors: limited to 245 cases. *) + constructors: limited to 245 + 1 (0 tag) cases. *) exception TooLargeInductive of Id.t let max_nb_const = 0x7FFFFF -let max_nb_block = 0x7FFFFF + max_tag - 1 +let max_nb_block = 0x7FFFFF + last_variant_tag - 1 let str_max_constructors = Format.sprintf @@ -350,19 +350,17 @@ let check_compilable ib = (* Inv: arity > 0 *) let const_bn tag args = - if tag < max_tag then Const_bn(tag, args) + if tag < last_variant_tag then Const_bn(tag, args) else - Const_bn(max_tag, - [|Const_b0 (tag - max_tag); - Const_bn (0, args) |]) + Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args) + let code_makeblock arity tag cont = - if tag < max_tag then + if tag < last_variant_tag then Kmakeblock(arity, tag) :: cont else - Kmakeblock(arity, 0) :: Kpush :: (* Const_bn (0, args) *) - Kconst (Const_b0 (tag - max_tag)) :: (* Const_b0 (tag - max_tag)) *) - Kmakeblock(2, max_tag) :: cont + Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) :: + Kmakeblock(arity+1, last_variant_tag) :: cont (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = @@ -370,8 +368,11 @@ let code_construct tag nparams arity cont = add_pop nparams (if Int.equal arity 0 then [Kconst (Const_b0 tag); Kreturn 0] + else if tag < last_variant_tag then + [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0] else - Kacc 0:: Kpop 1 :: code_makeblock arity tag [Kreturn 0]) + [Kconst (Const_b0 (tag - last_variant_tag)); + Kmakeblock(arity+1, last_variant_tag); Kreturn 0]) in let lbl = Label.create() in fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; @@ -651,9 +652,9 @@ let rec compile_constr reloc c sz cont = let tbl = oib.mind_reloc_tbl in let lbl_consts = Array.make oib.mind_nb_constant Label.no in let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *) - let nblock = min nallblock (max_tag + 1) in + let nblock = min nallblock (last_variant_tag + 1) in let lbl_blocks = Array.make nblock Label.no in - let neblock = max 0 (nallblock - max_tag) in + let neblock = max 0 (nallblock - last_variant_tag) in let lbl_eblocks = Array.make neblock Label.no in let branch1,cont = make_branch cont in (* Compiling return type *) @@ -674,12 +675,12 @@ let rec compile_constr reloc c sz cont = in lbl_blocks.(0) <- lbl_accu; let c = ref code_accu in - (* perform the extra match if needed (to many block constructor) *) + (* perform the extra match if needed (to many block constructors) *) if neblock <> 0 then begin let lbl_b, code_b = label_code ( - Kpushfields 2 :: Kacc 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in - lbl_blocks.(max_tag) <- lbl_b; + Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in + lbl_blocks.(last_variant_tag) <- lbl_b; c := code_b end; @@ -694,25 +695,24 @@ let rec compile_constr reloc c sz cont = else let args, body = decompose_lam branchs.(i) in let nargs = List.length args in + let code_b = if Int.equal nargs arity then - Kpushfields arity :: - compile_constr (push_param arity sz_b reloc) + compile_constr (push_param arity sz_b reloc) body (sz_b+arity) (add_pop arity (branch :: !c)) else let sz_appterm = if is_tailcall then sz_b + arity else arity in - Kpushfields arity :: - compile_constr reloc branchs.(i) (sz_b+arity) + compile_constr reloc branchs.(i) (sz_b+arity) (Kappterm(arity,sz_appterm) :: !c) in let code_b = - if tag < max_tag then code_b - else Kacc 1::Kpop 2::code_b in - let lbl_b,code_b = label_code code_b in - if tag < max_tag then lbl_blocks.(tag) <- lbl_b - else lbl_eblocks.(tag - max_tag) <- lbl_b; + if tag < last_variant_tag then Kpushfields arity :: code_b + else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b in + let lbl_b,code_b = label_code code_b in + if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b + else lbl_eblocks.(tag - last_variant_tag) <- lbl_b; c := code_b done; - c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; + c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; let code_sw = match branch1 with (* spiwack : branch1 can't be a lbl anymore it's a Branch instead diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 6044e1846b..1c31cc0414 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -63,7 +63,8 @@ and conv_whd env pb k whd1 whd2 cu = else conv_arguments env k args1 args2 (conv_cofix env k cf1 cf2 cu) | Vconstr_const i1, Vconstr_const i2 -> if Int.equal i1 i2 then cu else raise NotConvertible - | Vconstr_block (tag1, b1), Vconstr_block (tag2, b2) -> + | Vconstr_block b1, Vconstr_block b2 -> + let tag1 = btag b1 and tag2 = btag b2 in let sz = bsize b1 in if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then let rcu = ref cu in diff --git a/kernel/vm.ml b/kernel/vm.ml index 65d84e882d..d4bf461b39 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -161,7 +161,7 @@ type whd = | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int - | Vconstr_block of int * vblock + | Vconstr_block of vblock | Vatom_stk of atom * stack (*************************************************) @@ -225,15 +225,8 @@ let whd_val : values -> whd = | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) else - if tag = max_tag then - let tag = Obj.obj (Obj.field o 0) + max_tag in - let block = Obj.obj (Obj.field o 1) in - Vconstr_block(tag, block) - else - Vconstr_block(tag, Obj.obj o) - - - + Vconstr_block(Obj.obj o) + (************************************************) (* Abstrct machine ******************************) (************************************************) @@ -524,22 +517,15 @@ let type_of_switch sw = let branch_arg k (tag,arity) = if Int.equal arity 0 then ((Obj.magic tag):values) else - let init b = - for i = 0 to arity - 1 do - Obj.set_field b i (Obj.repr (val_of_rel (k+i))) - done in - let b = - if tag < max_tag then - let b = Obj.new_block tag arity in - init b; - b + let b, ofs = + if tag < last_variant_tag then Obj.new_block tag arity, 0 else - let b0 = Obj.new_block 0 arity in - init b0; - let b = Obj.new_block max_tag 2 in - Obj.set_field b 0 (Obj.repr (tag - max_tag)); - Obj.set_field b 1 (Obj.repr b0); - b in + let b = Obj.new_block last_variant_tag (arity+1) in + Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); + b,1 in + for i = ofs to ofs + arity - 1 do + Obj.set_field b i (Obj.repr (val_of_rel (k+i))) + done; val_of_obj b let apply_switch sw arg = diff --git a/kernel/vm.mli b/kernel/vm.mli index 139202f090..5190356828 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -46,7 +46,7 @@ type whd = | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int - | Vconstr_block of int * vblock + | Vconstr_block of vblock | Vatom_stk of atom * stack (** Constructors *) @@ -94,6 +94,7 @@ val reduce_cofix : int -> vcofix -> values array * values array (** Block *) +val btag : vblock -> int val bsize : vblock -> int val bfield : vblock -> int -> values -- cgit v1.2.3 From 596a4a5251cc50f50bd6d25e36c81341bf65cfed Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Mon, 30 Mar 2015 10:47:12 +0200 Subject: fix code and bound for SWITCH instruction. --- kernel/byterun/coq_fix_code.c | 4 ++-- kernel/byterun/coq_interp.c | 4 ++-- kernel/cbytegen.ml | 4 ++-- kernel/cemitcodes.ml | 45 ++++++++++++++++--------------------------- 4 files changed, 23 insertions(+), 34 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index f1f9c92153..1be3e65113 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -150,8 +150,8 @@ value coq_tcode_of_code (value code, value size) { uint32_t i, sizes, const_size, block_size; COPY32(q,p); p++; sizes=*q++; - const_size = sizes & 0x7FFFFF; - block_size = sizes >> 23; + const_size = sizes & 0xFFFFFF; + block_size = sizes >> 24; sizes = const_size + block_size; for(i=0; i= String.length !out_buffer then begin - let len = String.length !out_buffer in - let new_buffer = String.create (2 * len) in - String.blit !out_buffer 0 new_buffer 0 len; - out_buffer := new_buffer - end; - String.unsafe_set !out_buffer p (Char.unsafe_chr b1); - String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2); - String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3); - String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4); - out_position := p + 4 -*) - let out_word b1 b2 b3 b4 = let p = !out_position in if p >= String.length !out_buffer then begin @@ -66,13 +54,10 @@ let out_word b1 b2 b3 b4 = String.blit !out_buffer 0 new_buffer 0 len; out_buffer := new_buffer end; - String.unsafe_set !out_buffer p (Char.unsafe_chr b1); - String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2); - String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3); - String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4); + patch_char4 !out_buffer p (Char.unsafe_chr b1) + (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4); out_position := p + 4 - let out opcode = out_word opcode 0 0 0 @@ -101,7 +86,7 @@ let extend_label_table needed = let backpatch (pos, orig) = let displ = (!out_position - orig) asr 2 in - !out_buffer.[pos] <- Char.unsafe_chr displ; + !out_buffer.[pos] <- Char.unsafe_chr displ; !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8); !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16); !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24) @@ -222,8 +207,12 @@ let emit_instr = function out_label typlbl; out_label swlbl; slot_for_annot annot;out_int sz | Kswitch (tbl_const, tbl_block) -> + let lenb = Array.length tbl_block in + let lenc = Array.length tbl_const in + assert (lenb < 0x100 && lenc < 0x1000000); out opSWITCH; - out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); + out_word lenc (lenc asr 8) (lenc asr 16) (lenb); +(* out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *) let org = !out_position in Array.iter (out_label_with_orig org) tbl_const; Array.iter (out_label_with_orig org) tbl_block -- cgit v1.2.3