diff options
| author |  Benjamin Gregoire <Benjamin.Gregoire@inria.fr> | 2015-03-26 19:00:00 +0100 |
|---|---|---|
| committer | Benjamin Gregoire <Benjamin.Gregoire@inria.fr> | 2015-03-26 19:00:00 +0100 |
| commit | 00894adf6fc11f4336a3ece0c347676bbf0b4c11 (patch) | |
| tree | a3d46465df90fac47629a483f6cd75be40d9656e /kernel | |
| parent | f920ae56ffacf80f85dcf33d3f1ccf0acb4375b1 (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.c | 4 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 4 | ||||
| -rw-r--r-- | kernel/cbytegen.ml | 13 | ||||
| -rw-r--r-- | kernel/cemitcodes.ml | 2 |
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 |