From 36126508495a64221c4a3695406d2ccf2cd099b7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 27 Oct 2021 16:47:33 +0200
Subject: [PATCH] [wp/doc] Document terminates support
---
src/plugins/wp/Changelog | 4 +-
src/plugins/wp/doc/manual/wp_plugin.tex | 96 ++++++++++++++++++++++++-
2 files changed, 97 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 7c0fa5e2fee..2a4bb7b5026 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -27,9 +27,9 @@ Plugin WP <next-release>
- WP [2021-10-25] Removes -wp-overflows option (unsound)
- WP [2021-06-11] Adds an experimental support of "terminates" clauses.
Adds the options -wp-declaration-terminate and
- -wp-frama-c-stdlib to claims that external functions
+ -wp-frama-c-stdlib to claim that external functions
terminates.
- Adds -wp-declarations-terminate option to claims that
+ Adds -wp-definitions-terminate option to claim that
defined function terminates.
Adds -wp-variant-with-terminates to verify loop
variants under the termination hypothesis.
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index abeb02c808f..afb8bee6f60 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -986,7 +986,7 @@ weakest precondition calculus.
\texttt{terminates \textbackslash{}false}, any loop variant proof is trivial)
(default is: \texttt{no}).
\item[\tt -wp-(no)-dynamic] handles calls \textit{via} function pointers
- thanks to the dedicated \verb+@calls f1,...,fn+ code annotation (default is: \texttt{yes}).
+ thanks to the dedicated code annotation \verb+@calls f1,...,fn+ (default is: \texttt{yes}).
\end{description}
\subsubsection{ACSL extension \texttt{@calls}}
@@ -1018,6 +1018,100 @@ These annotations split post-conditions to the dynamic call into two sub-goals:
a second for the call to \verb+f2+. A last goal is generated at the call
site: one must prove that \verb+fp+ is either \verb+f1+ or \verb+f2+.
+\subsubsection{Proof of \texttt{@terminates}}
+
+In ACSL, a function can be specified to terminate some condition \verb+P+ holds
+in precondition.
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+/*@ terminates P ; */
+void function(void){
+ ...
+}
+\end{lstlisting}
+
+If terminates verification is active, WP collects all function calls and loops
+and generate different VCs.
+
+\paragraph{Loop variants.} When a loop has a variant, no particular verification
+is generated for termination. However, if \verb+-wp-variant-with-terminates+ is
+active, the variant is verified only if \verb+P+ holds at this program point.
+Basically, "the variant has to hold only if the function has to terminate". For
+example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i >= 0 ;
+void positive(int i){
+ /*@ loop invariant \at(i, Pre) >= 0 ==> 0 <= i <= \at(i, Pre) ;
+ loop assigns i ;
+ loop variant i ; // verified when i >= 0 at pre
+ */
+ while(i) --i;
+}
+\end{lstlisting}
+
+Note that it means that when one specifies \verb+terminates \false+ any loop
+variant trivially holds.
+
+When a loop does not have a variant, WP checks that the loop is unreachable
+when \verb+P+ holds in precondition, which means "a loop is allowed not
+terminating when the function does not have to". For example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i >= 0 ;
+void function(int i){
+ if(i < 0){
+ // note i >= 0 && i < 0 ==> \false
+ while(1);
+ }
+}
+\end{lstlisting}
+
+\paragraph{Function call.} When a function \verb+f+ that terminates when
+\verb+P+, calls a function \verb+g+ that terminates when \verb+Q+, WP tries to
+prove that \verb+P@pre ==> Q@call-point+, "when \verb+f+ terminates, we must
+call \verb+g+ in a way that guarantees that it also terminates". Note that it
+means that if the function under verification must terminate, any call to a
+non terminating function must be unreachable. For example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i <= 0 ;
+void f(int i) ;
+
+//@ terminates i > 0 ;
+void g(int i) ;
+
+/*@ requires i <= 0 ;
+ terminates \true ; */
+void caller(int i){
+ f(i); // succeeds
+ g(i); // fails, thus global termination is not proved
+}
+\end{lstlisting}
+
+When a called function does not have a terminates specification, WP assumes one
+as specified by the options:
+
+\begin{itemize}
+\item \verb+-wp-frama-c-stdlib-terminate+,
+\item \verb+-wp-declarations-terminate+,
+\item \verb+-wp-definitions-terminate+.
+\end{itemize}
+
+\paragraph{(Mutually) recursive function.} When a function is in a recursive
+cluster (as defined in the ACSL manual) and must terminate, WP checks that a
+\verb+decreases+ clause is available for the function. Proving that existing
+recursive calls might be unreachable is delegated to the proof of the
+\verb+decreases+ clause. Note however that currenlty the proof of such a clause
+is not supported.
+
+\paragraph{Function pointers. } On a call via a function pointer, WP checks that
+a \verb+@calls+ is specified for this function pointer. If so, WP just behave
+as explained before for function calls. If this specification is not available,
+WP considers that the pointed function might call the function under
+verification and thus that it is part of a recursive cluster and must provide
+a \verb+decreases+ clause.
+
\subsection{Smoke Tests}
During modular deductive verification, inconsistencies in function requirements
--
GitLab