diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.build | 18 | ||||
| -rw-r--r-- | default.nix | 1 | ||||
| -rw-r--r-- | kernel/byterun/coq_instruct.h | 67 | ||||
| -rw-r--r-- | kernel/byterun/dune | 7 | ||||
| -rwxr-xr-x | kernel/byterun/make_jumptbl.sh | 3 | ||||
| -rw-r--r-- | kernel/dune | 9 | ||||
| -rw-r--r-- | kernel/genOpcodeFiles.ml | 193 | ||||
| -rw-r--r-- | kernel/make-opcodes | 3 | ||||
| -rwxr-xr-x | kernel/make_opcodes.sh | 4 |
11 files changed, 221 insertions, 88 deletions
diff --git a/.gitignore b/.gitignore index c30fd850a1..4e02e7617c 100644 --- a/.gitignore +++ b/.gitignore @@ -145,7 +145,9 @@ plugins/ssr/ssrvernac.ml # other auto-generated files +kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +kernel/genOpcodeFiles.exe kernel/copcodes.ml kernel/uint63.ml ide/index_urls.txt @@ -101,7 +101,7 @@ export GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Gramma export GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) $(addsuffix .mli, $(GRAMFILES)) export GENGRAMFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml -export GENHFILES:=kernel/byterun/coq_jumptbl.h +export GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) ## More complex file lists diff --git a/Makefile.build b/Makefile.build index ea356d5f8e..e348b2b9b8 100644 --- a/Makefile.build +++ b/Makefile.build @@ -316,11 +316,21 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(notdir $(BYTERUN)) -kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h kernel/byterun/make_jumptbl.sh - kernel/byterun/make_jumptbl.sh $< $@ +kernel/genOpcodeFiles.exe: kernel/genOpcodeFiles.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) -o $@ $< + +kernel/byterun/coq_instruct.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< enum > $@ -kernel/copcodes.ml: kernel/byterun/coq_instruct.h kernel/make_opcodes.sh kernel/make-opcodes - kernel/make_opcodes.sh $< $@ +kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< jump > $@ + +kernel/copcodes.ml: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< copml > $@ %.o: %.c $(SHOW)'OCAMLC $<' diff --git a/default.nix b/default.nix index b65d736d79..3290f5dee8 100644 --- a/default.nix +++ b/default.nix @@ -78,7 +78,6 @@ stdenv.mkDerivation rec { !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; preConfigure = '' - patchShebangs kernel/ patchShebangs dev/tools/ ''; 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}" |