Fix vm compiler to refuse to compile code making use of inductives with

more than 245 constructors (unsupported by OCaml's runtime).

11 files changed, 73 insertions, 40 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 3b0c93b32..83f0a3721 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 8fb6601a9..1128f0d0b 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 ed8b0a6d1..b29f06c65 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 c68e39ce3..27c1c3f3f 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 48a6098ee..a7051d5c1 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 0ebff440a..a79abbb7e 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 de960eccc..ede356e69 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 99d353aae..26dd45f5f 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 d8f319fa7..d52fe611c 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 543397df5..383f81029 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 b54511e40..a316b4492 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;