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<sizes; i++) { COPY32(q,p); p++; q++; };
     } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index d74affdea9..df71f4585a 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -791,12 +791,12 @@ value coq_interprete
       Instruct(SWITCH) {
 	uint32_t sizes = *pc++;
 	print_instr("SWITCH");
-	print_int(sizes & 0xFFFF);
+	print_int(sizes & 0x7FFFFF);
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
 	  print_int(index);
-	  pc += pc[(sizes & 0xFFFF) + index];
+	  pc += pc[(sizes & 0xFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
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
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