From 311373891569f2c44db11d481fa6663876e784fa Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 23 May 2008 20:49:19 +0000 Subject: 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 --- checker/check.ml | 94 ++++++++++++++++++++---------------- checker/safe_typing.ml | 119 ---------------------------------------------- doc/refman/RefMan-com.tex | 90 +++++++++++++++++++++++++++++++---- 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$ -- cgit v1.2.3