doc of coqchk + improved module cache and computation of module sets

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

3 files changed, 135 insertions, 168 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 7169d709f..f8844975a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -70,6 +70,7 @@ module LibraryOrdered =
         (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
   end
 
+module LibrarySet = Set.Make(LibraryOrdered)
 module LibraryMap = Map.Make(LibraryOrdered)
 
 (* This is a map from names to loaded libraries *)
@@ -100,7 +101,7 @@ let check_one_lib admit (dir,m) =
   (* Look up if the library is to be admitted correct. We could
      also check if it carries a validation certificate (yet to
      be implemented). *)
-  if LibraryMap.mem dir admit then
+  if LibrarySet.mem dir admit then
     (Flags.if_verbose msgnl
       (str "Admitting library: " ++ pr_dirpath dir);
       Safe_typing.unsafe_import file md dig)
@@ -200,7 +201,6 @@ let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
 
 exception LibUnmappedDir
 exception LibNotFound
-type library_location = LibLoaded | LibInPath
 
 let locate_absolute_library dir =
   (* Search in loadpath *)
@@ -234,9 +234,9 @@ let locate_qualified_library qid =
       extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
     (* Look if loaded *)
     try 
-      (LibLoaded, dir, library_full_filename dir)      
+      (dir, library_full_filename dir)      
     with Not_found ->
-      (LibInPath, dir, file)
+      (dir, file)
   with Not_found -> raise LibNotFound
 
 let explain_locate_library_error qid = function
@@ -258,8 +258,7 @@ let try_locate_absolute_library dir =
 
 let try_locate_qualified_library qid =
   try
-    let (_,dir,f) = locate_qualified_library qid in
-    dir,f
+    locate_qualified_library qid
   with e -> 
     explain_locate_library_error qid e
 
@@ -291,7 +290,15 @@ let mk_library md f digest = {
   library_deps = md.md_deps;
   library_digest = digest }
 
-let intern_from_file f =
+let name_clash_message dir mdir f =
+  str ("The file " ^ f ^ " contains library") ++ spc () ++
+  pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
+  pr_dirpath dir
+
+(* Dependency graph *)
+let depgraph = ref LibraryMap.empty
+
+let intern_from_file (dir, f) =
   Flags.if_verbose msg (str"[intern "++str f++str" ...");
   let (md,digest) = 
     try
@@ -299,60 +306,67 @@ let intern_from_file f =
       let (md:library_disk) = System.marshal_in ch in
       let digest = System.marshal_in ch in
       close_in ch;
+      if dir <> md.md_name then
+        errorlabstrm "load_physical_library"
+          (name_clash_message dir md.md_name f);
       Flags.if_verbose msgnl(str" done]");
       md,digest
     with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
+  depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; 
   mk_library md f digest
 
-
-let name_clash_message dir mdir f =
-  str ("The file " ^ f ^ " contains library") ++ spc () ++
-  pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
-  pr_dirpath dir
-
-let rec library_dep dir needed =
-  try let _ = find_library dir in needed
+let get_deps (dir, f) =
+  try LibraryMap.find dir !depgraph
   with Not_found ->
-  try let _ = LibraryMap.find dir needed in needed
-  with Not_found ->
-    let (_,f) = try_locate_absolute_library dir in
-    let m = intern_from_file f in
-    let deps = m.library_deps in
-    if dir <> m.library_name then
-      errorlabstrm "load_physical_library"
-        (name_clash_message dir m.library_name f);
-    LibraryMap.add dir f
-      (List.fold_right (fun (d,_) n -> library_dep d n) deps needed)
+    let _ = intern_from_file (dir,f) in
+    LibraryMap.find dir !depgraph
 
+(* Read a compiled library and all dependencies, in reverse order.
+   Do not include files that are already in the context. *)
 let rec intern_library (dir, f) needed =
   (* Look if in the current logical environment *)
   try let _ = find_library dir in needed
   with Not_found ->
   (* Look if already listed and consequently its dependencies too *)
-  try let _ = List.assoc dir needed in needed
-  with Not_found ->
-  (* [dir] is an absolute name which matches [f] which must be in loadpath *)
-  let m = intern_from_file f in
-  if dir <> m.library_name then
-    errorlabstrm "load_physical_library"
-      (name_clash_message dir m.library_name f);
-  (dir,m)::List.fold_right intern_mandatory_library m.library_deps needed
+  if List.mem_assoc dir needed then needed
+  else
+    (* [dir] is an absolute name which matches [f] which must be in loadpath *)
+    let m = intern_from_file (dir,f) in
+    (dir,m)::List.fold_right intern_mandatory_library m.library_deps needed
 
 (* digest error with checked modules could be a warning *)
 and intern_mandatory_library (dir,_) needed =
   intern_library (try_locate_absolute_library dir) needed
 
+(* Compute the reflexive transitive dependency closure *)
+let rec fold_deps ff (dir,f) s =
+  if  LibrarySet.mem dir s then s
+  else
+    let deps = get_deps (dir,f) in
+    let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in
+    ff dir (List.fold_right (fold_deps ff) deps s)
+
+and fold_deps_list  ff modl needed =
+  List.fold_right (fold_deps ff) modl needed
+
 let recheck_library ~norec ~admit ~check =
-  let nrl = List.map (fun q -> fst(try_locate_qualified_library q)) norec in
-  let al =  List.map (fun q -> fst(try_locate_qualified_library q)) admit in
-  let admit = List.fold_right library_dep (nrl@al) LibraryMap.empty in
-  let admit = List.fold_right LibraryMap.remove nrl admit in
-  let modl = List.map try_locate_qualified_library (norec@check) in
-  let needed = List.rev (List.fold_right intern_library modl []) in
+  let ml = List.map try_locate_qualified_library check in
+  let nrl = List.map try_locate_qualified_library norec in
+  let al =  List.map try_locate_qualified_library admit in
+  let needed = List.rev (List.fold_right intern_library (ml@nrl) []) in
+  (* first compute the closure of norec, remove closure of check,
+     add closure of admit, and finally remove norec and check *)
+  let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in
+  let nochk = fold_deps_list LibrarySet.remove ml nochk in
+  let nochk = fold_deps_list LibrarySet.add al nochk in
+  (* explicitely required modules cannot be skipped... *)
+  let nochk =
+    List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
+  (* *)
   Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
-  List.iter (check_one_lib admit) needed;
+  List.iter (check_one_lib nochk) needed;
   Flags.if_verbose msgnl(str"Modules were successfully checked")
 
 open Printf
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 4bed9796a..4b156e7ec 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -15,125 +15,6 @@ open Declarations
 open Environ
 open Mod_checking
 
-(*
-let type_modpath env mp = 
-  strengthen env (lookup_module mp env).mod_type mp
-
-let rec check_spec_body env mp lab = function
-  | SPBconst cb ->
-      let kn = mp, empty_dirpath, lab in
-      check_constant_declaration env kn cb
-  | SPBmind mib ->
-      let kn = mp, empty_dirpath, lab in
-      Indtypes.check_inductive env kn mib
-  | SPBmodule msb ->
-      check_mod_spec env msb;
-      Modops.add_module (MPdot(mp,lab)) (module_body_of_type msb.msb_modtype)
-        (add_modtype_constraints env msb.msb_modtype)
-  | SPBmodtype mty ->
-      let kn = mp, empty_dirpath, lab in
-      check_modtype env mty;
-      add_modtype kn mty (add_modtype_constraints env mty)
-
-and check_mod_spec env msb =
-  let env' = add_constraints msb.msb_constraints env in
-  check_modtype env' msb.msb_modtype;
-
-(*  Subtyping.check_equal env' msb.msb_modtype (MTBident *)
-  (* TODO: check equiv *)
-  env'
-
-(* !!!: modtype needs mp (the name it will be given) because
-   submodule should be added without reference to self *)
-and check_modtype env = function
-  | MTBident kn ->
-      (try let _ = lookup_modtype kn env in ()
-      with Not_found -> failwith ("unbound module type "(*^string_of_kn kn*)))
-  | MTBfunsig (mbid,marg,mbody) ->
-      check_modtype env marg;
-      let env' = 
-	add_module (MPbound mbid) (module_body_of_type marg)
-          (add_modtype_constraints env marg) in
-      check_modtype env' mbody
-  | MTBsig (msid,sign) ->
-      let _ =
-        List.fold_left (fun env (lab,mb) ->
-          check_spec_body env (MPself msid) lab mb) env sign in
-      ()
-
-
-let elem_spec_of_body (lab,e) =
-  lab,
-  match e with
-      SEBconst cb -> SPBconst cb
-    | SEBmind mind -> SPBmind mind
-    | SEBmodule msb -> SPBmodule (module_spec_of_body msb)
-    | SEBmodtype mtb -> SPBmodtype mtb
-
-let rec check_module env mb =
-  let env' = add_module_constraints env mb in
-  (* mod_type *)
-  check_modtype env' mb.mod_type;
-  (* mod_expr *)
-  let msig =
-    match mb.mod_expr with
-        Some mex ->
-          let msig = infer_mod_expr env' mex in
-          Subtyping.check_subtypes env' msig mb.mod_type;
-          msig
-      | None -> mb.mod_type in
-  (* mod_user_type *)
-  (match mb.mod_user_type with
-      Some usig -> Subtyping.check_subtypes env' msig usig
-    | None -> ());
-  (* mod_equiv *)
-  (match mb.mod_equiv with
-      Some mid ->
-        if mb.mod_expr <> Some(MEBident mid) then
-          failwith "incorrect module alias"
-    | None -> ());
-
-and infer_mod_expr env = function
-    MEBident mp -> type_modpath env mp
-  | MEBstruct(msid,msb) ->
-      let mp = MPself msid in
-      let _ =
-        List.fold_left (fun env (lab,mb) ->
-          struct_elem_body env mp lab mb) env msb in
-      MTBsig(msid,List.map elem_spec_of_body msb)
-  | MEBfunctor (arg_id, arg, body) ->
-      check_modtype env arg;
-      let env' = add_module (MPbound arg_id) (module_body_of_type arg) env in
-      let body_ty = infer_mod_expr env' body in
-      MTBfunsig (arg_id, arg, body_ty)
-  | MEBapply (fexpr,MEBident mp,_) ->
-      let ftb = infer_mod_expr env fexpr in
-      let ftb = scrape_modtype env ftb in
-      let farg_id, farg_b, fbody_b = destr_functor ftb in
-      let mtb = type_modpath env mp in
-      Subtyping.check_subtypes env mtb farg_b;
-      subst_modtype (map_mbid farg_id mp) fbody_b
-  | MEBapply _ ->
-      failwith "functor argument must be a module variable"
-
-and struct_elem_body env mp lab = function
-  | SEBconst cb ->
-      let kn = mp, empty_dirpath, lab in
-      check_constant_declaration env kn cb
-  | SEBmind mib ->
-      let kn = mp, empty_dirpath, lab in
-      Indtypes.check_inductive env kn mib
-  | SEBmodule msb ->
-      check_module env msb;
-(*msgnl(str"MODULE OK: "++prkn(make_kn mp empty_dirpath lab)++fnl());*)
-      Modops.add_module (MPdot(mp,lab)) msb 
-        (add_module_constraints env msb)
-  | SEBmodtype mty ->
-      check_modtype env mty;
-      add_modtype (mp, empty_dirpath, lab) mty
-        (add_modtype_constraints env mty)
-*)
-
 (************************************************************************)
 (*
  * Global environment
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 845ef7889..f74ace29f 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -2,12 +2,13 @@
 \ttindex{coqtop}
 \ttindex{coqc}}
 
-There are two \Coq~commands: 
+There are three \Coq~commands: 
 \begin{itemize}
 \item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ; 
 \item {\tt coqc} : The \Coq\ compiler (batch compilation).
+\item {\tt coqchk} : The \Coq\ checker (validation of compiled libraries)
 \end{itemize}
-The options are (basically) the same for the two commands, and
+The options are (basically) the same for the first two commands, and
 roughly described below. You can also look at the \verb!man! pages of
 \verb!coqtop! and \verb!coqc! for more details.
 
@@ -74,7 +75,7 @@ option \verb:-q:.
 
 There are three environment variables used by the \Coq\ system.
 \verb:$COQBIN: for the directory where the binaries are,
-\verb:$COQLIB: for the directory whrer the standard library is, and 
+\verb:$COQLIB: for the directory where the standard library is, and 
 \verb:$COQTOP: for the directory of the sources. The latter is useful
 only for developers that are writing their own tactics and are using
 \texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or
@@ -267,13 +268,84 @@ The following command-line options are recognized by the commands {\tt
 
 \end{description}
 
-% {\tt coqtop} has an additional option:
 
-% \begin{description}
-% \item[{\tt -searchisos}]\ \\
-%   Launch the {\sf Coq\_SearchIsos} toplevel
-%   (see Section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
-% \end{description}
+\section{Compiled libraries checker ({\tt coqchk})}
+
+The {\tt coqchk} command takes a list of library paths as argument.
+The corresponding compiled libraries (.vo files) are searched in the
+path, recursively processing the libraries they depend on. The content
+of all these libraries is then type-checked. The effect of {\tt
+  coqchk} is only to return with normal exit code in case of success,
+and with positive exit code if an error has been found. Error messages
+are not deemed to help the user understand what is wrong. In the
+current version, it does not modify the compiled libraries to mark
+them as succesfully checked.
+
+Note that non-logical information is not checked. By logical
+information, we mean the type and optional body associated to names.
+It excludes for instance anything related to the concrete syntax of
+objects (customized syntax rules, association between short and long
+names), implicit arguments, etc.
+
+This tool can be used for several purposes. One is to check that a
+compiled library provided by a third-party has not been forged and
+that loading it cannot introduce inconsistencies.\footnote{Ill-formed
+  non-logical information might for instance bind {\tt
+    Coq.Init.Logic.True} to short name {\tt False}, so apprently {\tt
+    False} is inhabited, but using fully qualified names, {\tt
+    Coq.Init.Logic.False} will always refer to the absurd proposition,
+  what we guarantee is that there is no proof of this latter
+  constant.}
+Another point is to get an even higher level of security. Since {\tt
+  coqtop} can be extended with custom tactics, possibly ill-typed
+code, it cannot be guaranteed that the produced compiled libraries are
+correct. {\tt coqchk} is a standalone verifier, and thus it cannot be
+tainted by such malicious code.
+
+Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
+{\tt -impredicative-set} are supported by {\tt coqchk} and have the
+same meaning as for {\tt coqtop}. Extra options are:
+\begin{description}
+\item[{\tt -norec} $module$]\ 
+
+  Check $module$ but do not force check of its dependencies.
+\item[{\tt -admit} $module$] \
+
+  Do not check $module$ and any of its dependencies, unless
+  explicitely required.
+\item[{\tt -o}]\ 
+
+  At exit, print a summary about the context. List the names of all
+  assumptions and variables (constants without body).
+\item[{\tt -silent}]\ 
+
+  Do not write progress information in standard output.
+\end{description}
+
+Environment variable \verb:$COQLIB: can be set to override the
+location of the standard library.
+
+The algorithm for deciding which modules are checked or admitted is
+the following: assuming that {\tt coqchk} is called with argument $M$,
+option {\tt -norec} $N$, and {\tt -admit} $A$. Let us write
+$\overline{S}$ the set of reflexive transitive dependencies of set
+$S$. Then:
+\begin{itemize}
+\item Modules $C=\overline{M}\backslash\overline{A}\cup M\cup N$ are
+  loaded and type-checked before being added to the context.
+\item And $\overline{M}\cup\overline{N}\backslash C$ is the set of
+  modules that are loaded and added to the context without
+  type-checking. Basic integrity checks (checksums) are nonetheless
+  performed.
+\end{itemize}
+
+As a rule of thumb, the {\tt -admit} can be used to tell that some
+libraries have already been checked. So {\tt coqchk A B} can be split
+in {\tt coqchk A \&\& coqchk B -admit A} without type-checking any
+definition twice. Of course, the latter is slightly slower since it
+makes more disk access. It is also less secure since an attacker might
+have replaced the compiled library $A$ after it has been read by the
+first command, but before it has been read by the second command.
 
 % $Id$