aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml64
-rw-r--r--checker/check.mllib1
-rw-r--r--checker/checkFlags.ml23
-rw-r--r--checker/checkFlags.mli12
-rw-r--r--checker/checkInductive.ml11
-rw-r--r--checker/mod_checking.ml9
-rw-r--r--checker/validate.ml9
-rw-r--r--checker/validate.mli2
-rw-r--r--checker/values.ml18
-rw-r--r--checker/votour.ml92
10 files changed, 159 insertions, 82 deletions
diff --git a/checker/check.ml b/checker/check.ml
index bb3255338f..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 ~debug:!Flags.debug value v 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/check.mllib b/checker/check.mllib
index d47a93c70d..a16a871dc3 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,5 +1,6 @@
Analyze
+CheckFlags
CheckInductive
Mod_checking
CheckTypes
diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml
new file mode 100644
index 0000000000..1f5e76bd83
--- /dev/null
+++ b/checker/checkFlags.ml
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* * 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 Declarations
+
+let set_local_flags flags env =
+ let flags =
+ { (Environ.typing_flags env) with
+ check_guarded = flags.check_guarded;
+ check_positive = flags.check_positive;
+ check_universes = flags.check_universes;
+ conv_oracle = flags.conv_oracle;
+ cumulative_sprop = flags.cumulative_sprop;
+ }
+ in
+ Environ.set_typing_flags flags env
diff --git a/checker/checkFlags.mli b/checker/checkFlags.mli
new file mode 100644
index 0000000000..2e41e656f1
--- /dev/null
+++ b/checker/checkFlags.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* * 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 set_local_flags : Declarations.typing_flags -> Environ.env -> Environ.env
+(** Set flags except for those ignored by the checker (eg vm_compute). *)
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index a1d5aedb01..c370a77ea0 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -164,16 +164,7 @@ let check_inductive env mind mb =
mind_private; mind_typing_flags; }
=
(* Locally set typing flags for further typechecking *)
- let mb_flags = mb.mind_typing_flags in
- let env = Environ.set_typing_flags
- {env.env_typing_flags with
- check_guarded = mb_flags.check_guarded;
- check_positive = mb_flags.check_positive;
- check_universes = mb_flags.check_universes;
- conv_oracle = mb_flags.conv_oracle;
- }
- env
- in
+ let env = CheckFlags.set_local_flags mb.mind_typing_flags env in
Indtypes.check_inductive env ~sec_univs:None mind entry
in
let check = check mind in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 44b7089fd0..8fd81d43be 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -17,14 +17,7 @@ let set_indirect_accessor f = indirect_accessor := f
let check_constant_declaration env kn cb =
Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn);
- let cb_flags = cb.const_typing_flags in
- let env = Environ.set_typing_flags
- {env.env_typing_flags with
- check_guarded = cb_flags.check_guarded;
- check_universes = cb_flags.check_universes;
- conv_oracle = cb_flags.conv_oracle;}
- env
- in
+ let env = CheckFlags.set_local_flags cb.const_typing_flags env in
let poly, env =
match cb.const_universes with
| Monomorphic ctx ->
diff --git a/checker/validate.ml b/checker/validate.ml
index 66367cb002..20884c4d01 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -208,11 +208,10 @@ let print_frame = function
| CtxField i -> Printf.sprintf "fld=%i" i
| CtxTag i -> Printf.sprintf "tag=%i" i
-let validate ~debug v (o, mem) =
+let validate v (o, mem) =
try val_gen v mem mt_ec o
with ValidObjError(msg,ctx,obj) ->
- (if debug then
- let ctx = List.rev_map print_frame ctx in
- print_endline ("Context: "^String.concat"/"ctx);
- pr_obj mem obj);
+ let rctx = List.rev_map print_frame ctx in
+ print_endline ("Context: "^String.concat"/"rctx);
+ pr_obj mem obj;
failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")")
diff --git a/checker/validate.mli b/checker/validate.mli
index 9ddc510e4a..1204b528f9 100644
--- a/checker/validate.mli
+++ b/checker/validate.mli
@@ -10,4 +10,4 @@
open Analyze
-val validate : debug:bool -> Values.value -> data * obj LargeArray.t -> unit
+val validate : Values.value -> data * obj LargeArray.t -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 12f7135cdf..9bd381e4a9 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -241,7 +241,10 @@ let v_cst_def =
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|]
let v_typing_flags =
- v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+ v_tuple "typing_flags"
+ [|v_bool; v_bool; v_bool;
+ v_oracle; v_bool; v_bool;
+ v_bool; v_bool; v_bool|]
let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
@@ -372,6 +375,17 @@ let v_compiled_lib =
let v_obj = Dyn
+let v_globref = Sum("globref",0,[|
+ [|v_id|];
+ [|v_cst|];
+ [|v_ind|];
+ [|v_cons|]
+ |])
+
+let v_ext_gref = Sum("extended_global_reference",0,[|[|v_globref|];[|v_kn|]|])
+
+let v_open_filter = Sum ("open_filter",1,[|[|v_hset v_ext_gref|]|])
+
let rec v_aobjs = Sum("algebraic_objects", 0,
[| [|v_libobjs|];
[|v_mp;v_subst|]
@@ -383,7 +397,7 @@ and v_libobjt = Sum("Libobject.t",0,
[| v_substobjs |];
[| v_aobjs |];
[| v_libobjs |];
- [| List v_mp |];
+ [| List (v_pair v_open_filter v_mp)|];
[| v_obj |]
|])
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 01:10:08 +0000