4 files changed, 8 insertions, 67 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++; };
     }
   }
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/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))))