summaryrefslogtreecommitdiff
path: root/checker/safe_typing.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /checker/safe_typing.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'checker/safe_typing.ml')
-rw-r--r--checker/safe_typing.ml137
1 files changed, 137 insertions, 0 deletions
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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
+
+open Pp
+open Util
+open Names
+open Declarations
+open Environ
+open Mod_checking
+
+(************************************************************************)
+(*
+ * Global environment
+ *)
+
+let genv = ref empty_env
+let reset () = genv := empty_env
+let get_env () = !genv
+
+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 env = !genv in
+ let mp = MPfile dp in
+ let env = add_module_constraints env mb in
+ let env = Modops.add_module mp mb env in
+ genv := add_digest env dp digest
+
+(* Check that the engagement expected by a library matches the initial one *)
+let check_engagement env c =
+ match engagement env, c with
+ | Some ImpredicativeSet, Some ImpredicativeSet -> ()
+ | _, 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