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/byterun/coq_fix_code.c |  4 ++--
 kernel/byterun/coq_interp.c   |  4 ++--
 kernel/cbytegen.ml            |  4 ++--
 kernel/cemitcodes.ml          | 45 ++++++++++++++++---------------------------
 4 files changed, 23 insertions(+), 34 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index f1f9c92153..1be3e65113 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 & 0x7FFFFF;
-      block_size = sizes >> 23;
+      const_size = sizes & 0xFFFFFF;
+      block_size = sizes >> 24;
       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 df71f4585a..0ab9f89ffa 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 & 0x7FFFFF);
+	print_int(sizes & 0xFFFFFF);
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
 	  print_int(index);
-	  pc += pc[(sizes & 0xFFFFF) + index];
+	  pc += pc[(sizes & 0xFFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
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 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index aa1bba02d7..2535a64d3c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -23,34 +23,22 @@ type reloc_info =
 
 type patch = reloc_info * int
 
+let patch_char4 buff pos c1 c2 c3 c4 = 
+  String.unsafe_set buff pos       c1;
+  String.unsafe_set buff (pos + 1) c2;
+  String.unsafe_set buff (pos + 2) c3;
+  String.unsafe_set buff (pos + 3) c4 
+  
 let patch_int buff pos n =
-  String.unsafe_set buff pos (Char.unsafe_chr n);
-  String.unsafe_set buff (pos + 1) (Char.unsafe_chr (n asr 8));
-  String.unsafe_set buff (pos + 2) (Char.unsafe_chr (n asr 16));
-  String.unsafe_set buff (pos + 3) (Char.unsafe_chr (n asr 24))
-
+  patch_char4 buff pos 
+    (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8))  (Char.unsafe_chr (n asr 16))
+    (Char.unsafe_chr (n asr 24))
 
 (* Buffering of bytecode *)
 
 let out_buffer = ref(String.create 1024)
 and out_position = ref 0
 
-(*
-let out_word b1 b2 b3 b4 =
-  let p = !out_position in
-  if p >= String.length !out_buffer then begin
-    let len = String.length !out_buffer in
-    let new_buffer = String.create (2 * len) in
-    String.blit !out_buffer 0 new_buffer 0 len;
-    out_buffer := new_buffer
-  end;
-  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
-  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
-  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
-  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
-  out_position := p + 4
-*)
-
 let out_word b1 b2 b3 b4 =
   let p = !out_position in
   if p >= String.length !out_buffer then begin
@@ -66,13 +54,10 @@ let out_word b1 b2 b3 b4 =
     String.blit !out_buffer 0 new_buffer 0 len;
     out_buffer := new_buffer
   end;
-  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
-  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
-  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
-  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
+  patch_char4 !out_buffer p (Char.unsafe_chr b1)
+   (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4);
   out_position := p + 4
 
-
 let out opcode =
   out_word opcode 0 0 0
 
@@ -101,7 +86,7 @@ let extend_label_table needed =
 
 let backpatch (pos, orig) =
   let displ = (!out_position - orig) asr 2 in
-  !out_buffer.[pos] <- Char.unsafe_chr displ;
+  !out_buffer.[pos]   <- Char.unsafe_chr displ;
   !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
   !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
   !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
@@ -222,8 +207,12 @@ let emit_instr = function
       out_label typlbl; out_label swlbl;
       slot_for_annot annot;out_int sz
   | Kswitch (tbl_const, tbl_block) ->
+      let lenb = Array.length tbl_block in
+      let lenc = Array.length tbl_const in
+      assert (lenb < 0x100 && lenc < 0x1000000);
       out opSWITCH;
-      out_int (Array.length tbl_const + (Array.length tbl_block lsl 23));
+      out_word lenc (lenc asr 8) (lenc asr 16) (lenb);
+(*      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