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
automated theorem provers such as
\textsf{Alt-Ergo}~\cite{AltErgo2006},
\textsf{CVC4}~\cite{CVC4} and
\textsf{Z3}~\cite{Z3}
or by interactive proof assistants
like \textsf{Coq}~\cite{Coq84} and more generally, any automated or interactive
prover supported by \textsf{Why3}~\cite{Why3}.

\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.

\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}.

With memory model unmangled, the encoding in logic formulae is revealed and no label are displayed.

\subsection{Tactics}

The right panel display a palette of tactics to be applied on the current goal. Tooltips are provided to help the user understanding how to configure and run tactics.

Only applicable tactics are displayed, with respect to current term or clause selected. Many tactics can be configured by the user to tune their effect. Click on the tactic button to toggle its control panel. Once a tactic is correctly configured, it can be applied by clicking its « Play » button.

\subsection{Term Composer}

Some tactic require one or several terms to be selected.
In such case, the normal view display the selected term.
It can be edited by buttons in the view, like a \texttt{RPN} calculator. More buttons appear with respect to already selected terms. Numerical constants can be composed, and combined with selected terms.

Typically, the composer displays a stack of values, like for instance:
\begin{ccode}
  A: 45
  B: a[0]@Pre (int)
\end{ccode}

In such a case, the user can select the value \texttt{45} with the \texttt{Select A} button, or add the two numbers with the \texttt{Add A+B} button.

Sometimes, like for the Instance tactic, a \emph{range} of numerical values can be selected. In such a case, when two numbers are selected, a special button \texttt{Select A..B} appears.

The list of all available composer buttons is displayed by the \texttt{Help} button.

A composer worth to be mentioned is \texttt{Destruct}, typically available on complex expressions. It allows to decompose a value into its sub-components. For instance, destructuring the value \texttt{B} above will reveal the address \texttt{« a+0 »@Pre} and memory \texttt{µ:Mint@Pre}.

\subsection{Proof Script}

The top toolbar upon the goal display show the current status of the goal and the number of pending goals. The media buttons allow to navigate in the proof tree.
\begin{quote}
\begin{tabular}{ll}
\verb+Next/Prev:+ & navigate among the list of pending (non proved) sub-goals; \\
\verb+Forward:+ & goes to the next pending sub-goal; \\
\verb+Backward:+ & cancel the current tactic and prover results; \\
\verb+Clear:+ & restart all the interactive proof from the initial goal.
\end{tabular}