Wrap VM bytecode used on the OCaml side in an OCaml block.

This prevents the existence of a few naked pointers to C heap from the OCaml
heap. VM bytecode is represented as any block of size at least 1 whose first
field points to a C-allocated string.

This representation is compatible with the Coq VM representation of
(potentially recursive) closures, which are already specifically tailored
in the OCaml GC to be able to contain out-of-heap data.

5 files changed, 89 insertions, 36 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..9102af702 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -10,6 +10,7 @@
 
 #include <stdio.h>
 #include <string.h> 
+#include <caml/alloc.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -46,7 +47,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);
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);
+}