Merge PR #13678: Cleaning up the bytecode interpreter

Reviewed-by: ppedrot

10 files changed, 22 insertions, 83 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 */
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index dc2cd349ce..0e1cd0c56a 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -28,7 +28,6 @@ let opcodes =
     "ACC7";
     "ACC";
     "PUSH";
-    "PUSHACC0";
     "PUSHACC1";
     "PUSHACC2";
     "PUSHACC3";
@@ -83,8 +82,6 @@ let opcodes =
     "GETFIELD0";
     "GETFIELD1";
     "GETFIELD";
-    "SETFIELD0";
-    "SETFIELD1";
     "SETFIELD";
     "PROJ";
     "ENSURESTACKCAPACITY";
@@ -101,7 +98,6 @@ let opcodes =
     "ACCUMULATE";
     "MAKESWITCHBLOCK";
     "MAKEACCU";
-    "MAKEPROD";
     "BRANCH";
     "CHECKADDINT63";
     "CHECKADDCINT63";
@@ -121,8 +117,6 @@ let opcodes =
     "CHECKLSLINT63";
     "CHECKLSRINT63";
     "CHECKADDMULDIVINT63";
-    "CHECKLSLINT63CONST1";
-    "CHECKLSRINT63CONST1";
     "CHECKEQINT63";
     "CHECKLTINT63";
     "CHECKLEINT63";
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 988611df3e..4f2cbc4262 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -206,9 +206,7 @@ let () =
   Callback.register "uint63 leq" le;
   Callback.register "uint63 lor" l_or;
   Callback.register "uint63 lsl" l_sl;
-  Callback.register "uint63 lsl1" (fun x -> l_sl x Int64.one);
   Callback.register "uint63 lsr" l_sr;
-  Callback.register "uint63 lsr1" (fun x -> l_sr x Int64.one);
   Callback.register "uint63 lt" lt;
   Callback.register "uint63 lxor" l_xor;
   Callback.register "uint63 mod" rem;
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index 4977aec00a..c2b087f061 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -49,7 +49,6 @@ type instruction =
   | Kgetglobal of Constant.t
   | Kconst of structured_constant
   | Kmakeblock of int * tag
-  | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
   | Kswitch of Label.t array * Label.t array
   | Kpushfields of int
@@ -123,7 +122,6 @@ let rec pp_instr i =
       str "const " ++ pp_struct_const sc
   | Kmakeblock(n, m) ->
       str "makeblock " ++ int n ++ str ", " ++ int m
-  | Kmakeprod -> str "makeprod"
   | Kmakeswitchblock(lblt,lbls,_,sz) ->
       str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
         pp_lbl lbls ++ str ", " ++ int sz
diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli
index 003a77ab78..eeca0d2ad1 100644
--- a/kernel/vmbytecodes.mli
+++ b/kernel/vmbytecodes.mli
@@ -47,7 +47,6 @@ type instruction =
   | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
                                          ** is accu, all others are popped from
                                          ** the top of the stack  *)
-  | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
   | Kswitch of Label.t array * Label.t array (** consts,blocks *)
   | Kpushfields of int
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 70c92fd8f0..20de4bc81b 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -569,7 +569,7 @@ let rec compile_lam env cenv lam sz cont =
 
   | Lprod (dom,codom) ->
      let cont1 =
-       Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in
+       Kpush :: compile_lam env cenv dom (sz+1) (Kmakeblock (2,0) :: cont) in
      compile_lam env cenv codom sz cont1
 
   | Llam (ids,body) ->
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index c1d8fcb855..d3af8bf09b 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -135,6 +135,16 @@ let out env opcode =
 
 let is_immed i = Uint63.le (Uint63.of_int i) Uint63.maxuint31
 
+(* Detect whether the current value of the accu register is no longer
+   needed (i.e., the register is written before being read). If so, the
+   register can be used freely; no need to save and restore it. *)
+let is_accu_dead = function
+  | [] -> false
+  | c :: _ ->
+      match c with
+      | Kacc _ | Kenvacc _ | Kconst _ | Koffsetclosure _ | Kgetglobal _ -> true
+      | _ -> false
+
 let out_int env n =
   out_word env n (n asr 8) (n asr 16) (n asr 24)
 
@@ -327,8 +337,6 @@ let emit_instr env = function
       if Int.equal n 0 then invalid_arg "emit_instr : block size = 0"
       else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t)
       else (out env opMAKEBLOCK; out_int env n; out_int env t)
-  | Kmakeprod ->
-      out env opMAKEPROD
   | Kmakeswitchblock(typlbl,swlbl,annot,sz) ->
       out env opMAKESWITCHBLOCK;
       out_label env typlbl; out_label env swlbl;
@@ -349,8 +357,7 @@ let emit_instr env = function
       if n <= 1 then out env (opGETFIELD0+n)
       else (out env opGETFIELD;out_int env n)
   | Ksetfield n ->
-      if n <= 1 then out env (opSETFIELD0+n)
-      else (out env opSETFIELD;out_int env n)
+      out env opSETFIELD; out_int env n
   | Ksequence _ -> invalid_arg "Vmemitcodes.emit_instr"
   | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
   | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
@@ -375,7 +382,9 @@ let rec emit env insns remaining = match insns with
      | (first::rest) -> emit env first rest)
   (* Peephole optimizations *)
   | Kpush :: Kacc n :: c ->
-      if n < 8 then out env(opPUSHACC0 + n) else (out env opPUSHACC; out_int env n);
+      if n = 0 then out env opPUSH
+      else if n < 8 then out env (opPUSHACC1 + n - 1)
+      else (out env opPUSHACC; out_int env n);
       emit env c remaining
   | Kpush :: Kenvacc n :: c ->
       if n >= 0 && n <= 3
@@ -397,6 +406,9 @@ let rec emit env insns remaining = match insns with
   | Kpush :: Kconst const :: c ->
       out env opPUSHGETGLOBAL; slot_for_const env const;
       emit env c remaining
+  | Kpushfields 1 :: c when is_accu_dead c ->
+      out env opGETFIELD0;
+      emit env (Kpush :: c) remaining
   | Kpop n :: Kjump :: c ->
       out env opRETURN; out_int env n; emit env c remaining
   | Ksequence c1 :: c ->