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.

1 files changed, 29 insertions, 2 deletions

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);
+}