Rename VM-related kernel/cfoo files to kernel/vmfoo

1 files changed, 0 insertions, 497 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
deleted file mode 100644
index ed475dca7e..0000000000
--- a/kernel/cemitcodes.ml
+++ /dev/null
@@ -1,497 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction
-   machine, Oct 2004 *)
-(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
-
-open Names
-open Vmvalues
-open Cbytecodes
-open Copcodes
-open Mod_subst
-open CPrimitives
-
-type emitcodes = String.t
-
-external tcode_of_code : Bytes.t -> Vmvalues.tcode = "coq_tcode_of_code"
-
-(* Relocation information *)
-type reloc_info =
-  | Reloc_annot of annot_switch
-  | Reloc_const of structured_constant
-  | Reloc_getglobal of Names.Constant.t
-  | Reloc_proj_name of Projection.Repr.t
-  | Reloc_caml_prim of CPrimitives.t
-
-let eq_reloc_info r1 r2 = match r1, r2 with
-| Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2
-| Reloc_annot _, _ -> false
-| Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2
-| Reloc_const _, _ -> false
-| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
-| Reloc_getglobal _, _ -> false
-| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2
-| Reloc_proj_name _, _ -> false
-| Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2
-| Reloc_caml_prim _, _ -> false
-
-let hash_reloc_info r =
-  let open Hashset.Combine in
-  match r with
-  | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
-  | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
-  | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
-  | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p)
-  | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p)
-
-module RelocTable = Hashtbl.Make(struct
-  type t = reloc_info
-  let equal = eq_reloc_info
-  let hash = hash_reloc_info
-end)
-
-(** We use arrays for on-disk representation. On 32-bit machines, this means we
-    can only have a maximum amount of about 4.10^6 relocations, which seems
-    quite a lot, but potentially reachable if e.g. compiling big proofs. This
-    would prevent VM computing with these terms on 32-bit architectures. Maybe
-    we should use a more robust data structure? *)
-type patches = {
-  reloc_infos : (reloc_info * int array) array;
-}
-
-let patch_char4 buff pos c1 c2 c3 c4 =
-  Bytes.unsafe_set buff pos       c1;
-  Bytes.unsafe_set buff (pos + 1) c2;
-  Bytes.unsafe_set buff (pos + 2) c3;
-  Bytes.unsafe_set buff (pos + 3) c4
-
-let patch1 buff pos n =
-  patch_char4 buff pos
-    (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8))  (Char.unsafe_chr (n asr 16))
-    (Char.unsafe_chr (n asr 24))
-
-let patch_int buff reloc =
-  (* copy code *before* patching because of nested evaluations:
-     the code we are patching might be called (and thus "concurrently" patched)
-     and results in wrong results. Side-effects... *)
-  let buff = Bytes.of_string buff in
-  let iter (reloc, npos) = Array.iter (fun pos -> patch1 buff pos reloc) npos in
-  let () = CArray.iter iter reloc in
-  buff
-
-let patch buff pl f =
-  (** Order seems important here? *)
-  let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in
-  let buff = patch_int buff reloc in
-  tcode_of_code buff
-
-(* Buffering of bytecode *)
-
-type label_definition =
-    Label_defined of int
-  | Label_undefined of (int * int) list
-
-type env = {
-  mutable out_buffer : Bytes.t;
-  mutable out_position : int;
-  mutable label_table : label_definition array;
-  (* le ieme element de la table = Label_defined n signifie que l'on a
-    deja rencontrer le label i et qu'il est a l'offset n.
-                                = Label_undefined l signifie que l'on a
-    pas encore rencontrer ce label, le premier entier indique ou est l'entier
-    a patcher dans la string, le deuxieme son origine  *)
-  reloc_info : int list RelocTable.t;
-}
-
-let out_word env b1 b2 b3 b4 =
-  let p = env.out_position in
-  if p >= Bytes.length env.out_buffer then begin
-    let len = Bytes.length env.out_buffer in
-    let new_len =
-      if len <= Sys.max_string_length / 2
-      then 2 * len
-      else
-        if len = Sys.max_string_length
-        then invalid_arg "String.create"  (* Pas la bonne exception .... *)
-        else Sys.max_string_length in
-    let new_buffer = Bytes.create new_len in
-    Bytes.blit env.out_buffer 0 new_buffer 0 len;
-    env.out_buffer <- new_buffer
-  end;
-  patch_char4 env.out_buffer p (Char.unsafe_chr b1)
-   (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4);
-  env.out_position <- p + 4
-
-let out env opcode =
-  out_word env opcode 0 0 0
-
-let is_immed i = Uint63.le (Uint63.of_int i) Uint63.maxuint31
-
-let out_int env n =
-  out_word env n (n asr 8) (n asr 16) (n asr 24)
-
-(* Handling of local labels and backpatching *)
-
-let extend_label_table env needed =
-  let new_size = ref(Array.length env.label_table) in
-  while needed >= !new_size do new_size := 2 * !new_size done;
-  let new_table = Array.make !new_size (Label_undefined []) in
-  Array.blit env.label_table 0 new_table 0 (Array.length env.label_table);
-  env.label_table <- new_table
-
-let backpatch env (pos, orig) =
-  let displ = (env.out_position - orig) asr 2 in
-  Bytes.set env.out_buffer  pos    @@ Char.unsafe_chr displ;
-  Bytes.set env.out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
-  Bytes.set env.out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
-  Bytes.set env.out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
-
-let define_label env lbl =
-  if lbl >= Array.length env.label_table then extend_label_table env lbl;
-  match (env.label_table).(lbl) with
-    Label_defined _ ->
-      raise(Failure "CEmitcode.define_label")
-  | Label_undefined patchlist ->
-      List.iter (fun p -> backpatch env p) patchlist;
-      (env.label_table).(lbl) <- Label_defined env.out_position
-
-let out_label_with_orig env orig lbl =
-  if lbl >= Array.length env.label_table then extend_label_table env lbl;
-  match (env.label_table).(lbl) with
-    Label_defined def ->
-      out_int env ((def - orig) asr 2)
-  | Label_undefined patchlist ->
-      (* spiwack: patchlist is supposed to be non-empty all the time
-         thus I commented that out. If there is no problem I suggest
-         removing it for next release (cur: 8.1) *)
-      (*if patchlist = [] then *)
-        (env.label_table).(lbl) <-
-          Label_undefined((env.out_position, orig) :: patchlist);
-      out_int env 0
-
-let out_label env l = out_label_with_orig env env.out_position l
-
-(* Relocation information *)
-
-let enter env info =
-  let pos = env.out_position in
-  let old = try RelocTable.find env.reloc_info info with Not_found -> [] in
-  RelocTable.replace env.reloc_info info (pos :: old)
-
-let slot_for_const env c =
-  enter env (Reloc_const c);
-  out_int env 0
-
-let slot_for_annot env a =
-  enter env (Reloc_annot a);
-  out_int env 0
-
-let slot_for_getglobal env p =
-  enter env (Reloc_getglobal p);
-  out_int env 0
-
-let slot_for_proj_name env p =
-  enter env (Reloc_proj_name p);
-  out_int env 0
-
-let slot_for_caml_prim env op =
-  enter env (Reloc_caml_prim op);
-  out_int env 0
-
-(* Emission of one instruction *)
-
-let nocheck_prim_op = function
-  | Int63add -> opADDINT63
-  | Int63sub -> opSUBINT63
-  | Int63lt  -> opLTINT63
-  | Int63le  -> opLEINT63
-  | _ -> assert false
-
-
-let check_prim_op = function
-  | Int63head0     -> opCHECKHEAD0INT63
-  | Int63tail0     -> opCHECKTAIL0INT63
-  | Int63add       -> opCHECKADDINT63
-  | Int63sub       -> opCHECKSUBINT63
-  | Int63mul       -> opCHECKMULINT63
-  | Int63div       -> opCHECKDIVINT63
-  | Int63mod       -> opCHECKMODINT63
-  | Int63lsr       -> opCHECKLSRINT63
-  | Int63lsl       -> opCHECKLSLINT63
-  | Int63land      -> opCHECKLANDINT63
-  | Int63lor       -> opCHECKLORINT63
-  | Int63lxor      -> opCHECKLXORINT63
-  | Int63addc      -> opCHECKADDCINT63
-  | Int63subc      -> opCHECKSUBCINT63
-  | Int63addCarryC -> opCHECKADDCARRYCINT63
-  | Int63subCarryC -> opCHECKSUBCARRYCINT63
-  | Int63mulc      -> opCHECKMULCINT63
-  | Int63diveucl   -> opCHECKDIVEUCLINT63
-  | Int63div21     -> opCHECKDIV21INT63
-  | Int63addMulDiv -> opCHECKADDMULDIVINT63
-  | Int63eq        -> opCHECKEQINT63
-  | Int63lt        -> opCHECKLTINT63
-  | Int63le        -> opCHECKLEINT63
-  | Int63compare   -> opCHECKCOMPAREINT63
-  | Float64opp     -> opCHECKOPPFLOAT
-  | Float64abs     -> opCHECKABSFLOAT
-  | Float64eq      -> opCHECKEQFLOAT
-  | Float64lt      -> opCHECKLTFLOAT
-  | Float64le      -> opCHECKLEFLOAT
-  | Float64compare -> opCHECKCOMPAREFLOAT
-  | Float64classify -> opCHECKCLASSIFYFLOAT
-  | Float64add     -> opCHECKADDFLOAT
-  | Float64sub     -> opCHECKSUBFLOAT
-  | Float64mul     -> opCHECKMULFLOAT
-  | Float64div     -> opCHECKDIVFLOAT
-  | Float64sqrt    -> opCHECKSQRTFLOAT
-  | Float64ofInt63 -> opCHECKFLOATOFINT63
-  | Float64normfr_mantissa -> opCHECKFLOATNORMFRMANTISSA
-  | Float64frshiftexp -> opCHECKFRSHIFTEXP
-  | Float64ldshiftexp -> opCHECKLDSHIFTEXP
-  | Float64next_up    -> opCHECKNEXTUPFLOAT
-  | Float64next_down  -> opCHECKNEXTDOWNFLOAT
-  | Arraymake -> opISINT_CAML_CALL2
-  | Arrayget -> opISARRAY_INT_CAML_CALL2
-  | Arrayset -> opISARRAY_INT_CAML_CALL3
-  | Arraydefault | Arraycopy | Arrayreroot | Arraylength ->
-      opISARRAY_CAML_CALL1
-
-let emit_instr env = function
-  | Klabel lbl -> define_label env lbl
-  | Kacc n ->
-      if n < 8 then out env(opACC0 + n) else (out env opACC; out_int env n)
-  | Kenvacc n ->
-      if n >= 1 && n <= 4
-      then out env(opENVACC1 + n - 1)
-      else (out env opENVACC; out_int env n)
-  | Koffsetclosure ofs ->
-      if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
-      then out env (opOFFSETCLOSURE0 + ofs / 2)
-      else (out env opOFFSETCLOSURE; out_int env ofs)
-  | Kpush ->
-      out env opPUSH
-  | Kpop n ->
-      out env opPOP; out_int env n
-  | Kpush_retaddr lbl ->
-      out env opPUSH_RETADDR; out_label env lbl
-  | Kapply n ->
-      if n <= 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n)
-  | Kappterm(n, sz) ->
-      if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz)
-               else (out env opAPPTERM; out_int env n; out_int env sz)
-  | Kreturn n ->
-      out env opRETURN; out_int env n
-  | Kjump ->
-      out env opRETURN; out_int env 0
-  | Krestart ->
-      out env opRESTART
-  | Kgrab n ->
-      out env opGRAB; out_int env n
-  | Kgrabrec(rec_arg) ->
-      out env opGRABREC; out_int env rec_arg
-  | Kclosure(lbl, n) ->
-      out env opCLOSURE; out_int env n; out_label env lbl
-  | Kclosurerec(nfv,init,lbl_types,lbl_bodies) ->
-      out env opCLOSUREREC;out_int env (Array.length lbl_bodies);
-      out_int env nfv; out_int env init;
-      let org = env.out_position in
-      Array.iter (out_label_with_orig env org) lbl_types;
-      let org = env.out_position in
-      Array.iter (out_label_with_orig env org) lbl_bodies
-  | Kclosurecofix(nfv,init,lbl_types,lbl_bodies) ->
-      out env opCLOSURECOFIX;out_int env (Array.length lbl_bodies);
-      out_int env nfv; out_int env init;
-      let org = env.out_position in
-      Array.iter (out_label_with_orig env org) lbl_types;
-      let org = env.out_position in
-      Array.iter (out_label_with_orig env org) lbl_bodies
-  | Kgetglobal q ->
-      out env opGETGLOBAL; slot_for_getglobal env q
-  | Kconst (Const_b0 i) when is_immed i ->
-      if i >= 0 && i <= 3
-          then out env (opCONST0 + i)
-          else (out env opCONSTINT; out_int env i)
-  | Kconst c ->
-      out env opGETGLOBAL; slot_for_const env c
-  | Kmakeblock(n, t) ->
-      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;
-      slot_for_annot env annot;out_int env sz
-  | Kswitch (tbl_const, tbl_block) ->
-      let lenb = Array.length tbl_block in
-      let lenc = Array.length tbl_const in
-      assert (lenb < 0x100 && lenc < 0x1000000);
-      out env opSWITCH;
-      out_word env lenc (lenc asr 8) (lenc asr 16) (lenb);
-(*      out_int env (Array.length tbl_const + (Array.length tbl_block lsl 23)); *)
-      let org = env.out_position in
-      Array.iter (out_label_with_orig env org) tbl_const;
-      Array.iter (out_label_with_orig env org) tbl_block
-  | Kpushfields n ->
-      out env opPUSHFIELDS;out_int env n
-  | Kfield n ->
-      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)
-  | Ksequence _ -> invalid_arg "Cemitcodes.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
-  | Kbranch lbl -> out env opBRANCH; out_label env lbl
-  | Kprim (op,None) ->
-      out env (nocheck_prim_op op)
-
-  | Kprim(op,Some (q,_u)) ->
-      out env (check_prim_op op);
-      slot_for_getglobal env q
-
-  | Kcamlprim (op,lbl) ->
-    out env (check_prim_op op);
-    out_label env lbl;
-    slot_for_caml_prim env op
-
-  | Kareint 1 -> out env opISINT
-  | Kareint 2 -> out env opAREINT2;
-
-  | Kstop -> out env opSTOP
-
-  | Kareint _ -> assert false
-
-(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
-
-let rec emit env insns remaining = match insns with
-  | [] ->
-     (match remaining 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);
-      emit env c remaining
-  | Kpush :: Kenvacc n :: c ->
-      if n >= 1 && n <= 4
-      then out env(opPUSHENVACC1 + n - 1)
-      else (out env opPUSHENVACC; out_int env n);
-      emit env c remaining
-  | Kpush :: Koffsetclosure ofs :: c ->
-      if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
-      then out env(opPUSHOFFSETCLOSURE0 + ofs / 2)
-      else (out env opPUSHOFFSETCLOSURE; out_int env ofs);
-      emit env c remaining
-  | Kpush :: Kgetglobal id :: c ->
-      out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining
-  | Kpush :: Kconst (Const_b0 i) :: c when is_immed i ->
-      if i >= 0 && i <= 3
-      then out env (opPUSHCONST0 + i)
-      else (out env opPUSHCONSTINT; out_int env i);
-      emit env c remaining
-  | Kpush :: Kconst const :: c ->
-      out env opPUSHGETGLOBAL; slot_for_const env const;
-      emit env c remaining
-  | Kpop n :: Kjump :: c ->
-      out env opRETURN; out_int env n; emit env c remaining
-  | Ksequence(c1,c2)::c ->
-      emit env c1 (c2::c::remaining)
-  (* Default case *)
-  | instr :: c ->
-      emit_instr env instr; emit env c remaining
-
-(* Initialization *)
-
-type to_patch = emitcodes * patches * fv
-
-(* Substitution *)
-let subst_strcst s sc =
-  match sc with
-  | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ | Const_uint _
-  | Const_float _ -> sc
-  | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
-
-let subst_annot _ (a : annot_switch) = a
-
-let subst_reloc s ri =
-  match ri with
-  | Reloc_annot a -> Reloc_annot (subst_annot s a)
-  | Reloc_const sc -> Reloc_const (subst_strcst s sc)
-  | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
-  | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p)
-  | Reloc_caml_prim _ -> ri
-
-let subst_patches subst p =
-  let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in
-  { reloc_infos = infos; }
-
-let subst_to_patch s (code,pl,fv) =
-  code, subst_patches s pl, fv
-
-type body_code =
-  | BCdefined of to_patch
-  | BCalias of Names.Constant.t
-  | BCconstant
-
-type to_patch_substituted =
-| PBCdefined of to_patch substituted
-| PBCalias of Names.Constant.t substituted
-| PBCconstant
-
-let from_val = function
-| BCdefined tp -> PBCdefined (from_val tp)
-| BCalias cu -> PBCalias (from_val cu)
-| BCconstant -> PBCconstant
-
-let force = function
-| PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCalias cu -> BCalias (force subst_constant cu)
-| PBCconstant -> BCconstant
-
-let subst_to_patch_subst s = function
-| PBCdefined tp -> PBCdefined (subst_substituted s tp)
-| PBCalias cu -> PBCalias (subst_substituted s cu)
-| PBCconstant -> PBCconstant
-
-let repr_body_code = function
-| PBCdefined tp ->
-  let (s, tp) = repr_substituted tp in
-  (s, BCdefined tp)
-| PBCalias cu ->
-  let (s, cu) = repr_substituted cu in
-  (s, BCalias cu)
-| PBCconstant -> (None, BCconstant)
-
-let to_memory (init_code, fun_code, fv) =
-  let env = {
-    out_buffer = Bytes.create 1024;
-    out_position = 0;
-    label_table = Array.make 16 (Label_undefined []);
-    reloc_info = RelocTable.create 91;
-  } in
-  emit env init_code [];
-  emit env fun_code [];
-  (** Later uses of this string are all purely functional *)
-  let code = Bytes.sub_string env.out_buffer 0 env.out_position in
-  let code = CString.hcons code in
-  let fold reloc npos accu = (reloc, Array.of_list npos) :: accu in
-  let reloc = RelocTable.fold fold env.reloc_info [] in
-  let reloc = { reloc_infos = CArray.of_list reloc } in
-  Array.iter (fun lbl ->
-    (match lbl with
-      Label_defined _ -> assert true
-    | Label_undefined patchlist ->
-        assert (patchlist = []))) env.label_table;
-  (code, reloc, fv)