Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228(************************************************************************)(* * The Rocq Prover / The Rocq 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 Ppopen System
let magic_number = 0x436F7121l (* "Coq!" *)
let error_corrupted file s = CErrors.user_err (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 (str "Can't open " ++ str name ++ spc() ++ str "(" ++ CErrors.print e ++ str ").")
(*
int32: big-endian, 4 bytesint64: big-endian, 8 bytes
-- string --int32 | length of the next fielddata |
-- segment summary --string | nameint64 | absolute positionint64 | length (without hash)hash | MD5 (16 bytes)
-- segment --... | binary datahash | MD5 (16 bytes)
-- summary --int32 | number of segment summariess1 |... | segment summariessn |
-- vo --int32 | magic numberint32 | Coq versionint64 | absolute position of the summary... | segmentssummary |
*)
type 'a segment = { name : string; pos : int64; len : int64; hash : Digest.t;}
type in_handle = { in_filename : string; in_channel : in_channel; in_segments : Obj.t segment CString.Map.t;}
type out_handle = { out_filename : string; out_channel : out_channel; mutable out_segments : Obj.t segment CString.Map.t;}
type 'a id = { id : string }
let make_id id = { id }
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.id 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.id 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_bin 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.id; pos; len; hash } in let () = h.out_segments <- CString.Map.add segment.id s h.out_segments in ()
let marshal_out_binary h ~segment = let { out_channel = ch } = h in let () = assert (not (CString.Map.mem segment.id 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_bin 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.id; pos; len; hash } in h.out_segments <- CString.Map.add segment.id 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 = magic; 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 (type a) ch ~(segment : a id) : a segment = (CString.Map.find segment.id ch.in_segments :> a segment)
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
(** cf library.ml for real type *)type summary_disk
let summary_seg : summary_disk id = make_id "summary"
let rec assert_string_list v = if Obj.is_int v then assert (Int.equal (Obj.magic v) 0) else let () = assert (Obj.tag v = 0 && Obj.size v = 2 && Obj.tag (Obj.field v 0) = Obj.string_tag) in assert_string_list (Obj.field v 1)
let library_name f = let ch = with_magic_number_check (fun file -> open_in ~file) f in let md, _ = marshal_in_segment ch ~segment: summary_seg in let md = Obj.repr md in assert (Obj.tag md = 0 && Obj.size md > 1); let v = Obj.field (Obj.repr md) 0 in assert_string_list v; (Obj.magic v : string list)