From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- checker/safe_typing.ml | 153 ++++++++++++++++++++++++++++++++++--------------- 1 file changed, 107 insertions(+), 46 deletions(-) (limited to 'checker/safe_typing.ml') diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index a669c5e8..bc067dc5 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -1,19 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* SFBconst {x with const_body=None} - | (SFBconst _ | SFBmind _ ) as x -> x - | SFBmodule m -> SFBmodule (lighten_module m) - | SFBmodtype m -> SFBmodtype - ({m with - typ_expr = lighten_modexpr m.typ_expr})) - in - List.map lighten_body struc - -and lighten_modexpr = function - | SEBfunctor (mbid,mty,mexpr) -> - SEBfunctor (mbid, - ({mty with - typ_expr = lighten_modexpr mty.typ_expr}), - lighten_modexpr mexpr) - | SEBident mp as x -> x - | SEBstruct ( struc) -> - SEBstruct ( lighten_struct struc) - | SEBapply (mexpr,marg,u) -> - SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) - | SEBwith (seb,wdcl) -> - SEBwith (lighten_modexpr seb,wdcl) - -let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s) - - type compiled_library = dir_path * module_body * (dir_path * Digest.t) list * 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 + open Validate -let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|]) -let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|] +let val_deps = val_list (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|] (* This function should append a certificate to the .vo file. The digest must be part of the certicate to rule out attackers @@ -124,15 +185,15 @@ let import file (dp,mb,depends,engmt as vo) digest = let env = !genv in check_imports msg_warning dp env depends; check_engagement env engmt; - check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb; + Mod_checking.check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb; stamp_library file digest; (* We drop proofs once checked *) (* let mb = lighten_module mb in*) full_add_module dp mb digest (* When the module is admitted, digests *must* match *) -let unsafe_import file (dp,mb,depends,engmt) digest = -(* if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*) +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; check_engagement env engmt; -- cgit v1.2.3