From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- checker/safe_typing.ml | 137 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 checker/safe_typing.ml (limited to 'checker/safe_typing.ml') diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml new file mode 100644 index 00000000..4b156e7e --- /dev/null +++ b/checker/safe_typing.ml @@ -0,0 +1,137 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* () + | _, None -> () + | _, Some ImpredicativeSet -> + error "Needs option -impredicative-set" + +(* Libraries = Compiled modules *) + +let report_clash f caller dir = + let msg = + str "compiled library " ++ str(string_of_dirpath caller) ++ + spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ + str(string_of_dirpath dir) ++ fnl() in + f msg + + +let check_imports f caller env needed = + let check (dp,stamp) = + try + 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)) + in + List.iter check needed + + + +(* Remove the body of opaque constants in modules *) +(* also remove mod_expr ? *) +let rec lighten_module mb = + { mb with + mod_expr = Option.map lighten_modexpr mb.mod_expr; + mod_type = Option.map lighten_modexpr mb.mod_type } + +and lighten_struct struc = + let lighten_body (l,body) = (l,match body with + | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None} + | (SFBconst _ | SFBmind _ | SFBalias _) 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 (msid, struc) -> + SEBstruct (msid, 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 + +(* This function should append a certificate to the .vo file. + The digest must be part of the certicate to rule out attackers + that could change the .vo file between the time it was read and + the time the stamp is written. + For the moment, .vo are not signed. *) +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.val_vo (Obj.repr vo); + Flags.if_verbose msgnl (str "*** vo structure validated ***"); + let env = !genv in + check_imports msg_warning dp env depends; + check_engagement env engmt; + check_module env 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 = + 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 -- cgit v1.2.3