Merge PR #12092: Implement a name-based representation for vo files.

Reviewed-by: ejgallego
Ack-by: gares

5 files changed, 280 insertions, 44 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..96db51a010
--- /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_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; 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_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; 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..b15b04ee54
--- /dev/null
+++ b/lib/objFile.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   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)
+(** [marshal_out_binary oh segment] is a low level, stateful, API returning
+    [oc, stop]. Once called no other API can be used on the same [oh] and only
+    [Stdlib.output_*] APIs should be used on [oc]. [stop ()] must be invoked in
+    order to signal that all data was written to [oc] (which should not be used
+    afterwards). Only after calling [stop] the other API can be used on [oh]. *)
diff --git a/lib/system.ml b/lib/system.ml
index d7f5fa26ab..4e98651d6e 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -182,36 +182,9 @@ let marshal_in filename ch =
   | End_of_file -> error_corrupted filename "premature end of file"
   | Failure s -> error_corrupted filename s
 
-let digest_out = Digest.output
-let digest_in filename ch =
-  try Digest.input ch
-  with
-  | End_of_file -> error_corrupted filename "premature end of file"
-  | Failure s -> error_corrupted filename s
-
-let marshal_out_segment f ch v =
-  let start = pos_out ch in
-  output_binary_int ch 0;  (* dummy value for stop *)
-  marshal_out ch v;
-  let stop = pos_out ch in
-  seek_out ch start;
-  output_binary_int ch stop;
-  seek_out ch stop;
-  digest_out ch (Digest.file f)
-
-let marshal_in_segment f ch =
-  let stop = (input_binary_int f ch : int) in
-  let v = marshal_in f ch in
-  let digest = digest_in f ch in
-  v, stop, digest
-
-let skip_in_segment f ch =
-  let stop = (input_binary_int f ch : int) in
-  seek_in ch stop;
-  stop, digest_in f ch
-
-type magic_number_error = {filename: string; actual: int; expected: int}
+type magic_number_error = {filename: string; actual: int32; expected: int32}
 exception Bad_magic_number of magic_number_error
+exception Bad_version_number of magic_number_error
 
 let raw_extern_state magic filename =
   let channel = open_trapping_failure filename in
@@ -225,8 +198,8 @@ let raw_intern_state magic filename =
     if not (Int.equal actual_magic magic) then
         raise (Bad_magic_number {
             filename=filename;
-            actual=actual_magic;
-            expected=magic});
+            actual=Int32.of_int actual_magic;
+            expected=Int32.of_int magic});
     channel
   with
   | End_of_file -> error_corrupted filename "premature end of file"
@@ -256,10 +229,14 @@ let intern_state magic filename =
 
 let with_magic_number_check f a =
   try f a
-  with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
+  with
+  | Bad_magic_number {filename=fname; _} ->
+    CErrors.user_err ~hdr:"with_magic_number_check"
+    (str"File " ++ str fname ++ strbrk" is corrupted.")
+  | Bad_version_number {filename=fname;actual=actual;expected=expected} ->
     CErrors.user_err ~hdr:"with_magic_number_check"
-    (str"File " ++ str fname ++ strbrk" has bad magic number " ++
-    int actual ++ str" (expected " ++ int expected ++ str")." ++
+    (str"File " ++ str fname ++ strbrk" has bad version number " ++
+    (str @@ Int32.to_string actual) ++ str" (expected " ++ (str @@ Int32.to_string expected) ++ str")." ++
     spc () ++
     strbrk "It is corrupted or was compiled with another version of Coq.")
 
diff --git a/lib/system.mli b/lib/system.mli
index 00701379bd..4a8c35b6ea 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -68,8 +68,9 @@ val file_exists_respecting_case : string -> string -> bool
   when the check fails, with the full file name and expected/observed magic
   numbers. *)
 
-type magic_number_error = {filename: string; actual: int; expected: int}
+type magic_number_error = {filename: string; actual: int32; expected: int32}
 exception Bad_magic_number of magic_number_error
+exception Bad_version_number of magic_number_error
 
 val raw_extern_state : int -> string -> out_channel
 
@@ -87,15 +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
 
-(** Clones of Digest.output and Digest.input (with nice error message) *)
-
-val digest_out : out_channel -> Digest.t -> unit
-val digest_in : string -> in_channel -> Digest.t
-
-val marshal_out_segment : string -> out_channel -> 'a -> unit
-val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t
-val skip_in_segment : string -> in_channel -> int * Digest.t
-
 (** {6 Time stamps.} *)
 
 type time