From 745696124240963616a38f41b1a20f199646c5dc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 27 Nov 2017 11:25:39 +0100 Subject: 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. --- kernel/cbytecodes.ml | 49 ++++++++++++++++++++++++++++++++++++++++ kernel/cbytecodes.mli | 6 +++++ kernel/cemitcodes.ml | 62 +++++++++++++++++++++++++++++++-------------------- kernel/csymtable.ml | 50 ----------------------------------------- 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 -- cgit v1.2.3