From f5ab2e37b0609d8edb8d65dfae49741442a90657 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 2 Apr 2013 22:08:44 +0000 Subject: [PATCH] Revised infrastructure for lazy loading of opaque proofs Get rid of the LightenLibrary hack : no more last-minute collect of opaque terms and Obj.magic tricks. Instead, we make coqc accumulate the opaque terms as soon as constant_bodies are created outside sections. In these cases, the opaque terms are placed in a special table, and some (DirPath.t * int) are used as indexes in constant_body. In an interactive session, the local opaque terms stay directly stored in the constant_body. The structure of .vo file stays similar : magic number, regular library structure, digest of the first part, array of opaque terms. In addition, we now have a final checksum for checking the integrity of the whole .vo file. The other difference is that lazy_constr aren't changed into int indexes in .vo files, but are now coded as (substitution list * DirPath.t * int). In particular this approach allows to refer to opaque terms from another library. This (and accumulating substitutions in lazy_constr) seems to greatly help decreasing the size of opaque tables : -20% of vo size on the standard library :-). The compilation times are slightly better, but that can be statistic noise. The -force-load-proofs isn't active anymore : it behaves now just like -lazy-load-proofs. The -dont-load-proofs mode has slightly changed : opaque terms aren't seen as axioms anymore, but accessing their bodies will raise an error. Btw, API change : Declareops.body_of_constant now produces directly a constr option instead of a constr_substituted option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/check.ml | 37 ++++- checker/declarations.ml | 36 +++-- checker/declarations.mli | 13 +- checker/mod_checking.ml | 2 +- checker/safe_typing.ml | 113 +------------ checker/safe_typing.mli | 18 +-- doc/refman/RefMan-com.tex | 14 +- kernel/declareops.ml | 14 +- kernel/declareops.mli | 8 +- kernel/lazyconstr.ml | 57 +++++-- kernel/lazyconstr.mli | 35 +++- kernel/safe_typing.ml | 149 +----------------- kernel/safe_typing.mli | 11 -- kernel/term_typing.ml | 37 +++-- library/assumptions.ml | 2 +- library/library.ml | 133 +++++++++++++--- library/states.ml | 2 - .../funind/functional_principles_proofs.ml | 6 +- plugins/funind/functional_principles_types.ml | 3 +- plugins/funind/indfun.ml | 3 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/recdef.ml | 2 +- plugins/xml/xmlcommand.ml | 3 +- printing/prettyp.ml | 2 +- toplevel/coqtop.ml | 3 +- toplevel/lemmas.ml | 2 +- 26 files changed, 296 insertions(+), 411 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index eb4016f5f0d6..1b9fd07013a3 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -40,7 +40,7 @@ type compilation_unit_name = DirPath.t type library_disk = { md_name : compilation_unit_name; - md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library; + md_compiled : Safe_typing.compiled_library; md_objects : library_objects; md_deps : (compilation_unit_name * Digest.t) array; md_imports : compilation_unit_name array } @@ -56,6 +56,7 @@ type library_t = { library_name : compilation_unit_name; library_filename : CUnix.physical_path; library_compiled : Safe_typing.compiled_library; + library_opaques : Term.constr array; library_deps : (compilation_unit_name * Digest.t) array; library_digest : Digest.t } @@ -91,6 +92,19 @@ let library_full_filename dir = (find_library dir).library_filename let register_loaded_library m = libraries_table := LibraryMap.add m.library_name m !libraries_table +(* Map from library names to table of opaque terms *) +let opaque_tables = ref LibraryMap.empty + +let access_opaque_table dp i = + let t = + try LibraryMap.find dp !opaque_tables + with Not_found -> assert false + in + assert (i < Array.length t); + t.(i) + +let _ = Declarations.indirect_opaque_access := access_opaque_table + let check_one_lib admit (dir,m) = let file = m.library_filename in let md = m.library_compiled in @@ -105,7 +119,7 @@ let check_one_lib admit (dir,m) = else (Flags.if_verbose ppnl (str "Checking library: " ++ pr_dirpath dir); - Safe_typing.import file md dig); + Safe_typing.import file md m.library_opaques dig); Flags.if_verbose pp (fnl()); pp_flush (); register_loaded_library m @@ -280,7 +294,8 @@ let with_magic_number_check f a = let mk_library md f table digest = { library_name = md.md_name; library_filename = f; - library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled; + library_compiled = md.md_compiled; + library_opaques = table; library_deps = md.md_deps; library_digest = digest } @@ -298,16 +313,24 @@ let intern_from_file (dir, f) = try let ch = with_magic_number_check raw_intern_library f in let (md:library_disk) = System.marshal_in f ch in - let digest = System.marshal_in f ch in - let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in - close_in ch; + let (digest:Digest.t) = System.marshal_in f ch in + let (table:Term.constr array) = System.marshal_in f ch in + (* Verification of the final checksum *) + let pos = pos_in ch in + let (checksum:Digest.t) = System.marshal_in f ch in + let () = close_in ch in + let ch = open_in f in + if not (String.equal (Digest.channel ch pos) checksum) then + errorlabstrm "intern_from_file" (str "Checksum mismatch"); + let () = close_in ch in if dir <> md.md_name then - errorlabstrm "load_physical_library" + errorlabstrm "intern_from_file" (name_clash_message dir md.md_name f); Flags.if_verbose ppnl (str" done]"); md,table,digest with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; + opaque_tables := LibraryMap.add md.md_name table !opaque_tables; mk_library md f table digest let get_deps (dir, f) = diff --git a/checker/declarations.ml b/checker/declarations.ml index af8b1f21764d..cfaa2f5f732b 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -480,24 +480,34 @@ let subst_substituted s r = let force_constr = force subst_mps +let from_val c = ref (LSval c) + type constr_substituted = constr substituted let val_cstr_subst = val_substituted val_constr let subst_constr_subst = subst_substituted -(** Beware! In .vo files, lazy_constr are stored as integers - used as indexes for a separate table. The actual lazy_constr is restored - later, by [Safe_typing.LightenLibrary.load]. This allows us - to use here a different definition of lazy_constr than coqtop: - since the checker will inspect all proofs parts, even opaque - ones, no need to use Lazy.t here *) +(* Nota : in coqtop, the [lazy_constr] type also have a [Direct] + constructor, but it shouldn't occur inside a .vo, so we ignore it *) + +type lazy_constr = + | Indirect of substitution list * DirPath.t * int +(* | Direct of constr_substituted *) + +let subst_lazy_constr sub = function + | Indirect (l,dp,i) -> Indirect (sub::l,dp,i) + +let indirect_opaque_access = + ref ((fun dp i -> assert false) : DirPath.t -> int -> constr) + +let force_lazy_constr = function + | Indirect (l,dp,i) -> + let c = !indirect_opaque_access dp i in + force_constr (List.fold_right subst_constr_subst l (from_val c)) -type lazy_constr = constr_substituted -let subst_lazy_constr = subst_substituted -let force_lazy_constr = force_constr -let lazy_constr_from_val c = c -let val_lazy_constr = val_cstr_subst +let val_lazy_constr = + val_sum "lazy_constr" 0 [|[|val_list val_subst;val_dp;val_int|]|] (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -532,8 +542,8 @@ type constant_body = { let body_of_constant cb = match cb.const_body with | Undef _ -> None - | Def c -> Some c - | OpaqueDef c -> Some c + | Def c -> Some (force_constr c) + | OpaqueDef c -> Some (force_lazy_constr c) let constant_has_body cb = match cb.const_body with | Undef _ -> false diff --git a/checker/declarations.mli b/checker/declarations.mli index 80c895bbe9b4..cc3123ca7ddf 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -30,16 +30,9 @@ type constr_substituted val force_constr : constr_substituted -> constr val from_val : constr -> constr_substituted -(** Beware! In .vo files, lazy_constr are stored as integers - used as indexes for a separate table. The actual lazy_constr is restored - later, by [Safe_typing.LightenLibrary.load]. This allows us - to use here a different definition of lazy_constr than coqtop: - since the checker will inspect all proofs parts, even opaque - ones, no need to use Lazy.t here *) - type lazy_constr -val force_lazy_constr : lazy_constr -> constr -val lazy_constr_from_val : constr_substituted -> lazy_constr + +val indirect_opaque_access : (DirPath.t -> int -> constr) ref (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -63,7 +56,7 @@ type constant_body = { const_native_name : native_name ref; const_inline_code : bool } -val body_of_constant : constant_body -> constr_substituted option +val body_of_constant : constant_body -> constr option val constant_has_body : constant_body -> bool val is_opaque : constant_body -> bool diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index bc4ea7c692bd..ebe44997dafd 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -35,7 +35,7 @@ let check_constant_declaration env kn cb = let _ = infer_type envty ty in (match body_of_constant cb with | Some bd -> - let j = infer env' (force_constr bd) in + let j = infer env' bd in conv_leq envty j ty | None -> ()) | PolymorphicArity(ctxt,par) -> diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 5cbcc00f573a..492f5bc20e67 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -59,117 +59,19 @@ let check_imports f caller env needed = in Array.iter check needed +type nativecode_symb_array type compiled_library = DirPath.t * module_body * (DirPath.t * Digest.t) array * - engagement option - - (* Store the body of modules' opaque constants inside a table. - - This module is used during the serialization and deserialization - of vo files. - - By adding an indirection to the opaque constant definitions, we - gain the ability not to load them. As these constant definitions - are usually big terms, we save a deserialization time as well as - some memory space. *) -module LightenLibrary : sig - type table - type lightened_compiled_library - val load : table -> lightened_compiled_library -> compiled_library -end = struct - - (* The table is implemented as an array of [constr_substituted]. - Keys are hence integers. To avoid changing the [compiled_library] - type, we brutally encode integers into [lazy_constr]. This isn't - pretty, but shouldn't be dangerous since the produced structure - [lightened_compiled_library] is abstract and only meant for writing - to .vo via Marshal (which doesn't care about types). - *) - type table = constr_substituted array - let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int) - - (* To avoid any future misuse of the lightened library that could - interpret encoded keys as real [constr_substituted], we hide - these kind of values behind an abstract datatype. *) - type lightened_compiled_library = compiled_library - - (* Map a [compiled_library] to another one by just updating - the opaque term [t] to [on_opaque_const_body t]. *) - let traverse_library on_opaque_const_body = - let rec traverse_module mb = - match mb.mod_expr with - None -> - { mb with - mod_expr = None; - mod_type = traverse_modexpr mb.mod_type; - } - | Some impl when impl == mb.mod_type-> - let mtb = traverse_modexpr mb.mod_type in - { mb with - mod_expr = Some mtb; - mod_type = mtb; - } - | Some impl -> - { mb with - mod_expr = Option.map traverse_modexpr mb.mod_expr; - mod_type = traverse_modexpr mb.mod_type; - } - and traverse_struct struc = - let traverse_body (l,body) = (l,match body with - | (SFBconst cb) when is_opaque cb -> - SFBconst {cb with const_body = on_opaque_const_body cb.const_body} - | (SFBconst _ | SFBmind _ ) as x -> - x - | SFBmodule m -> - SFBmodule (traverse_module m) - | SFBmodtype m -> - SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr})) - in - List.map traverse_body struc - - and traverse_modexpr = function - | SEBfunctor (mbid,mty,mexpr) -> - SEBfunctor (mbid, - ({mty with - typ_expr = traverse_modexpr mty.typ_expr}), - traverse_modexpr mexpr) - | SEBident mp as x -> x - | SEBstruct (struc) -> - SEBstruct (traverse_struct struc) - | SEBapply (mexpr,marg,u) -> - SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u) - | SEBwith (seb,wdcl) -> - SEBwith (traverse_modexpr seb,wdcl) - in - fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s) - - (* Loading is also a traversing that decodes the embedded keys that - are inside the [lightened_library]. If the [load_proof] flag is - set, we lookup inside the table to graft the - [constr_substituted]. Otherwise, we set the [const_body] field - to [None]. - *) - let load table lightened_library = - let decode_key = function - | Undef _ | Def _ -> assert false - | OpaqueDef k -> - let k = key_of_lazy_constr k in - let body = - try table.(k) - with _ -> error "Error while retrieving an opaque body" - in - OpaqueDef (lazy_constr_from_val body) - in - traverse_library decode_key lightened_library - -end + engagement option * + nativecode_symb_array open Validate let val_deps = val_array (val_tuple ~name:"dep"[|val_dp;no_val|]) -let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|] +let val_vo = val_tuple ~name:"vo" + [|val_dp;val_module;val_deps;val_opt val_eng; no_val|] (* This function should append a certificate to the .vo file. The digest must be part of the certicate to rule out attackers @@ -180,8 +82,9 @@ let stamp_library file digest = () (* When the module is checked, digests do not need to match, but a warning is issued in case of mismatch *) -let import file (dp,mb,depends,engmt as vo) digest = +let import file (dp,mb,depends,engmt,_ as vo) table digest = Validate.apply !Flags.debug val_vo vo; + Validate.apply !Flags.debug (val_array Term.val_constr) table; Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush (); let env = !genv in check_imports msg_warning dp env depends; @@ -193,7 +96,7 @@ let import file (dp,mb,depends,engmt as vo) digest = full_add_module dp mb digest (* When the module is admitted, digests *must* match *) -let unsafe_import file (dp,mb,depends,engmt as vo) digest = +let unsafe_import file (dp,mb,depends,engmt,_ as vo) digest = if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*) let env = !genv in check_imports (errorlabstrm"unsafe_import") dp env depends; diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index 4e3c25b1ce6b..a5f014935d3f 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -19,22 +19,6 @@ type compiled_library val set_engagement : Declarations.engagement -> unit val import : - CUnix.physical_path -> compiled_library -> Digest.t -> unit + CUnix.physical_path -> compiled_library -> constr array -> Digest.t -> unit val unsafe_import : CUnix.physical_path -> compiled_library -> Digest.t -> unit - -(** Store the body of modules' opaque constants inside a table. - - This module is used during the serialization and deserialization - of vo files. -*) -module LightenLibrary : -sig - type table - type lightened_compiled_library - - (** [load table lcl] builds a compiled library from a - lightened library [lcl] by remplacing every index by its related - opaque terms inside [table]. *) - val load : table -> lightened_compiled_library -> compiled_library -end diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 3bf9e7cb551c..543dce18fa53 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -219,25 +219,19 @@ \subsection{By command line options\index{Options of the command line} \item[{\tt -dont-load-proofs}]\ - Warning: this is an unsafe mode. - Instead of loading in memory the proofs of opaque theorems, they are - treated as axioms. This results in smaller memory requirement and - faster compilation, but the behavior of the system might slightly change - (for instance during module subtyping), and some features won't be - available (for example {\tt Print Assumptions}). + In this mode, it is an error to access the body of opaque theorems + (for example via {\tt Print} or {\tt Print Assumptions}). \item[{\tt -lazy-load-proofs}]\ This is the default behavior. Proofs of opaque theorems aren't loaded immediately in memory, but only when necessary, for instance during some module subtyping or {\tt Print Assumptions}. This should be - almost as fast and efficient as {\tt -dont-load-proofs}, with none - of its drawbacks. + almost as fast and efficient as {\tt -dont-load-proofs}. \item[{\tt -force-load-proofs}]\ - Proofs of opaque theorems are loaded in memory as soon as the - corresponding {\tt Require} is done. This used to be Coq's default behavior. + Deprecated, now the same as {\tt -lazy-load-proofs}. \item[{\tt -no-hash-consing}] \mbox{} diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 90327da6c37a..3c1f6a415d07 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -18,8 +18,8 @@ open Util let body_of_constant cb = match cb.const_body with | Undef _ -> None - | Def c -> Some c - | OpaqueDef lc -> Some (force_lazy_constr lc) + | Def c -> Some (Lazyconstr.force c) + | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc) let constant_has_body cb = match cb.const_body with | Undef _ -> false @@ -84,14 +84,8 @@ let hcons_const_type = function let hcons_const_def = function | Undef inl -> Undef inl - | Def l_constr -> - let constr = force l_constr in - Def (from_val (Term.hcons_constr constr)) - | OpaqueDef lc -> - if lazy_constr_is_val lc then - let constr = force_opaque lc in - OpaqueDef (opaque_from_val (Term.hcons_constr constr)) - else OpaqueDef lc + | Def cs -> Def (from_val (Term.hcons_constr (Lazyconstr.force cs))) + | OpaqueDef lc -> OpaqueDef (Lazyconstr.hcons_lazy_constr lc) let hcons_const_body cb = { cb with diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 1616e463932b..c4d67ba52c2f 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -8,7 +8,6 @@ open Declarations open Mod_subst -open Lazyconstr (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -18,13 +17,14 @@ open Lazyconstr val subst_const_def : substitution -> constant_def -> constant_def val subst_const_body : substitution -> constant_body -> constant_body -(** Is there a actual body in const_body or const_body_opaque ? *) +(** Is there a actual body in const_body ? *) val constant_has_body : constant_body -> bool -(** Accessing const_body_opaque or const_body *) +(** Accessing const_body, forcing access to opaque proof term if needed. + Only use this function if you know what you're doing. *) -val body_of_constant : constant_body -> constr_substituted option +val body_of_constant : constant_body -> Term.constr option val is_opaque : constant_body -> bool diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml index 31cb76575ecb..21aba6348aee 100644 --- a/kernel/lazyconstr.ml +++ b/kernel/lazyconstr.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names open Term open Mod_subst @@ -20,24 +21,56 @@ let force = force subst_mps let subst_constr_subst = subst_substituted -(** Opaque proof terms are not loaded immediately, but are there - in a lazy form. Forcing this lazy may trigger some unmarshal of - the necessary structure. The ['a substituted] type isn't really great - here, so we store "manually" a substitution list, the younger one at top. +(** Opaque proof terms might be in some external tables. + The [force_opaque] function below allows to access these tables, + this might trigger the read of some extra parts of .vo files. + In the [Indirect] case, we accumulate "manually" a substitution + list, the younger one coming first. Nota: no [Direct] constructor + should end in a .vo, this is checked by coqchk. *) -type lazy_constr = constr_substituted Lazy.t * substitution list +type lazy_constr = + | Indirect of substitution list * DirPath.t * int (* lib,index *) + | Direct of constr_substituted (* opaque in section or interactive session *) -let force_lazy_constr (c,l) = - List.fold_right subst_constr_subst l (Lazy.force c) +(* TODO : this hcons function could probably be improved (for instance + hash the dir_path in the Indirect case) *) -let lazy_constr_is_val (c,_) = Lazy.lazy_is_val c +let hcons_lazy_constr = function + | Direct c -> Direct (from_val (hcons_constr (force c))) + | Indirect _ as lc -> lc -let make_lazy_constr c = (c, []) +let subst_lazy_constr sub = function + | Direct cs -> Direct (subst_constr_subst sub cs) + | Indirect (l,dp,i) -> Indirect (sub::l,dp,i) -let force_opaque lc = force (force_lazy_constr lc) +let default_get_opaque dp _ = + Errors.error + ("Cannot access an opaque term in library " ^ DirPath.to_string dp) + +let default_mk_opaque _ = None + +let get_opaque = ref default_get_opaque +let mk_opaque = ref default_mk_opaque +let set_indirect_opaque_accessor f = (get_opaque := f) +let set_indirect_opaque_creator f = (mk_opaque := f) +let reset_indirect_opaque_creator () = (mk_opaque := default_mk_opaque) -let opaque_from_val c = (Lazy.lazy_from_val (from_val c), []) +let force_lazy_constr = function + | Direct c -> c + | Indirect (l,dp,i) -> + List.fold_right subst_constr_subst l (from_val (!get_opaque dp i)) -let subst_lazy_constr sub (c,l) = (c,sub::l) +let turn_indirect lc = match lc with + | Indirect _ -> + Errors.anomaly (Pp.str "Indirecting an already indirect opaque") + | Direct c -> + (* this constr_substituted shouldn't have been substituted yet *) + assert (fst (Mod_subst.repr_substituted c) == None); + match !mk_opaque (force c) with + | None -> lc + | Some (dp,i) -> Indirect ([],dp,i) + +let force_opaque lc = force (force_lazy_constr lc) +let opaque_from_val c = Direct (from_val c) diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli index 17c9bcc76ba7..f6188f536417 100644 --- a/kernel/lazyconstr.mli +++ b/kernel/lazyconstr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names open Term open Mod_subst @@ -19,16 +20,34 @@ val force : constr_substituted -> constr val subst_constr_subst : substitution -> constr_substituted -> constr_substituted -(** Opaque proof terms are not loaded immediately, but are there - in a lazy form. Forcing this lazy may trigger some unmarshal of - the necessary structure. *) +(** Opaque proof terms might be in some external tables. The + [force_opaque] function below allows to access these tables, + this might trigger the read of some extra parts of .vo files *) type lazy_constr -val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr -val force_lazy_constr : lazy_constr -> constr_substituted -val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr -val lazy_constr_is_val : lazy_constr -> bool +(** From a [constr] to some (immediate) [lazy_constr]. *) +val opaque_from_val : constr -> lazy_constr + +(** Turn an immediate [lazy_constr] into an indirect one, thanks + to the indirect opaque creator configured below. *) +val turn_indirect : lazy_constr -> lazy_constr +(** From a [lazy_constr] back to a [constr]. This might use the + indirect opaque accessor configured below. *) val force_opaque : lazy_constr -> constr -val opaque_from_val : constr -> lazy_constr + +val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr + +val hcons_lazy_constr : lazy_constr -> lazy_constr + +(** When stored indirectly, opaque terms are indexed by their library + dirpath and an integer index. The following two functions activate + this indirect storage, by telling how to store and retrieve terms. + Default creator always returns [None], preventing the creation of + any indirect link, and default accessor always raises an error. +*) + +val set_indirect_opaque_creator : (constr -> (DirPath.t * int) option) -> unit +val set_indirect_opaque_accessor : (DirPath.t -> int -> constr) -> unit +val reset_indirect_opaque_creator : unit -> unit diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 20ca16476362..a1b820466763 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -272,6 +272,13 @@ let add_constant dir l decl senv = let cb = Term_typing.translate_recipe senv.env r in if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb in + let cb = match cb.const_body with + | OpaqueDef lc when DirPath.is_empty dir -> + (* In coqc, opaque constants outside sections will be stored + indirectly in a specific table *) + { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) } + | _ -> cb + in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with | Undef (Some lev) -> @@ -767,148 +774,6 @@ let import lib digest senv = mp, senv, lib.comp_natsymbs - (* Store the body of modules' opaque constants inside a table. - - This module is used during the serialization and deserialization - of vo files. - - By adding an indirection to the opaque constant definitions, we - gain the ability not to load them. As these constant definitions - are usually big terms, we save a deserialization time as well as - some memory space. *) -module LightenLibrary : sig - type table - type lightened_compiled_library - val save : compiled_library -> lightened_compiled_library * table - val load : load_proof:Flags.load_proofs -> table Lazy.t - -> lightened_compiled_library -> compiled_library -end = struct - - (* The table is implemented as an array of [constr_substituted]. - Keys are hence integers. To avoid changing the [compiled_library] - type, we brutally encode integers into [lazy_constr]. This isn't - pretty, but shouldn't be dangerous since the produced structure - [lightened_compiled_library] is abstract and only meant for writing - to .vo via Marshal (which doesn't care about types). - *) - type table = Lazyconstr.constr_substituted array - let key_as_lazy_constr (i:int) = (Obj.magic i : Lazyconstr.lazy_constr) - let key_of_lazy_constr (c:Lazyconstr.lazy_constr) = (Obj.magic c : int) - - (* To avoid any future misuse of the lightened library that could - interpret encoded keys as real [constr_substituted], we hide - these kind of values behind an abstract datatype. *) - type lightened_compiled_library = compiled_library - - (* Map a [compiled_library] to another one by just updating - the opaque term [t] to [on_opaque_const_body t]. *) - let traverse_library on_opaque_const_body = - let rec traverse_module mb = - match mb.mod_expr with - None -> - { mb with - mod_expr = None; - mod_type = traverse_modexpr mb.mod_type; - } - | Some impl when impl == mb.mod_type-> - let mtb = traverse_modexpr mb.mod_type in - { mb with - mod_expr = Some mtb; - mod_type = mtb; - } - | Some impl -> - { mb with - mod_expr = Option.map traverse_modexpr mb.mod_expr; - mod_type = traverse_modexpr mb.mod_type; - } - and traverse_struct struc = - let traverse_body (l,body) = (l,match body with - | SFBconst cb when Declareops.is_opaque cb -> - SFBconst {cb with const_body = on_opaque_const_body cb.const_body} - | (SFBconst _ | SFBmind _ ) as x -> - x - | SFBmodule m -> - SFBmodule (traverse_module m) - | SFBmodtype m -> - SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr})) - in - List.map traverse_body struc - - and traverse_modexpr = function - | SEBfunctor (mbid,mty,mexpr) -> - SEBfunctor (mbid, - ({mty with - typ_expr = traverse_modexpr mty.typ_expr}), - traverse_modexpr mexpr) - | SEBident mp as x -> x - | SEBstruct (struc) -> - SEBstruct (traverse_struct struc) - | SEBapply (mexpr,marg,u) -> - SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u) - | SEBwith (seb,wdcl) -> - SEBwith (traverse_modexpr seb,wdcl) - in - fun clib -> { clib with comp_mod = traverse_module clib.comp_mod } - - (* To disburden a library from opaque definitions, we simply - traverse it and add an indirection between the module body - and its reference to a [const_body]. *) - let save library = - let ((insert : constant_def -> constant_def), - (get_table : unit -> table)) = - (* We use an integer as a key inside the table. *) - let counter = ref (-1) in - - (* During the traversal, the table is implemented by a list - to get constant time insertion. *) - let opaque_definitions = ref [] in - - ((* Insert inside the table. *) - (fun def -> - let opaque_definition = match def with - | OpaqueDef lc -> Lazyconstr.force_lazy_constr lc - | _ -> assert false - in - incr counter; - opaque_definitions := opaque_definition :: !opaque_definitions; - OpaqueDef (key_as_lazy_constr !counter)), - - (* Get the final table representation. *) - (fun () -> Array.of_list (List.rev !opaque_definitions))) - in - let lightened_library = traverse_library insert library in - (lightened_library, get_table ()) - - (* Loading is also a traversing that decodes the embedded keys that - are inside the [lightened_library]. If the [load_proof] flag is - set, we lookup inside the table to graft the - [constr_substituted]. Otherwise, we set the [const_body] field - to [None]. - *) - let load ~load_proof (table : table Lazy.t) lightened_library = - let decode_key = function - | Undef _ | Def _ -> assert false - | OpaqueDef k -> - let k = key_of_lazy_constr k in - let access key = - try (Lazy.force table).(key) - with e when Errors.noncritical e -> - error "Error while retrieving an opaque body" - in - match load_proof with - | Flags.Force -> - let lc = Lazy.lazy_from_val (access k) in - OpaqueDef (Lazyconstr.make_lazy_constr lc) - | Flags.Lazy -> - let lc = lazy (access k) in - OpaqueDef (Lazyconstr.make_lazy_constr lc) - | Flags.Dont -> - Undef None - in - traverse_library decode_key lightened_library - -end - type judgment = unsafe_judgment let j_val j = j.uj_val diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1bb43a53e754..cd24bd8d0e25 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -112,17 +112,6 @@ val export : safe_environment -> DirPath.t val import : compiled_library -> Digest.t -> safe_environment -> module_path * safe_environment * Nativecode.symbol array -(** Remove the body of opaque constants *) - -module LightenLibrary : -sig - type table - type lightened_compiled_library - val save : compiled_library -> lightened_compiled_library * table - val load : load_proof:Flags.load_proofs -> table Lazy.t -> - lightened_compiled_library -> compiled_library -end - (** {6 Typing judgments } *) type judgment diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c70a3f2eb894..67d80fa500bd 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -80,26 +80,31 @@ let global_vars_set_constant_type env = function (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty +let check_declared_variables declared inferred = + let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in + let undeclared_set = Id.Set.diff (mk_set inferred) (mk_set declared) in + if not (Id.Set.is_empty undeclared_set) then + error ("The following section variables are used but not declared:\n"^ + (String.concat ", " + (List.map Id.to_string (Id.Set.elements undeclared_set)))) + let build_constant_declaration env (def,typ,cst,inline_code,ctx) = - let hyps = + let hyps = let inferred = let ids_typ = global_vars_set_constant_type env typ in let ids_def = match def with - | Undef _ -> Id.Set.empty - | Def cs -> global_vars_set env (Lazyconstr.force cs) - | OpaqueDef lc -> - global_vars_set env (Lazyconstr.force_opaque lc) in - keep_hyps env (Id.Set.union ids_typ ids_def) in - let declared = match ctx with - | None -> inferred - | Some declared -> declared in - let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in - let inferred_set, declared_set = mk_set inferred, mk_set declared in - if not (Id.Set.subset inferred_set declared_set) then - error ("The following section variable are used but not declared:\n"^ - (String.concat ", " (List.map Id.to_string - (Id.Set.elements (Id.Set.diff inferred_set declared_set))))); - declared in + | Undef _ -> Id.Set.empty + | Def cs -> global_vars_set env (Lazyconstr.force cs) + | OpaqueDef lc -> global_vars_set env (Lazyconstr.force_opaque lc) + in + keep_hyps env (Id.Set.union ids_typ ids_def) + in + match ctx with + | None -> inferred + | Some declared -> + check_declared_variables declared inferred; + declared + in let tps = Cemitcodes.from_val (compile_constant_body env def) in { const_hyps = hyps; const_body = def; diff --git a/library/assumptions.ml b/library/assumptions.ml index 2d99aca8ce69..2418f0648d82 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -239,7 +239,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = in match Declareops.body_of_constant cb with | None -> do_type (Axiom kn) - | Some body -> do_constr (Lazyconstr.force body) s acc + | Some body -> do_constr body s acc and do_memoize_kn kn = try_and_go (Axiom kn) (add_kn kn) diff --git a/library/library.ml b/library/library.ml index b7a2f81494b1..7c34a62d077e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -24,7 +24,7 @@ type compilation_unit_name = DirPath.t type library_disk = { md_name : compilation_unit_name; - md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library; + md_compiled : Safe_typing.compiled_library; md_objects : Declaremods.library_objects; md_deps : (compilation_unit_name * Digest.t) array; md_imports : compilation_unit_name array } @@ -290,42 +290,114 @@ let try_locate_qualified_library (loc,qid) = | LibNotFound -> error_lib_not_found qid (************************************************************************) -(* Internalise libraries *) +(** {6 Tables of opaque proof terms} *) -let mk_library md table digest = - let md_compiled = - Safe_typing.LightenLibrary.load ~load_proof:!Flags.load_proofs - table md.md_compiled - in { - library_name = md.md_name; - library_compiled = md_compiled; - library_objects = md.md_objects; - library_deps = md.md_deps; - library_imports = md.md_imports; - library_digest = digest - } +(** We now store opaque proof terms apart from the rest of the environment. + See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way, + we can quickly load a first half of a .vo file without these opaque + terms, and access them only when a specific command (e.g. Print or + Print Assumptions) needs it. *) + +exception Faulty + +(** Fetching a table of opaque terms at position [pos] in file [f], + expecting to find first a copy of [digest]. *) let fetch_opaque_table (f,pos,digest) = + if !Flags.load_proofs == Flags.Dont then + error "Not accessing an opaque term due to option -dont-load-proofs."; try + Pp.msg_info (Pp.str "Fetching opaque terms in " ++ str f); let ch = System.with_magic_number_check raw_intern_library f in let () = seek_in ch pos in - if not (String.equal (System.marshal_in f ch) digest) then failwith "File changed!"; - let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in + if not (String.equal (System.marshal_in f ch) digest) then raise Faulty; + let table = (System.marshal_in f ch : Term.constr array) in + (* Verification of the final digest (the one also covering the opaques) *) + let pos' = pos_in ch in + let digest' = (System.marshal_in f ch : Digest.t) in let () = close_in ch in + let ch' = open_in f in + if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty; + let () = close_in ch' in table with e when Errors.noncritical e -> error - ("The file "^f^" is inaccessible or has changed,\n" ^ - "cannot load some opaque constant bodies in it.\n") + ("The file "^f^" is inaccessible or corrupted,\n" + ^ "cannot load some opaque constant bodies in it.\n") + +(** Delayed / available tables of opaque terms *) + +type opaque_table_status = + | ToFetch of string * int * Digest.t + | Fetched of Term.constr array + +let opaque_tables = ref (LibraryMap.empty : opaque_table_status LibraryMap.t) + +let add_opaque_table dp st = + opaque_tables := LibraryMap.add dp st !opaque_tables + +let access_opaque_table dp i = + let t = match LibraryMap.find dp !opaque_tables with + | Fetched t -> t + | ToFetch (f,pos,digest) -> + let t = fetch_opaque_table (f,pos,digest) in + add_opaque_table dp (Fetched t); + t + in + assert (i < Array.length t); t.(i) + +(** Table of opaque terms from the library currently being compiled *) + +module OpaqueTables = struct + + let a_constr = Term.mkRel 1 + + let local_table = ref (Array.make 100 a_constr) + let local_index = ref 0 + + let get dp i = + if DirPath.equal dp (Lib.library_dp ()) + then (!local_table).(i) + else access_opaque_table dp i + + let store c = + let n = !local_index in + incr local_index; + if n = Array.length !local_table then begin + let t = Array.make (2*n) a_constr in + Array.blit !local_table 0 t 0 n; + local_table := t + end; + (!local_table).(n) <- c; + Some (Lib.library_dp (), n) + + let dump () = Array.sub !local_table 0 !local_index + +end + +let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get + +(************************************************************************) +(* Internalise libraries *) + +let mk_library md digest = + { + library_name = md.md_name; + library_compiled = md.md_compiled; + library_objects = md.md_objects; + library_deps = md.md_deps; + library_imports = md.md_imports; + library_digest = digest + } let intern_from_file f = let ch = System.with_magic_number_check raw_intern_library f in let lmd = System.marshal_in f ch in let pos = pos_in ch in let digest = System.marshal_in f ch in - let table = lazy (fetch_opaque_table (f,pos,digest)) in register_library_filename lmd.md_name f; - let library = mk_library lmd table digest in + add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); + let library = mk_library lmd digest in close_in ch; library @@ -528,6 +600,7 @@ let start_library f = let id = Id.of_string (Filename.basename f) in check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in + Lazyconstr.set_indirect_opaque_creator OpaqueTables.store; Declaremods.start_library ldir; ldir,longf @@ -546,11 +619,21 @@ let error_recursively_dependent_library dir = strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") +(* We now use two different digests in a .vo file. The first one + only covers half of the file, without the opaque table. It is + used for identifying this version of this library : this digest + is the one leading to "inconsistent assumptions" messages. + The other digest comes at the very end, and covers everything + before it. This one is used for integrity check of the whole + file when loading the opaque table. *) + (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) + let save_library_to dir f = + Lazyconstr.reset_indirect_opaque_creator (); let cenv, seg, ast = Declaremods.end_library dir in - let cenv, table = Safe_typing.LightenLibrary.save cenv in + let table = OpaqueTables.dump () in let md = { md_name = dir; md_compiled = cenv; @@ -563,14 +646,12 @@ let save_library_to dir f = try System.marshal_out ch md; flush ch; - (* The loading of the opaque definitions table is optional whereas - the digest is loaded all the time. As a consequence, the digest - must be serialized before the table (if we want to keep the - current simple layout of .vo files). This also entails that the - digest does not take opaque terms into account anymore. *) let di = Digest.file f' in System.marshal_out ch di; System.marshal_out ch table; + flush ch; + let di = Digest.file f' in + System.marshal_out ch di; close_out ch; if not !Flags.no_native_compiler then begin let lp = Loadpath.get_load_paths () in diff --git a/library/states.ml b/library/states.ml index 9d15dfc6c7bc..eb597670f9d7 100644 --- a/library/states.ml +++ b/library/states.ml @@ -23,8 +23,6 @@ let (extern_state,intern_state) = extern_intern Coq_config.state_magic_number in (fun s -> let s = ensure_suffix s in - if !Flags.load_proofs <> Flags.Force then - Errors.error "Write State only works with option -force-load-proofs"; raw_extern s (freeze())), (fun s -> let s = ensure_suffix s in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ef4dca26de09..74d7194380b1 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -940,8 +940,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Global.lookup_constant (destConst f) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in - let f_body = - Lazyconstr.force (Option.get (body_of_constant f_def)) + let f_body = Option.get (body_of_constant f_def) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in @@ -1058,8 +1057,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let get_body const = match body_of_constant (Global.lookup_constant const) with - | Some b -> - let body = Lazyconstr.force b in + | Some body -> Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) (Global.env ()) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 09637d273f8f..50a4703f6f17 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -403,8 +403,7 @@ let get_funs_constant mp dp = function const -> let find_constant_body const = match body_of_constant (Global.lookup_constant const) with - | Some b -> - let body = Lazyconstr.force b in + | Some body -> let body = Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) (Global.env ()) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f0f76860a3d9..609e2916dadf 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -766,9 +766,8 @@ let make_graph (f_ref:global_reference) = Dumpglob.pause (); (match body_of_constant c_body with | None -> error "Cannot build a graph over an axiom !" - | Some b -> + | Some body -> let env = Global.env () in - let body = Lazyconstr.force b in let extern_body,extern_type = with_full_print (fun () -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 4d1cefe5a531..1e8f4afdf4ea 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -116,7 +116,7 @@ let def_of_const t = match (Term.kind_of_term t) with Term.Const sp -> (try (match Declareops.body_of_constant (Global.lookup_constant sp) with - | Some c -> Lazyconstr.force c + | Some c -> c | _ -> assert false) with Not_found -> assert false) |_ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 597233d01b9a..a8ffd51ef430 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -69,7 +69,7 @@ let def_of_const t = match (kind_of_term t) with Const sp -> (try (match body_of_constant (Global.lookup_constant sp) with - | Some c -> Lazyconstr.force c + | Some c -> c | _ -> raise Not_found) with Not_found -> anomaly (str "Cannot find definition of constant " ++ diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index a34d4a682a30..ddc4725c358d 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -229,8 +229,7 @@ let mk_constant_obj id bo ty variables hyps = Acic.Constant (Names.Id.to_string id,None,ty,params) | Some c -> Acic.Constant - (Names.Id.to_string id, Some (Unshare.unshare (Lazyconstr.force c)), - ty,params) + (Names.Id.to_string id, Some (Unshare.unshare c), ty,params) ;; let mk_inductive_obj sp mib packs variables nparams hyps finite = diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 4d7501ff9fa1..ee6a5e18dac5 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -400,7 +400,7 @@ let gallina_print_section_variable id = with_line_skip (print_name_infos (VarRef id)) let print_body = function - | Some lc -> pr_lconstr (Lazyconstr.force lc) + | Some c -> pr_lconstr c | None -> (str"") let print_typed_body (val_0,typ) = diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 386567deea38..1f0ccf0fccb3 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -218,8 +218,7 @@ let parse_args arglist = | "-batch" :: rem -> set_batch_mode (); parse rem | "-boot" :: rem -> boot := true; no_load_rc (); parse rem | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem - | "-outputstate" :: s :: rem -> - Flags.load_proofs := Flags.Force; set_outputstate s; parse rem + | "-outputstate" :: s :: rem -> set_outputstate s; parse rem | "-outputstate" :: [] -> usage () | ("-noinit"|"-nois") :: rem -> load_init := false; parse rem diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index e1f17b57113a..3779815e97f6 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -41,7 +41,7 @@ let retrieve_first_recthm = function (pi2 (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - (Option.map Lazyconstr.force (body_of_constant cb), is_opaque cb) + (body_of_constant cb, is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function