diff options
| author | Pierre-Marie Pédrot | 2021-02-26 13:32:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-02-26 13:32:20 +0100 |
| commit | e494ea6c94e191dc8e9faf8ece29e5a57cc08515 (patch) | |
| tree | b95aaae276fe05f0acd94a9458137e214a231de6 /kernel/byterun/coq_fix_code.c | |
| parent | 7b2cab92eb2d76f4768a2b0ff6d8ccf12102f101 (diff) | |
| parent | d39a01caf4cbbc22cddbaa23234622b21412f058 (diff) | |
Merge PR #13868: Make genOpcodeFiles.ml handle opcode arity.
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/byterun/coq_fix_code.c')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 67 |
1 files changed, 4 insertions, 63 deletions
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++; }; } } |
