From c7bbe4729dc53ddf3a02a7ae3816ec3c146d452e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 17 Feb 2021 12:09:00 +0100 Subject: 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. --- kernel/byterun/coq_fix_code.c | 5 +- kernel/byterun/dune | 4 + kernel/genOpcodeFiles.ml | 313 +++++++++++++++++++++--------------------- 3 files changed, 166 insertions(+), 156 deletions(-) (limited to 'kernel') 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 #include #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 () -- cgit v1.2.3 From ab94a2a5dbe142d972d65a33d977e8e9f8d52f01 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 17 Feb 2021 12:12:29 +0100 Subject: Make the generated file the official source of arity. --- kernel/byterun/coq_fix_code.c | 61 ------------------------------------------- kernel/byterun/coq_fix_code.h | 1 - kernel/byterun/coq_memory.c | 3 --- kernel/genOpcodeFiles.ml | 2 +- 4 files changed, 1 insertion(+), 66 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 40aaa5c021..f986095f59 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -27,67 +27,6 @@ #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]=-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/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/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 25da7c2685..bda65956be 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -178,7 +178,7 @@ let pp_coq_jumptbl_h fmt = let pp_coq_arity_h fmt = pp_header false fmt; - Format.fprintf fmt "static signed char arity2[] = {@."; + Format.fprintf fmt "static signed char arity[] = {@."; Array.iter (fun (_, arity) -> Format.fprintf fmt " %d,@." arity ) opcodes; -- cgit v1.2.3 From d39a01caf4cbbc22cddbaa23234622b21412f058 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 17 Feb 2021 12:13:32 +0100 Subject: Be less permissive with respect to nonsensical bytecode. --- kernel/byterun/coq_fix_code.c | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index f986095f59..20890a28dc 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -108,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; @@ -127,8 +125,9 @@ value coq_tcode_of_code (value code) { q++; for(i=1; i