Port native_compute to OCaml 5.

Author: silene

kernel/byterun/coq_values.c

@@ -107,13 +107,32 @@ value coq_tcode_array(value tcodes) {
   CAMLreturn(res);
 }
 
-CAMLprim value coq_obj_set_tag (value arg, value new_tag)
-{
-#if OCAML_VERSION >= 50000
-// Placeholder used by native_compute
-  abort();
-#else
-  Tag_val (arg) = Int_val (new_tag);
-#endif
-  return Val_unit;
+code_t coq_accumulate_addr;
+
+value coq_proxy_accu(value clos) {
+  value v;
+  CAMLassert(Tag_val(clos) == Closure_tag && Arity_closinfo(Closinfo_val(clos)) == 2);
+  /* Field 2 of the closure contains the code pointer for the arity-2 direct call. */
+  coq_accumulate_addr = ((code_t *)clos)[2];
+  /* The following assembly block does not perform any meaningful computation;
+     it just returns a pointer to the inner code (notice the initial "jmp").
+     The inner code translates the call "foo x" (i.e., "%apply x foo") into
+     "accumulate foo.2 x". For both calls, the two arguments are stored in %rax
+     and %rbx, while register %rdi is caller-saved. */
+  asm("jmp 1f\n\t"
+      ".align 8\n\t"
+      ".quad 3067\n"
+      "2:\n\t"
+      "mov %%rax, %%rdi\n\t"
+      "mov 16(%%rbx), %%rax\n\t"
+      "mov %%rdi, %%rbx\n\t"
+      "mov coq_accumulate_addr@GOTPCREL(%%rip), %%rdi\n\t"
+      "jmp *(%%rdi)\n"
+      "1:\n\t"
+      "lea 2b(%%rip), %0\n\t"
+      : "=r"(v));
+  /* v is a pointer that can be used as field 0 of an OCaml closure. But it is
+     also a pointer to a block that is ignored by the garbage collector (notice
+     the header 3067). So, v can be put inside closures that do not have tag 247. */
+  return v;
 }

kernel/nativevalues.ml

@@ -121,23 +121,29 @@ let ret_accu = Obj.repr (ref ())
 
 type accu_val = { mutable acc_atm : atom; acc_arg : t list }
 
-external set_tag : Obj.t -> int -> unit = "coq_obj_set_tag"
-
-let mk_accu (a : atom) : t =
-  let rec accumulate data x =
-    if Obj.repr x == ret_accu then Obj.repr data
-    else
-      let data = { data with acc_arg = x :: data.acc_arg } in
-      let ans = Obj.repr (accumulate data) in
-      let () = set_tag ans accumulate_tag in
-      ans
-  in
-  let acc = { acc_atm = a; acc_arg = [] } in
-  let ans = Obj.repr (accumulate acc) in
-  (** FIXME: use another representation for accumulators, this causes naked
-      pointers. *)
-  let () = set_tag ans accumulate_tag in
-  (Obj.obj ans : t)
+(** Returns a pointer to the code of a partial application of [accumulate], yet also recognized as an unscannable block *)
+external get_proxy_accu : (accu_val -> t -> t) -> Obj.t = "coq_proxy_accu"
+
+[@@@warning "-69"]
+type accu_clos = { clos_addr : Obj.t; clos_arity : int; clos_env : Obj.t }
+
+let proxy_accu = ref None
+
+let mk_accu data =
+  let ans = { clos_addr = Option.get !proxy_accu; clos_arity = 2; clos_env = Obj.repr data } in
+  (* [ans] is indistinguishable from [accumulate data] *)
+  (Obj.magic ans : t)
+
+let accumulate data x =
+  if Obj.repr x == ret_accu then (Obj.magic data : t)
+  else mk_accu { data with acc_arg = x :: data.acc_arg }
+
+let () =
+  proxy_accu := Some (get_proxy_accu accumulate)
+
+let mk_accu a : t =
+  let data = { acc_atm = a; acc_arg = [] } in
+  mk_accu data
 
 let get_accu (k : accumulator) =
   (Obj.magic k : Obj.t -> accu_val) ret_accu

tools/configure/configure.ml

@@ -101,10 +101,7 @@ let caml_version_nums { CamlConf.caml_version; _ } =
   generic_version_nums ~name:"the OCaml compiler" caml_version
 
 let check_caml_version prefs caml_version caml_version_nums =
-  if caml_version_nums >= [5;0;0] && prefs.nativecompiler <> NativeNo then
-    let () = cprintf prefs "Your version of OCaml is %s." caml_version in
-    die "You have enabled Coq's native compiler, however it is not compatible with OCaml >= 5.0.0"
-  else if caml_version_nums >= [4;9;0] then
+  if caml_version_nums >= [4;9;0] then
     cprintf prefs "You have OCaml %s. Good!" caml_version
   else
     let () = cprintf prefs "Your version of OCaml is %s." caml_version in