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 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 35 insertions(+), 14 deletions(-) (limited to 'kernel/cbytegen.ml') 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 *) -- 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/cbytegen.ml | 78 +++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 57 insertions(+), 21 deletions(-) (limited to 'kernel/cbytegen.ml') 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 -- 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/cbytegen.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'kernel/cbytegen.ml') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 95ce2da344..0cd250113d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -335,8 +335,16 @@ let init_fun_code () = fun_code := [] exception TooLargeInductive of Id.t +let max_nb_const = 0x7FFFFF +let max_nb_block = 0x7FFFFF + max_tag - 1 + +let str_max_constructors = + Format.sprintf + " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block + let check_compilable ib = - if not (ib.mind_nb_args <= 0xFFFF && ib.mind_nb_constant <= 0xFFFF) then + + if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then raise (TooLargeInductive ib.mind_typename) (* Inv: arity > 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 -- 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/cbytegen.ml | 52 ++++++++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'kernel/cbytegen.ml') 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 -- 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/cbytegen.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/cbytegen.ml') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 45808b0729..07fab06a42 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -335,8 +335,8 @@ let init_fun_code () = fun_code := [] exception TooLargeInductive of Id.t -let max_nb_const = 0x7FFFFF -let max_nb_block = 0x7FFFFF + last_variant_tag - 1 +let max_nb_const = 0x1000000 +let max_nb_block = 0x1000000 + last_variant_tag - 1 let str_max_constructors = Format.sprintf -- cgit v1.2.3