From 75e394770b534994830f6d80e649734275de5006 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 29 Mar 2020 18:02:46 +0200 Subject: Implement a name-based representation for vo files. See CEP#44 for futher details. --- checker/check.ml | 62 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 31 insertions(+), 31 deletions(-) (limited to 'checker/check.ml') diff --git a/checker/check.ml b/checker/check.ml index 4212aac6ea..8881e05ab6 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 + System.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.System.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.System.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 = System.ObjFile.get_segment ch ~segment:"summary" in + let seg_md = System.ObjFile.get_segment ch ~segment:"library" in + let seg_univs = System.ObjFile.get_segment ch ~segment:"universes" in + let seg_tasks = System.ObjFile.get_segment ch ~segment:"tasks" in + let seg_opaque = System.ObjFile.get_segment ch ~segment:"opaques" in + let () = System.ObjFile.close_in ch in + (* Actually read the data *) + let ch = open_in 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 System.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; -- cgit v1.2.3 From 3dc9ec53041b4b34a601c2d454d0e47005561b30 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 Apr 2020 19:09:34 +0200 Subject: Move the ObjFile module to its own file. --- checker/check.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'checker/check.ml') diff --git a/checker/check.ml b/checker/check.ml index 8881e05ab6..8554c5a677 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.ObjFile.open_in ~file:f + ObjFile.open_in ~file:f (************************************************************************) (* Internalise libraries *) @@ -295,13 +295,13 @@ type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = depe let depgraph = ref LibraryMap.empty let marshal_in_segment ~validate ~value ~segment f ch = - let () = LargeFile.seek_in ch segment.System.ObjFile.pos in + let () = LargeFile.seek_in ch segment.ObjFile.pos in if validate then let v = try let v = Analyze.parse_channel ch in let digest = Digest.input ch in - let () = if not (String.equal digest segment.System.ObjFile.hash) then raise Exit in + let () = if not (String.equal digest segment.ObjFile.hash) then raise Exit in v with _ -> user_err (str "Corrupted file " ++ quote (str f)) @@ -326,12 +326,12 @@ let intern_from_file ~intern_mode (dir, f) = try (* First pass to read the metadata of the file *) let ch = System.with_magic_number_check raw_intern_library f in - let seg_sd = System.ObjFile.get_segment ch ~segment:"summary" in - let seg_md = System.ObjFile.get_segment ch ~segment:"library" in - let seg_univs = System.ObjFile.get_segment ch ~segment:"universes" in - let seg_tasks = System.ObjFile.get_segment ch ~segment:"tasks" in - let seg_opaque = System.ObjFile.get_segment ch ~segment:"opaques" in - let () = System.ObjFile.close_in 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 f in @@ -360,7 +360,7 @@ let intern_from_file ~intern_mode (dir, f) = end; Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = - let open System.ObjFile 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 -- cgit v1.2.3 From 0520fa60a855b4c5f7b9d9298607cfd9e346c0e3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 26 Apr 2020 14:25:22 +0200 Subject: Open object files in binary mode. --- checker/check.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/check.ml') diff --git a/checker/check.ml b/checker/check.ml index 8554c5a677..31bfebc3d5 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -333,7 +333,7 @@ let intern_from_file ~intern_mode (dir, f) = let seg_opaque = ObjFile.get_segment ch ~segment:"opaques" in let () = ObjFile.close_in ch in (* Actually read the data *) - let ch = open_in f in + 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 -- cgit v1.2.3