Merge PR #7079: Remove naked pointers from the VM

7 files changed, 121 insertions, 53 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index d5feafbf9..be2b05da8 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 5c85389dd..638d6b5ab 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 cfeb0a9ee..8ac1ecc79 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"
@@ -629,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]);
 	}
@@ -665,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]);
 	}
@@ -1071,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];
@@ -1476,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;
@@ -1516,8 +1528,10 @@ value coq_push_vstack(value stk, value max_stack_size) {
 }
 
 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, t, g, e, Long_val(ea));
+  CAMLreturn (coq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea)));
   print_instr("end coq_interprete");
 }
 
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index b2917a55e..542a05fd2 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"
@@ -46,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);
@@ -56,6 +62,10 @@ static void coq_scan_roots(scanning_action action)
   register value * i;
   /* 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 */
@@ -94,8 +104,12 @@ value init_coq_vm(value unit) /* ML */
     /* 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 */
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 528babebf..e05f3fb82 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);
+}
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 14f4f27c0..cea09c510 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -20,7 +20,7 @@ open Mod_subst
 
 type emitcodes = String.t
 
-external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code"
+external tcode_of_code : Bytes.t -> Vmvalues.tcode = "coq_tcode_of_code"
 
 (* Relocation information *)
 type reloc_info =
@@ -82,7 +82,7 @@ let patch buff pl f =
   (** Order seems important here? *)
   let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in
   let buff = patch_int buff reloc in
-  tcode_of_code buff (Bytes.length buff)
+  tcode_of_code buff
 
 (* Buffering of bytecode *)
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 6a41efac2..7a703e653 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -59,14 +59,17 @@ let vm_global (v : values array) = (Obj.magic v : vm_global)
 (*******************************************)
 
 type tcode
+(** A block whose first field is a C-allocated VM bytecode, encoded as char*.
+    This is compatible with the representation of the Coq VM closures. *)
+
+type tcode_array
 
 external mkAccuCode : int -> tcode = "coq_makeaccu"
 external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
 
-let tcode_of_obj v = ((Obj.obj v):tcode)
-let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0)
-let fix_code v = fun_code v
-let cofix_upd_code v = fun_code v
+let fun_code v = (Obj.magic v : tcode)
+let fix_code = fun_code
+let cofix_upd_code = fun_code
 
 
 type vswitch = {
@@ -255,6 +258,7 @@ external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
 external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
 external int_tcode : tcode -> int -> int = "coq_int_tcode"
 external accumulate : unit -> tcode = "accumulate_code"
+external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field"
 let accumulate = accumulate ()
 
 let whd_val : values -> whd =
@@ -284,7 +288,7 @@ let whd_val : values -> whd =
 let obj_of_atom : atom -> Obj.t =
   fun a ->
     let res = Obj.new_block accu_tag 2 in
-    Obj.set_field res 0 (Obj.repr accumulate);
+    set_bytecode_field res 0 accumulate;
     Obj.set_field res 1 (Obj.repr a);
     res
 
@@ -370,17 +374,20 @@ external closure_arity : vfun -> int = "coq_closure_arity"
 external offset : Obj.t -> int = "coq_offset"
 external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
 external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
+external tcode_array : tcode_array -> tcode array = "coq_tcode_array"
 
 let first o = (offset_closure o (offset o))
 let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix)
 
 let last o = (Obj.field o (Obj.size o - 1))
-let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array)
-let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array)
+let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
+let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
 
 let current_fix vf = - (offset (Obj.repr vf) / 2)
 
-let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i))
+let unsafe_fb_code fb i =
+  let off = (2 * i) * (Sys.word_size / 8) in
+  Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off))
 
 let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
 
@@ -442,13 +449,12 @@ let relaccu_code i =
 let mk_fix_body k ndef fb =
   let e = Obj.dup (Obj.repr fb) in
   for i = 0 to ndef - 1 do
-    Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i)))
+    set_bytecode_field e (2 * i) (relaccu_code (k + i))
   done;
   let fix_body i =
-    let jump_grabrec c = offset_tcode c 2 in
-    let c = jump_grabrec (unsafe_fb_code fb i)  in
+    let c = offset_tcode (unsafe_fb_code fb i) 2 in
     let res = Obj.new_block Obj.closure_tag 2 in
-    Obj.set_field res 0 (Obj.repr c);
+    set_bytecode_field res 0 c;
     Obj.set_field res 1 (offset_closure e (2*i));
     ((Obj.obj res) : vfun)  in
   Array.init ndef fix_body
@@ -486,7 +492,7 @@ let mk_cofix_body apply_varray k ndef vcf =
     Obj.set_field e 0 c;
     let atom = Obj.new_block cofix_tag 1 in
     let self = Obj.new_block accu_tag 2 in
-    Obj.set_field self 0 (Obj.repr accumulate);
+    set_bytecode_field self 0 accumulate;
     Obj.set_field self 1 (Obj.repr atom);
     apply_varray (Obj.obj e) [|Obj.obj self|] in
   Array.init ndef cofix_body