[Kernel] Simpler generation of opcode files

Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.

7 files changed, 204 insertions, 82 deletions

diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
deleted file mode 100644
index c7abedaed6..0000000000
--- a/kernel/byterun/coq_instruct.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/***********************************************************************/
-/*                                                                     */
-/*                           Coq Compiler                              */
-/*                                                                     */
-/*        Benjamin Gregoire, projets Logical and Cristal               */
-/*                        INRIA Rocquencourt                           */
-/*                                                                     */
-/*                                                                     */
-/***********************************************************************/
-
-#ifndef _COQ_INSTRUCT_
-#define _COQ_INSTRUCT_
-
-/* Nota: this list of instructions is parsed to produce derived files */
-/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase    */
-/* and alone on lines starting by two spaces.                         */
-/* 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.     */
-
-enum instructions {
-  ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
-  PUSH, 
-  PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4,
-  PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC, 
-  POP,
-  ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC,
-  PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC,
-  PUSH_RETADDR,
-  APPLY, APPLY1, APPLY2, APPLY3, APPLY4,
-  APPTERM, APPTERM1, APPTERM2, APPTERM3,
-  RETURN, RESTART, GRAB, GRABREC, 
-  CLOSURE, CLOSUREREC, CLOSURECOFIX,
-  OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE,
-  PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, 
-  PUSHOFFSETCLOSURE,
-  GETGLOBAL, PUSHGETGLOBAL,
-  MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4,
-  SWITCH, PUSHFIELDS, 
-  GETFIELD0, GETFIELD1, GETFIELD, 
-  SETFIELD0, SETFIELD1, SETFIELD,
-  PROJ,
-  ENSURESTACKCAPACITY,
-  CONST0, CONST1, CONST2, CONST3, CONSTINT,
-  PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
-  ACCUMULATE,
-  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, 
-/* spiwack: */
-  BRANCH,
-  CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63,
-  CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63,
-  CHECKMULINT63, CHECKMULCINT63,
-  CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63,
-  CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63,
-  CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63,
-  CHECKLSLINT63CONST1, CHECKLSRINT63CONST1,
-
-  CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63,
-  CHECKCOMPAREINT63,
-
-  CHECKHEAD0INT63, CHECKTAIL0INT63,
-
-  ISINT, AREINT2,
-
-  STOP
-};
-
-#endif /* _COQ_INSTRUCT_ */
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index c3c44670be..20bdf28e54 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -5,6 +5,9 @@
  (c_names coq_fix_code coq_memory coq_values coq_interp))
 
 (rule
+ (targets coq_instruct.h)
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum))))
+
+(rule
  (targets coq_jumptbl.h)
- (deps (:h-file coq_instruct.h) make_jumptbl.sh)
- (action (bash "./make_jumptbl.sh %{h-file} %{targets}")))
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))
diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh
deleted file mode 100755
index eacd4daac8..0000000000
--- a/kernel/byterun/make_jumptbl.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/usr/bin/env bash
-
-sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2}
diff --git a/kernel/dune b/kernel/dune
index 1f2d696a36..a8a87a3e95 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -3,13 +3,16 @@
  (synopsis "The Coq Kernel")
  (public_name coq.kernel)
  (wrapped false)
- (modules (:standard \ uint63_x86 uint63_amd64 write_uint63))
+ (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63))
  (libraries lib byterun))
 
+(executable
+  (name genOpcodeFiles)
+  (modules genOpcodeFiles))
+
 (rule
  (targets copcodes.ml)
- (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh)
- (action (bash "./make_opcodes.sh %{h-file} %{targets}")))
+ (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml))))
 
 (executable
   (name write_uint63)
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
new file mode 100644
index 0000000000..6564954dfd
--- /dev/null
+++ b/kernel/genOpcodeFiles.ml
@@ -0,0 +1,193 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** List of opcodes.
+
+    It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and
+    [copcodes.ml] files.
+
+    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.
+*)
+let opcodes =
+  [|
+    "ACC0";
+    "ACC1";
+    "ACC2";
+    "ACC3";
+    "ACC4";
+    "ACC5";
+    "ACC6";
+    "ACC7";
+    "ACC";
+    "PUSH";
+    "PUSHACC0";
+    "PUSHACC1";
+    "PUSHACC2";
+    "PUSHACC3";
+    "PUSHACC4";
+    "PUSHACC5";
+    "PUSHACC6";
+    "PUSHACC7";
+    "PUSHACC";
+    "POP";
+    "ENVACC1";
+    "ENVACC2";
+    "ENVACC3";
+    "ENVACC4";
+    "ENVACC";
+    "PUSHENVACC1";
+    "PUSHENVACC2";
+    "PUSHENVACC3";
+    "PUSHENVACC4";
+    "PUSHENVACC";
+    "PUSH_RETADDR";
+    "APPLY";
+    "APPLY1";
+    "APPLY2";
+    "APPLY3";
+    "APPLY4";
+    "APPTERM";
+    "APPTERM1";
+    "APPTERM2";
+    "APPTERM3";
+    "RETURN";
+    "RESTART";
+    "GRAB";
+    "GRABREC";
+    "CLOSURE";
+    "CLOSUREREC";
+    "CLOSURECOFIX";
+    "OFFSETCLOSUREM2";
+    "OFFSETCLOSURE0";
+    "OFFSETCLOSURE2";
+    "OFFSETCLOSURE";
+    "PUSHOFFSETCLOSUREM2";
+    "PUSHOFFSETCLOSURE0";
+    "PUSHOFFSETCLOSURE2";
+    "PUSHOFFSETCLOSURE";
+    "GETGLOBAL";
+    "PUSHGETGLOBAL";
+    "MAKEBLOCK";
+    "MAKEBLOCK1";
+    "MAKEBLOCK2";
+    "MAKEBLOCK3";
+    "MAKEBLOCK4";
+    "SWITCH";
+    "PUSHFIELDS";
+    "GETFIELD0";
+    "GETFIELD1";
+    "GETFIELD";
+    "SETFIELD0";
+    "SETFIELD1";
+    "SETFIELD";
+    "PROJ";
+    "ENSURESTACKCAPACITY";
+    "CONST0";
+    "CONST1";
+    "CONST2";
+    "CONST3";
+    "CONSTINT";
+    "PUSHCONST0";
+    "PUSHCONST1";
+    "PUSHCONST2";
+    "PUSHCONST3";
+    "PUSHCONSTINT";
+    "ACCUMULATE";
+    "MAKESWITCHBLOCK";
+    "MAKEACCU";
+    "MAKEPROD";
+    "BRANCH";
+    "CHECKADDINT63";
+    "ADDINT63";
+    "CHECKADDCINT63";
+    "CHECKADDCARRYCINT63";
+    "CHECKSUBINT63";
+    "SUBINT63";
+    "CHECKSUBCINT63";
+    "CHECKSUBCARRYCINT63";
+    "CHECKMULINT63";
+    "CHECKMULCINT63";
+    "CHECKDIVINT63";
+    "CHECKMODINT63";
+    "CHECKDIVEUCLINT63";
+    "CHECKDIV21INT63";
+    "CHECKLXORINT63";
+    "CHECKLORINT63";
+    "CHECKLANDINT63";
+    "CHECKLSLINT63";
+    "CHECKLSRINT63";
+    "CHECKADDMULDIVINT63";
+    "CHECKLSLINT63CONST1";
+    "CHECKLSRINT63CONST1";
+    "CHECKEQINT63";
+    "CHECKLTINT63";
+    "LTINT63";
+    "CHECKLEINT63";
+    "LEINT63";
+    "CHECKCOMPAREINT63";
+    "CHECKHEAD0INT63";
+    "CHECKTAIL0INT63";
+    "ISINT";
+    "AREINT2";
+    "STOP"
+  |]
+
+let pp_c_comment fmt =
+  Format.fprintf fmt "/* %a */"
+
+let pp_ocaml_comment fmt =
+  Format.fprintf fmt "(* %a *)"
+
+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)
+    "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 "};"
+
+let pp_coq_jumptbl_h fmt =
+  pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s")
+
+let pp_copcodes_ml fmt =
+  pp_header true fmt;
+  Array.iteri (fun n s ->
+      Format.fprintf fmt "let op%s = %d@.@." s n
+    ) opcodes
+
+let usage () =
+  Format.eprintf "usage: %s [enum|jump|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
+  | "copml" -> pp_copcodes_ml Format.std_formatter
+  | _ -> usage ()
+  | exception Invalid_argument _ -> usage ()
+
+let () = main ()
diff --git a/kernel/make-opcodes b/kernel/make-opcodes
deleted file mode 100644
index e1371b3d0c..0000000000
--- a/kernel/make-opcodes
+++ /dev/null
@@ -1,3 +0,0 @@
-$1=="enum" {n=0; next; }
-           {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n");
-           for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}}
diff --git a/kernel/make_opcodes.sh b/kernel/make_opcodes.sh
deleted file mode 100755
index bb8aba2f07..0000000000
--- a/kernel/make_opcodes.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/usr/bin/env bash
-
-script_dir="$(dirname "$0")"
-tr -d "\r" < "${1}" | sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' | awk -f "$script_dir"/make-opcodes > "${2}"