diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-02 22:08:44 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-02 22:08:44 +0000 |
commit | f5ab2e37b0609d8edb8d65dfae49741442a90657 (patch) | |
tree | 72bb704f147a824b743566b447c4e98685ab2db6 /checker | |
parent | 5635c35ea4ec172fd81147effed4f33e2f581aaa (diff) |
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
Diffstat (limited to 'checker')
-rw-r--r-- | checker/check.ml | 37 | ||||
-rw-r--r-- | checker/declarations.ml | 36 | ||||
-rw-r--r-- | checker/declarations.mli | 13 | ||||
-rw-r--r-- | checker/mod_checking.ml | 2 | ||||
-rw-r--r-- | checker/safe_typing.ml | 113 | ||||
-rw-r--r-- | checker/safe_typing.mli | 18 |
6 files changed, 66 insertions, 153 deletions
diff --git a/checker/check.ml b/checker/check.ml index eb4016f5f..1b9fd0701 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 af8b1f217..cfaa2f5f7 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 80c895bbe..cc3123ca7 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 bc4ea7c69..ebe44997d 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 5cbcc00f5..492f5bc20 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 4e3c25b1c..a5f014935 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 |