Merge PR #6908: Move VM global tables from C to ML

10 files changed, 70 insertions, 113 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index af89712d5..cfeb0a9ee 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -163,8 +163,11 @@ extern void caml_process_pending_signals(void);
 /* The interpreter itself */
 
 value coq_interprete
-(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args)
+(code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args)
 {
+  /* coq_accu is not allocated on the OCaml heap */
+  CAMLparam2(coq_atom_tbl, coq_global_data);
+
   /*Declaration des variables */
 #ifdef PC_REG
   register code_t pc PC_REG;
@@ -196,7 +199,7 @@ value coq_interprete
     coq_instr_table = (char **) coq_jumptable;
     coq_instr_base = coq_Jumptbl_base;
 #endif
-    return Val_unit;
+    CAMLreturn(Val_unit);
   }
 #if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
   coq_jumptbl_base = coq_Jumptbl_base;
@@ -1460,7 +1463,7 @@ value coq_interprete
       Instruct(STOP){
 	print_instr("STOP");
 	coq_sp = sp;
-	return accu;
+        CAMLreturn(accu);
       }
       
   
@@ -1512,12 +1515,16 @@ value coq_push_vstack(value stk, value max_stack_size) {
   return Val_unit;
 }
 
-value  coq_interprete_ml(value tcode, value a, value e, value ea) {
+value  coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) {
   print_instr("coq_interprete");
-  return coq_interprete((code_t)tcode, a, e, Long_val(ea));
+  return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea));
   print_instr("end coq_interprete");
 }
 
-value coq_eval_tcode (value tcode, value e) {
-  return coq_interprete_ml(tcode, Val_unit, e, 0);
+value coq_interprete_byte(value* argv, int argn){
+  return coq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]);
+}
+
+value coq_eval_tcode (value tcode, value t, value g, value e) {
+  return coq_interprete_ml(tcode, Val_unit, t, g, e, 0);
 }
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
index 60865c32e..c04e9e00b 100644
--- a/kernel/byterun/coq_interp.h
+++ b/kernel/byterun/coq_interp.h
@@ -17,11 +17,10 @@ value coq_push_arguments(value args);
 
 value coq_push_vstack(value stk);
 
-value  coq_interprete_ml(value tcode, value a, value e, value ea);
+value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea);
+value coq_interprete_byte(value* argv, int argn);
 
 value coq_interprete
-    (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args);
-
-value coq_eval_tcode (value tcode, value e);
-
+    (code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args);
 
+value coq_eval_tcode (value tcode, value t, value g, value e);
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 45cfae509..b2917a55e 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -24,10 +24,6 @@ value * coq_stack_threshold;
 asize_t coq_max_stack_size = Coq_max_stack_size;
 /* global_data */
 
-
-value coq_global_data;
-value coq_atom_tbl;
-
 int drawinstr;
 /* interp state */
 
@@ -58,9 +54,6 @@ static void (*coq_prev_scan_roots_hook) (scanning_action);
 static void coq_scan_roots(scanning_action action)
 {
   register value * i;
-  /* Scan the global variables */
-  (*action)(coq_global_data, &coq_global_data);
-  (*action)(coq_atom_tbl, &coq_atom_tbl);
   /* Scan the stack */
   for (i = coq_sp; i < coq_stack_high; i++) {
     (*action) (*i, i);
@@ -79,24 +72,10 @@ void init_coq_stack()
   coq_max_stack_size = Coq_max_stack_size;
 }  
 
-void init_coq_global_data(long requested_size)
-{
-  int i;
-  coq_global_data = alloc_shr(requested_size, 0);
-  for (i = 0; i < requested_size; i++) 
-    Field (coq_global_data, i) = Val_unit;
-}
-
-void init_coq_atom_tbl(long requested_size){
-  int i;
-  coq_atom_tbl = alloc_shr(requested_size, 0);
-  for (i = 0; i < requested_size; i++) Field (coq_atom_tbl, i) = Val_unit;
-}
-
 void init_coq_interpreter()
 {
   coq_sp = coq_stack_high;
-  coq_interprete(NULL, Val_unit, Val_unit, 0);
+  coq_interprete(NULL, Val_unit, Atom(0), Atom(0), Val_unit, 0);
 }
 
 static int coq_vm_initialized = 0;
@@ -112,8 +91,6 @@ value init_coq_vm(value unit) /* ML */
 #endif /* THREADED_CODE */
     /* Allocate the table of global and the stack */
     init_coq_stack();
-    init_coq_global_data(Coq_global_data_Size);
-    init_coq_atom_tbl(40);
     /* Initialing the interpreter */
     init_coq_interpreter();
     
@@ -157,53 +134,6 @@ void realloc_coq_stack(asize_t required_space)
 #undef shift
 }
 
-value get_coq_global_data(value unit)                /* ML */
-{
-  return coq_global_data;
-}
-
-value get_coq_atom_tbl(value unit)                  /* ML */
-{
-  return coq_atom_tbl;
-}
-
-value realloc_coq_global_data(value size)           /* ML */
-{
-  mlsize_t requested_size, actual_size, i;
-  value new_global_data;
-  requested_size = Long_val(size);
-  actual_size = Wosize_val(coq_global_data);
-  if (requested_size >= actual_size) {
-    requested_size = (requested_size + 0x100) & 0xFFFFFF00;
-    new_global_data = alloc_shr(requested_size, 0);
-    for (i = 0; i < actual_size; i++)
-      initialize(&Field(new_global_data, i), Field(coq_global_data, i));
-    for (i = actual_size; i < requested_size; i++){
-      Field (new_global_data, i) = Val_long (0);
-    }
-    coq_global_data = new_global_data;
-  }
-  return Val_unit;
-}
-
-value realloc_coq_atom_tbl(value size)            /* ML */
-{
-  mlsize_t requested_size, actual_size, i;
-  value new_atom_tbl;
-  requested_size = Long_val(size);
-  actual_size = Wosize_val(coq_atom_tbl);
-  if (requested_size >= actual_size) {
-    requested_size = (requested_size + 0x100) & 0xFFFFFF00;
-    new_atom_tbl = alloc_shr(requested_size, 0);
-    for (i = 0; i < actual_size; i++)
-      initialize(&Field(new_atom_tbl, i), Field(coq_atom_tbl, i));
-    for (i = actual_size; i < requested_size; i++)
-      Field (new_atom_tbl, i) = Val_long (0);
-    coq_atom_tbl = new_atom_tbl;
-  }
-  return Val_unit;
-}
-
 value coq_set_drawinstr(value unit)
 {
   drawinstr = 1;
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index cec34f566..9375b15de 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -20,7 +20,6 @@
 
 #define Coq_stack_size (4096 * sizeof(value))
 #define Coq_stack_threshold (256 * sizeof(value))
-#define Coq_global_data_Size (4096 * sizeof(value))
 #define Coq_max_stack_size (256 * 1024)
 
 #define TRANSP 0
@@ -34,9 +33,7 @@ extern value * coq_stack_threshold;
 
 /* global_data */
 
-extern value coq_global_data;
 extern int coq_all_transp;
-extern value coq_atom_tbl;
 
 extern int drawinstr;
 /* interp state */
@@ -53,10 +50,6 @@ value init_coq_vm(value unit); /* ML */
 value re_init_coq_vm(value unit); /* ML */
 
 void  realloc_coq_stack(asize_t required_space); 
-value get_coq_global_data(value unit); /* ML */
-value realloc_coq_global_data(value size); /* ML */
-value get_coq_atom_tbl(value unit); /* ML */
-value realloc_coq_atom_tbl(value size); /* ML */
 value coq_set_transp_value(value transp); /* ML */
 value get_coq_transp_value(value unit); /* ML */
 #endif /* _COQ_MEMORY_ */
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 012948954..4f3cbf289 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -26,7 +26,9 @@ open Cbytegen
 module NamedDecl = Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 
-external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
+external eval_tcode : tcode -> atom array -> vm_global -> values array -> values = "coq_eval_tcode"
+
+type global_data = { mutable glob_len : int; mutable glob_val : values array }
 
 (*******************)
 (* Linkage du code *)
@@ -37,21 +39,28 @@ external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
 (* [global_data] contient les valeurs des constantes globales
    (axiomes,definitions), les annotations des switch et les structured
    constant *)
-external global_data : unit -> values array = "get_coq_global_data"
+let global_data = {
+  glob_len = 0;
+  glob_val = Array.make 4096 crazy_val;
+}
 
-(* [realloc_global_data n] augmente de n la taille de [global_data] *)
-external realloc_global_data : int -> unit = "realloc_coq_global_data"
+let get_global_data () = Vmvalues.vm_global global_data.glob_val
 
-let check_global_data n =
-  if n >= Array.length (global_data()) then realloc_global_data n
+let realloc_global_data n =
+  let n = min (2 * n + 0x100) Sys.max_array_length in
+  let ans = Array.make n crazy_val in
+  let src = global_data.glob_val in
+  let () = Array.blit src 0 ans 0 (Array.length src) in
+  global_data.glob_val <- ans
 
-let num_global = ref 0
+let check_global_data n =
+  if n >= Array.length global_data.glob_val then realloc_global_data n
 
 let set_global v =
-  let n = !num_global in
+  let n = global_data.glob_len in
   check_global_data n;
-  (global_data()).(n) <- v;
-  incr num_global;
+  global_data.glob_val.(n) <- v;
+  global_data.glob_len <- global_data.glob_len + 1;
   n
 
 (* table pour les structured_constant et les annotations des switchs *)
@@ -164,7 +173,7 @@ and eval_to_patch env (buff,pl,fv) =
   in
   let tc = patch buff pl slots in
   let vm_env = Array.map (slot_for_fv env) fv in
-  eval_tcode tc vm_env
+  eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
 
 and val_of_constr env c =
   match compile ~fail_on_error:true env c with
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 19b2b8b50..d32cfba36 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -18,3 +18,5 @@ val val_of_constr : env -> constr -> Vmvalues.values
 
 val set_opaque_const      : Constant.t -> unit
 val set_transparent_const : Constant.t -> unit
+
+val get_global_data : unit -> Vmvalues.vm_global
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 370185a72..5d270125a 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -43,6 +43,6 @@ Subtyping
 Mod_typing
 Nativelibrary
 Safe_typing
-Vm
 Csymtable
+Vm
 Vconv
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 14aeb732f..d7eedc226 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -42,8 +42,11 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack"
 
 
 (* interpreteur *)
-external interprete : tcode -> values -> vm_env -> int -> values =
-  "coq_interprete_ml"
+external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env -> int -> values =
+  "coq_interprete_byte" "coq_interprete_ml"
+
+let interprete code v env k =
+  coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k
 
 (* Functions over arguments *)
 
@@ -184,6 +187,6 @@ let apply_whd k whd =
       push_val v;
       interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0
   | Vatom_stk(a,stk) ->
-      apply_stack (val_of_atom a) stk v 
+      apply_stack (val_of_atom a) stk v
   | Vuniv_level lvl -> assert false
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 0e0cb4e58..6a41efac2 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -43,6 +43,7 @@ let fix_val v = (Obj.magic v : values)
 let cofix_upd_val v = (Obj.magic v : values)
 
 type vm_env
+type vm_global
 let fun_env v = (Obj.magic v : vm_env)
 let fix_env v = (Obj.magic v : vm_env)
 let cofix_env v = (Obj.magic v : vm_env)
@@ -51,6 +52,8 @@ type vstack = values array
 
 let fun_of_val v = (Obj.magic v : vfun)
 
+let vm_global (v : values array) = (Obj.magic v : vm_global)
+
 (*******************************************)
 (* Machine code *** ************************)
 (*******************************************)
@@ -407,13 +410,20 @@ let check_fix f1 f2 =
     else false
   else false
 
-external atom_rel : unit -> atom array = "get_coq_atom_tbl"
-external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
+let atom_rel : atom array ref =
+  let init i = Aid (RelKey i) in
+  ref (Array.init 40 init)
+
+let get_atom_rel () = !atom_rel
+
+let realloc_atom_rel n =
+  let n = min (2 * n + 0x100) Sys.max_array_length in
+  let init i = Aid (RelKey i) in
+  let ans = Array.init n init in
+  atom_rel := ans
 
 let relaccu_tbl =
-  let atom_rel = atom_rel() in
-  let len = Array.length atom_rel in
-  for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done;
+  let len = Array.length !atom_rel in
   ref (Array.init len mkAccuCode)
 
 let relaccu_code i =
@@ -422,9 +432,7 @@ let relaccu_code i =
   else
     begin
       realloc_atom_rel i;
-      let atom_rel = atom_rel () in
-      let nl = Array.length atom_rel in
-      for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done;
+      let nl = Array.length !atom_rel in
       relaccu_tbl :=
         Array.init nl
           (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index c6e342a96..550791b2c 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -15,6 +15,7 @@ open Cbytecodes
 
 type values
 type vm_env
+type vm_global
 type vprod
 type vfun
 type vfix
@@ -33,6 +34,8 @@ val fix_env : vfix -> vm_env
 val cofix_env : vcofix -> vm_env
 val cofix_upd_env : to_update -> vm_env
 
+val vm_global : values array -> vm_global
+
 (** Cast a value known to be a function, unsafe in general *)
 val fun_of_val : values -> vfun
 
@@ -69,6 +72,9 @@ type atom =
   | Aind of inductive
   | Asort of Sorts.t
 
+val get_atom_rel : unit -> atom array
+(** Global table of rels *)
+
 (** Zippers *)
 
 type zipper =