Commit 0ba1183e authored by POTTIER Francois's avatar POTTIER Francois
parents d43c59d9 b44fd3ae
......@@ -2919,6 +2919,17 @@
URL = "http://www.ccs.neu.edu/scheme/pubs/esop2003-cf.ps.gz",
}
@InProceedings{clochard-marche-paskevich-14,
author = "Martin Clochard and Claude March{\'{e}} and Andrei
Paskevich",
title = "Verified programs with binders",
booktitle = plpv,
pages = "29--40",
month = jan,
year = "2014",
URL = "https://hal.inria.fr/hal-00913431",
}
@Article{cohen-search-06,
author = "Albert Cohen and Sébastien Donadio and Maria-Jesus
Garzaran and Christoph Herrmann and Oleg Kiselyov and
......@@ -7567,6 +7578,15 @@
URL = "http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf",
}
@Misc{compcert,
author = "Xavier Leroy",
title = "The {CompCert} verified compiler, software and
commented proof",
month = sep,
year = "2014",
howpublished = "\url{http://compcert.inria.fr/}",
}
@TechReport{leroy-phd-92,
author = "Xavier Leroy",
title = "Polymorphic typing of an algorithmic language",
......
......@@ -382,6 +382,7 @@ grammar specification files, the order in which they are copied to the \ml
file is unspecified.
\subsubsection{Parameters}
\label{sec:parameter}
A declaration of the form:
\begin{quote}
......@@ -434,6 +435,7 @@ Associativity status and priority levels allow shift/reduce conflicts to be
silently resolved (\sref{sec:conflicts}).
\subsubsection{Types}
\label{sec:type}
A declaration of the form:
\begin{quote}
......@@ -445,6 +447,7 @@ For start symbols, providing an \ocaml type is mandatory, but is usually done as
the quality of \ocaml's type error messages.
\subsubsection{Start symbols}
\label{sec:start}
A declaration of the form:
\begin{quote}
......@@ -1914,43 +1917,56 @@ in the near future.
\section{Coq back-end}
\label{sec:coq}
Using the Coq proof assistant, \menhir is able to generate formally
verified parsers~\cite{jourdan-leroy-pottier-12}: when used with the
\ocoq option, menhir shall be given a \texttt{.vy}, and will generate
a \texttt{.v} file. This file contains both a description of the
grammar and semantic actions in the Coq language. \texttt{.vy} files
use the same syntax as \texttt{.mly} files. There are however, several
additional restrictions:
\menhir is able to generate a parser that whose correctness can be formally
verified using the Coq proof assistant~\cite{jourdan-leroy-pottier-12}. This
feature is used to construct the parser of the CompCert certified C
compiler~\cite{compcert}.
Setting the \ocoq switch on the command line enables the Coq back-end. When
this switch is set, \menhir expects an input file whose name ends
in \texttt{.vy}, and generates a Coq file, whose name ends
in \texttt{.v}.
Like a \texttt{.mly} file, a \texttt{.vy} file is a grammar specification,
with embedded semantic actions. The main difference is that the semantic
actions in a \texttt{.vy} file are expressed in Coq instead
of \ocaml. A \texttt{.vy} file otherwise uses the same syntax as
a \texttt{.mly} file. There are however several restrictions:
%
\begin{itemize}
\item Error handling is not supported: thus, the use of
\verb+$syntaxerror+ or the \error token is not supported.
\item Location information is not propagated: the input file cannot
contain any \verb+$start*+ or \verb+$end*+ special keywords.
\item \dparameter is not supported.
\item \dinline is not supported.
\item The standard library is not supported.
\item As the type inference algorithm of Coq is rather unpredictable,
every nonterminal symbol has to be annotated with either the \dtype
or the \dstart keyword.
\item If the proof of completeness has not been deactivated via
\ocoqnocomplete, the grammar cannot contains conflicts, even
benign. The reason is that there is no simple formal specification
\item The error handling mechanism (\sref{sec:errors}) is absent.
The \verb+$syntaxerror+ keyword and the \error token are not supported.
\item Location information is not propagated. The \verb+$start*+ and \verb+$end*+
keywords (\fref{fig:pos}) are not supported.
\item \dparameter (\sref{sec:parameter}) is not supported.
\item \dinline (\sref{sec:inline}) is not supported.
\item The standard library (\sref{sec:library}) is not supported, of course,
since its semantic actions are expressed in \ocaml. If desired, the user can define
an analogous library, whose semantic actions are expressed in Coq.
\item Because Coq's type inference algorithm is rather unpredictable,
the Coq type of every nonterminal symbol must be provided via a
\dtype or \dstart declaration (\sref{sec:type}, \sref{sec:start}).
\item Unless the proof of completeness has been deactivated (see
\ocoqnocomplete below), the grammar must not have a conflict.
That is, the grammar must be LR(1). Conflict resolution via
priority and associativity declarations (\sref{sec:assoc})
is not supported.
The reason is that there is no simple formal specification
of how conflict resolution should work.
\end{itemize}
The generated file contains several modules:
\begin{itemize}
\item Module \verb+Gram+ contains the types of terminals and
non-terminals, the grammar description, and semantic actions.
\item Module \verb+Aut+ contains description of the automaton
generated by \menhir, with a certificate that will be checked in
order to prove the soundness and completeness of the parser.
\item The module \verb+Gram+ defines the terminal and
non-terminal symbols, the grammar, and the semantic actions.
\item The module \verb+Aut+ contains the automaton
generated by \menhir, together with a certificate that is checked by Coq
while establishing the soundness and completeness of the parser.
\end{itemize}
The type of terminals is a big inductive type, with a constructor for
each terminal, but it does not contains the semantic values: we also
The type of the terminal symbols is an inductive type, with one constructor for
each terminal symbol. but it does not contains the semantic values: we also
define the type \verb+token+, which is a dependant pair of a terminal
and a semantic value of the corresponding type. Thus, we model the
lexer by an object of type \verb+Stream.Stream token+.
......@@ -1989,7 +2005,7 @@ function. Two theorems are provided, \verb+entry_point_correct+ and
\verb+entry_point_complete+.
Parsers generated with the Coq back-end need to be compiled with
libraries: those can be found in the CompCert tree, under the
libraries: those can be found in the CompCert tree~\cite{compcert}, under the
\verb+cparser/validator+ subdirectory. Additionnally, CompCert can be
used as an example if one wants to use menhir to generate formally
verified parsers in another project.
......
B _stage1
......@@ -19,7 +19,7 @@ endif
# ----------------------------------------------------------------------------
# Ocamlbuild tool and settings.
OCAMLBUILD := ocamlbuild -classic-display -j 0 -cflags "-safe-string"
OCAMLBUILD := ocamlbuild -classic-display -j 0 -cflags "-safe-string -bin-annot"
# ----------------------------------------------------------------------------
# For everyday development.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment