aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-27 11:25:39 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-14 16:21:19 +0100
commit745696124240963616a38f41b1a20f199646c5dc (patch)
tree4ee26cc79bbc88fc0ec789981acb47a0e93722bb
parentda659eeeb413c488f5efae0269c5d37837c62dc2 (diff)
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.
-rw-r--r--kernel/cbytecodes.ml49
-rw-r--r--kernel/cbytecodes.mli6
-rw-r--r--kernel/cemitcodes.ml62
-rw-r--r--kernel/csymtable.ml50
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