Skip to content

Commit

Permalink
Merge pull request #673 from gasche/safe-string
Browse files Browse the repository at this point in the history
`-safe-string` compilation for Batteries
  • Loading branch information
gasche authored Oct 6, 2017
2 parents d682509 + 2b67824 commit ce92e34
Show file tree
Hide file tree
Showing 30 changed files with 541 additions and 380 deletions.
10 changes: 10 additions & 0 deletions ChangeLog
Original file line number Diff line number Diff line change
@@ -1,6 +1,16 @@
Changelog
---------

## v2.8.0 (minor release)

This minor release supports the -safe-string mode for OCaml
compilation, enforcing a type-level separation between (immutable)
strings and mutable byte sequences.

- support -safe-string compilation
#673
(Gabriel Scherer)

## v2.7.0 (minor release)

This minor release is the first to support OCaml 4.05.0. As with
Expand Down
2 changes: 2 additions & 0 deletions _tags
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,5 @@ true: package(bytes), warn_-3, bin_annot
".git": -traverse
"examples": -traverse
<src/batOpaqueInnerSys.*>: opaque
true: safe_string

2 changes: 1 addition & 1 deletion src/batBase64.ml
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ let encode ?(tbl=chars) ch =
in
let output s p l =
for i = p to p + l - 1 do
write (String.unsafe_get s i)
write (Bytes.unsafe_get s i)
done;
l
in
Expand Down
2 changes: 1 addition & 1 deletion src/batBig_int.mliv
Original file line number Diff line number Diff line change
Expand Up @@ -345,7 +345,7 @@ val nat_of_big_int : big_int -> Nat.nat
val big_int_of_nat : Nat.nat -> big_int
val base_power_big_int: int -> int -> big_int -> big_int
val sys_big_int_of_string: string -> int -> int -> big_int
val round_futur_last_digit : string -> int -> int -> bool
val round_futur_last_digit : Bytes.t -> int -> int -> bool
val approx_big_int: int -> big_int -> string
##V>=4.3##val round_big_int_to_float: big_int -> bool -> float

Expand Down
16 changes: 10 additions & 6 deletions src/batBig_int.mlv
Original file line number Diff line number Diff line change
Expand Up @@ -21,11 +21,15 @@


let big_int_base_default_symbols =
let s = Bytes.create (10 + 26*2) in
let set off c k = Bytes.set s k (char_of_int (k - off + (int_of_char c))) in
for k = 0 to String.length s - 1 do
if k < 10 then set 0 '0' k else if k < 36 then set 10 'a' k else set 36 'A' k
done; s
let symbol offset base k =
char_of_int (k - offset + (int_of_char base)) in
String.init (10 + 26*2) (fun k ->
if k < 10
then symbol 0 '0' k
else if k < 36
then symbol 10 'a' k
else symbol 36 'A' k
)


let to_string_in_custom_base
Expand Down Expand Up @@ -65,7 +69,7 @@ let to_string_in_custom_base
done;
addchar symbols.[int_of_big_int !n];
if isnegative then addchar '-';
String.sub buff (!curr + 1) !count
Bytes.sub_string buff (!curr + 1) !count

let to_string_in_base b n =
if b <= 1 || b > 36 then invalid_arg
Expand Down
7 changes: 4 additions & 3 deletions src/batBitSet.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,14 +37,15 @@ let print_array =
Array.init 256 print_bchar

let print out t =
for i = 0 to (String.length !t) - 1 do
let buf = !t in
for i = 0 to (Bytes.length buf) - 1 do
BatInnerIO.nwrite out
(Array.unsafe_get print_array (Char.code (Bytes.unsafe_get !t i)))
(Array.unsafe_get print_array (Char.code (Bytes.unsafe_get buf i)))
done

let capacity t = (Bytes.length !t) * 8

let empty () = ref ""
let empty () = ref (Bytes.create 0)

let create_ sfun c n = (* n is in bits *)
if n < 0 then invalid_arg ("BitSet."^sfun^": negative size");
Expand Down
11 changes: 6 additions & 5 deletions src/batBuffer.mliv
Original file line number Diff line number Diff line change
Expand Up @@ -63,12 +63,13 @@ val to_bytes : t -> Bytes.t
*)

val sub : t -> int -> int -> string
(** [Buffer.sub b off len] returns (a copy of) the substring of the
current contents of the buffer [b] starting at offset [off] of length
[len] bytes. May raise [Invalid_argument] if out of bounds request. The
buffer itself is unaffected. *)
(** [Buffer.sub b off len] returns a copy of [len] bytes from the
current contents of the buffer [b], starting at offset [off].

val blit : t -> int -> string -> int -> int -> unit
Raise [Invalid_argument] if [srcoff] and [len] do not designate a valid
range of [b]. *)

val blit : t -> int -> Bytes.t -> int -> int -> unit
(** [Buffer.blit src srcoff dst dstoff len] copies [len] characters from
the current contents of the buffer [src], starting at offset [srcoff]
to string [dst], starting at character [dstoff].
Expand Down
2 changes: 1 addition & 1 deletion src/batBuffer.mlv
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ let add_input t inp n =
let output_buffer buf =
BatInnerIO.create_out
~write: (add_char buf)
~output:(fun s p l -> add_substring buf s p l; l)
~output:(fun s p l -> add_subbytes buf s p l; l)
~close: (fun () -> contents buf)
~flush: BatInnerIO.noop

Expand Down
16 changes: 8 additions & 8 deletions src/batBytes.mlv
Original file line number Diff line number Diff line change
Expand Up @@ -47,13 +47,13 @@ include Bytes
##V<4.3##let lowercase_ascii s = map BatChar.lowercase_ascii s

(*$T uppercase_ascii
equal ("five" |> of_string |> uppercase_ascii |> to_string) "FIVE"
equal ("école" |> of_string |> uppercase_ascii |> to_string) "éCOLE"
String.equal ("five" |> of_string |> uppercase_ascii |> to_string) "FIVE"
String.equal ("école" |> of_string |> uppercase_ascii |> to_string) "éCOLE"
*)

(*$T lowercase_ascii
equal ("FIVE" |> of_string |> lowercase_ascii |> to_string) "five"
equal ("ÉCOLE" |> of_string |> lowercase_ascii |> to_string) "École"
String.equal ("FIVE" |> of_string |> lowercase_ascii |> to_string) "five"
String.equal ("ÉCOLE" |> of_string |> lowercase_ascii |> to_string) "École"
*)

##V<4.3##let map_first_char f s =
Expand All @@ -66,13 +66,13 @@ include Bytes
##V<4.3##let uncapitalize_ascii s = map_first_char BatChar.lowercase_ascii s

(*$T capitalize_ascii
equal ("five" |> of_string |> capitalize_ascii |> to_string) "Five"
equal ("école" |> of_string |> capitalize_ascii |> to_string) "école"
String.equal ("five" |> of_string |> capitalize_ascii |> to_string) "Five"
String.equal ("école" |> of_string |> capitalize_ascii |> to_string) "école"
*)

(*$T uncapitalize_ascii
equal ("Five" |> of_string |> uncapitalize_ascii |> to_string) "five"
equal ("École" |> of_string |> uncapitalize_ascii |> to_string) "École"
String.equal ("Five" |> of_string |> uncapitalize_ascii |> to_string) "five"
String.equal ("École" |> of_string |> uncapitalize_ascii |> to_string) "École"
*)


Expand Down
19 changes: 4 additions & 15 deletions src/batDigest.mlv
Original file line number Diff line number Diff line change
Expand Up @@ -21,14 +21,9 @@

include Digest

open BatIO

(*Imported from [Digest.input] -- the functions used take advantage of
[BatIO.input] rather than [in_channel]*)
let input inp =
let digest = Bytes.create 16 in
let _ = really_input inp digest 0 16 in
digest
let input inp = BatIO.really_nread inp 16
(*$T
let digest = Digest.string "azerty" in \
input (BatIO.input_string digest) = digest
Expand All @@ -38,10 +33,8 @@ let output = BatIO.nwrite
let print oc t = BatIO.nwrite oc (to_hex t)

let channel inp len = (*TODO: Make efficient*)
if len >= 0 then
let buf = Bytes.create len in
let _ = BatIO.really_input inp buf 0 len in
Digest.string buf
if len >= 0
then Digest.string (BatIO.really_nread inp len)
else Digest.channel (BatIO.to_input_channel inp) len
(*$T
let digest = Digest.string "azerty" in \
Expand Down Expand Up @@ -78,11 +71,7 @@ let from_hex s =
| _ -> raise (Invalid_argument "Digest.from_hex")
in
let byte i = digit s.[i] lsl 4 + digit s.[i+1] in
let result = Bytes.create 16 in
for i = 0 to 15 do
Bytes.set result i (Char.chr (byte (2 * i)));
done;
result
String.init 16 (fun i -> Char.chr (byte (2 * i)))

(*$Q
Q.string (fun s -> \
Expand Down
4 changes: 2 additions & 2 deletions src/batFormat.mlv
Original file line number Diff line number Diff line change
Expand Up @@ -25,13 +25,13 @@ include Format

(* internal functions *)

let output_of out = fun s i o -> ignore (really_output out s i o)
let output_of out = fun s i o -> ignore (really_output_substring out s i o)
let flush_of out = BatInnerIO.get_flush out
let newline_of out = fun () -> BatInnerIO.write out '\n'
let spaces_of out =
(* Default function to output spaces.
Copied from base format.ml*)
let blank_line = String.make 80 ' ' in
let blank_line = Bytes.make 80 ' ' in
let rec display_blanks n =
if n > 0 then
if n <= 80 then ignore (really_output out blank_line 0 n) else
Expand Down
6 changes: 3 additions & 3 deletions src/batGenlex.ml
Original file line number Diff line number Diff line change
Expand Up @@ -51,16 +51,16 @@ let to_enum_filter kwd_table =
let reset_buffer () = buffer := initial_buffer; bufpos := 0 in

let store c =
if !bufpos >= String.length !buffer then
if !bufpos >= Bytes.length !buffer then
begin
let newbuffer = Bytes.create (2 * !bufpos) in
String.blit !buffer 0 newbuffer 0 !bufpos; buffer := newbuffer
Bytes.blit !buffer 0 newbuffer 0 !bufpos; buffer := newbuffer
end;
Bytes.set !buffer !bufpos c;
incr bufpos in

let get_string () =
let s = String.sub !buffer 0 !bufpos in buffer := initial_buffer; s
let s = Bytes.sub_string !buffer 0 !bufpos in buffer := initial_buffer; s
in
let ident_or_keyword id =
try Hashtbl.find kwd_table id with
Expand Down
46 changes: 26 additions & 20 deletions src/batIO.ml
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ let output_enum() =
Buffer.add_char b x
)
~output:(fun s p l ->
Buffer.add_substring b s p l;
Buffer.add_subbytes b s p l;
l
)
~close:(fun () ->
Expand Down Expand Up @@ -401,7 +401,7 @@ let from_in_channel ch =
let read() =
try
if ch#input cbuf 0 1 = 0 then raise Sys_blocked_io;
String.unsafe_get cbuf 0
Bytes.unsafe_get cbuf 0
with
End_of_file -> raise No_more_input
in
Expand Down Expand Up @@ -449,7 +449,7 @@ let from_in_chars ch =
let from_out_chars ch =
let output s p l =
for i = p to p + l - 1 do
ch#put (String.unsafe_get s i)
ch#put (Bytes.unsafe_get s i)
done;
l
in
Expand Down Expand Up @@ -498,20 +498,25 @@ let lines_of2 ic =
let find_eol () =
let rec find_loop pos =
if pos >= !end_pos then !read_pos - pos
else if buf.[pos] = '\n' then 1 + pos - !read_pos (* TODO: HANDLE CRLF *)
else if Bytes.get buf pos = '\n'
then 1 + pos - !read_pos (* TODO: HANDLE CRLF *)
else find_loop (pos+1)
in
find_loop !read_pos
in
let rec join_strings buf pos = function
| [] -> buf
let join_strings total_len accu =
let rec loop buf pos = function
| [] -> ()
| h::t ->
let len = String.length h in
String.blit h 0 buf (pos-len) len;
join_strings buf (pos-len) t
let len = Bytes.length h in
Bytes.blit h 0 buf (pos-len) len;
loop buf (pos-len) t in
let buf = Bytes.create total_len in
loop buf total_len accu;
Bytes.unsafe_to_string buf
in
let input_buf s o l =
String.blit buf !read_pos s o l;
Bytes.blit buf !read_pos s o l;
read_pos := !read_pos + l;
if !end_pos = !read_pos then
try
Expand All @@ -529,15 +534,15 @@ let lines_of2 ic =
let n = find_eol () in
if n = 0 then match accu with (* EOF *)
| [] -> close_in ic; raise BatEnum.No_more_elements
| _ -> join_strings (Bytes.create len) len accu
| _ -> join_strings len accu
else if n > 0 then (* newline found *)
let res = Bytes.create (n-1) in
input_buf res 0 (n-1);
input_buf " " 0 1; (* throw away EOL *)
input_buf (Bytes.of_string " ") 0 1; (* throw away EOL *)
match accu with
| [] -> res
| [] -> Bytes.unsafe_to_string res
| _ -> let len = len + n-1 in
join_strings (Bytes.create len) len (res :: accu)
join_strings len (res :: accu)
else (* n < 0 ; no newline found *)
let piece = Bytes.create (-n) in
input_buf piece 0 (-n);
Expand All @@ -564,17 +569,18 @@ let tab_out ?(tab=' ') n out =
write out c;
if is_newline c then nwrite out spaces;
)
~output:(fun s p l -> (*Replace each newline within the segment with newline^spaces*) (*FIXME?: performance - instead output each line and a newline between each char? *)
let length = String.length s in
let buffer = Buffer.create (String.length s) in
~output:(fun s p l ->
(*Replace each newline within the segment with newline^spaces*)
let length = Bytes.length s in
let buffer = Buffer.create length in
for i = p to min (length - 1) l do
let c = String.unsafe_get s i in
let c = Bytes.unsafe_get s i in
Buffer.add_char buffer c;
if is_newline c then
Buffer.add_string buffer spaces
done;
let s' = Buffer.contents buffer in
output out s' 0 (String.length s'))
let s' = Buffer.to_bytes buffer in
really_output out s' 0 (Bytes.length s'))
~flush:noop
~close:noop
~underlying:[out]
Expand Down
Loading

0 comments on commit ce92e34

Please sign in to comment.