From 3a050f305293676ccf66d415ab386d9521f0f765 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 04:04:33 +0100 Subject: [safe_string] kernel/term_typing No functional change, we create the new string beforehand and `id_of_string` will become a noop with `-safe-string`. --- kernel/term_typing.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3a0d1a2a5e..b9cf8101da 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -76,8 +76,7 @@ let inline_side_effects env body ctx side_eff = let cbl = List.filter not_exists cbl in let cname c = let name = string_of_con c in - for i = 0 to String.length name - 1 do - if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done; + let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in Name (id_of_string name) in let rec sub c i x = match kind_of_term x with | Const (c', _) when eq_constant c c' -> mkRel i -- cgit v1.2.3 From 6098d329afc1e212ff866212a8f7815969a460ad Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 13:33:39 +0100 Subject: [safe-string] kernel/nativevalues No functional change. --- kernel/nativevalues.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 8093df3044..965ed67b07 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -491,12 +491,12 @@ let str_encode expr = let str_decode s = let mshl_expr_len = String.length s / 2 in let mshl_expr = Buffer.create mshl_expr_len in - let buf = String.create 2 in + let buf = Bytes.create 2 in for i = 0 to mshl_expr_len - 1 do - String.blit s (2*i) buf 0 2; - Buffer.add_char mshl_expr (bin_of_hex buf) + Bytes.blit_string s (2*i) buf 0 2; + Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf)) done; - Marshal.from_string (Buffer.contents mshl_expr) 0 + Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0 (** Retroknowledge, to be removed when we switch to primitive integers *) -- cgit v1.2.3 From 581b8d52fe93d666045d4878a1b48dad916451ec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 04:09:33 +0100 Subject: [safe_string] kernel/cemitcodes The `emitcodes` string type was used in both a functional and an imperative way, so we have to handle it with care in order to preserve the previous optimizations and semantics. --- kernel/cemitcodes.ml | 39 +++++++++++++++++++++++++-------------- 1 file changed, 25 insertions(+), 14 deletions(-) (limited to 'kernel') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ad7a41a347..a0a13174ff 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -24,33 +24,45 @@ type reloc_info = type patch = reloc_info * int let patch_char4 buff pos c1 c2 c3 c4 = - String.unsafe_set buff pos c1; - String.unsafe_set buff (pos + 1) c2; - String.unsafe_set buff (pos + 2) c3; - String.unsafe_set buff (pos + 3) 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 patch 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)) +(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *) let patch_int buff patches = (* 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 = String.copy buff in + let buff = Bytes.of_string buff in let () = List.iter (fun p -> patch buff p) patches in - buff + (* 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 (* Buffering of bytecode *) -let out_buffer = ref(String.create 1024) +let out_buffer = ref(Bytes.create 1024) and out_position = ref 0 let out_word b1 b2 b3 b4 = let p = !out_position in - if p >= String.length !out_buffer then begin - let len = String.length !out_buffer in + if p >= Bytes.length !out_buffer then begin + let len = Bytes.length !out_buffer in let new_len = if len <= Sys.max_string_length / 2 then 2 * len @@ -58,8 +70,8 @@ let out_word b1 b2 b3 b4 = if len = Sys.max_string_length then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in - let new_buffer = String.create new_len in - String.blit !out_buffer 0 new_buffer 0 len; + let new_buffer = Bytes.create new_len in + Bytes.blit !out_buffer 0 new_buffer 0 len; out_buffer := new_buffer end; patch_char4 !out_buffer p (Char.unsafe_chr b1) @@ -305,7 +317,7 @@ let init () = label_table := Array.make 16 (Label_undefined []); reloc_info := [] -type emitcodes = string +type emitcodes = String.t let length = String.length @@ -369,9 +381,8 @@ let to_memory (init_code, fun_code, fv) = init(); emit init_code; emit fun_code; - let code = String.create !out_position in - String.unsafe_blit !out_buffer 0 code 0 !out_position; (** Later uses of this string are all purely functional *) + let code = Bytes.sub_string !out_buffer 0 !out_position in let code = CString.hcons code in let reloc = List.rev !reloc_info in Array.iter (fun lbl -> -- cgit v1.2.3 From 7601ddc3500cae2da39883b339951205be19c41d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 03:48:50 +0100 Subject: [safe_string] library/nameops We add a more convenient API to create identifiers from mutable strings. We cannot solve the `String.copy` deprecation problem until we enable `-safe-string`. --- kernel/names.ml | 5 +++++ kernel/names.mli | 1 + 2 files changed, 6 insertions(+) (limited to 'kernel') diff --git a/kernel/names.ml b/kernel/names.ml index 1f138581cc..831b6ad46e 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -50,6 +50,11 @@ struct | None -> true | Some _ -> false + let of_bytes s = + let s = Bytes.to_string s in + check_soft s; + String.hcons s + let of_string s = let () = check_soft s in let s = String.copy s in diff --git a/kernel/names.mli b/kernel/names.mli index 6b0a80625b..be9b9422b7 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -43,6 +43,7 @@ sig (** Check that a string may be converted to an identifier. @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters. -- cgit v1.2.3 From 5e2574cbef1ba132aacc73b4a079cc0b5584f589 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 14:57:59 +0100 Subject: [safe-string] Enable -safe-string ! We now build Coq with `-safe-string`, which enforces functional use of the `string` datatype. Coq was pretty safe in these regard so only a few tweaks were needed. - coq_makefile: build plugins with -safe-string too. - `names.ml`: we remove `String.copy` uses, as they are not needed. --- kernel/names.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'kernel') diff --git a/kernel/names.ml b/kernel/names.ml index 831b6ad46e..ee8d838da1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -57,15 +57,13 @@ struct let of_string s = let () = check_soft s in - let s = String.copy s in String.hcons s let of_string_soft s = let () = check_soft ~warn:false s in - let s = String.copy s in String.hcons s - let to_string id = String.copy id + let to_string id = id let print id = str id -- cgit v1.2.3 From d25b1431eb73a04bdfc0f1ad2922819b69bba93a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 20 Mar 2017 15:14:01 +0100 Subject: [misc] Remove warnings about String.set The `a.[i] <- x` notation is deprecated and we were getting a couple of warnings. --- kernel/cemitcodes.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index a0a13174ff..f2c3b402b3 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -106,10 +106,10 @@ let extend_label_table needed = let backpatch (pos, orig) = let displ = (!out_position - orig) asr 2 in - !out_buffer.[pos] <- Char.unsafe_chr displ; - !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8); - !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16); - !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24) + Bytes.set !out_buffer pos @@ Char.unsafe_chr displ; + Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); + Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); + Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) let define_label lbl = if lbl >= Array.length !label_table then extend_label_table lbl; -- cgit v1.2.3