aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Benjamin Gregoire <Benjamin.Gregoire@inria.fr>2015-03-26 19:00:00 +0100
committerGravatar Benjamin Gregoire <Benjamin.Gregoire@inria.fr>2015-03-26 19:00:00 +0100
commit00894adf6fc11f4336a3ece0c347676bbf0b4c11 (patch)
treea3d46465df90fac47629a483f6cd75be40d9656e /kernel
parentf920ae56ffacf80f85dcf33d3f1ccf0acb4375b1 (diff)
allows the vm to deal with inductive type with 8388607 constant constructors and 8388851 non-constant constructor.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_fix_code.c4
-rw-r--r--kernel/byterun/coq_interp.c4
-rw-r--r--kernel/cbytegen.ml13
-rw-r--r--kernel/cemitcodes.ml2
4 files changed, 15 insertions, 8 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 52dc49bf8..f1f9c9215 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 d74affdea..df71f4585 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 95ce2da34..0cd250113 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 c5f88f6f5..aa1bba02d 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