Merge PR #18967: Add a PUSHACCMANY opcode.

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

kernel/byterun/coq_interp.c

@@ -418,6 +418,18 @@ value coq_interprete
         Next;
       }
 
+      Instruct(PUSHACCMANY) {
+        int first = *pc++;
+        int size = *pc++;
+        int i;
+        print_instr("PUSHACCMANY");
+        sp -= size;
+        for (i = 1; i < size; ++i) sp[i - 1] = sp[first + i];
+        sp[size - 1] = accu;
+        accu = sp[first];
+        Next;
+      }
+
       Instruct(POP){
         print_instr("POP");
         sp += *pc++;

kernel/genOpcodeFiles.ml

@@ -37,6 +37,7 @@ let opcodes =
     "PUSHACC6", 0;
     "PUSHACC7", 0;
     "PUSHACC", 1;
+    "PUSHACCMANY", 2;
     "POP", 1;
     "ENVACC0", 0;
     "ENVACC1", 0;

kernel/vmemitcodes.ml

@@ -490,10 +490,20 @@ let rec emit env insns remaining = match insns with
      | (first::rest) -> emit env first rest)
   (* Peephole optimizations *)
   | Kpush :: Kacc n :: c ->
-      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
+      let rec aux n c nb =
+        match c with
+        | Kpush :: Kacc j :: c when j = n -> aux n c (nb + 1)
+        | _ -> (nb, c) in
+      let (nb, c') = aux n c 1 in
+      if nb >= 3 || (nb >= 2 && n > 7)
+      then (
+        out env opPUSHACCMANY; out_int env n; out_int env nb;
+        emit env c' remaining)
+      else (
+        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 ->
       let rec aux n c nb =
         match c with