Merge PR #13868: Make genOpcodeFiles.ml handle opcode arity.

Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot

8 files changed, 172 insertions, 223 deletions

diff --git a/.gitignore b/.gitignore
index aab1d1ede7..7d05a12cfe 100644
--- a/.gitignore
+++ b/.gitignore
@@ -152,6 +152,7 @@ plugins/ssr/ssrvernac.ml
 
 kernel/byterun/coq_instruct.h
 kernel/byterun/coq_jumptbl.h
+kernel/byterun/coq_arity.h
 kernel/genOpcodeFiles.exe
 kernel/vmopcodes.ml
 kernel/uint63.ml
diff --git a/Makefile.build b/Makefile.build
index b307bde5df..d619fd3c85 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -367,6 +367,10 @@ kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe
 	$(SHOW)'WRITE $@'
 	$(HIDE)$< jump > $@
 
+kernel/byterun/coq_arity.h: kernel/genOpcodeFiles.exe
+	$(SHOW)'WRITE $@'
+	$(HIDE)$< arity > $@
+
 kernel/vmopcodes.ml: kernel/genOpcodeFiles.exe
 	$(SHOW)'WRITE $@'
 	$(HIDE)$< copml > $@
diff --git a/Makefile.make b/Makefile.make
index eeb3e9b539..5e45e71c8c 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -109,7 +109,7 @@ GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml no
 GENMLGFILES:= $(MLGFILES:.mlg=.ml)
 GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml kernel/float64.ml
 GENMLIFILES:=$(GRAMMLIFILES)
-GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h
+GENHFILES:=$(addprefix kernel/byterun/, coq_instruct.h coq_jumptbl.h coq_arity.h)
 GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe
 COQ_EXPORTED += GRAMFILES GRAMMLFILES GRAMMLIFILES GENMLFILES GENHFILES GENFILES
 
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 2c0b580e24..20890a28dc 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -21,70 +21,12 @@
 #include <caml/alloc.h>
 #include <caml/memory.h>
 #include "coq_instruct.h"
+#include "coq_arity.h"
 #include "coq_fix_code.h"
 
 #ifdef THREADED_CODE
 char ** coq_instr_table;
 char * coq_instr_base;
-int arity[STOP+1];
-
-void init_arity () {
-  /* instruction with zero operand */
-  arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]=
-    arity[ACC6]=arity[ACC7]=
-    arity[PUSH]=arity[PUSHACC1]=
-    arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=
-    arity[PUSHACC6]=arity[PUSHACC7]=
-    arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=
-    arity[PUSHENVACC0]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=
-    arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]=
-    arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]=
-    arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]=
-    arity[GETFIELD0]=arity[GETFIELD1]=
-    arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
-    arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
-    arity[ACCUMULATE]=arity[STOP]=
-    0;
-  /* instruction with one operand */
-  arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
-    arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
-    arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]=
-    arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
-    arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
-    arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
-    arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=
-    arity[BRANCH]=arity[ENSURESTACKCAPACITY]=
-    arity[CHECKADDINT63]=arity[CHECKADDCINT63]=arity[CHECKADDCARRYCINT63]=
-    arity[CHECKSUBINT63]=arity[CHECKSUBCINT63]=arity[CHECKSUBCARRYCINT63]=
-    arity[CHECKMULINT63]=arity[CHECKMULCINT63]=
-    arity[CHECKDIVINT63]=arity[CHECKMODINT63]=arity[CHECKDIVEUCLINT63]=
-    arity[CHECKDIV21INT63]=
-    arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]=
-    arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
-    arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
-    arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
-    arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]=
-    arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]=
-    arity[CHECKCLASSIFYFLOAT]=
-    arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]=
-    arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]=
-    arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]=
-    arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=
-    arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=
-    arity[CHECKNEXTUPFLOATINPLACE]=arity[CHECKNEXTDOWNFLOATINPLACE]=
-    1;
-  /* instruction with two operands */
-  arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
-    arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]=
-    arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]=
-    arity[PROJ]=
-    2;
-  /* instruction with four operands */
-  arity[MAKESWITCHBLOCK]=4;
-  /* instruction with arbitrary operands */
-  arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
-}
-
 #endif /*  THREADED_CODE */
 
 
@@ -166,9 +108,7 @@ value coq_tcode_of_code (value code) {
     opcode_t instr;
     COPY32(&instr,p);
     p++;
-    if (instr < 0 || instr > STOP){
-      instr = STOP;
-    };
+    if (instr < 0 || instr > STOP) abort();
     *q++ = VALINSTR(instr);
     if (instr == SWITCH) {
       uint32_t i, sizes, const_size, block_size;
@@ -185,8 +125,9 @@ value coq_tcode_of_code (value code) {
       q++;
       for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
     } else {
-      uint32_t i, ar;
+      int i, ar;
       ar = arity[instr];
+      if (ar < 0) abort();
       for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
     }
   }
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 5a233e6178..916d9753a4 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -18,7 +18,6 @@ void * coq_stat_alloc (asize_t sz);
 #ifdef THREADED_CODE
 extern char ** coq_instr_table;
 extern char * coq_instr_base;
-void init_arity();
 #define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base))
 #else
 #define VALINSTR(instr) instr
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index fe076f8f04..a55ff57c8d 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -100,9 +100,6 @@ value init_coq_vm(value unit) /* ML */
     fprintf(stderr,"already open \n");fflush(stderr);}
   else {
     drawinstr=0;
-#ifdef THREADED_CODE
-    init_arity();
-#endif /* THREADED_CODE */
     /* Allocate the table of global and the stack */
     init_coq_stack();
     /* Initialing the interpreter */
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index d3e2a2fa7f..a2484f79a7 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -14,3 +14,7 @@
 (rule
  (targets coq_jumptbl.h)
  (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))
+
+(rule
+ (targets coq_arity.h)
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe arity))))
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 0e1cd0c56a..bda65956be 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -10,192 +10,195 @@
 
 (** List of opcodes.
 
-    It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and
-    [vmopcodes.ml] files.
+    It is used to generate the files [coq_instruct.h], [coq_jumptbl.h],
+    [coq_arity.h], and [vmopcodes.ml].
 
-    If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c
-    with the arity of the instruction and maybe coq_tcode_of_code.
+    [STOP] needs to be the last opcode.
+
+    Arity -1 designates opcodes that need special handling in [coq_fix_code.c].
 *)
 let opcodes =
   [|
-    "ACC0";
-    "ACC1";
-    "ACC2";
-    "ACC3";
-    "ACC4";
-    "ACC5";
-    "ACC6";
-    "ACC7";
-    "ACC";
-    "PUSH";
-    "PUSHACC1";
-    "PUSHACC2";
-    "PUSHACC3";
-    "PUSHACC4";
-    "PUSHACC5";
-    "PUSHACC6";
-    "PUSHACC7";
-    "PUSHACC";
-    "POP";
-    "ENVACC0";
-    "ENVACC1";
-    "ENVACC2";
-    "ENVACC3";
-    "ENVACC";
-    "PUSHENVACC0";
-    "PUSHENVACC1";
-    "PUSHENVACC2";
-    "PUSHENVACC3";
-    "PUSHENVACC";
-    "PUSH_RETADDR";
-    "APPLY";
-    "APPLY1";
-    "APPLY2";
-    "APPLY3";
-    "APPLY4";
-    "APPTERM";
-    "APPTERM1";
-    "APPTERM2";
-    "APPTERM3";
-    "RETURN";
-    "RESTART";
-    "GRAB";
-    "GRABREC";
-    "CLOSURE";
-    "CLOSUREREC";
-    "CLOSURECOFIX";
-    "OFFSETCLOSURE0";
-    "OFFSETCLOSURE1";
-    "OFFSETCLOSURE";
-    "PUSHOFFSETCLOSURE0";
-    "PUSHOFFSETCLOSURE1";
-    "PUSHOFFSETCLOSURE";
-    "GETGLOBAL";
-    "PUSHGETGLOBAL";
-    "MAKEBLOCK";
-    "MAKEBLOCK1";
-    "MAKEBLOCK2";
-    "MAKEBLOCK3";
-    "MAKEBLOCK4";
-    "SWITCH";
-    "PUSHFIELDS";
-    "GETFIELD0";
-    "GETFIELD1";
-    "GETFIELD";
-    "SETFIELD";
-    "PROJ";
-    "ENSURESTACKCAPACITY";
-    "CONST0";
-    "CONST1";
-    "CONST2";
-    "CONST3";
-    "CONSTINT";
-    "PUSHCONST0";
-    "PUSHCONST1";
-    "PUSHCONST2";
-    "PUSHCONST3";
-    "PUSHCONSTINT";
-    "ACCUMULATE";
-    "MAKESWITCHBLOCK";
-    "MAKEACCU";
-    "BRANCH";
-    "CHECKADDINT63";
-    "CHECKADDCINT63";
-    "CHECKADDCARRYCINT63";
-    "CHECKSUBINT63";
-    "CHECKSUBCINT63";
-    "CHECKSUBCARRYCINT63";
-    "CHECKMULINT63";
-    "CHECKMULCINT63";
-    "CHECKDIVINT63";
-    "CHECKMODINT63";
-    "CHECKDIVEUCLINT63";
-    "CHECKDIV21INT63";
-    "CHECKLXORINT63";
-    "CHECKLORINT63";
-    "CHECKLANDINT63";
-    "CHECKLSLINT63";
-    "CHECKLSRINT63";
-    "CHECKADDMULDIVINT63";
-    "CHECKEQINT63";
-    "CHECKLTINT63";
-    "CHECKLEINT63";
-    "CHECKCOMPAREINT63";
-    "CHECKHEAD0INT63";
-    "CHECKTAIL0INT63";
-    "CHECKOPPFLOAT";
-    "CHECKABSFLOAT";
-    "CHECKEQFLOAT";
-    "CHECKLTFLOAT";
-    "CHECKLEFLOAT";
-    "CHECKCOMPAREFLOAT";
-    "CHECKCLASSIFYFLOAT";
-    "CHECKADDFLOAT";
-    "CHECKSUBFLOAT";
-    "CHECKMULFLOAT";
-    "CHECKDIVFLOAT";
-    "CHECKSQRTFLOAT";
-    "CHECKFLOATOFINT63";
-    "CHECKFLOATNORMFRMANTISSA";
-    "CHECKFRSHIFTEXP";
-    "CHECKLDSHIFTEXP";
-    "CHECKNEXTUPFLOAT";
-    "CHECKNEXTDOWNFLOAT";
-    "CHECKNEXTUPFLOATINPLACE";
-    "CHECKNEXTDOWNFLOATINPLACE";
-    "CHECKCAMLCALL2_1";
-    "CHECKCAMLCALL1";
-    "CHECKCAMLCALL2";
-    "CHECKCAMLCALL3_1";
-    "STOP"
+    "ACC0", 0;
+    "ACC1", 0;
+    "ACC2", 0;
+    "ACC3", 0;
+    "ACC4", 0;
+    "ACC5", 0;
+    "ACC6", 0;
+    "ACC7", 0;
+    "ACC", 1;
+    "PUSH", 0;
+    "PUSHACC1", 0;
+    "PUSHACC2", 0;
+    "PUSHACC3", 0;
+    "PUSHACC4", 0;
+    "PUSHACC5", 0;
+    "PUSHACC6", 0;
+    "PUSHACC7", 0;
+    "PUSHACC", 1;
+    "POP", 1;
+    "ENVACC0", 0;
+    "ENVACC1", 0;
+    "ENVACC2", 0;
+    "ENVACC3", 0;
+    "ENVACC", 1;
+    "PUSHENVACC0", 0;
+    "PUSHENVACC1", 0;
+    "PUSHENVACC2", 0;
+    "PUSHENVACC3", 0;
+    "PUSHENVACC", 1;
+    "PUSH_RETADDR", 1;
+    "APPLY", 1;
+    "APPLY1", 0;
+    "APPLY2", 0;
+    "APPLY3", 0;
+    "APPLY4", 0;
+    "APPTERM", 2;
+    "APPTERM1", 1;
+    "APPTERM2", 1;
+    "APPTERM3", 1;
+    "RETURN", 1;
+    "RESTART", 0;
+    "GRAB", 1;
+    "GRABREC", 1;
+    "CLOSURE", 2;
+    "CLOSUREREC", -1;
+    "CLOSURECOFIX", -1;
+    "OFFSETCLOSURE0", 0;
+    "OFFSETCLOSURE1", 0;
+    "OFFSETCLOSURE", 1;
+    "PUSHOFFSETCLOSURE0", 0;
+    "PUSHOFFSETCLOSURE1", 0;
+    "PUSHOFFSETCLOSURE", 1;
+    "GETGLOBAL", 1;
+    "PUSHGETGLOBAL", 1;
+    "MAKEBLOCK", 2;
+    "MAKEBLOCK1", 1;
+    "MAKEBLOCK2", 1;
+    "MAKEBLOCK3", 1;
+    "MAKEBLOCK4", 1;
+    "SWITCH", -1;
+    "PUSHFIELDS", 1;
+    "GETFIELD0", 0;
+    "GETFIELD1", 0;
+    "GETFIELD", 1;
+    "SETFIELD", 1;
+    "PROJ", 2;
+    "ENSURESTACKCAPACITY", 1;
+    "CONST0", 0;
+    "CONST1", 0;
+    "CONST2", 0;
+    "CONST3", 0;
+    "CONSTINT", 1;
+    "PUSHCONST0", 0;
+    "PUSHCONST1", 0;
+    "PUSHCONST2", 0;
+    "PUSHCONST3", 0;
+    "PUSHCONSTINT", 1;
+    "ACCUMULATE", 0;
+    "MAKESWITCHBLOCK", 4;
+    "MAKEACCU", 1;
+    "BRANCH", 1;
+    "CHECKADDINT63", 1;
+    "CHECKADDCINT63", 1;
+    "CHECKADDCARRYCINT63", 1;
+    "CHECKSUBINT63", 1;
+    "CHECKSUBCINT63", 1;
+    "CHECKSUBCARRYCINT63", 1;
+    "CHECKMULINT63", 1;
+    "CHECKMULCINT63", 1;
+    "CHECKDIVINT63", 1;
+    "CHECKMODINT63", 1;
+    "CHECKDIVEUCLINT63", 1;
+    "CHECKDIV21INT63", 1;
+    "CHECKLXORINT63", 1;
+    "CHECKLORINT63", 1;
+    "CHECKLANDINT63", 1;
+    "CHECKLSLINT63", 1;
+    "CHECKLSRINT63", 1;
+    "CHECKADDMULDIVINT63", 1;
+    "CHECKEQINT63", 1;
+    "CHECKLTINT63", 1;
+    "CHECKLEINT63", 1;
+    "CHECKCOMPAREINT63", 1;
+    "CHECKHEAD0INT63", 1;
+    "CHECKTAIL0INT63", 1;
+    "CHECKOPPFLOAT", 1;
+    "CHECKABSFLOAT", 1;
+    "CHECKEQFLOAT", 1;
+    "CHECKLTFLOAT", 1;
+    "CHECKLEFLOAT", 1;
+    "CHECKCOMPAREFLOAT", 1;
+    "CHECKCLASSIFYFLOAT", 1;
+    "CHECKADDFLOAT", 1;
+    "CHECKSUBFLOAT", 1;
+    "CHECKMULFLOAT", 1;
+    "CHECKDIVFLOAT", 1;
+    "CHECKSQRTFLOAT", 1;
+    "CHECKFLOATOFINT63", 1;
+    "CHECKFLOATNORMFRMANTISSA", 1;
+    "CHECKFRSHIFTEXP", 1;
+    "CHECKLDSHIFTEXP", 1;
+    "CHECKNEXTUPFLOAT", 1;
+    "CHECKNEXTDOWNFLOAT", 1;
+    "CHECKNEXTUPFLOATINPLACE", 1;
+    "CHECKNEXTDOWNFLOATINPLACE", 1;
+    "CHECKCAMLCALL2_1", 2;
+    "CHECKCAMLCALL1", 2;
+    "CHECKCAMLCALL2", 2;
+    "CHECKCAMLCALL3_1", 2;
+    "STOP", 0
   |]
 
 let pp_c_comment fmt =
-  Format.fprintf fmt "/* %a */"
+  Format.fprintf fmt "/* %s */"
 
 let pp_ocaml_comment fmt =
-  Format.fprintf fmt "(* %a *)"
+  Format.fprintf fmt "(* %s *)"
 
 let pp_header isOcaml fmt =
   Format.fprintf fmt "%a"
-    (fun fmt ->
-       (if isOcaml then pp_ocaml_comment else pp_c_comment) fmt
-         Format.pp_print_string)
+    (if isOcaml then pp_ocaml_comment else pp_c_comment)
     "DO NOT EDIT: automatically generated by kernel/genOpcodeFiles.ml"
 
-let pp_with_commas fmt k =
-  Array.iteri (fun n s ->
-      Format.fprintf fmt "  %a%s@."
-        k s
-        (if n + 1 < Array.length opcodes
-         then "," else "")
-    ) opcodes
-
 let pp_coq_instruct_h fmt =
-  let line = Format.fprintf fmt "%s@." in
   pp_header false fmt;
-  line "#pragma once";
-  line "enum instructions {";
-  pp_with_commas fmt Format.pp_print_string;
-  line "};"
+  Format.fprintf fmt "#pragma once@.enum instructions {@.";
+  Array.iter (fun (name, _) ->
+      Format.fprintf fmt "  %s,@." name
+    ) opcodes;
+  Format.fprintf fmt "};@."
 
 let pp_coq_jumptbl_h fmt =
-  pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s")
+  pp_header false fmt;
+  Array.iter (fun (name, _) ->
+      Format.fprintf fmt "  &&coq_lbl_%s,@." name
+    ) opcodes
+
+let pp_coq_arity_h fmt =
+  pp_header false fmt;
+  Format.fprintf fmt "static signed char arity[] = {@.";
+  Array.iter (fun (_, arity) ->
+      Format.fprintf fmt "  %d,@." arity
+    ) opcodes;
+  Format.fprintf fmt "};@."
 
 let pp_vmopcodes_ml fmt =
   pp_header true fmt;
   Array.iteri (fun n s ->
       Format.fprintf fmt "let op%s = %d@.@." s n
-    ) opcodes
+    ) (Array.map fst opcodes)
 
 let usage () =
-  Format.eprintf "usage: %s [enum|jump|copml]@." Sys.argv.(0);
+  Format.eprintf "usage: %s [enum|jump|arity|copml]@." Sys.argv.(0);
   exit 1
 
 let main () =
   match Sys.argv.(1) with
   | "enum" -> pp_coq_instruct_h Format.std_formatter
   | "jump" -> pp_coq_jumptbl_h Format.std_formatter
+  | "arity" -> pp_coq_arity_h Format.std_formatter
   | "copml" -> pp_vmopcodes_ml Format.std_formatter
   | _ -> usage ()
   | exception Invalid_argument _ -> usage ()