wp_plugin.tex

\item[\tt -wp-(no)-run-all-provers] Run all specified provers on each goal not
  proved by Qed. When a prover succeeds in proving the goal, the others are not
  stopped. (default is: no).
\item[\tt -wp-gen] only generates proof obligations, does not run provers.
  See option \texttt{-wp-out} to obtain the generated proof obligations.
\item[\tt -wp-par <n>] limits the number of parallel process runs for
  decision procedures. Default is 4 processes. With
  \texttt{-wp-par~1}, the order of logged results is fixed. With more
  processes, the order is runtime dependent.
\item[\tt -wp-filename-truncation <n>] truncates the basename of proof
  obligation files to the first \texttt{n} characters.
  Since numbers can be added as suffixes to ensure unique filenames,
  their length can be longer than \texttt{n}.
  No truncation is performed when the value equals zero. (default is: 60)
\item[\tt -wp-(no)-proof-trace] asks for provers to output extra information
  on proved goals when available (default is: \texttt{no}).
\item[\tt -wp-timeout <n>] sets the timeout (in seconds) for the calls
  to the decision prover (defaults to 10 seconds).
\item[\tt -wp-time-extra <n>] additional time allocated to provers when
  replaying a script. This is used to cope with variable machine load.
  Default is \verb+5s+.
\item[\tt -wp-time-margin <n>] margin time for considering a proof to be
  replayable without a script. When a proof succeed within \verb+timeout-margin+
  seconds, it is considered fully automatic. Otherwise, a script is created
  by prover \verb+tip+ to register the proof time. This is used to decrease the
  impact of machine load when proof time is closed to the timeout.
  Default is \verb+5s+.
\item[\tt -wp-steps <$n$>] sets the maximal number of prover
  steps. This can be used as a machine-independent alternative to timeout.
\item[\tt -wp-why3-opt='options,...'] provides additional options to the
  \verb+why3+ command.
\end{description}

\paragraph{Example of using provers.}
Suppose you have the following configuration:

\begin{logs}
# frama-c -wp-detect
[wp] Why3 provers detected:
   - Alt-Ergo 2.0.0 [alt-ergo,altergo]
   - CVC4 1.6 [cvc4]
   - CVC4 1.6 (counterexamples) [cvc4-ce]
   - Coq 8.9.0 [coq]
   - Z3 4.6.0 [z3]
   - Z3 4.6.0 (counterexamples) [z3-ce]
   - Z3 4.6.0 (noBV) [z3-nobv]
\end{logs}

Then, to use (for instance) \textsf{CVC4 1.6},
you can use \verb+-wp-prover cvc4+.
Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use \verb+-wp-prover z3-nobv+.
Finally, since \textsf{Why-3} also provides the alias
\verb+altergo+ for this prover, \verb+-wp-prover altergo+ will also run it \emph{via} \textsf{Why-3}.

Notice that \textsf{Why-3} provers benefit from a cache management when used in combination with a \textsf{WP}-session, see Section~\ref{wp-cache} for more details.

%% \paragraph{Sessions.}
%% Your \textsf{Why3} session is saved in the \texttt{"project.session"}
%% sub-directory of \texttt{-wp-out}. You may run
%% \texttt{why3ide} by hand by issuing the following command:
%% \begin{shell}
%% # why3ide -I <frama-c-share>/wp <out>/project.session
%% \end{shell}

%% Proof recovering features of \textsf{Why3} are fully available, and
%% you can interleave proving from \textsf{WP} with manual runs of
%% \texttt{why3ide}. Interactive proofs with \textsf{Why3} are completely
%% separated from those managed by the native \textsf{WP} interface with
%% \textsf{Coq}.

\subsection{Generated Proof Obligations}
Your proof obligations are generated and saved to several text
files. With the \texttt{-wp-out} option, you can specify a directory
of your own where all these files are generated. By default, this
output directory is determined as follows: in the GUI, it is
\texttt{<home>/.frama-c-wp} where \texttt{<home>} is the user's home
directory returned by the \texttt{HOME} environment variable. In
command-line, a temporary directory is automatically created and
removed when \textsf{Frama-C} exits.

Other options controlling the output of generated proof
obligations are:
\begin{description}
\item[\tt -wp-(no)-print] pretty-prints the generated proof obligations on
  the standard output. Results obtained by provers are reported as
  well (default is: \texttt{no}).
\item[\tt -wp-out <dir>] sets the user directory where proof
  obligations are saved. The directory is created if it does not exist
  yet. Its content is not cleaned up automatically.
\end{description}

\subsection{Additional Proof Libraries}
\label{prooflibs}

It is possible to add additional bases of knowledge to decision
procedures thanks to the following option:
\begin{description}
\item[\tt -wp-share <dir>] modifies the default directory where
  resources are found.  This option can be useful for running a modified or
  patched distribution of \textsf{WP}.
\end{description}

\subsection{Linking \textsf{ACSL} Symbols to External Libraries}
\label{drivers}

Besides additional proof libraries, it is also possible to
\emph{link} declared \textsf{ACSL} symbols to external or predefined
symbols. In such case, the corresponding \textsf{ACSL} definitions,
if any, are not exported by \textsf{WP}s.

External linkage is specified in \emph{driver files}. It is possible
to load one or several drivers with the following \textsf{WP} plug-in option:
\begin{description}
\item[\tt -wp-driver <file,\ldots>] load specified driver files.

\end{description}

\newcommand{\ccc}{\texttt{,}\ldots\texttt{,}}
\newcommand{\user}[1]{\texttt{"}\textit{#1}\texttt{"}}
Each driver file contains a list of bindings with the following syntax:
\begin{center}
  \begin{tabular}{|l}
  \texttt{library} \user{lib}\verb':' \user{lib} \ldots \user{lib} \\
  \quad\begin{tabular}{rll}
  \rule{0em}{1.2em}
  \textit{group}.\textit{field} &\texttt{:=} \textit{string} \\
  \textit{group}.\textit{field} &\texttt{+=} \textit{string} \\
  \texttt{type} & \textit{symbol} & \verb'=' \user{link} \verb';' \\
  \texttt{ctor} & \textit{type} \textit{symbol}
                   \verb'(' \textit{type}\ccc\textit{type} \verb')'
                 & \verb'=' \user{link} \verb';' \\
  \texttt{logic} & \textit{type} \textit{symbol}
                   \verb'(' \textit{type}\ccc\textit{type} \verb')'
                 & \verb'=' \textit{property-tags} \user{link} \verb';' \\
  \texttt{predicate} & \textit{symbol}
                   \verb'(' \textit{type}\ccc\textit{type} \verb')'
                 & \verb'=' \user{link} \verb';'
  \end{tabular}
  \end{tabular}
\end{center}

It is also possible to define \emph{aliases} to other ACSL symbols, rather
than external links. In this case, you may replace \verb+=+ by
\verb+:=+ and use an ACSL identifier in place of the external \user{link}.
No property tag is allowed when defining aliases.

Library specification is optional and applies to subsequent linked
symbols. If provided, the \textsf{WP} plug-in automatically loads the
specified external libraries when linked symbols are used in a
goal. Dependencies among libraries can also be specified, after the
'\verb':''.

Generic \textit{group}.\textit{field} options have a specific
value for each theory. The binding applies to the current theory.
Binding with the \verb':=' operator
resets the option to the singleton of the given string
and binding with the \verb'+=' operator
adds the given string to the current value of the option.
The following options are defined by the plugin:
\texttt{why3.file} and \texttt{why3.import}.

\textsf{C}-Comments are allowed in the file. For overloaded
\textsf{ACSL} symbols, it is necessary to provide one \user{link} symbol for
each existing signature. The same \user{link} symbol is used for all provers,
and must be defined in the specified libraries, or in the external
ones (see~\ref{prooflibs}).

Alternatively, a link-name can be an arbitrary string
with patterns substituted by arguments, \verb="(%1+%2)"= for instance.

When a library \user{lib} is specified, the loaded module depends on the
option:
\begin{center}\tt
  \begin{tabular}{lll}
    \textrm{Option} & \textrm{Format} \\
    \hline
    why3.file & \verb+path.why[:name][:as]+ \\
    why3.import & \verb+theory[:as]+ \\
  \end{tabular}
\end{center}

Precise meaning of formats is given by the following examples (all filenames are relatives to the driver file's directory):
\begin{description}
\item[\tt why3.file="mydir/foo.why"] Imports theory \verb+foo.Foo+ from directory \verb+mydir+.
\item[\tt why3.file="mydir/foo.why:Bar"] Imports theory \verb+foo.Bar+ from directory \verb+mydir+.
\item[\tt why3.file="mydir/foo.why:Bar:T"] Imports theory \verb+foo.Bar as T+ from directory \verb+mydir+.
\item[\tt why3.import="foo.Bar"] Imports theory \verb+foo.Bar+ with no additional includes.
\item[\tt why3.import="foo.Bar:T"] Imports theory \verb+foo.Bar as T+ with no additional includes.
\end{description}

See also the default \textsf{WP} driver file, in \verb+[wp-share]/wp.driver+.

Optional \textit{property-tags} can be given to
\texttt{logic} \user{link} symbols to allow the \textsf{WP} plugin to perform
additional simplifications (See section~\ref{wp-simplifier}).  Tags
consist of an identifier with column (`\verb+:+'), sometimes followed
by a link (`\user{link};'). The available tags are depicted on figure~\ref{wp-driver-tags}.

\begin{figure}[htbp]
\begin{center}
  \begin{tabular}{lp{10cm}}
    \quad Tags & Operator Properties \\
    \hline
\texttt{commutative:} & specify a commutative symbol:
                        $x \odot y = y \odot x$ \\
\texttt{associative:} & specify an associative symbol:
                        $(x \odot y) \odot z = x \odot (y \odot z)$ \\
\texttt{ac:} & shortcut for \texttt{associative:} \texttt{commutative:} \\
\texttt{left:}  & balance the operator on left during export to solvers (requires the associative tag):
                  $x \odot y \odot z = (x \odot y) \odot z$ \\
\texttt{right:} & balance the operator on right during export to solvers (requires the associative tag):
                      $x \odot y \odot z = x \odot (y \odot z)$ \\
\texttt{absorbant:} \user{a-link}\texttt{:} & specify \user{a-link} as being the absorbant element of the symbol: \\
                     & $\user{a-link} \odot x = \user{a-link}$ \\
                     & $x \odot \user{a-link} = \user{a-link}$ \\
\texttt{neutral:} \user{e-link}\texttt{:} & specify \user{e-link} as being the neutral element of the symbol: \\
                     &  $\user{e-link} \odot x = x$ \\
                     &  $x \odot \user{e-link} = x$ \\
\texttt{invertible:} & specify simplification relying on the existence of an inverse: \\
                     &  $x \odot y = x \odot z \Longleftrightarrow y = z$ \\
                     &  $y \odot x = z \odot x \Longleftrightarrow y = z$ \\
\texttt{idempotent:} & specify an idempotent symbol: $x \odot x = x$ \\
\hline
\texttt{injective:} &  specify an injective function:\\
                      & $f(x_1,\ldots,x_n) = f(y_1,\ldots,y_n) \Longrightarrow \forall i \; x_i = y_i$ \\
\texttt{constructor:} & specify an injective function, that constructs different values
                        from any other constructor. Formally, whenever $f$ and $g$ are two
                        distinct constructors, they are both injective and:
                        $f(x_1,\ldots,x_n) \neq g(y_1,\ldots,y_m)$ forall $x_i$ and $y_j$. \\
\hline
\end{tabular}
\end{center}
\caption{Driver Property Tags}
\label{wp-driver-tags}
\end{figure}

\clearpage
\subsection{Proof Session \& Cache}
\label{wp-cache}

The \textsf{WP} plugin can use a session directory to store informations to be used from one execution to another one.
It is used to store proof scripts edited from the TIP (see Section~\ref{wp-proof-editor}) and to replay them from the command line.
And it is also used to speedup the invocation of provers by reusing previous runs.

Actually, running provers can be demanding in terms of memory and CPU resources. When working
interactively or incrementally, it is often the case where most proof obligations remain unchanged
from one \textsf{WP} execution to the other. To reduce this costs, a cache of prover results can be used
and stored in your session.

% The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers.
There are different ways of using the cache, depending on your precise needs.
The main option to control cache usage is \verb+-wp-cache+, documented below:

\begin{description}
\item[\tt -wp-session <dir>] select the directory where cached results and proof scripts
  are stored. If the local directory \verb+'.frama-c'+ already exists, the default session
  directory \verb+'.frama-c/wp'+ will be used to setup the \textsf{WP} session.
\item[\tt -wp-cache <mode>] selects the cache mode to use with \textsf{Why-3} provers. The default mode is \verb'update'
  if a \textsf{WP} session is set, and \verb+none+ otherwise. The cache entries are stored in the session directory,
  which is \verb+./.frama-c/wp/cache+ by default.
\end{description}

The available cache modes are described below:
\begin{description}
\item [\tt -wp-cache update]: use cache entries or run the provers, and store new results in the cache. This mode is useful when you are working interactively : proofs can be partial and volatile, and you want to accumulate and keep as much previous results as you can.
\item [\tt -wp-cache cleanup]: same as \verb+update+ mode but at the end of \textsf{Frama-C} execution, any cache entry that was not used nor updated will be deleted. This mode shall be only used when you want to cleanup your cache with old useless entries, typically at the end of an interactive session.
\item [\tt -wp-cache replay]: same as \verb+update+ mode but new results are \emph{not} stored in the cache. This mode is useful for continuous integration, when you are not sure your cache is complete but don't want to modify it.
\item [\tt -wp-cache offline]: similar to \verb+replay+ mode but cache entries are the unique source of results. Provers are never run and missing cache entries would result in a «~Failed~» verdict. This mode is useful to fasten continuous integration and enforcing cache completeness.
\item [\tt -wp-cache rebuild]: force prover execution and store all results in the cache. Previous results will be replaced with new onces, but entries for non relevant proofs would be kept and you might need a cleanup stage after. This mode is useful when you modify your \textsf{Why-3} or prover installation and you don't want to reuse your previous cache entries.
\item [\tt -wp-cache none]: do not use nor modify cache entries; provers are run normally. This option must be used if you have a session set and you don't want to use the cache, since the default is mode \verb+update+ in this case. But you probably always to benefit from a cache when you have an (interactive) session.
\end{description}

When using cache with a non-\verb+offline+ mode, time and steps limits recorded in the cache are compared to the command line settings to produce meaningful and consistent results. Hence, if you provide more time or more steps from the command line than before, the prover would be run again. If you provide less or equal limits, the cache entries are reused, but \textsf{WP} still report the cached time and step limits to inform you of your previous attempts. For instance, if you have in the cache a « Valid » entry with time 12.4s and re-run it with a timeout of 5s, you will have a « Timeout » result with time 12.4s printed on the console.
Cached usage is indicated on the standard output, unless you specify \verb+-wp-msg-key no-cache-info+.

\section{Plug-in Developer Interface}
\label{wp-api}

A full featured \textsf{OCaml} API is exported with the
\textsf{WP} plug-in. As documented in the \textsf{Frama-C} user manual, simply add the directive \verb!PLUGIN_DEPENDENCIES+=Wp! to the Makefile of your plug-in.

The high-level API for generating and proving properties is exported
in module \textsf{Wp.API}. The logical interface, compilers, and memory models are also accessible. See the generated \textsf{HTML} documentation of the platform for details.

\section{Proof Obligation Reports}

The \textsf{WP} plug-in can export statistics on generated proof
obligations. These statistics are called \textit{WP reports} and are
distinct from those \textit{property reports} generated by the
\textsf{Report} plug-in. Actually, \textit{WP reports} are statistics
on proof obligations generated by \textsf{WP}, whereas
\textit{property reports} are consolidated status of properties,
generated by the \textsf{Frama-C} kernel from various analyzers.
We only discuss \textit{WP reports} in this section.

Reports are generated with the following command-line options:
\begin{description}
\item[\tt -wp-report <Rspec$_1$,...,Rspec$_n$>] specifies the list of
  reports to export.
  Each value \texttt{Rspec$_i$} is a \textit{WP report} specification file
  (described below).
\item[\tt -wp-report-basename <name>] set the basename for exported
  reports (described below).
\item[\tt -wp-report-json <file>.json] output the reports in JSON format.
  If the file already exists, it is used to stabilize the \verb+range+ of steps
  reports in all other reports (see below).
\end{description}

Reports are created from user defined wp-report specification files.
The general format of a wp-report file is as follows:

\begin{logs}
  <configuration section...>
  @HEAD
  <head contents...>
  @CHAPTER
  <per chapter contents...>
  @SECTION
  <per section contents of a chapter...>
  @TAIL
  <tail contents...>
  @END
\end{logs}

The configuration section consists of optional commands, one per line,
among:
\begin{description}
\item[\tt @CONSOLE] the report is printed on the standard output. \\
  Also prints all numbers right-aligned on 4 ASCII characters.
\item[\tt @FILE "<\textit{file}>"] the report is generated in file \textit{file}.
\item[\tt @SUFFIX "<\textit{ext}>"] the report is generated in file \textit{base.ext},\\
  where \textit{base} can be set with \texttt{-wp-report-basename} option.
\item[\tt @ZERO "<\textit{text}>"] text to be printed for $0$-numbers. Default is \verb+"-"+.

\item[\tt @GLOBAL\_SECTION "<\textit{text}>"] text to be printed for the chapter name about globals
\item[\tt @AXIOMATIC\_SECTION "<\textit{text}>"] text to be printed for the chapter name about axiomatics
\item[\tt @FUNCTION\_SECTION "<\textit{text}>"] text to be printed for the chapter name about functions

\item[\tt @AXIOMATIC\_PREFIX "<\textit{text}>"] text to be printed before axiomatic names.
  Default is \verb+"Axiomatic"+ (with a trailing space).
\item[\tt @FUNCTION\_PREFIX "<\textit{text}>"] text to be printed before function names. Default is empty.
\item[\tt @GLOBAL\_PREFIX "<\textit{text}>"] text to be printed before global property names.
  Default is \verb+"(Global)"+ (with a trailing space).
\item[\tt @LEMMA\_PREFIX "<\textit{text}>"] text to be printed before lemma names.
  Default is \verb+"Lemma"+ (with a trailing space).
\item[\tt @PROPERTY\_PREFIX "<\textit{text}>"] text to be printed before other property names.
\end{description}

The generated report consists of several optional parts, corresponding
to Head, Chapter and Tail sections of the wp-report specification file.
First, the head contents lines are produced.
Then the chapters and their sections are produced.
Finally, the Tail content lines are printed.

The different chapters are about globals, axiomatics and functions.
Outputs for these chapters can be specified using these directives:
\begin{description}
\item[\tt @CHAPTER] <\textit{chapter header...>}
\item[\tt @GLOBAL] <\textit{global section contents...>}
\item[\tt @AXIOMATIC] <\textit{per axiomatic section contents...>}\\
For each axiomatic, a specific section is produced under the chapter about axiomatics.
\item[\tt @FUNCTION] <\textit{per function section contents...>}\\
For each function analyzed by \textsf{WP}, a specific section is produced under the chapter about functions.
\item[\tt @SECTION] <\textit{default section contents...>}
\item[\tt @PROPERTY] <\textit{per property contents...>}\\
For each property of a section, a specific textual content can be specified.
\end{description}

Textual contents use special formatters that will be replaced by
actual statistic values when the report is generated. There are
several categories of formatters (PO stands for \emph{Proof Obligations}):

\begin{center}
  \begin{tabular}{ll}
    \textbf{Formatters} & \textbf{Description} \\
    \hline\hline
    \verb+&<+{\it col}\verb+>:+ & insert spaces up to column \textit{col} \\
    \verb+&&+ & prints a \verb+"&"+ \\
    \verb+%%+ & prints a \verb+"%"+ \\
    \hline
    \verb+%<+{\it stat}\verb+>+ & statistics for section \\
    \verb+%prop+ & percentage of proved properties in section \\
    \verb+%prop:total+ & number of covered properties \\
    \verb+%prop:valid+ & number of proved properties \\
    \verb+%prop:failed+ & number of remaining unproved properties \\
    \verb+%<+{\it prover}\verb+>+ & PO discharged by \textit{prover} \\
    \verb+%<+{\it prover}\verb+>:<+{\it stat}\verb+>+ & statistics for \textit{prover} in section \\
    \hline
  \end{tabular}
\end{center}

\begin{center}
  \begin{tabular}{ll}
    \hline
    \textbf{Provers} \\
    (\verb+<+{\it prover}\verb+>+) & A prover name (see \texttt{-wp-prover}) \\
    \hline
    \hline
    \textbf{Statistics} \\
    (\verb+<+{\it prover}\verb+>+) \\
    \verb+total+ & number of generated PO \\
    \verb+valid+ & number of discharged PO \\
    \verb+failed+ & number of non-discharged PO \\
    \verb+time+ & maximal time used by prover for one PO \\
    \verb+steps+ & maximal steps used by prover for one PO \\
    \verb+range+ & range of maximal steps used by prover (more stable)\\
    \verb+success+ & percentage of discharged PO \\
    \hline
  \end{tabular}
\end{center}

\textbf{Remarks:} \verb+&ergo+ is a shortcut for \verb+&alt-ergo+. Formatters
can be written \verb+"%.."+ or \verb+"%{..}"+. When \verb+range+ is used
instead of \verb+steps+, the maximal number $n$ of steps is printed as a range $a..b$ that
contains $n$.
When option \verb+-report-json+ is used, the previous rank $a$ and $b$ are kept when
available and still fits with the new maximal step number. Otherwise, $a$ and $b$ are re-adjusted
following an heurisitics designed to increase the stability for non-regression testing.

Textual contents can use naming formatters that will be replaced by
current names:
\begin{center}
  \begin{tabular}{ll}
   \textbf{Names} & \textbf{Description} \\
    \hline\hline
    \verb+%chapter+ & current chapter name \\
    \verb+%section+ & current section name \\
    \verb+%global+ & current global name (under the chapter about globals)\\
    \verb+%axiomatic+ & current axiomatic name (under the chapter about axiomatics) \\
    \verb+%function+ & current function name (under the chapter about functions)\\
    \verb+%name+ & current name defined by the context:\\
                 & - property name inside \texttt{@PROPERTY} contents,\\
                 & - function name inside \texttt{@FUNCTION} contents,\\
                 & - axiomatic name inside \texttt{@AXIOMATIC} contents,\\
                 & - global name inside \texttt{@GLOBAL} contents,\\
                 & - section name inside \texttt{@SECTION} contents,\\
                 & - chapter name inside \texttt{@CHAPTER} contents.\\
    \hline
  \end{tabular}
\end{center}
\clearpage

%-----------------------------------------------------------------------------
\section{Plug-in Persistent Data}
\label{wp-persistent}

As a general observation, almost \emph{none} of the internal
\textsf{WP} data is kept in memory after each execution. Most of the
generated proof-obligation data is stored on disk before being sent to
provers, and they are stored in a temporary directory that is removed
upon \textsf{Frama-C} exit (see also \texttt{-wp-out} option).

The only information which is added to the \textsf{Frama-C} kernel
consists in a new status for those properties proved by \textsf{WP} plug-in with
their dependencies.

Thus, when combining \textsf{WP}
options with \texttt{-then}, \texttt{-save} and \texttt{-load}
options, the user should be aware of the following precisions:
\begin{description}
\item[\tt -wp, -wp-prop, -wp-fct, -wp-bhv.] These options make the
  \textsf{WP} plug-in generate proof-obligations for the selected
  properties. The values of theses options are never saved and they are
  cleared by \texttt{-then}. Hence, running \texttt{-wp-prop A}
  \texttt{-then} \texttt{-wp-fct F} does what you expect:
  properties tagged by \texttt{A} are proved only once.
\item[\tt -wp-print, -wp-prover, -wp-gen, -wp-detect.] These options do not
  generate new proof-obligations, but run other actions on all
  previously generated ones. For the same reasons, they are not saved
  and cleared by \texttt{-then}.
\item[\tt -wp-xxx.] All other options are tunings that can be easily
  turned on and off or set to the desired value.
  They are saved and kept across \texttt{-then} commands.
\end{description}

%-----------------------------------------------------------------------------

% vim: spell spelllang=en