From d009572893913b889320f2fa3435543ee4c63f82 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 27 Dec 2020 10:36:31 +0100
Subject: Remove PUSHACC0, as it is strictly equivalent to PUSH.

---
 kernel/byterun/coq_fix_code.c | 3 ++-
 kernel/byterun/coq_interp.c   | 4 ----
 kernel/genOpcodeFiles.ml      | 1 -
 kernel/vmemitcodes.ml         | 4 +++-
 4 files changed, 5 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1ba6a8c8fe..f562c15aa8 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]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 6255250218..a124a51c7d 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;
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index dc2cd349ce..e2932ec330 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -28,7 +28,6 @@ let opcodes =
     "ACC7";
     "ACC";
     "PUSH";
-    "PUSHACC0";
     "PUSHACC1";
     "PUSHACC2";
     "PUSHACC3";
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index c1d8fcb855..e70285d9ab 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -375,7 +375,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
-- 
cgit v1.2.3


From 944757e10651fda0d63d9291a6bcb1b6fdbaa256 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 27 Dec 2020 10:42:33 +0100
Subject: Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.

---
 kernel/byterun/coq_fix_code.c      |  1 -
 kernel/byterun/coq_interp.c        | 28 ----------------------------
 kernel/byterun/coq_uint63_emul.h   |  4 ----
 kernel/byterun/coq_uint63_native.h |  2 --
 kernel/genOpcodeFiles.ml           |  2 --
 kernel/uint63_31.ml                |  2 --
 6 files changed, 39 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index f562c15aa8..ab6e393178 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -61,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 a124a51c7d..62683b87a6 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1497,34 +1497,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 e2932ec330..ca9985d079 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -120,8 +120,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;
-- 
cgit v1.2.3


From ee5fa81585a67cc556b19e145f518b641c40ffb7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 27 Dec 2020 11:24:07 +0100
Subject: Add a peephole optimization for PUSHFIELDS(1).

The PUSHFIELDS opcode is a costly one, yet lots of constructors have at
most one usable argument (e.g., option, nat, positive, Z, Acc). For those
constructors, PUSHFIELDS(1) is replaced by GETFIELD(0);PUSH, assuming
the accu register is no longer used afterwards.

Replacing one single opcode by two opcodes might seem like a
pessimization, but it is not. Indeed, pattern-matching branches usually
start by filling the accu register with a constructor argument or the
value of a free variable or a constant. All of those offer peephole
optimizations for PUSH, which means that the number of opcodes actually
stay constant.

Note that, for the same reason, the assumption above holds in practice:
the accu register is no longer used after PUSHFIELDS.
---
 kernel/vmemitcodes.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'kernel')

diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index e70285d9ab..5849641c20 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)
 
@@ -399,6 +409,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 ->
-- 
cgit v1.2.3


From d1215d47c3cda09f4df2f07ce9362b3e6fc5b164 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 27 Dec 2020 11:29:51 +0100
Subject: Remove SETFIELD0 and SETFIELD1.

The generated bytecode almost never needs to modify the field of an OCaml
object. The only exception is the laziness mechanism of coinductive types.
But it modifies field 2, and thus uses the generic opcode SETFIELD anyway.
---
 kernel/byterun/coq_fix_code.c |  2 +-
 kernel/byterun/coq_interp.c   | 14 --------------
 kernel/genOpcodeFiles.ml      |  2 --
 kernel/vmemitcodes.ml         |  3 +--
 4 files changed, 2 insertions(+), 19 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index ab6e393178..51ac290ad0 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -40,7 +40,7 @@ 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]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 62683b87a6..a1537cd963 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1011,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);
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index ca9985d079..6e79b431a5 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -82,8 +82,6 @@ let opcodes =
     "GETFIELD0";
     "GETFIELD1";
     "GETFIELD";
-    "SETFIELD0";
-    "SETFIELD1";
     "SETFIELD";
     "PROJ";
     "ENSURESTACKCAPACITY";
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index 5849641c20..85b5ca03e5 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -359,8 +359,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
-- 
cgit v1.2.3


From 5820a964a5b380d82923be7905cdacd6fa6bd6c3 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 27 Dec 2020 14:55:17 +0100
Subject: Remove MAKEPROD.

MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is
never encountered in the fast path, this optimization is not worth the
extra complexity.
---
 kernel/byterun/coq_fix_code.c |  2 +-
 kernel/byterun/coq_interp.c   | 10 ----------
 kernel/genOpcodeFiles.ml      |  1 -
 kernel/vmbytecodes.ml         |  2 --
 kernel/vmbytecodes.mli        |  1 -
 kernel/vmbytegen.ml           |  2 +-
 kernel/vmemitcodes.ml         |  2 --
 7 files changed, 2 insertions(+), 18 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 51ac290ad0..4bc6848ba7 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -43,7 +43,7 @@ void init_arity () {
     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]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a1537cd963..a9ea6d9f46 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1270,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");
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 6e79b431a5..0e1cd0c56a 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -98,7 +98,6 @@ let opcodes =
     "ACCUMULATE";
     "MAKESWITCHBLOCK";
     "MAKEACCU";
-    "MAKEPROD";
     "BRANCH";
     "CHECKADDINT63";
     "CHECKADDCINT63";
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 85b5ca03e5..d3af8bf09b 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -337,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;
-- 
cgit v1.2.3