diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/lib.mllib | 1 | ||||
| -rw-r--r-- | lib/objFile.ml | 229 | ||||
| -rw-r--r-- | lib/objFile.mli | 34 | ||||
| -rw-r--r-- | lib/system.ml | 214 | ||||
| -rw-r--r-- | lib/system.mli | 30 |
5 files changed, 264 insertions, 244 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib index 2db59712b9..4e08e87084 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -14,6 +14,7 @@ CWarnings AcyclicGraph Rtree System +ObjFile Explore CProfile Future diff --git a/lib/objFile.ml b/lib/objFile.ml new file mode 100644 index 0000000000..190b1833bd --- /dev/null +++ b/lib/objFile.ml @@ -0,0 +1,229 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open System + +let magic_number = 0x436F7121l (* "Coq!" *) + +let error_corrupted file s = + CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") + +let open_trapping_failure name = + try open_out_bin name + with e when CErrors.noncritical e -> + CErrors.user_err ~hdr:"System.open" (str "Can't open " ++ str name) + +(* + +int32: big-endian, 4 bytes +int64: big-endian, 8 bytes + +-- string -- +int32 | length of the next field +data | + +-- segment summary -- +string | name +int64 | absolute position +int64 | length (without hash) +hash | MD5 (16 bytes) + +-- segment -- +... | binary data +hash | MD5 (16 bytes) + +-- summary -- +int32 | number of segment summaries +s1 | +... | segment summaries +sn | + +-- vo -- +int32 | magic number +int32 | Coq version +int64 | absolute position of the summary +... | segments +summary | + +*) + +type segment = { + name : string; + pos : int64; + len : int64; + hash : Digest.t; +} + +type in_handle = { + in_filename : string; + in_channel : in_channel; + in_segments : segment CString.Map.t; +} + +type out_handle = { + out_filename : string; + out_channel : out_channel; + mutable out_segments : segment CString.Map.t; +} + +let input_int32 ch = + let accu = ref 0l in + for _i = 0 to 3 do + let c = input_byte ch in + accu := Int32.add (Int32.shift_left !accu 8) (Int32.of_int c) + done; + !accu + +let input_int64 ch = + let accu = ref 0L in + for _i = 0 to 7 do + let c = input_byte ch in + accu := Int64.add (Int64.shift_left !accu 8) (Int64.of_int c) + done; + !accu + +let output_int32 ch n = + for i = 0 to 3 do + output_byte ch (Int32.to_int (Int32.shift_right_logical n (24 - 8 * i))) + done + +let output_int64 ch n = + for i = 0 to 7 do + output_byte ch (Int64.to_int (Int64.shift_right_logical n (56 - 8 * i))) + done + +let input_segment_summary ch = + let nlen = input_int32 ch in + let name = really_input_string ch (Int32.to_int nlen) in + let pos = input_int64 ch in + let len = input_int64 ch in + let hash = Digest.input ch in + { name; pos; len; hash } + +let output_segment_summary ch seg = + let nlen = Int32.of_int (String.length seg.name) in + let () = output_int32 ch nlen in + let () = output_string ch seg.name in + let () = output_int64 ch seg.pos in + let () = output_int64 ch seg.len in + let () = Digest.output ch seg.hash in + () + +let rec input_segment_summaries ch n accu = + if Int32.equal n 0l then accu + else + let s = input_segment_summary ch in + let accu = CString.Map.add s.name s accu in + input_segment_summaries ch (Int32.pred n) accu + +let marshal_in_segment (type a) h ~segment : a * Digest.t = + let { in_channel = ch } = h in + let s = CString.Map.find segment h.in_segments in + let () = LargeFile.seek_in ch s.pos in + let (v : a) = marshal_in h.in_filename ch in + let () = assert (Int64.equal (LargeFile.pos_in ch) (Int64.add s.pos s.len)) in + let h = Digest.input ch in + let () = assert (String.equal h s.hash) in + (v, s.hash) + +let marshal_out_segment h ~segment v = + let { out_channel = ch } = h in + let () = assert (not (CString.Map.mem segment h.out_segments)) in + let pos = LargeFile.pos_out ch in + let () = Marshal.to_channel ch v [] in + let () = flush ch in + let pos' = LargeFile.pos_out ch in + let len = Int64.sub pos' pos in + let hash = + let in_ch = open_in h.out_filename in + let () = LargeFile.seek_in in_ch pos in + let digest = Digest.channel in_ch (Int64.to_int len) in + let () = close_in in_ch in + digest + in + let () = Digest.output ch hash in + let s = { name = segment; pos; len; hash } in + let () = h.out_segments <- CString.Map.add segment s h.out_segments in + () + +let marshal_out_binary h ~segment = + let { out_channel = ch } = h in + let () = assert (not (CString.Map.mem segment h.out_segments)) in + let pos = LargeFile.pos_out ch in + let finish () = + let () = flush ch in + let pos' = LargeFile.pos_out ch in + let len = Int64.sub pos' pos in + let hash = + let in_ch = open_in h.out_filename in + let () = LargeFile.seek_in in_ch pos in + let digest = Digest.channel in_ch (Int64.to_int len) in + let () = close_in in_ch in + digest + in + let () = Digest.output ch hash in + let s = { name = segment; pos; len; hash } in + h.out_segments <- CString.Map.add segment s h.out_segments + in + ch, finish + +let open_in ~file = + try + let ch = open_in_bin file in + let magic = input_int32 ch in + let version = input_int32 ch in + let () = + if not (Int32.equal magic magic_number) then + let e = { filename = file; actual = version; expected = magic_number } in + raise (Bad_magic_number e) + in + let () = + let expected = Coq_config.vo_version in + if not (Int32.equal version expected) then + let e = { filename = file; actual = version; expected } in + raise (Bad_version_number e) + in + let summary_pos = input_int64 ch in + let () = LargeFile.seek_in ch summary_pos in + let nsum = input_int32 ch in + let seg = input_segment_summaries ch nsum CString.Map.empty in + { in_filename = file; in_channel = ch; in_segments = seg } + with + | End_of_file -> error_corrupted file "premature end of file" + | Failure s | Sys_error s -> error_corrupted file s + +let close_in ch = + close_in ch.in_channel + +let get_segment ch ~segment = + CString.Map.find segment ch.in_segments + +let segments ch = ch.in_segments + +let open_out ~file = + let ch = open_trapping_failure file in + let () = output_int32 ch magic_number in + let () = output_int32 ch Coq_config.vo_version in + let () = output_int64 ch 0L (* placeholder *) in + { out_channel = ch; out_segments = CString.Map.empty; out_filename = file } + +let close_out { out_channel = ch; out_segments = seg } = + let () = flush ch in + let pos = LargeFile.pos_out ch in + (* Write the segment summary *) + let () = output_int32 ch (Int32.of_int (CString.Map.cardinal seg)) in + let iter _ s = output_segment_summary ch s in + let () = CString.Map.iter iter seg in + (* Overwrite the position place holder *) + let () = LargeFile.seek_out ch 8L in + let () = output_int64 ch pos in + let () = flush ch in + close_out ch diff --git a/lib/objFile.mli b/lib/objFile.mli new file mode 100644 index 0000000000..36db7f4208 --- /dev/null +++ b/lib/objFile.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val magic_number : int32 + +type segment = { + name : string; + pos : int64; + len : int64; + hash : Digest.t; +} + +type in_handle +type out_handle + +val open_in : file:string -> in_handle +val close_in : in_handle -> unit +val marshal_in_segment : in_handle -> segment:string -> 'a * Digest.t +val get_segment : in_handle -> segment:string -> segment +val segments : in_handle -> segment CString.Map.t + +val open_out : file:string -> out_handle +val close_out : out_handle -> unit +val marshal_out_segment : out_handle -> segment:string -> 'a -> unit +val marshal_out_binary : out_handle -> segment:string -> out_channel * (unit -> unit) +(** Low-level API. This function returns a channel and a closure. The channel + should only be written to, and once done, the closure should be invoked. *) diff --git a/lib/system.ml b/lib/system.ml index 32e5a53821..4e98651d6e 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -240,220 +240,6 @@ let with_magic_number_check f a = spc () ++ strbrk "It is corrupted or was compiled with another version of Coq.") -module ObjFile = -struct - -let magic_number = 0x436F7121l (* "Coq!" *) - -(* - -int32: big-endian, 4 bytes -int64: big-endian, 8 bytes - --- string -- -int32 | length of the next field -data | - --- segment summary -- -string | name -int64 | absolute position -int64 | length (without hash) -hash | MD5 (16 bytes) - --- segment -- -... | binary data -hash | MD5 (16 bytes) - --- summary -- -int32 | number of segment summaries -s1 | -... | segment summaries -sn | - --- vo -- -int32 | magic number -int32 | Coq version -int64 | absolute position of the summary -... | segments -summary | - -*) - -type segment = { - name : string; - pos : int64; - len : int64; - hash : Digest.t; -} - -type in_handle = { - in_filename : string; - in_channel : in_channel; - in_segments : segment CString.Map.t; -} - -type out_handle = { - out_filename : string; - out_channel : out_channel; - mutable out_segments : segment CString.Map.t; -} - -let input_int32 ch = - let accu = ref 0l in - for _i = 0 to 3 do - let c = input_byte ch in - accu := Int32.add (Int32.shift_left !accu 8) (Int32.of_int c) - done; - !accu - -let input_int64 ch = - let accu = ref 0L in - for _i = 0 to 7 do - let c = input_byte ch in - accu := Int64.add (Int64.shift_left !accu 8) (Int64.of_int c) - done; - !accu - -let output_int32 ch n = - for i = 0 to 3 do - output_byte ch (Int32.to_int (Int32.shift_right_logical n (24 - 8 * i))) - done - -let output_int64 ch n = - for i = 0 to 7 do - output_byte ch (Int64.to_int (Int64.shift_right_logical n (56 - 8 * i))) - done - -let input_segment_summary ch = - let nlen = input_int32 ch in - let name = really_input_string ch (Int32.to_int nlen) in - let pos = input_int64 ch in - let len = input_int64 ch in - let hash = Digest.input ch in - { name; pos; len; hash } - -let output_segment_summary ch seg = - let nlen = Int32.of_int (String.length seg.name) in - let () = output_int32 ch nlen in - let () = output_string ch seg.name in - let () = output_int64 ch seg.pos in - let () = output_int64 ch seg.len in - let () = Digest.output ch seg.hash in - () - -let rec input_segment_summaries ch n accu = - if Int32.equal n 0l then accu - else - let s = input_segment_summary ch in - let accu = CString.Map.add s.name s accu in - input_segment_summaries ch (Int32.pred n) accu - -let marshal_in_segment (type a) h ~segment : a * Digest.t = - let { in_channel = ch } = h in - let s = CString.Map.find segment h.in_segments in - let () = LargeFile.seek_in ch s.pos in - let (v : a) = marshal_in h.in_filename ch in - let () = assert (Int64.equal (LargeFile.pos_in ch) (Int64.add s.pos s.len)) in - let h = Digest.input ch in - let () = assert (String.equal h s.hash) in - (v, s.hash) - -let marshal_out_segment h ~segment v = - let { out_channel = ch } = h in - let () = assert (not (CString.Map.mem segment h.out_segments)) in - let pos = LargeFile.pos_out ch in - let () = Marshal.to_channel ch v [] in - let () = flush ch in - let pos' = LargeFile.pos_out ch in - let len = Int64.sub pos' pos in - let hash = - let in_ch = open_in h.out_filename in - let () = LargeFile.seek_in in_ch pos in - let digest = Digest.channel in_ch (Int64.to_int len) in - let () = close_in in_ch in - digest - in - let () = Digest.output ch hash in - let s = { name = segment; pos; len; hash } in - let () = h.out_segments <- CString.Map.add segment s h.out_segments in - () - -let marshal_out_binary h ~segment = - let { out_channel = ch } = h in - let () = assert (not (CString.Map.mem segment h.out_segments)) in - let pos = LargeFile.pos_out ch in - let finish () = - let () = flush ch in - let pos' = LargeFile.pos_out ch in - let len = Int64.sub pos' pos in - let hash = - let in_ch = open_in h.out_filename in - let () = LargeFile.seek_in in_ch pos in - let digest = Digest.channel in_ch (Int64.to_int len) in - let () = close_in in_ch in - digest - in - let () = Digest.output ch hash in - let s = { name = segment; pos; len; hash } in - h.out_segments <- CString.Map.add segment s h.out_segments - in - ch, finish - -let open_in ~file = - try - let ch = open_in_bin file in - let magic = input_int32 ch in - let version = input_int32 ch in - let () = - if not (Int32.equal magic magic_number) then - let e = { filename = file; actual = version; expected = magic_number } in - raise (Bad_magic_number e) - in - let () = - let expected = Coq_config.vo_version in - if not (Int32.equal version expected) then - let e = { filename = file; actual = version; expected } in - raise (Bad_version_number e) - in - let summary_pos = input_int64 ch in - let () = LargeFile.seek_in ch summary_pos in - let nsum = input_int32 ch in - let seg = input_segment_summaries ch nsum CString.Map.empty in - { in_filename = file; in_channel = ch; in_segments = seg } - with - | End_of_file -> error_corrupted file "premature end of file" - | Failure s | Sys_error s -> error_corrupted file s - -let close_in ch = - close_in ch.in_channel - -let get_segment ch ~segment = - CString.Map.find segment ch.in_segments - -let segments ch = ch.in_segments - -let open_out ~file = - let ch = open_trapping_failure file in - let () = output_int32 ch magic_number in - let () = output_int32 ch Coq_config.vo_version in - let () = output_int64 ch 0L (* placeholder *) in - { out_channel = ch; out_segments = CString.Map.empty; out_filename = file } - -let close_out { out_channel = ch; out_segments = seg } = - let () = flush ch in - let pos = LargeFile.pos_out ch in - (* Write the segment summary *) - let () = output_int32 ch (Int32.of_int (CString.Map.cardinal seg)) in - let iter _ s = output_segment_summary ch s in - let () = CString.Map.iter iter seg in - (* Overwrite the position place holder *) - let () = LargeFile.seek_out ch 8L in - let () = output_int64 ch pos in - let () = flush ch in - close_out ch - -end - (* Time stamps. *) type time = float * float * float diff --git a/lib/system.mli b/lib/system.mli index 7e02b76203..4a8c35b6ea 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -88,36 +88,6 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b val marshal_out : out_channel -> 'a -> unit val marshal_in : string -> in_channel -> 'a -module ObjFile : -sig - -val magic_number : int32 - -type segment = { - name : string; - pos : int64; - len : int64; - hash : Digest.t; -} - -type in_handle -type out_handle - -val open_in : file:string -> in_handle -val close_in : in_handle -> unit -val marshal_in_segment : in_handle -> segment:string -> 'a * Digest.t -val get_segment : in_handle -> segment:string -> segment -val segments : in_handle -> segment CString.Map.t - -val open_out : file:string -> out_handle -val close_out : out_handle -> unit -val marshal_out_segment : out_handle -> segment:string -> 'a -> unit -val marshal_out_binary : out_handle -> segment:string -> out_channel * (unit -> unit) -(** Low-level API. This function returns a channel and a closure. The channel - should only be written to, and once done, the closure should be invoked. *) - -end - (** {6 Time stamps.} *) type time |