Factorize the relocations in the on-disk VM representation.

Instead of using a linear representation, we simply use a table that maps
every kind of relocation to the list of positions it needs to be applied to.

4 files changed, 93 insertions, 74 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 9febc6449..6d91c3ec9 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -45,6 +45,55 @@ type reloc_table = (tag * int) array
 type annot_switch =
    {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
 
+let rec eq_structured_constant c1 c2 = match c1, c2 with
+| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
+| Const_sorts _, _ -> false
+| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_ind _, _ -> false
+| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
+| Const_proj _, _ -> false
+| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
+| Const_b0 _, _ -> false
+| Const_bn (t1, a1), Const_bn (t2, a2) ->
+  Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2
+| Const_bn _, _ -> false
+| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
+| Const_univ_level _ , _ -> false
+| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
+| Const_type _ , _ -> false
+
+let rec hash_structured_constant c =
+  let open Hashset.Combine in
+  match c with
+  | Const_sorts s -> combinesmall 1 (Sorts.hash s)
+  | Const_ind i -> combinesmall 2 (ind_hash i)
+  | Const_proj p -> combinesmall 3 (Constant.hash p)
+  | Const_b0 t -> combinesmall 4 (Int.hash t)
+  | Const_bn (t, a) ->
+    let fold h c = combine h (hash_structured_constant c) in
+    let h = Array.fold_left fold 0 a in
+    combinesmall 5 (combine (Int.hash t) h)
+  | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
+  | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
+
+let eq_annot_switch asw1 asw2 =
+  let eq_ci ci1 ci2 =
+    eq_ind ci1.ci_ind ci2.ci_ind &&
+    Int.equal ci1.ci_npar ci2.ci_npar &&
+    CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
+  in
+  let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
+  eq_ci asw1.ci asw2.ci &&
+  CArray.equal eq_rlc asw1.rtbl asw2.rtbl &&
+  (asw1.tailcall : bool) == asw2.tailcall
+
+let hash_annot_switch asw =
+  let open Hashset.Combine in
+  let h1 = Constr.case_info_hash asw.ci in
+  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
+  let h3 = if asw.tailcall then 1 else 0 in
+  combine3 h1 h2 h3
+
 module Label =
   struct
     type t = int
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 5d37a5840..bf2e462e8 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -41,6 +41,12 @@ type reloc_table = (tag * int) array
 type annot_switch =
    {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
 
+val eq_structured_constant : structured_constant -> structured_constant -> bool
+val hash_structured_constant : structured_constant -> int
+
+val eq_annot_switch : annot_switch -> annot_switch -> bool
+val hash_annot_switch : annot_switch -> int
+
 module Label :
   sig
     type t = int
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index d1a4e4885..856b0b465 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -10,6 +10,7 @@
    machine, Oct 2004 *)
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
+open Names
 open Term
 open Cbytecodes
 open Copcodes
@@ -25,14 +26,34 @@ type reloc_info =
   | Reloc_const of structured_constant
   | Reloc_getglobal of Names.Constant.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
+
+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)
+
+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 = {
-  positions : int array;
-  reloc_infos : reloc_info array;
+  reloc_infos : (reloc_info * int array) array;
 }
 
 let patch_char4 buff pos c1 c2 c3 c4 = 
@@ -46,19 +67,19 @@ let patch1 buff pos n =
     (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8))  (Char.unsafe_chr (n asr 16))
     (Char.unsafe_chr (n asr 24))
 
-(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *)
-let patch_int buff pos reloc =
+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 () = CArray.iter2 (fun pos reloc -> patch1 buff pos reloc) pos reloc 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_left f pl.reloc_infos in
-  let buff = patch_int buff pl.positions reloc in
+  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 (Bytes.length buff)
 
 (* Buffering of bytecode *)
@@ -76,7 +97,7 @@ type env = {
                                 = 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  *)
-  mutable reloc_info : (reloc_info * int) list;
+  reloc_info : int list RelocTable.t;
 }
 
 let out_word env b1 b2 b3 b4 =
@@ -148,7 +169,9 @@ let out_label env l = out_label_with_orig env env.out_position l
 (* Relocation information *)
 
 let enter env info =
-  env.reloc_info <- (info, env.out_position) :: env.reloc_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);
@@ -342,15 +365,8 @@ let subst_reloc s ri =
   | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
 
 let subst_patches subst p =
-  (** This looks suspicious, is order really relevant here? *)
-  let positions = CArray.copy p.positions in
-  let infos = CArray.map_left (fun r -> subst_reloc subst r) p.reloc_infos in
-  let () = CArray.rev positions in
-  let () = CArray.rev infos in
-  {
-    positions = positions;
-    reloc_infos = infos;
-  }
+  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
@@ -394,18 +410,16 @@ let to_memory (init_code, fun_code, fv) =
     out_buffer = Bytes.create 1024;
     out_position = 0;
     label_table = Array.make 16 (Label_undefined []);
-    reloc_info = [];
+    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 reloc = List.rev env.reloc_info in
-  let reloc = {
-    positions = CArray.map_of_list snd reloc;
-    reloc_infos = CArray.map_of_list fst reloc;
-  } 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
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8022eae7d..55430a9d8 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -14,7 +14,6 @@
 
 open Util
 open Names
-open Constr
 open Vmvalues
 open Cemitcodes
 open Cbytecodes
@@ -55,61 +54,12 @@ let set_global v =
 
 (* table pour les structured_constant et les annotations des switchs *)
 
-let rec eq_structured_constant c1 c2 = match c1, c2 with
-| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_sorts _, _ -> false
-| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
-| Const_ind _, _ -> false
-| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
-| Const_proj _, _ -> false
-| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
-| Const_b0 _, _ -> false
-| Const_bn (t1, a1), Const_bn (t2, a2) ->
-  Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
-| Const_bn _, _ -> false
-| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
-| Const_univ_level _ , _ -> false
-| Const_type u1, Const_type u2 -> Univ.Universe.equal u1 u2
-| Const_type _ , _ -> false
-
-let rec hash_structured_constant c =
-  let open Hashset.Combine in
-  match c with
-  | Const_sorts s -> combinesmall 1 (Sorts.hash s)
-  | Const_ind i -> combinesmall 2 (ind_hash i)
-  | Const_proj p -> combinesmall 3 (Constant.hash p)
-  | Const_b0 t -> combinesmall 4 (Int.hash t)
-  | Const_bn (t, a) ->
-    let fold h c = combine h (hash_structured_constant c) in
-    let h = Array.fold_left fold 0 a in
-    combinesmall 5 (combine (Int.hash t) h)
-  | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
-  | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
-
 module SConstTable = Hashtbl.Make (struct
   type t = structured_constant
   let equal = eq_structured_constant
   let hash = hash_structured_constant
 end)
 
-let eq_annot_switch asw1 asw2 =
-  let eq_ci ci1 ci2 =
-    eq_ind ci1.ci_ind ci2.ci_ind &&
-    Int.equal ci1.ci_npar ci2.ci_npar &&
-    Array.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
-  in
-  let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
-  eq_ci asw1.ci asw2.ci &&
-  Array.equal eq_rlc asw1.rtbl asw2.rtbl &&
-  (asw1.tailcall : bool) == asw2.tailcall
-
-let hash_annot_switch asw =
-  let open Hashset.Combine in
-  let h1 = Constr.case_info_hash asw.ci in
-  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
-  let h3 = if asw.tailcall then 1 else 0 in
-  combine3 h1 h2 h3
-
 module AnnotTable = Hashtbl.Make (struct
   type t = annot_switch
   let equal = eq_annot_switch