Merge PR #13678: Cleaning up the bytecode interpreter

Reviewed-by: ppedrot

4 files changed, 4 insertions, 66 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1ba6a8c8fe..4bc6848ba7 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -31,7 +31,8 @@ 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[PUSHACC0]=arity[PUSHACC1]=
+    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]=
@@ -39,10 +40,10 @@ void init_arity () {
     arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]=
     arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]=
     arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]=
-    arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
+    arity[GETFIELD0]=arity[GETFIELD1]=
     arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
-    arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
+    arity[ACCUMULATE]=arity[STOP]=
     0;
   /* instruction with one operand */
   arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
@@ -60,7 +61,6 @@ void init_arity () {
     arity[CHECKDIV21INT63]=
     arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]=
     arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
-    arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
     arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
     arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
     arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 6255250218..a9ea6d9f46 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -338,10 +338,6 @@ value coq_interprete
         print_instr("PUSH");
         *--sp = accu; Next;
       }
-      Instruct(PUSHACC0) {
-        print_instr("PUSHACC0");
-        *--sp = accu; Next;
-      }
       Instruct(PUSHACC1){
         print_instr("PUSHACC1");
         *--sp = accu; accu = sp[1]; Next;
@@ -1015,20 +1011,6 @@ value coq_interprete
         Next;
       }
 
-      Instruct(SETFIELD0){
-        print_instr("SETFIELD0");
-        caml_modify(&Field(accu, 0),*sp);
-        sp++;
-        Next;
-      }
-
-      Instruct(SETFIELD1){
-        print_instr("SETFIELD1");
-        caml_modify(&Field(accu, 1),*sp);
-        sp++;
-        Next;
-      }
-
       Instruct(SETFIELD){
         print_instr("SETFIELD");
         caml_modify(&Field(accu, *pc),*sp);
@@ -1288,16 +1270,6 @@ value coq_interprete
         Next;
       }
 
-      Instruct(MAKEPROD) {
-        print_instr("MAKEPROD");
-        *--sp=accu;
-        Alloc_small(accu,2,0);
-        Field(accu, 0) = sp[0];
-        Field(accu, 1) = sp[1];
-        sp += 2;
-        Next;
-      }
-
       Instruct(BRANCH) {
         /* unconditional branching */
         print_instr("BRANCH");
@@ -1501,34 +1473,6 @@ value coq_interprete
         Next;
       }
 
-      Instruct(CHECKLSLINT63CONST1) {
-        print_instr("CHECKLSLINT63CONST1");
-        if (Is_uint63(accu)) {
-          pc++;
-          Uint63_lsl1(accu);
-          Next;
-        } else {
-          *--sp = uint63_one();
-          *--sp = accu;
-          accu = Field(coq_global_data, *pc++);
-          goto apply2;
-        }
-      }
-
-      Instruct(CHECKLSRINT63CONST1) {
-        print_instr("CHECKLSRINT63CONST1");
-        if (Is_uint63(accu)) {
-          pc++;
-          Uint63_lsr1(accu);
-          Next;
-        } else {
-          *--sp = uint63_one();
-          *--sp = accu;
-          accu = Field(coq_global_data, *pc++);
-          goto apply2;
-        }
-      }
-
       Instruct (CHECKADDMULDIVINT63) {
         print_instr("CHECKADDMULDIVINT63");
         CheckInt3();
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index 13568957c2..dd9b9e55be 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -119,12 +119,8 @@ DECLARE_BINOP(lor)
 #define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
 DECLARE_BINOP(lsl)
 #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
-DECLARE_UNOP(lsl1)
-#define Uint63_lsl1(x) CALL_UNOP(lsl1, x)
 DECLARE_BINOP(lsr)
 #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
-DECLARE_UNOP(lsr1)
-#define Uint63_lsr1(x) CALL_UNOP(lsr1, x)
 DECLARE_BINOP(lt)
 #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
 DECLARE_BINOP(lxor)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 27696e8856..731ae8f46e 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -55,8 +55,6 @@
   else \
     accu = uint63_zero; \
   }while(0)
-#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1))
-#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1))
 
 /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
 /* (modulo 2^63) for p <= 63 */