Use the Alloc_small macro from the OCaml runtime rather than our own.

We cannot use caml_alloc_small because the macros Setup_for_gc and
Restore_after_gc are still relevant (and critical). This means defining
the CAML_INTERNALS macro, but it is a legit use and actually documented
in the OCaml manual.

This will help with forward compatibility with OCaml compilers, e.g.,
issue #10603. Unfortunately, it also means that we can no longer use #9914
to prevent memory corruption.

The old macro is still used for OCaml versions prior to 4.10, as the
upstream macro might process Ctrl+C when it is called.

3 files changed, 24 insertions, 62 deletions

diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
deleted file mode 100644
index 38eda4d11f..0000000000
--- a/kernel/byterun/coq_gc.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/***********************************************************************/
-/*                                                                     */
-/*                           Coq Compiler                              */
-/*                                                                     */
-/*        Benjamin Gregoire, projets Logical and Cristal               */
-/*                        INRIA Rocquencourt                           */
-/*                                                                     */
-/*                                                                     */
-/***********************************************************************/
-
-#ifndef _COQ_CAML_GC_
-#define _COQ_CAML_GC_
-#include <caml/mlvalues.h>
-#include <caml/alloc.h>
-#include <caml/memory.h>
-
-typedef void (*scanning_action) (value, value *);
-
-
-CAMLextern char *young_ptr;
-CAMLextern char *young_limit;
-CAMLextern void (*scan_roots_hook) (scanning_action);
-CAMLextern void minor_collection (void);
-
-#define Caml_white (0 << 8)
-#define Caml_black (3 << 8)
-
-#ifdef HAS_OCP_MEMPROF
-
-/*  This code is necessary to make the OCamlPro memory profiling branch of
-    OCaml compile. */
-
-#define Make_header(wosize, tag, color)                                 \
-  caml_make_header(wosize, tag, color)
-
-#else
-
-#define Make_header(wosize, tag, color)                                 \
-  (((header_t) (((header_t) (wosize) << 10)                             \
-                + (color)                                               \
-                + (tag_t) (tag)))                                       \
-   )
-#endif
-
-#define Alloc_small(result, wosize, tag) do{                            \
-  young_ptr -= Bhsize_wosize (wosize);                                  \
-  if (young_ptr < young_limit){                                         \
-    young_ptr += Bhsize_wosize (wosize);                                \
-    Setup_for_gc;                                                       \
-    minor_collection ();                                                \
-    Restore_after_gc;                                                   \
-    young_ptr -= Bhsize_wosize (wosize);                                \
-  }                                                                     \
-  Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black);        \
-  (result) = Val_hp (young_ptr);                                        \
-  }while(0)
-
-
-#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 606cce0127..c30648197f 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -16,17 +16,35 @@
 #include <stdio.h>
 #include <signal.h>
 #include <stdint.h>
+#include <math.h>
+
+#define CAML_INTERNALS
 #include <caml/memory.h>
 #include <caml/signals.h>
 #include <caml/version.h>
-#include <math.h>
-#include "coq_gc.h"
+
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 #include "coq_memory.h"
 #include "coq_values.h"
 #include "coq_float64.h"
 
+#if OCAML_VERSION < 41000
+#undef Alloc_small
+#define Alloc_small(result, wosize, tag) do{                            \
+  young_ptr -= Bhsize_wosize (wosize);                                  \
+  if (young_ptr < young_limit){                                         \
+    young_ptr += Bhsize_wosize (wosize);                                \
+    Setup_for_gc;                                                       \
+    minor_collection ();                                                \
+    Restore_after_gc;                                                   \
+    young_ptr -= Bhsize_wosize (wosize);                                \
+  }                                                                     \
+  Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black);        \
+  (result) = Val_hp (young_ptr);                                        \
+  }while(0)
+#endif
+
 #ifdef ARCH_SIXTYFOUR
 #include "coq_uint63_native.h"
 #else
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 91d6773b1f..6233675c66 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -10,9 +10,12 @@
 
 #include <stdio.h>
 #include <string.h>
+
+#define CAML_INTERNALS
 #include <caml/alloc.h>
 #include <caml/address_class.h>
-#include "coq_gc.h"
+#include <caml/roots.h>
+
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 #include "coq_memory.h"