wp_plugin.tex

\chapter{Using the WP Plug-in}
\label{wp-plugin}

The \textsf{WP} plug-in can be used from the \textsf{Frama-C} command line
or within its graphical user interface. It is a
dynamically loaded plug-in, distributed with the kernel since the
\textsf{Carbon} release of \textsf{Frama-C}.

This plug-in computes proof obligations of programs annotated with
\textsf{ACSL} annotations by \emph{weakest precondition calculus},
using a parametrized memory model to represent pointers and heap
values. The proof obligations may then be discharged by external
decision procedures, which range over automated theorem provers such
as \textsf{Alt-Ergo}~\cite{AltErgo2006}, interactive proof assistants
like \textsf{Coq}~\cite{Coq84} and the interactive proof manager
\textsf{Why3}~\cite{Why3}.

This chapter describes how to use the plug-in, from the
\textsf{Frama-C} graphical user interface (section~\ref{wp-gui}), from
the command line (section~\ref{wp-cmdline}), or from another plug-in
(section~\ref{wp-api}).  Additionally, the combination of the \textsf{WP}
plug-in with the load and save commands of \textsf{Frama-C} and/or the
\texttt{-then} command-line option is explained in section~\ref{wp-persistent}.

\clearpage
%-----------------------------------------------------------------------------
\section{Installing Provers}
\label{wp-install-provers}
%-----------------------------------------------------------------------------

The \textsf{WP} plug-in requires external provers to work.
The recommended versions for external provers are:
\begin{center}
  \begin{tabular}{crlc}
    Prover & Versions & Download &\\
    \hline
    \textsf{Alt-Ergo} & \verb|2.0.0|  &
    \url{http://alt-ergo.ocamlpro.com} & \cite{AltErgo2006}\\
    \textsf{Coq} & \verb|8.9.0| &
    \url{http://coq.inria.fr} & \cite{Coq84}\\
    \textsf{Why3} & \verb|1.2.0| &
    \url{http://why3.lri.fr} & \cite{Why3}\\
  \end{tabular}
\end{center}

Recent \textsf{OPAM}-provided versions should work smoothly.
Other versions might be supported as well, typically, as far as we know:
\begin{itemize}
\item \textsf{Alt-Ergo} \verb+2.2.0+ and \verb+2.3.0+, although distributed under a non-commercial licence.
\item \textsf{Coq} \verb+8.7.2+ and \verb+8.8.2+, although proof scripts compatibility can be an issue.
\item \textsf{Why3} \verb+1.0.0+ and \verb+1.1.1+, although only \verb+1.2.0+ is provided with Coq support.
\end{itemize}

Other provers, like \textsf{Gappa}, \textsf{Z3}, \textsf{CVC3},
\textsf{CVC4}, \textsf{PVS}, and many others, are accessible from
\textsf{WP} through \textsf{Why3}. We refer the user to the manual of
\textsf{Why3} to handle specific configuration tasks.

\clearpage
%-----------------------------------------------------------------------------
\section{Graphical User Interface}
\label{wp-gui}
%-----------------------------------------------------------------------------

\newcommand{\loadicon}[1]{\raisebox{-3pt}{\rule{0pt}{13pt}\includegraphics[height=12pt]{#1}}}

To use the \textsf{WP} plug-in with the GUI, you simply need to run the
\textsf{Frama-C} graphical user interface. No additional option is
required, although you can preselect some of the \textsf{WP} options
described in section~\ref{wp-cmdline}:

\begin{shell}
  \$ frama-c-gui [options...] *.c
\end{shell}

\begin{figure}[p]
\begin{center}
\includegraphics[width=\textwidth]{wp-gui-main.png}
\end{center}
\caption{\textsf{WP} in the Frama-C GUI}
\label{wp-gui-panel}
\end{figure}

\begin{figure}[p]
\begin{center}
\includegraphics[width=\textwidth]{wp-gui-run.png}
\end{center}
\caption{\textsf{WP} run from the GUI}
\label{wp-gui-run}
\end{figure}

As we can see in figure~\ref{wp-gui-panel}, the memory model, the
decision procedure, and some \textsf{WP} options can be tuned from the
\textsf{WP} side panel. Other options of the \textsf{WP} plug-in are still
modifiable from the \texttt{Properties} button in the main GUI toolbar.

To prove a property, just select it in the internal source view and
choose \textsf{WP} from the contextual menu. The \texttt{Console}
window outputs some information about the
computation. Figure~\ref{wp-gui-run} displays an example of such a
session.

If everything succeeds, a green bullet should appear on the left of
the property. The computation can also be run for a bundle of
properties if the contextual menu is open from a function or behavior
selection.

The options from the \textsf{WP} side panel correspond to some options
of the plug-in command-line. Please refer to section~\ref{wp-cmdline}
for more details. In the graphical user interface, there are also
specific panels that display more details related to the \textsf{WP} plug-in,
that we shortly describe below.

\paragraph{Source Panel.} On the center of the \textsf{Frama-C} window, the status
of each code annotation is reported in the left margin. The meaning of
icons is the same for all plug-ins in \textsf{Frama-C} and more precisely described
in the general user's manual of the platform. The status emitted by the \textsf{WP} plug-in are:
\begin{center}
  \begin{tabular}{cl}
    \multicolumn{2}{l}{\bf Icons for properties:} \\
    \hline
    \loadicon{feedback/never_tried.png} & No proof attempted. \\
    \loadicon{feedback/unknown.png} & The property has not been validated. \\
    \loadicon{feedback/valid_under_hyp.png} & The property is \emph{valid} but has dependencies. \\
    \loadicon{feedback/surely_valid.png} & The property and \emph{all} its dependencies are \emph{valid}. \\
    \hline
  \end{tabular}
\end{center}

\paragraph{\textsf{WP} Goals Panel.}
This panel is dedicated to the \textsf{WP} plug-in. It shows the
generated proof obligations and their status for each prover.
By clicking on a prover
column, you can also submit a proof obligation to a prover by
hand. Right-click provides more options depending on the prover, such
as proof-script editing for \textsf{Coq}.

\paragraph{Interactive Proof Editor.}
From the Goals Panel view, you can double-click on a row and open the \emph{interactive proof editor} panel as described in section~\ref{wp-proof-editor}.

\paragraph{Properties Panel.} This panel summarizes the consolidated
status of properties, from various plug-ins. This panel is not
automatically refreshed. You should press the \texttt{Refresh} button
to update it. This panel is described in more details in the general
\textsf{Frama-C} platform user's manual.

\clearpage
%-----------------------------------------------------------------------------
\section{Interactive Proof Editor}
\label{wp-proof-editor}
%-----------------------------------------------------------------------------

This panel focus on one goal generated by \textsf{WP}, and allow the user to visualize the logical sequent to be proved, and to interactively decompose a complex proof into smaller pieces by applying \emph{tactics}.

\begin{figure}[htbp]
\begin{center}
\includegraphics[width=\textwidth]{wp-tip-run.png}
\end{center}
\caption{Interactive Proof Editing}
\label{wp-tip-run}
\end{figure}

The general structure of the panel is illustrated figure~\ref{wp-tip-run}. The central text area prints the logical sequent to proved. In consists of a formula to \verb+Prove+ under the hypotheses listed in the \verb+Assume+ section. Each hypothesis can consists of :
\begin{quote}
\begin{tabular}{ll}
\verb+Type:+& formula expressing a typing constraint;\\
\verb+Init:+& formula characterizing global variable initialisation;\\
\verb+Have:+& formula from an assertion or an instruction in the code;\\
\verb+When:+& condition from a simplification performed by \textsf{Qed};\\
\verb+If:+& structured hypothesis from a conditional statement;\\
\verb+Either:+& structured disjunction from a switch statement.\\
\verb+Stmt:+& labels and C-like instructions representing the memory updates during code execution;\\
\end{tabular}
\end{quote}

\subsection{Display Modes}

There are several modes to display the current goal:
\begin{quote}
\begin{tabular}{ll}
\verb+Autofocus:+ & filter out clauses not mentioning \emph{focused} terms (see below);\\
\verb+Full Context:+ & disable autofocus mode --- all clauses are visible; \\
\verb+Unmangled Memory:+ & autofocus mode with low-level details of memory model; \\
\verb+Raw Obligation:+ & no autofocus and low-level details of memory model.
\end{tabular}
\end{quote}

\paragraph{Remark:} the fold/unfold operations only affect the goal display. It does not \emph{transform} the goal to be proven.

The autofocus mode is based on a ring of \emph{focused terms}. Clicking a term of a clause automatically focus this term. Shift-clicking a term adds the term to the focus ring. When autofocus mode is active, only the clauses that contains a \emph{focused} term are displayed. Hidden clauses are mentioned by an ellipsis \texttt{[...]}.

Low-level details of the memory model are normally hidden, and represented by C-like instructions such as:

\begin{ccode}
   Stmt { Label A: a.f[0] = y@Pre; }
\end{ccode}

This reads as follows: a program point is defined by the label \texttt{A}. At this point, the left-value \texttt{a.f[0]} receives the value that variable \texttt{y} holds at label \texttt{Pre}. More generally, \texttt{lv@L} means the value of l-value \texttt{lv} at label \texttt{L:}, and for more complex expression, \texttt{« e »@L} means the expression \texttt{e} evaluated at label \texttt{L}. Redundant labels are removed when possible. This is a short-hand for \textsf{ACSL} notation \lstinline{\at(e,L)} but is generally more readable.

Sometimes, some memory operations can not be rendered as C instructions, typically after transforming a goal so far. In such situations, the memory model encoding might appear with terms like \texttt{µ:Mint@L}.