Checker: vo validation is now done in check.ml (and always)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16402 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 51 insertions, 34 deletions

diff --git a/checker/check.ml b/checker/check.ml
index db2c537aa..267fdb886 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -34,30 +34,17 @@ let pr_path sp =
       [] -> str sp.basename
     | sl -> pr_dirlist sl ++ str"." ++ str sp.basename
 
-type library_objects
-
-type compilation_unit_name = DirPath.t
-
-type library_disk = {
-  md_name : compilation_unit_name;
-  md_compiled : Cic.compiled_library;
-  md_objects : library_objects;
-  md_deps : (compilation_unit_name * Digest.t) array;
-  md_imports : compilation_unit_name array }
-
 (************************************************************************)
-(*s Modules on disk contain the following informations (after the magic
-    number, and before the digest). *)
 
 (*s Modules loaded in memory contain the following informations. They are
     kept in the global table [libraries_table]. *)
 
 type library_t = {
-  library_name : compilation_unit_name;
+  library_name : Cic.compilation_unit_name;
   library_filename : CUnix.physical_path;
   library_compiled : Cic.compiled_library;
-  library_opaques : Cic.constr array;
-  library_deps : (compilation_unit_name * Digest.t) array;
+  library_opaques : Cic.opaque_table;
+  library_deps : Cic.library_deps;
   library_digest : Digest.t }
 
 module LibraryOrdered =
@@ -119,7 +106,7 @@ let check_one_lib admit (dir,m) =
   else
     (Flags.if_verbose ppnl
       (str "Checking library: " ++ pr_dirpath dir);
-      Safe_typing.import file md m.library_opaques dig);
+      Safe_typing.import file md dig);
   Flags.if_verbose pp (fnl());
   pp_flush ();
   register_loaded_library m
@@ -291,6 +278,8 @@ let with_magic_number_check f a =
 (************************************************************************)
 (* Internalise libraries *)
 
+open Cic
+
 let mk_library md f table digest = {
   library_name = md.md_name;
   library_filename = f;
@@ -312,9 +301,9 @@ let intern_from_file (dir, f) =
   let (md,table,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
-      let (md:library_disk) = System.marshal_in f ch in
+      let (md:Cic.library_disk) = System.marshal_in f ch in
       let (digest:Digest.t) = System.marshal_in f ch in
-      let (table:Cic.constr array) = System.marshal_in f ch in
+      let (table:Cic.opaque_table) = 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
@@ -326,7 +315,10 @@ let intern_from_file (dir, f) =
       if dir <> md.md_name then
         errorlabstrm "intern_from_file"
           (name_clash_message dir md.md_name f);
-      Flags.if_verbose ppnl (str" done]");
+      (* Verification of the unmarshalled values *)
+      Validate.validate !Flags.debug Values.v_lib md;
+      Validate.validate !Flags.debug Values.v_opaques table;
+      Flags.if_verbose ppnl (str" done]"); pp_flush ();
       md,table,digest
     with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
diff --git a/checker/check.mllib b/checker/check.mllib
index e327e275e..2671788b4 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -39,9 +39,9 @@ Typeops
 Indtypes
 Subtyping
 Mod_checking
+Safe_typing
 Values
 Validate
-Safe_typing
 Check
 Check_stat
 Checker
diff --git a/checker/cic.mli b/checker/cic.mli
index b125e3c72..8682254e9 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -331,12 +331,40 @@ and module_type_body =
 
 type nativecode_symb_array
 
-type library_info = DirPath.t * Digest.t
+type compilation_unit_name = DirPath.t
+
+type library_info = compilation_unit_name * Digest.t
+
+type library_deps = library_info array
 
 type compiled_library = {
-  comp_name : DirPath.t;
+  comp_name : compilation_unit_name;
   comp_mod : module_body;
-  comp_deps : library_info array;
+  comp_deps : library_deps;
   comp_enga : engagement option;
   comp_natsymbs : nativecode_symb_array
 }
+
+
+(*************************************************************************)
+(** {4 From library.ml} *)
+
+type library_objects
+
+type library_disk = {
+  md_name : compilation_unit_name;
+  md_compiled : compiled_library;
+  md_objects : library_objects;
+  md_deps : library_deps;
+  md_imports : compilation_unit_name array }
+
+type opaque_table = constr array
+
+(** A .vo file is currently made of :
+
+    1) a magic number
+    2) a marshalled [library_disk] structure
+    3) a marshalled [Digest.t] string
+    4) a marshalled [opaque_table]
+    5) a marshalled [Digest.t] string
+*)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 7c96fda5b..b3060c153 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -60,8 +60,6 @@ let check_imports f caller env needed =
   in
   Array.iter check needed
 
-open Validate
-
 (* 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
@@ -71,10 +69,7 @@ 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 clib table digest =
-  Validate.validate !Flags.debug Values.v_compiled_lib clib;
-  Validate.validate !Flags.debug (Values.Array Values.v_constr) table;
-  Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush ();
+let import file clib digest =
   let env = !genv in
   check_imports msg_warning clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index cef93ad05..9f9afe922 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -16,6 +16,6 @@ val get_env : unit -> env
 
 val set_engagement : engagement -> unit
 val import         :
-  CUnix.physical_path -> compiled_library -> constr array -> Digest.t -> unit
+  CUnix.physical_path -> compiled_library -> Digest.t -> unit
 val unsafe_import  :
   CUnix.physical_path -> compiled_library -> Digest.t -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 386f85365..227f18ca2 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -267,14 +267,16 @@ let v_deps = Array (v_tuple "dep" [|v_dp;String|])
 let v_compiled_lib =
   v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
 
-(** Library objects (unused by the checker) *)
+(** Library objects *)
 
 let v_obj = Tuple ("Dyn.t",[|String;Any|])
 let v_libobj = Tuple ("libobj", [|v_id;v_obj|])
 let v_libobjs = List v_libobj
 let v_libraryobjs = Tuple ("library_objects",[|v_mp;v_libobjs;v_libobjs|])
 
-(** Main structure of a vo (opaque tables left aside) *)
+(** Main structures of a vo *)
 
 let v_lib =
-  Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps; List v_dp|])
+  Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
+
+let v_opaques = Array v_constr