Imported Upstream version 8.9.0upstream/8.9.0upstream

7 files changed, 119 insertions, 128 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index d5feafbf..be2b05da 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -18,6 +18,7 @@
 #include <caml/misc.h>
 #include <caml/mlvalues.h>
 #include <caml/fail.h>
+#include <caml/alloc.h>
 #include <caml/memory.h>
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -78,38 +79,41 @@ void * coq_stat_alloc (asize_t sz)
 }
 
 value coq_makeaccu (value i) {
-  code_t q;
-  code_t res = coq_stat_alloc(2 * sizeof(opcode_t));
-  q = res;
+  CAMLparam1(i);
+  CAMLlocal1(res);
+  code_t q = coq_stat_alloc(2 * sizeof(opcode_t));
+  res = caml_alloc_small(1, Abstract_tag);
+  Code_val(res) = q;
   *q++ = VALINSTR(MAKEACCU);
   *q = (opcode_t)Int_val(i);
-  return (value)res;
+  CAMLreturn(res);
 }
 
 value coq_pushpop (value i) {
-  code_t res;
-  int n;
-  n = Int_val(i);
+  CAMLparam1(i);
+  CAMLlocal1(res);
+  code_t q;
+  res = caml_alloc_small(1, Abstract_tag);
+  int n = Int_val(i);
   if (n == 0) {
-    res = coq_stat_alloc(sizeof(opcode_t));
-    *res = VALINSTR(STOP);
-    return (value)res;
+    q = coq_stat_alloc(sizeof(opcode_t));
+    Code_val(res) = q;
+    *q = VALINSTR(STOP);
+    CAMLreturn(res);
   }
   else {
-    code_t q;
-    res = coq_stat_alloc(3 * sizeof(opcode_t));
-    q = res;
+    q = coq_stat_alloc(3 * sizeof(opcode_t));
+    Code_val(res) = q;
     *q++ = VALINSTR(POP);
     *q++ = (opcode_t)n;
     *q = VALINSTR(STOP);
-    return (value)res;
+    CAMLreturn(res);
   }
 }
 
 value coq_is_accumulate_code(value code){
-  code_t q;
+  code_t q = Code_val(code);
   int res;
-  q = (code_t)code;
   res = Is_instruction(q,ACCUMULATE);
   return Val_bool(res);
 }
@@ -132,11 +136,14 @@ value coq_is_accumulate_code(value code){
 #define COPY32(dst,src) (*dst=*src)
 #endif /* ARCH_BIG_ENDIAN */
 
-value coq_tcode_of_code (value code, value size) {
-  code_t p, q, res; 
-  asize_t len = (asize_t) Long_val(size);
-  res = coq_stat_alloc(len);
-  q = res;
+value coq_tcode_of_code (value code) {
+  CAMLparam1 (code);
+  CAMLlocal1 (res);
+  code_t p, q;
+  asize_t len = (asize_t) caml_string_length(code);
+  res = caml_alloc_small(1, Abstract_tag);
+  q = coq_stat_alloc(len);
+  Code_val(res) = q;
   len /= sizeof(opcode_t);
   for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {  
     opcode_t instr;
@@ -166,5 +173,5 @@ value coq_tcode_of_code (value code, value size) {
       for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
     }
   }
-  return (value)res;
+  CAMLreturn(res);
 }
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 5c85389d..638d6b5a 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -26,7 +26,7 @@ void init_arity();
 
 #define Is_instruction(pc,instr) (*pc == VALINSTR(instr))
 
-value coq_tcode_of_code(value code, value len);
+value coq_tcode_of_code(value code);
 value coq_makeaccu (value i);
 value coq_pushpop (value i);
 value coq_is_accumulate_code(value code);
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index af89712d..a944dbb0 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -16,6 +16,7 @@
 #include <stdio.h>
 #include <signal.h>
 #include <stdint.h>
+#include <caml/memory.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -163,8 +164,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 +200,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;
@@ -626,7 +630,7 @@ value coq_interprete
 	print_instr("CLOSUREREC");
 	if (nvars > 0) *--sp = accu;
 	/* construction du vecteur de type */
-	Alloc_small(accu, nfuncs, 0);
+        Alloc_small(accu, nfuncs, Abstract_tag);
 	for(i = 0; i < nfuncs; i++) {
 	  Field(accu,i) = (value)(pc+pc[i]);
 	}
@@ -662,7 +666,7 @@ value coq_interprete
 	print_instr("CLOSURECOFIX");
 	if (nvars > 0) *--sp = accu;
 	/* construction du vecteur de type */
-	Alloc_small(accu, nfunc, 0);
+        Alloc_small(accu, nfunc, Abstract_tag);
 	for(i = 0; i < nfunc; i++) {
 	  Field(accu,i) = (value)(pc+pc[i]);
 	}
@@ -1028,7 +1032,7 @@ value coq_interprete
             CHECK_STACK(nargs+1);
 	    sp -= nargs;
 	    for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); 
-	    *--sp = accu; // Last argument is the pointer to the suspension
+            *--sp = accu; // Leftmost argument is the pointer to the suspension
 	    print_lint(nargs);
 	    coq_extra_args = nargs;
 	    pc = Code_val(coq_env); // Trigger evaluation
@@ -1068,12 +1072,22 @@ value coq_interprete
 	      }
 	    }
 	    *--sp = accu;
-	    /* We create the switch zipper */
-	    Alloc_small(accu, 5, Default_tag);
-	    Field(accu, 0) =  (value)typlbl; Field(accu, 1) = (value)swlbl; 
-	    Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; 
-	    Field(accu, 4) = coq_env;
-	    sp++;sp[0] = accu;
+            /* Create bytecode wrappers */
+            Alloc_small(accu, 1, Abstract_tag);
+            Code_val(accu) = typlbl;
+            *--sp = accu;
+            Alloc_small(accu, 1, Abstract_tag);
+            Code_val(accu) = swlbl;
+            *--sp = accu;
+            /* We create the switch zipper */
+            Alloc_small(accu, 5, Default_tag);
+            Field(accu, 0) = sp[1];
+            Field(accu, 1) = sp[0];
+            Field(accu, 2) = sp[3];
+            Field(accu, 3) = sp[2];
+            Field(accu, 4) = coq_env;
+            sp += 3;
+            sp[0] = accu;
 	    /* We create the atom */
 	    Alloc_small(accu, 2, ATOM_SWITCH_TAG);
 	    Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
@@ -1460,7 +1474,7 @@ value coq_interprete
       Instruct(STOP){
 	print_instr("STOP");
 	coq_sp = sp;
-	return accu;
+        CAMLreturn(accu);
       }
       
   
@@ -1473,7 +1487,8 @@ value coq_interprete
 #endif
 }
 
-value coq_push_ra(value tcode) { 
+value coq_push_ra(value code) {
+  code_t tcode = Code_val(code);
   print_instr("push_ra");
   coq_sp -= 3;
   coq_sp[0] = (value) tcode;
@@ -1512,12 +1527,18 @@ 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) {
+  // Registering the other arguments w.r.t. the OCaml GC is done by coq_interprete
+  CAMLparam1(tcode);
   print_instr("coq_interprete");
-  return coq_interprete((code_t)tcode, a, e, Long_val(ea));
+  CAMLreturn (coq_interprete(Code_val(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 60865c32..c04e9e00 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 45cfae50..542a05fd 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -10,6 +10,8 @@
 
 #include <stdio.h>
 #include <string.h> 
+#include <caml/alloc.h>
+#include <caml/address_class.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -24,10 +26,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 */
 
@@ -50,7 +48,11 @@ value coq_static_alloc(value size) /* ML */
 
 value accumulate_code(value unit) /* ML */
 {
-  return (value) accumulate;
+  CAMLparam1(unit);
+  CAMLlocal1(res);
+  res = caml_alloc_small(1, Abstract_tag);
+  Code_val(res) = accumulate;
+  CAMLreturn(res);
 }
 
 static void (*coq_prev_scan_roots_hook) (scanning_action);
@@ -58,11 +60,12 @@ 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++) {
+#ifdef NO_NAKED_POINTERS
+    /* The VM stack may contain C-allocated bytecode */
+    if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue;
+#endif
     (*action) (*i, i);
   };
   /* Hook */
@@ -79,24 +82,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,13 +101,15 @@ 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();
     
-    /* Some predefined pointer code */
-    accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t));
+    /* Some predefined pointer code.
+     * It is typically contained in accumlator blocks whose tag is 0 and thus
+     * scanned by the GC, so make it look like an OCaml block. */
+    value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
+    Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black);        \
+    accumulate = (code_t) Val_hp(accu_block);
     *accumulate = VALINSTR(ACCUMULATE);
 
   /* Initialize GC */
@@ -157,53 +148,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 cec34f56..9375b15d 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/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 528babeb..e05f3fb8 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -9,6 +9,7 @@
 /***********************************************************************/
 
 #include <stdio.h>
+#include <caml/memory.h>
 #include "coq_fix_code.h"
 #include "coq_instruct.h"
 #include "coq_memory.h"
@@ -58,10 +59,36 @@ value coq_offset_closure(value v, value offset){
   return (value)&Field(v, Int_val(offset));
 }
 
+value coq_set_bytecode_field(value v, value i, value code) {
+  // No write barrier because the bytecode does not live on the OCaml heap
+  Field(v, Long_val(i)) = (value) Code_val(code);
+  return Val_unit;
+}
+
 value coq_offset_tcode(value code,value offset){
-  return((value)((code_t)code + Int_val(offset)));
+  CAMLparam1(code);
+  CAMLlocal1(res);
+  res = caml_alloc_small(1, Abstract_tag);
+  Code_val(res) = Code_val(code) + Int_val(offset);
+  CAMLreturn(res);
 }
 
-value coq_int_tcode(value code, value offset) {
+value coq_int_tcode(value pc, value offset) {
+  code_t code = Code_val(pc);
   return Val_int(*((code_t) code + Int_val(offset)));
 }
+
+value coq_tcode_array(value tcodes) {
+  CAMLparam1(tcodes);
+  CAMLlocal2(res, tmp);
+  int i;
+  /* Assumes that the vector of types is small. This was implicit in the
+    previous code which was building the type array using Alloc_small. */
+  res = caml_alloc_small(Wosize_val(tcodes), Default_tag);
+  for (i = 0; i < Wosize_val(tcodes); i++) {
+    tmp = caml_alloc_small(1, Abstract_tag);
+    Code_val(tmp) = (code_t) Field(tcodes, i);
+    Store_field(res, i, tmp);
+  }
+  CAMLreturn(res);
+}