diff options
Diffstat (limited to 'checker/safe_typing.ml')
| -rw-r--r-- | checker/safe_typing.ml | 156 |
1 files changed, 21 insertions, 135 deletions
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index f7abd4dc..35f7f14b 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -1,15 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp +open Errors open Util +open Cic open Names -open Declarations open Environ (************************************************************************) @@ -24,9 +25,10 @@ let set_engagement c = genv := set_engagement c !genv (* full_add_module adds module with universes and constraints *) -let full_add_module dp mb digest = +let full_add_module dp mb univs digest = let env = !genv in let env = add_constraints mb.mod_constraints env in + let env = add_constraints univs env in let env = Modops.add_module mb env in genv := add_digest env dp digest @@ -42,9 +44,9 @@ let check_engagement env c = let report_clash f caller dir = let msg = - str "compiled library " ++ str(string_of_dirpath caller) ++ + str "compiled library " ++ str(DirPath.to_string caller) ++ spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ - str(string_of_dirpath dir) ++ fnl() in + str(DirPath.to_string dir) ++ fnl() in f msg @@ -54,121 +56,9 @@ let check_imports f caller env needed = let actual_stamp = lookup_digest env dp in if stamp <> actual_stamp then report_clash f caller dp with Not_found -> - error ("Reference to unknown module " ^ (string_of_dirpath dp)) + error ("Reference to unknown module " ^ (DirPath.to_string dp)) in - List.iter check needed - - -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 ~name:"dep"[|val_dp;no_val|]) -let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|] + Array.iter check needed (* This function should append a certificate to the .vo file. The digest must be part of the certicate to rule out attackers @@ -179,24 +69,20 @@ 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 = - Validate.apply !Flags.debug val_vo vo; - Flags.if_verbose msgnl (str "*** vo structure validated ***"); +let import file clib univs digest = let env = !genv in - check_imports msg_warning dp env depends; - check_engagement env engmt; - Mod_checking.check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb; + check_imports msg_warning clib.comp_name env clib.comp_deps; + check_engagement env clib.comp_enga; + let mb = clib.comp_mod in + Mod_checking.check_module + (add_constraints univs + (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 + full_add_module clib.comp_name mb univs digest (* When the module is admitted, digests *must* match *) -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 unsafe_import file clib univs digest = let env = !genv in - check_imports (errorlabstrm"unsafe_import") dp env depends; - check_engagement env engmt; - (* We drop proofs once checked *) -(* let mb = lighten_module mb in*) - full_add_module dp mb digest + check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; + check_engagement env clib.comp_enga; + full_add_module clib.comp_name clib.comp_mod univs digest |