Add a file coq_arity.h generated by genOpcodeFiles.ml.

This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents
arities being mistakenly set to zero.

6 files changed, 172 insertions, 157 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 2f6781439c..aafa323b4f 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..40aaa5c021 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -21,6 +21,7 @@
 #include <caml/alloc.h>
 #include <caml/memory.h>
 #include "coq_instruct.h"
+#include "coq_arity.h"
 #include "coq_fix_code.h"
 
 #ifdef THREADED_CODE
@@ -82,7 +83,9 @@ void init_arity () {
   /* instruction with four operands */
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
-  arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
+  arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=-1;
+  for (int i = 0; i <= STOP; ++i)
+    if (arity[i] != arity2[i]) { printf("bad: %d\n", i); abort(); }
 }
 
 #endif /*  THREADED_CODE */
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..25da7c2685 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 arity2[] = {@.";
+  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 ()