From 96a4c2a8e2b3de327331e55a9663d230027210e9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Nov 2017 15:05:50 +0100 Subject: Remove the unsafe bytes conversion function in Cemitcodes. This is actually not needed, as the only thing we do with this Bytes.t is to pass it to a C function which will use it in a read-only way. --- kernel/cemitcodes.ml | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 41494441b..f6b9f34ee 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -17,7 +17,7 @@ open Mod_subst type emitcodes = String.t -external tcode_of_code : emitcodes -> int -> Vmvalues.tcode = "coq_tcode_of_code" +external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code" (* Relocation information *) type reloc_info = @@ -46,25 +46,14 @@ let patch_int buff patches = and results in wrong results. Side-effects... *) let buff = Bytes.of_string buff in let () = List.iter (fun p -> patch buff p) patches in - (* Note: we follow the apporach suggested by Gabriel Scherer in - PR#136 here, and use unsafe as we own buff. - - The crux of the question that avoids defining emitcodes just as a - Byte.t is the call to hcons in to_memory below. Even if disabling - this optimization has no visible time impact, test data shows - that the optimization is indeed triggered quite often so we - choose ugliness over altering the semantics. - - Handle with care. - *) - Bytes.unsafe_to_string buff + buff let patch buff pl f = let map (r, pos) = (pos, f r) in (** Order seems important here? *) let patches = CList.map_left map pl in let buff = patch_int buff patches in - tcode_of_code buff (String.length buff) + tcode_of_code buff (Bytes.length buff) (* Buffering of bytecode *) -- cgit v1.2.3