From b5aed34bb8bbdda27646720db29a8d47c79653b9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Mar 2018 15:41:50 +0100
Subject: Moving the VM global data to a ML reference.

---
 kernel/byterun/coq_interp.c | 17 ++++++++++-------
 kernel/byterun/coq_interp.h |  8 +++-----
 kernel/byterun/coq_memory.c | 37 +------------------------------------
 kernel/byterun/coq_memory.h |  4 ----
 4 files changed, 14 insertions(+), 52 deletions(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index af89712d5e..ced2a175d0 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_global_data, value coq_env, long coq_extra_args)
 {
+  /* coq_accu is not allocated on the OCaml heap */
+  CAMLparam1(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,12 @@ 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 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, 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_eval_tcode (value tcode, value g, value e) {
+  return coq_interprete_ml(tcode, Val_unit, g, e, 0);
 }
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
index 60865c32ec..189c9a127c 100644
--- a/kernel/byterun/coq_interp.h
+++ b/kernel/byterun/coq_interp.h
@@ -17,11 +17,9 @@ 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 g, value e, value ea);
 
 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_global_data, value coq_env, long coq_extra_args);
 
+value coq_eval_tcode (value tcode, value g, value e);
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 45cfae509d..40dbda866a 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -25,7 +25,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
 /* global_data */
 
 
-value coq_global_data;
 value coq_atom_tbl;
 
 int drawinstr;
@@ -59,7 +58,6 @@ 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++) {
@@ -79,14 +77,6 @@ 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);
@@ -96,7 +86,7 @@ void init_coq_atom_tbl(long requested_size){
 void init_coq_interpreter()
 {
   coq_sp = coq_stack_high;
-  coq_interprete(NULL, Val_unit, Val_unit, 0);
+  coq_interprete(NULL, Val_unit, Atom(0), Val_unit, 0);
 }
 
 static int coq_vm_initialized = 0;
@@ -112,7 +102,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,35 +146,11 @@ 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;
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index cec34f566c..06711ad708 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,7 +33,6 @@ extern value * coq_stack_threshold;
 
 /* global_data */
 
-extern value coq_global_data;
 extern int coq_all_transp;
 extern value coq_atom_tbl;
 
@@ -53,8 +51,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 */
-- 
cgit v1.2.3


From fd5dc5b37e765bdb864e874c451d42d03d737792 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 3 Mar 2018 19:43:02 +0100
Subject: Moving the VM global atom table to a ML reference.

---
 kernel/byterun/coq_interp.c | 16 ++++++++++------
 kernel/byterun/coq_interp.h |  7 ++++---
 kernel/byterun/coq_memory.c | 37 +------------------------------------
 kernel/byterun/coq_memory.h |  3 ---
 4 files changed, 15 insertions(+), 48 deletions(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ced2a175d0..cfeb0a9ee1 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -163,10 +163,10 @@ extern void caml_process_pending_signals(void);
 /* The interpreter itself */
 
 value coq_interprete
-(code_t coq_pc, value coq_accu, value coq_global_data, 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 */
-  CAMLparam1(coq_global_data);
+  CAMLparam2(coq_atom_tbl, coq_global_data);
 
   /*Declaration des variables */
 #ifdef PC_REG
@@ -1515,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 g, 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, g, 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 g, value e) {
-  return coq_interprete_ml(tcode, Val_unit, g, 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 189c9a127c..c04e9e00b2 100644
--- a/kernel/byterun/coq_interp.h
+++ b/kernel/byterun/coq_interp.h
@@ -17,9 +17,10 @@ value coq_push_arguments(value args);
 
 value coq_push_vstack(value stk);
 
-value coq_interprete_ml(value tcode, value a, value g, 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_global_data, 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);
 
-value coq_eval_tcode (value tcode, value g, value e);
+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 40dbda866a..b2917a55ee 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -24,9 +24,6 @@ value * coq_stack_threshold;
 asize_t coq_max_stack_size = Coq_max_stack_size;
 /* global_data */
 
-
-value coq_atom_tbl;
-
 int drawinstr;
 /* interp state */
 
@@ -57,8 +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_atom_tbl, &coq_atom_tbl);
   /* Scan the stack */
   for (i = coq_sp; i < coq_stack_high; i++) {
     (*action) (*i, i);
@@ -77,16 +72,10 @@ void init_coq_stack()
   coq_max_stack_size = Coq_max_stack_size;
 }  
 
-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, Atom(0), Val_unit, 0);
+  coq_interprete(NULL, Val_unit, Atom(0), Atom(0), Val_unit, 0);
 }
 
 static int coq_vm_initialized = 0;
@@ -102,7 +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_atom_tbl(40);
     /* Initialing the interpreter */
     init_coq_interpreter();
     
@@ -146,29 +134,6 @@ void realloc_coq_stack(asize_t required_space)
 #undef shift
 }
 
-value get_coq_atom_tbl(value unit)                  /* ML */
-{
-  return coq_atom_tbl;
-}
-
-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 06711ad708..9375b15de2 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -34,7 +34,6 @@ extern value * coq_stack_threshold;
 /* global_data */
 
 extern int coq_all_transp;
-extern value coq_atom_tbl;
 
 extern int drawinstr;
 /* interp state */
@@ -51,8 +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_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_ */
-- 
cgit v1.2.3