1 files changed, 18 insertions, 74 deletions

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;