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

Reviewed-by: ejgallego
Ack-by: gares

2 files changed, 99 insertions, 55 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 4212aac6ea..31bfebc3d5 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -255,7 +255,7 @@ let try_locate_qualified_library lib = match lib with
 (*s Low-level interning of libraries from files *)
 
 let raw_intern_library f =
-  System.raw_intern_state Coq_config.vo_magic_number f
+  ObjFile.open_in ~file:f
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -294,57 +294,56 @@ type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = depe
 (* Dependency graph *)
 let depgraph = ref LibraryMap.empty
 
-let marshal_in_segment ~validate ~value f ch =
+let marshal_in_segment ~validate ~value ~segment f ch =
+  let () = LargeFile.seek_in ch segment.ObjFile.pos in
   if validate then
-    let v, stop, digest =
+    let v =
       try
-        let stop = input_binary_int ch in
         let v = Analyze.parse_channel ch in
         let digest = Digest.input ch in
-        v, stop, digest
+        let () = if not (String.equal digest segment.ObjFile.hash) then raise Exit in
+        v
       with _ ->
         user_err (str "Corrupted file " ++ quote (str f))
     in
     let () = Validate.validate value v in
     let v = Analyze.instantiate v in
-    Obj.obj v, stop, digest
+    Obj.obj v
   else
-    System.marshal_in_segment f ch
+    System.marshal_in f ch
 
-let skip_in_segment f ch =
-  try
-    let stop = (input_binary_int ch : int) in
-    seek_in ch stop;
-    let digest = Digest.input ch in
-    stop, digest
-  with _ ->
-    user_err (str "Corrupted file " ++ quote (str f))
-
-let marshal_or_skip ~validate ~value f ch =
+let marshal_or_skip ~validate ~value ~segment f ch =
   if validate then
-    let v, pos, digest = marshal_in_segment ~validate ~value f ch in
-    Some v, pos, digest
+    let v = marshal_in_segment ~validate:true ~value ~segment f ch in
+    Some v
   else
-    let pos, digest = skip_in_segment f ch in
-    None, pos, digest
+    None
 
 let intern_from_file ~intern_mode (dir, f) =
   let validate = intern_mode <> Dep in
   Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
+      (* First pass to read the metadata of the file *)
       let ch = System.with_magic_number_check raw_intern_library f in
-      let (sd:summary_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_libsum f ch in
-      let (md:library_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_lib f ch in
-      let (opaque_csts:seg_univ option), _, udg = marshal_in_segment ~validate ~value:Values.v_univopaques f ch in
-      let (tasks:'a option), _, _ = marshal_in_segment ~validate ~value:Values.(Opt Any) f ch in
-      let (table:seg_proofs option), pos, checksum =
-        marshal_or_skip ~validate ~value:Values.v_opaquetable f ch in
+      let seg_sd = ObjFile.get_segment ch ~segment:"summary" in
+      let seg_md = ObjFile.get_segment ch ~segment:"library" in
+      let seg_univs = ObjFile.get_segment ch ~segment:"universes" in
+      let seg_tasks = ObjFile.get_segment ch ~segment:"tasks" in
+      let seg_opaque = ObjFile.get_segment ch ~segment:"opaques" in
+      let () = ObjFile.close_in ch in
+      (* Actually read the data *)
+      let ch = open_in_bin f in
+
+      let (sd:summary_disk) = marshal_in_segment ~validate ~value:Values.v_libsum ~segment:seg_sd f ch in
+      let (md:library_disk) = marshal_in_segment ~validate ~value:Values.v_lib ~segment:seg_md f ch in
+      let (opaque_csts:seg_univ option) = marshal_in_segment ~validate ~value:Values.v_univopaques ~segment:seg_univs f ch in
+      let (tasks:'a option) = marshal_in_segment ~validate ~value:Values.(Opt Any) ~segment:seg_tasks f ch in
+      let (table:seg_proofs option) =
+        marshal_or_skip ~validate ~value:Values.v_opaquetable ~segment:seg_opaque f ch in
       (* Verification of the final checksum *)
       let () = close_in ch in
       let ch = open_in_bin f in
-      if not (String.equal (Digest.channel ch pos) checksum) then
-        user_err ~hdr:"intern_from_file" (str "Checksum mismatch");
       let () = close_in ch in
       if dir <> sd.md_name then
         user_err ~hdr:"intern_from_file"
@@ -361,8 +360,9 @@ let intern_from_file ~intern_mode (dir, f) =
       end;
       Flags.if_verbose chk_pp (str" done]" ++ fnl ());
       let digest =
-        if opaque_csts <> None then Safe_typing.Dvivo (digest,udg)
-        else (Safe_typing.Dvo_or_vi digest) in
+        let open ObjFile in
+        if opaque_csts <> None then Safe_typing.Dvivo (seg_md.hash, seg_univs.hash)
+        else (Safe_typing.Dvo_or_vi seg_md.hash) in
       sd,md,table,opaque_csts,digest
     with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
diff --git a/checker/votour.ml b/checker/votour.ml
index a83ba20dd6..3fb3ccadf4 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -349,14 +349,63 @@ let parse_header chan =
   let size64 = input_binary_int chan in
   { magic; length; size32; size64; objects }
 
+module ObjFile =
+struct
+
 type segment = {
   name : string;
-  mutable pos : int;
-  typ : Values.value;
+  pos : int64;
+  len : int64;
+  hash : Digest.t;
   mutable header : header;
 }
 
-let make_seg name typ = { name; typ; pos = 0; header = dummy_header }
+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 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; header = dummy_header }
+
+let rec input_segment_summaries ch n accu =
+  if Int32.equal n 0l then Array.of_list (List.rev accu)
+  else
+    let s = input_segment_summary ch in
+    let accu = s :: accu in
+    input_segment_summaries ch (Int32.pred n) accu
+
+let parse_segments ch =
+  let magic = input_int32 ch in
+  let version = input_int32 ch 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 [] in
+  for i = 0 to Array.length seg - 1 do
+    let () = LargeFile.seek_in ch seg.(i).pos in
+    let header = parse_header ch in
+    seg.(i).header <- header
+  done;
+  (magic, version, seg)
+
+end
 
 let visit_vo f =
   Printf.printf "\nWelcome to votour !\n";
@@ -364,13 +413,13 @@ let visit_vo f =
   Printf.printf "Object sizes are in words (%d bits)\n" Sys.word_size;
   Printf.printf
     "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
-  let segments = [|
-    make_seg "summary" Values.v_libsum;
-    make_seg "library" Values.v_lib;
-    make_seg "univ constraints of opaque proofs" Values.v_univopaques;
-    make_seg "STM tasks" (Opt Values.v_stm_seg);
-    make_seg "opaque proofs" Values.v_opaquetable;
-  |] in
+  let known_segments = [
+    "summary", Values.v_libsum;
+    "library", Values.v_lib;
+    "universes", Values.v_univopaques;
+    "tasks", (Opt Values.v_stm_seg);
+    "opaques", Values.v_opaquetable;
+  ] in
   let repr =
     if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S)
     (* On 32-bit machines, representation may exceed the max size of arrays *)
@@ -379,28 +428,23 @@ let visit_vo f =
   let module Visit = Visit(Repr) in
   while true do
     let ch = open_in_bin f in
-    let magic = input_binary_int ch in
-    Printf.printf "File format: %d\n%!" magic;
-    for i=0 to Array.length segments - 1 do
-      let pos = input_binary_int ch in
-      segments.(i).pos <- pos_in ch;
-      let header = parse_header ch in
-      segments.(i).header <- header;
-      seek_in ch pos;
-      ignore(Digest.input ch);
-    done;
+    let (_magic, version, segments) = ObjFile.parse_segments ch in
+    Printf.printf "File format: %ld\n%!" version;
     Printf.printf "The file has %d segments, choose the one to visit:\n"
       (Array.length segments);
-    Array.iteri (fun i { name; pos; header } ->
+    Array.iteri (fun i ObjFile.{ name; pos; header } ->
       let size = if Sys.word_size = 64 then header.size64 else header.size32 in
-      Printf.printf "  %d: %s, starting at byte %d (size %iw)\n" i name pos size)
+      Printf.printf "  %d: %s, starting at byte %Ld (size %iw)\n" i name pos size)
       segments;
     match read_num (Array.length segments) with
     | Some seg ->
-       seek_in ch segments.(seg).pos;
+       let seg = segments.(seg) in
+       let open ObjFile in
+       LargeFile.seek_in ch seg.pos;
        let o = Repr.input ch in
        let () = Visit.init () in
-       Visit.visit segments.(seg).typ o []
+       let typ = try List.assoc seg.name known_segments with Not_found -> Any in
+       Visit.visit typ o []
     | None -> ()
   done