Skip to content
Snippets Groups Projects
Commit f457a42f authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'remove-unused-wp-manual-chapters' into 'master' 

[Wp] remove unused manual sections

See merge request frama-c/frama-c!3807
parents 61311558 7b00705b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 1268 deletions
headers/header_spec.txt
+ 0
− 5
View file @ f457a42f
......@@ -1860,19 +1860,14 @@ src/plugins/wp/doc/manual/wp-unknown.png: .ignore
src/plugins/wp/doc/manual/wp-valid.png: .ignore
src/plugins/wp/doc/manual/wp.bib: .ignore
src/plugins/wp/doc/manual/wp.tex: .ignore
src/plugins/wp/doc/manual/wp_acsl.tex: .ignore
src/plugins/wp/doc/manual/wp_calculus.tex: .ignore
src/plugins/wp/doc/manual/wp_caveat.tex: .ignore
src/plugins/wp/doc/manual/wp_hoare.tex: .ignore
src/plugins/wp/doc/manual/wp_implementation.tex: .ignore
src/plugins/wp/doc/manual/wp_intro.tex: .ignore
src/plugins/wp/doc/manual/wp_logic.tex: .ignore
src/plugins/wp/doc/manual/wp_logicvar.tex: .ignore
src/plugins/wp/doc/manual/wp_models.tex: .ignore
src/plugins/wp/doc/manual/wp_plugin.tex: .ignore
src/plugins/wp/doc/manual/wp_runtime.tex: .ignore
src/plugins/wp/doc/manual/wp_simplifier.tex: .ignore
src/plugins/wp/doc/manual/wp_store.tex: .ignore
src/plugins/wp/doc/manual/wp_typed.tex: .ignore
src/plugins/wp/driver.mli: CEA_WP
src/plugins/wp/driver.mll: CEA_WP
......
src/plugins/wp/doc/manual/wp_acsl.tex deleted 100644 → 0
+ 0
− 388
View file @ 61311558
%% Chapter WP Models
\section{ACSL} \label{sec-acsl}
This section describes, firstly, the model of \textsf{ACSL} datum (or
logical values) such as reals and integers, the logical arrays and
records, the logical pointers and sets. Secondly, the translation
of the predicates and axiomatics of \textsf{ACSL} to $\cal{L}$ is
presented.
\subsection{ACSL values}
\subsubsection{Values of Basic types}
The basic types are the C arithmetic types and the logic integers and reals.
All integer types are translated into the type $\mathbb{Z}$ of $\cal{L}$.
In the same flavor, the object of the logic type \cinline{real} of
\textsf{ACSL} becomes object of type $\mathbb{R}$ of $\cal{L}$.
That is not sufficient for the translation of numerical values:
they have to be bound in a convenient domain.
To express that domain constraint, the notion of {\it format} is necessary.
A \whyinline{format} informs about the \textsf{ACSL} type of the
value. The table in the figure~\ref{fig:type_format} gathers some
primitive formats.
The format associated to a C arithmetic type handles the signess and
size information of the type. The predicate
\whyinline{is_in_format} expresses the domain constraint.
For example: \cinline{unsigned char i;} becomes in $\cal{L}$
\whyinline{forall i:Z. is_in_format(uint8_format,i)} which provide the
information that $0 \le i < 256$.
\TODO{Pointers and Formats have been completely modified}
\begin{figure}[ht!]
\begin{center}
\begin{tabular}{|l|r|r|}
\hline
\textsf{ACSL}: $\tau$ & $\cal{L}$: $\overline{\tau}$ & $\cal{L}$ format \\
\hline
\cinline{signed char/short/int/long int} &
$\mathbb{Z}$ & \whyinline{sint8/16/32/64_format} \\
\hline
\cinline{unsigned char/short/int/long int} &
$\mathbb{Z}$ & \whyinline{uint8/16/32/64_format} \\
\hline
\cinline{float,double} &$\mathbb{R}$ &
\whyinline{float16/32/64/96/128_format} \\
\hline
integer & $\mathbb{Z}$ & \whyinline{int_format} \\
\hline
real & $\mathbb{R}$ & \whyinline{real_format} \\
\hline
$\tau~*$ & pointer & \whyinline{pointer_format} \\
\hline
$\tau~$ array & $\overline{\tau}$ farray &
$\overline{\tau}$ \whyinline{array_dim_format} \\
\hline
struct S $\{ \ldots\tau_n~f_n; \ldots \}$ &
S & \whyinline{S_format} \\
\hline
\end{tabular}
\end{center}
\caption{Typed representation of objects}
\label{fig:type_format}
\end{figure}
\subsubsection{Logic pointers}\label{ssec-acsl-ptr}
The logic pointers of \textsf{ACSL} are translated into an opaque
type \whyinline{pointer} which is untyped.
All memory models use the logic arithmetic of pointers defined in
figure~\ref{fig:arithptr}, except for the shift operations which are
memory model dependent.
\begin{figure}[ht!]
\begin{center}
\begin{tabular}{|l|r|r|}
\hline
ACSL & $\cal{L}$ functional & $\cal{L}$ relational \\
\hline
\cinline{NULL} & \whyinline{null} & \whyinline{is_null} \\
\cinline{p == q}& \whyinline{equal_pointer(p,q)} & \whyinline{p=q} \\
\hline
\cinline{p < q} & \whyinline{lt_pointer(p,q)} &
\whyinline{lt_pointer_rel(p,q)} \\
\hline
\cinline{p <= q} & \whyinline{le_pointer(p,q)} &
\whyinline{le_pointer_rel(p,q)} \\
\hline
\cinline{p - q} & \whyinline{minus_pointer(p,q)} & $\emptyset$ \\
\hline
\cinline{p + i} & \multicolumn{2}{c|}{memory model dependent} \\
\hline
\end{tabular}
\end{center}
\caption{Translation of the arithmetic of pointers}
\label{fig:arithptr}
\end{figure}
As all the pointer arithmetic is done via the logic pointer,
the memory model has to provide coercion between a logic pointer
and its location type.
\subsubsection{Arrays}
An \textsf{ACSL} array of type $\tau$ is represented by an infinite
array of type $\overline{\tau}$ in $\cal{L}$
(see figure~\ref{fig:type_format} for interpretation of primitive types).
The classical operations over \textsf{ACSL} array are translated as
suspected:
\begin{description}
\item{access} to a value at the index \cinline{i} of an \textsf{ACSL} array
\cinline{t} :
\cinline{t[i]} becomes \whyinline{access(t,i)} in $\cal{L}$,
which also can be written as \whyinline{t[i]};
\item{functional update} of the value indexed by \cinline{i} of an
\textsf{ACSL} array \cinline{t} by the new value \cinline{v}:
\cinline{\{t with [i] = v\}}
becomes \whyinline{update (t, i, x)} in $\cal{L}$, which also can
be written \whyinline{t[i <- x ]}.
\end{description}
This is possible to access or update a set of indexes in a logic array:
\begin{description}
\item{\whyinline{get_range_index(t,s)}}
returns the set of values of \whyinline{t} of the indexes of
the set \whyinline{s}, when \whyinline{t} is an array;
\item{\whyinline{set_range_index(t,s)}} is an array such as all
elements \whyinline{set_range_index(t,s)[i]}= \whyinline{t[i]}
when \whyinline{i} $\notin$ \whyinline{s} holds.
\end{description}
\subsubsection{Logic records and unions }\label{ssec-acsl-rec}
\begin{description}
\item {\cinline{struct S {...}}} becomes \whyinline{type S}.
\item{\cinline{union U{...}}} becomes \whyinline{type U}.
\item{For each field \cinline{tf f;} of a structure or an union S}
two functions are generated in $\cal{L}$:
\begin{itemize}
\item \whyinline{get_field_f_S:S ->}$\overline{tf}$ returns the value
of the field \cinline{f} of a record or a union of type \cinline{S}
\item \whyinline{set_field_f_S:S,}$\overline{tf}$\whyinline{
-> S} returns the updated record or union at the field
\cinline{f}
\end{itemize}
and an axiom :
\begin{itemize}
\item\whyinline{axiom GetSetSame_f_S : forall r:S. forall
v:}$\overline{tf}$\whyinline{.}
\whyinline{get_field_f_S(set_field_f_S(r,v)) = r}
\end{itemize}
\item{For each disjoint pair of fields \cinline{...; tg g;...;tf
f;...} of a same structure definition S} an axiom is defined as follows:
\begin{itemize}
\item\whyinline{axiom GetSetOther_f_g_S : forall r:S. forall
v:}$\overline{tg}$\whyinline{.}
\whyinline{get_field_f_S(set_field_g_S(r,v)) = get_field_f_S(r)}
\end{itemize}
\item{\cinline{s.f}} becomes \whyinline{get_field_f_S(s)}.
\item{\cinline{s with .f = v}} becomes \whyinline{set_field_f_S(s,v)}.
\end{description}
Consider the following example: %(tests/wp_acsl/record.c):
\begin{ccode}
struct S {int a; int b;};
struct S s1,s2;
/*@
ensures {s1 \with .a = (int)1}.a == 1;
*/
void f (void) {}
\end{ccode}
The WP computation will give you this $\cal{L}$ specification:
\begin{whycode}
type S
logic get_a_S: S -> int
logic set_a_S: S , int -> S
logic get_b_S: S -> int
logic set_b_S: S , int -> S
(* Definition of the good properties of the field a*)
axiom GetSetSame_a:
forall r:S.forall v:int.
get_a_S(set_a_S(r,v))=
v
(* Definition of the commutativity of the get field a over the set field b*)
axiom GetSetOther_a_b:
forall r:S.forall v:int.
get_a_S(set_b_S(r,v))=
get_a_S(r)
(* Definition of the good properties of the field b*)
axiom GetSetSame_b:
forall r:S.forall v:int.
get_b_S(set_b_S(r,v))=
v
(* Definition of the commutativity of the get field b over the set field a*)
axiom GetSetOther_b_a:
forall r:S.forall v:int.
get_b_S(set_a_S(r,v))=
get_b_S(r)
\end{whycode}
\subsubsection{The equality of logical values, \whyinline{v == v'}}\label{ssec-acsl-eq}
Alike for the representation of logic values, the relations of
equality of logic values are directed by types. Hence,
the equality of logic values of basic type; integer, reals and pointers,
is the equality of $\cal{L}$, \whyinline{=}.
Concerning the equality of objects of more complex type; arrays, records
and union, the \textsf{ACSL} model generates a equality
relation for each type. \par
Two records of same type \cinline{S} are equals if their fields are equal.
Consider the following example:
\begin{ccode}
typedef struct T {float f;};
typedef struct S { int a; int * p; struct T t;};
\end{ccode}
If the WP computation needs to deal with object of type
\cinline{S},then an axiom in the environment over equality for object
of type \cinline{S} is defined \whyinline{Eqrec_S}:
\begin{whycode}
Equality for Struct 'S'
tests/wp_acsl/record.c:20: typedef struct S { ... }
logic Eqrec_S: S,S -> prop
Equality for Struct 'T'
tests/wp_acsl/record.c:18: typedef struct T { ... }
logic Eqrec_T: T,T -> prop
Equality for Struct 'S'
tests/wp_acsl/record.c:20: Axiomatic Definition
axiom EqrecDef_S:
forall a:S.
forall b:S.
Eqrec_S(a, b)
<-> ( (get_a_S(a) = get_a_S(b))
and (get_p_S(a) = get_p_S(b))
and Eqrec_T(get_t_S(a), get_t_S(b)))
Equality for Struct 'T'
tests/wp_acsl/record.c:18: Axiomatic Definition
axiom EqrecDef_T:
forall a:T.
forall b:T.
Eqrec_T(a, b)
<-> (get_f_T(a) = get_f_T(b))
Symmetry of Equality for Struct 'S'
tests/wp_acsl/record.c:20: Axiomatic Definition
axiom EqrecSym_S: forall a:S.
Eqrec_S(a, a)
Symmetry of Equality for Struct 'T'
tests/wp_acsl/record.c:18: Axiomatic Definition
axiom EqrecSym_T: forall a:T.
Eqrec_T(a, a)
Symmetry of Equality for Struct 'S'
tests/wp_acsl/record.c:20: Axiomatic Definition
axiom EqrecTrans_S:
forall a:S.
forall b:S.
forall c:S.
Eqrec_S(a, b)
-> Eqrec_S(b, c)
-> Eqrec_S(a, c)
Symmetry of Equality for Struct 'T'
tests/wp_acsl/record.c:18: Axiomatic Definition
axiom EqrecTrans_T:
forall a:T.
forall b:T.
forall c:T.
Eqrec_T(a, b)
-> Eqrec_T(b, c)
-> Eqrec_T(a, c)
\end{whycode}
As an object of type \cinline{S} has a field of type \cinline{T},
the equality over objects of type \cinline{T} is also defined. Then
two objects of type \cinline{S} are equals iff the values their
field are equal two by two. \par
The same mechanism defines the equality on objects of an union type. \par
Two arrays of the same type $\tau$ and the same length are equals iff
their elements are equals one by one according to the relation
of equality of objects of type $\tau$.
Consider:
\begin{ccode}
typedef struct S { ...};
struct S tab[10];
\end{ccode}
The generated equality relation of object of type \cinline{struct S tab[10]}
is :
\begin{whycode}
Equality for S[10]
Logic array
logic Eqarr_S_10: S farray,S farray -> prop
Equality for S[10]
Axiomatic Definition
axiom EqarrDef_S_10:
forall a:S farray.
forall b:S farray.
Eqarr_S_10(a, b)
<-> (forall i:int. 0 <= i -> i < 10 -> Eqrec_S(a[i], b[i]))
\end{whycode}
\subsubsection{Set}
The logic \textsf{ACSL} $\tau$ sets are specified into
$\overline{\tau}$ \whyinline{set} with all traditional constructors,
functions and properties.
\subsubsection{Logic cast}
Logic functions \whyinline{as_int} and \whyinline{as_float}
are used to represent the type conversions between
basic arithmetic types that map to the same type of $\cal{L}$.
They also use the {\it format} presented in \ref{fig:type_format}.
At the moment, these functions are underspecified.
For \whyinline{as_int} for instance, we only assume that :
\begin{whycode}
forall f: int format. forall x:int. is_in_format (f, x) -> as_int (f, x) = x
forall f: int format. forall x:int. is_in_format (f, (as_int (f, x)))
\end{whycode}
Two other logic functions (\whyinline{truncate_real_to_int} and
\whyinline{real_of_int}) are used to transform $\mathbb{R}$ to and from $\mathbb{Z}$.
Other casts involving pointers are memory model dependent.
\subsection{\textsf{ACSL} predicates and axiomatics}
\TODO{To be complete}
src/plugins/wp/doc/manual/wp_hoare.tex deleted 100644 → 0
+ 0
− 117
View file @ 61311558
%% Chapter WP Models
\section{Hoare}\label{sec-hoare}
\subsection{Description and limitations}
The Hoare model is the traditional one where
the memory state is a mapping between the C program
variables and their logical values.
It has been extended a little to be able to deal which structures, arrays
and even with pointers as long as they are not used to make an indirect
access to
the memory because Hoare model doesn't have any idea of what is an address
in the memory. It means that the C dereferencing (*) operation is not handled
neither in the program, nor in the properties.
Another limitation about Hoare model is that it can provide only a limited
support about pointer validity (\whyinline{valid} ACSL predicate).
This is because memory allocation is not represented at this abstract level.
\subsection{Operations}
The Hoare model mainly uses logical operations from ACSL.
It only has to define few more
operations on pointers because even if it doesn't deal with indirect access,
it can still work on address computations~:
\begin{description}
\item \whyinline{m0_addr (X_x)} : represent the value of the address of the
variable x;
\item \whyinline{shift_field (p,f)} :
represent \cinline{\&(p->f)} where p
holds the address of a structure;
\item \whyinline{shift_ufield (p,f)} :
represent \cinline{\&(p->f)} where p
holds the address of a union;
\item \whyinline{shift_index (p,i)} : represent \cinline{\&((*p)[i])}
where p holds the address of an array;
\item \whyinline{shift_pointer (p,i)} : represent \cinline{(p+i)}
where p
can have any type. Notice that this is different from the previous
operation, because the result of this one has the same type than p.
\end{description}
\subsection{Examples}
Let's take some elementary transformation examples to better understand to
generated proof obligations.
\subsubsection{Simple variable assignment}
To check this assertion after the assignment:
\begin{ccode}
x = y+1;
//@ assert x > 0;
\end{ccode}
the proof obligation to satisfy before the statement would be :
\begin{whycode}
let x= (y+1) in (0 < x))
\end{whycode}
So this first example shows that for Hoare model,
the WP of a variable assignment is a variable substitution.
\subsubsection{Pointer assignment}
In Hoare model, a pointer is not different from a simple variable,
but computation on pointers uses the model specific operations defined before.
For instance, to check:
\begin{ccode}
p++;
//@ assert p == &(t[3]);
\end{ccode}
the proof obligation is:
\begin{whycode}
let p= shift_pointer(p,1) in (p = shift_index(m0_addr(X_t),3))
\end{whycode}
which should be equivalent to:
\begin{whycode}
p = shift_index(m0_addr(X_t),2)
\end{whycode}
% \TODO: check that we have the rules in hoare.why...
\subsubsection{Structure field assignment}
To check:
\begin{ccode}
s.a = x;
//@ assert s.a > 0 && s.b > 0;
\end{ccode}
the proof obligation is:
\begin{whycode}
let s= s[F_a->{x}] in (0 < {s[F_a]}) and (0 < {s[F_b]})
\end{whycode}
where we see the structure update for the field $a$.
When applying the access/update rules, this can be simplified to :
\begin{whycode}
(0 < x) and (0 < {s[F_b]})
\end{whycode}
\subsubsection{Array element assignment}
To check:
\begin{ccode}
t[0] = x;
//@ assert t[i] > 0;
\end{ccode}
the proof obligation is:
\begin{whycode}
let t= t[0->x] in (0 < t[i])
\end{whycode}
meaning that we want $0 < t[i]$ after an update of $t$. Because of access/update
rules, this is equivalent to:
\begin{whycode}
if (i == 0) then (0 < x) else (0 < t[i])
\end{whycode}
src/plugins/wp/doc/manual/wp_logicvar.tex deleted 100644 → 0
+ 0
− 113
View file @ 61311558
\section{Logic variables}\label{sec-funvar}
As previously presented, there is two kinds of memory models. One
based on variables, as in the Hoare model see section~\ref{sec-hoare}
and the other based on the representation of the heap, as the Store
model (see section~\ref{sec-store}) and the Runtime model (see
section~\ref{sec-runtime}).
The second kind of memory model is more expressive since it can handle
dereferencing of pointers, and addresses of variables.
The cost is quite heavy: the generated formula are largest.
The ideal is to benefit this expressiveness only for the variables
involved in dereferencing of pointers and address management, in
other words the variables such as their addresses are computed. For
the other variables, variables such as their addresses are never
computed (notice that they behave as functional or logical variables)
they can be handled by a model {\it à la} Hoare. This kind of
optimization, with a generous definition of optimization, is quite
current in memory model specifications and implementations.
In the WP, the model {\it à la} Hoare is the Logicvar model and
to make it cooperate with a based on heap memory model, one has to set
the {\tt -wp-logicvar}.
A variable translated in Logicvar has in $\cal{L}$ a logic type then
it is translated as \textsf{ACSL} data (see section~\ref{sec-acsl}).
Let us consider this example:
\begin{ccode}
typedef struct S { int a; int * p; };
struct S s;
struct S r;
/*@
ensures \result == {s \with .a = (int)4 };
*/
struct S ret_struct(void)
{
struct S * ps;
r.a = s.a ;
s.a = 4;
ps = &r;
return r;
}
\end{ccode}
This example has a semantics only in a based on heap memory model,
because the address of \whyinline{r} is taken. Computing the
proof obligation associated to the post-condition with the memory model
Store in the WP plug-in gives:
\begin{whycode}
goal store_full_ret_struct_post_1:
forall m:data farray.
forall ta:int farray.
global(ta)
-> (ta[X_ps] = 0)
-> is_fresh(m, ta, X_ps)
-> is_fresh(
m[addr(X_r,0)
<-encode(int_format,decode(int_format,m[addr(X_s,0)]))][addr(X_s,
0)
<-encode(int_format,4)][addr(X_ps,0)
<-encode(addr_format,addr(X_r,0))], ta_2[X_ps<-1][X_ps<-0], X_ps)
-> Eqrec_S(
decode(Cfmt_S,
access_range(
m[addr(X_r,0)
<-encode(int_format,decode(int_format,m[addr(X_s,0)]))][
addr(X_s,0)
<-encode(int_format,4)][addr(X_ps,0)
<-encode(addr_format,addr(X_r,0))],zrange(X_r,0,2))),
decode(Cfmt_S,
access_range(
m[addr(X_r,0)
<-encode(int_format,decode(int_format,m[addr(X_s,0)]))][
addr(X_s,0)
<-encode(int_format,4)][addr(X_ps,0)
<-encode(addr_format,addr(X_r,0))],zrange(X_s,0,2)))[F_a
<-encode(int_format,as_int(sint32_format,4))])
\end{whycode}
For each variable, a location is created into the heap. The local
variables trigger two local allocations for their locations. The three
assignments take place in the same $\cal{L}$ array, the store.
Unless expressing the address taken of \whyinline{r} and the address
assignment \whyinline{ps= &r;}, this is uninteresting to use the Store
model. Moreover, this assignment is heavy noise for the automatic
provers. Then, using Logicvar, the WP plug-in generates the formula:
\begin{whycode}
goal store_ret_struct_post_1:
forall m:data farray.
forall s:data farray.
Eqrec_S(
decode(Cfmt_S,
access_range(
m[addr(X_r,0)<-encode(int_format,decode(int_format,s[F_a]))],
zrange(X_r,0,2))),
s[F_a<-encode(int_format,4)][F_a
<-encode(int_format,as_int(sint32_format,4))])
\end{whycode}
Since the assignment \whyinline{ps= &r;} is {\it mute} for the post-condition,
the WP plug-in ignores it. Hence, only \whyinline{r} is represented into the
memory, the other variables are handled as logic variables.
src/plugins/wp/doc/manual/wp_models.tex
+ 0
− 6
View file @ f457a42f
......@@ -51,12 +51,6 @@ that are formal parameters of function passed by reference.
%% which is independent of the memory model. The translation of
%% the other part of \textsf{ACSL} is described into specific sections
%% for each kind of memory model.
%% \input{wp_acsl}
%% \input{wp_hoare}
%% \input{wp_store}
%% \input{wp_runtime}
%% \input{wp_logicvar}
% vim: spell spelllang=en
src/plugins/wp/doc/manual/wp_runtime.tex deleted 100644 → 0
+ 0
− 115
View file @ 61311558
%% Chapter WP Models
\section{Runtime}\label{sec-runtime}
\subsection{Description and limitations}
This model is a very low level one, where the memory is just a big array of bits
indexed by addresses. The values, represented by bit vectors
(\whyinline{bits}),
are stored in memory zones (\whyinline{rt_zone})
represented by a starting address, and a size (number of bits).
The \whyinline{rt_load(m, z)} operation returns the bits stored in the zone
\whyinline{z}
of the memory \whyinline{m}, and \whyinline{rt_store (m, a, b)} returns a memory similar to
\whyinline{m} except that the bits \whyinline{b} have been stored at the address
\whyinline{a}.
Operations \whyinline{rt_to_bits} and \whyinline{rt_from_bits} specify
how to interpret the bit vectors into typed values.
In simple cases, we don't need to go into representation details,
but it can be necessary when the C program uses some casts
and other architecture dependent features
such as endianness for instance.
This model also deals with memory management of variables
(see \whyinline{rt_valloc} and \whyinline{rt_vfree})
to be able to prove the validity of pointers,
but the dynamic allocations are not handled yet.
\subsection{Examples}
\subsubsection{Simple variable assignment}
Let's begin with the simple assignment example used in Hoare presentation.
To check this assertion after this statement:
\begin{ccode}
x = y+1;
//@ assert x > 0;
\end{ccode}
the proof obligation with the Runtime model is a lot more complex:
\begin{whycode}
forall ma:memalloc.
forall mb:memory.
let mb=
rt_store(mb,rt_vaddr(ma,X_x),
rt_to_bits(sint32_format,
(rt_from_bits(rt_load(mb,rt_vzone(ma,X_y)),sint32_format)+1))) in
(0 < rt_from_bits(rt_load(mb,rt_vzone(ma,X_x)),sint32_format))
\end{whycode}
First of all, we see that the memory state is represented by two variables:
$ma$ is used for allocation information, and $mb$ for the values (bits).
The last line is the translated initial property which say that if we read
(\whyinline{
rt_load}) in $mb$ the bits stored in the zone where $x$ is allocated
(\whyinline{
rt_vzone(ma,X_x)}), and if we interpret (\whyinline{rt_from_bits})
those bits as a signed 32 bit integer (which is the type of $x$),
then we should get a positive value.
The other lines represent the bit memory update (\whyinline{rt_store(mb,...)})
due to the assignment.
Trying to complete the proof, the Runtime model requires us to prove
that \cinline{(y+1)} still fits in the \whyinline{sint32_format} which hasn't
been requested by the Hoare model because of its abstraction level.
This condition is implied by the RTE generated annotations
that should be check separately (see \verb!-rte! option).
This example might look a little frightening because of the size of the proof
obligation compared to the size of the code, and that is precisely why
it is not advisable to use the Runtime model when its low level features are not
required. But we will see in \S\ref{sec-funvar} that in some simple cases,
such as this one, dramatic simplifications can be done.
\subsubsection{Simple variable allocation}
Runtime model defines the operation \whyinline{rt_valloc} to represent
a modification of the allocation information. So checking the assertion
\begin{ccode}
int x;
//@ assert \valid (&x);
\end{ccode}
gives the following the proof obligation:
\begin{whycode}
forall ma:memalloc.
let ma= rt_valloc(ma,X_x,32) in
rt_valid(ma, rt_vzone(ma,X_x))
\end{whycode}
which is trivially true according to Runtime properties.
Conversely, the operation \whyinline{rt_vfree} is used to represent
the deallocation. It makes possible to check this kind of property:
\begin{ccode}
{ int x; p = &x; }
//@ assert ! \valid (p);
\end{ccode}
That gives the following proof obligation:
\begin{whycode}
forall ma:memalloc.
forall mb:memory.
let ma1 = rt_valloc(ma,X_x,32) in
let mb= rt_store(mb,rt_vaddr(ma1,X_p),
rt_to_bits(rt_addr_format,rt_vaddr(ma1,X_x_0_1))) in
let ma2= rt_vfree(ma1,X_x_0_1) in
(not rt_valid(ma2,
rt_zone(rt_from_bits(rt_load(mb,rt_vzone(ma2,X_p)),rt_addr_format),32)))
\end{whycode}
but could be simplified, using Runtime rules, to:
\begin{whycode}
forall ma:memalloc.
let ma1 = rt_valloc(ma0,X_x,32) in
let ma2= rt_vfree(ma1,X_x) in
not rt_valid (ma2, rt_zone(rt_vaddr(ma1,X_x), 32))
\end{whycode}
which is true because, of course, a zone is not valid after having been freed.
src/plugins/wp/doc/manual/wp_store.tex deleted 100644 → 0
+ 0
− 524
View file @ 61311558
%% Chapter WP Models
\section{Store}\label{sec-store}
The Store memory model is the default model for the \textsf{WP}
plug-in. Heap values are stored in a global array. Pointer values are
translated to an index of this array.\par
In order to generate reasonable proof obligations, the values stored
in the global array are not the machine-ones, but the logic
ones. Hence, all \textsf{C} integer types are represented by
mathematical integers.\par
A consequence is that heterogeneous cast of pointers can not be
translated with this model. For instance, you can not cast a pointer
to \whyinline{int} into a pointer to \whyinline{char}, and then access to
the internal representation of an \whyinline{int} value in memory. In the
same flavor, the Store model does not support union.
The Store model specifies the memory state by two arrays.
\begin{enumerate}
\item A {\it store} (also called {\it memory}) represents the whole heap see
figure~\ref{fig:mem}. A store is an array of elementary cells
(indexed by an address)
containing encoded \whyinline{data}.
The \whyinline{data} are described in the
section~\ref{ssec-acsl-value}
\item An {\it allocation table} informs about the validity
of the access to these cells.
\end{enumerate}
\subsection{C variable representation}
The Store model associates to each C variable $x$ a base of address
\whyinline{base(x)}.
At the allocation of a variable $x$, the allocation table is updated
such as it associates to \whyinline{base(x)} the number \whyinline{n}
of cells corresponding to the type of $x$ (see figure~\ref{fig:sz_base}
and~\ref{fig:sz_compl}). The number $0$ denotes unallocated variables.
Then, the encoded value of $x$ is stored to a block of the {\it memory}
corresponding to the \whyinline{n} first cells starting from the index
\whyinline{addr(base(x),0)}. \par
When using the \whyinline{-wp-logicvar} option, some C variables can be
viewed as logic variables.
In such case, another representation (described in
section~\ref{sec-funvar}) is used.\par
\begin{figure}[ht!]
\begin{center}
\includegraphics[height=4cm]{mem}
\end{center}
\caption{The {\it memory}}
\label{fig:mem}
\end{figure}
\subsection{Addresses}\label{ssec-store-addr}
The constructor for addresses is:
\begin{description}
\item{\whyinline{addr(b,ofs)}} returns an integer (which represent
an address). This integer is computed from a base
\whyinline{b} and an offset \whyinline{ofs} (think about a binary
applicative constructor)
\end{description}
Two projections can be defined for such addresses:
\begin{description}
\item{\whyinline{base(x)}} returns the base of an address
\whyinline{x} such that:\\
\whyinline{axiom base_addr: forall b,ofs:int. base(addr(b,ofs)) = b}
\item{\whyinline{offset(x)}} returns the offset of an address
\whyinline{x} such that:\\
\whyinline{axiom offset_addr: forall b,ofs:int. offset(addr(b,ofs)) = ofs}
\end{description}
An address can be shifted:
\begin{description}
\item \whyinline{addr_shift(a,ofs)} returns an address shifted of \whyinline{ofs}
cells from the address \whyinline{a} such that \\
\whyinline{base (addr_shift(a,ofs)) = base(a)} and \\
\whyinline{offset (addr_shift(a,ofs)) = offset(a)+ofs}.
\end{description}
An address \whyinline{a} has to be converted into a logic pointer
(see section~\ref{ssec-acsl-ptr}):\whyinline{pointer_of_addr(a)} and a logic
pointer \whyinline{p} can, also, be converted into an address:
\whyinline{addr_of_pointer(p)}.
\subsection{Blocks and zones}\label{ssec-store-addrg}
An address is too weak to specify the place into the heap where a
value is stored.
\begin{figure}[ht!]
\begin{center}
\includegraphics[height=4cm]{size_base}
\end{center}
\caption{Typed representation of objects}
\label{fig:sz_base}
\end{figure}
The address of base specifies the first cell where the value is stored,
and a value is stored over a number of cells corresponding to the size of
this value (Think about some kind of C \whyinline{sizeof}, but more abstract.).
In the Store model, the size of values of basic types is $1$,
this is the case of the integer \whyinline{i},
the float \whyinline{f} and the pointer \whyinline{p} in the
figure~\ref{fig:sz_base}.
The size of a more complex value, such as an array and a record, is the
number of objects of which it is comprised.
The figure~\ref{fig:sz_compl} considers the following code:
\begin{ccode}
struct S
{ int f[2];
float g;
} ;
S s;
S t[2];
\end{ccode}
\begin{figure}[ht!]
\begin{center}
\includegraphics[height=4cm]{size_compl}
\end{center}
\caption{Typed representation of objects}
\label{fig:sz_compl}
\end{figure}
The representation of \whyinline{s} needs three cells in the {\it memory},
the representation of \whyinline{t} needs six cells, three for each
element.
\subsubsection{Blocks}\label{ssec-store-bloc}
The pair of an address and a
number of cells forms a block of {\it memory}.
The constructors of such bocks are:
\begin{description}
\item{\whyinline{zempty}} is the empty block. Nothing can be stored
there.
\item{\whyinline{zrange(b,ofs,n)}} represents the {\it memory} block
composed of the
\whyinline{n} cells starting from the address \whyinline{addr(b,ofs)}.
This block can be used to load and store records and arrays in the
{\it memory}.
\item \whyinline{zrange_of_addr(a)} returns the {\it memory} block
composed of one cell for a basic type at the address \whyinline{a}.
Its definition is: \\
\whyinline{zrange_of_addr(a) = zrange(base(a),offset(a),1)}.
\item \whyinline{zrange_of_addr_range(a,ofs,n)} returns the {\it memory}
block of \whyinline{n} cells from the address \whyinline{a}
shifted by \whyinline{ofs}.
Its definition is: \\
\whyinline{zrange_of_addr_range(a,ofs,n) = zrange(base(a),offset(a)+ofs,n)}.
\end{description}
Then, the validity of an address and the separation between two
addresses hang on the number of cells associated to the addresses:
\begin{description}
\item{\whyinline{valid(ta,a,n)}} holds iff all \whyinline{n} cells
from the address \whyinline{a} are included into the number of
cells associated to the \whyinline{base(a)} into the allocation
table \whyinline{ta}.
\item{\whyinline{separated_on_addr(a,n,a',n')}} holds iff there is no
overlap between the \whyinline{n} cells from \whyinline{a} and the
\whyinline{n'} cells from \whyinline{a'}.
\end{description}
\subsubsection{Zones}\label{ssec-store-zone}
The type \whyinline{zone} is defined as sets of
blocks. Blocks identify a number of adjacent cells related to an
address of base, and zones allow the identification of any partition
of the whole {\it memory}\/. \par
In the logic language $\cal{L}$, block constructs are promoted to
singletons of type \whyinline{zone}.
Just an union operator is necessary to build complex zones from zones
and/or blocks. Zones can be compared using classical set operators:
\begin{description}
\item{\whyinline{zunion(z,z')}} unions of two {\it memory} zones.
\item{\whyinline{included(z,z')}} holds if the {\it memory} zone
\whyinline{z} is included in the {\it memory} zone \whyinline{z'}.
\item{\whyinline{separated(z,z')}} holds if the {\it memory} zone \whyinline{z} does not
intersect the {\it memory} zone \whyinline{z'}. This operation is used for
the translation of \whyinline{\\separated} function of \textsf{ACSL}.
\end{description}
A zone equivalents to singleton is a particular zone since it defined a block which
can content as well as basic data than complex data as arrays and records of $\cal{L}$.
It is possible to recognize such zone:
\begin{description}
\item{\whyinline{is_bloc(z)}} holds if and only if it exists
\whyinline{x, ofs>0, n>0} such that \whyinline{z = zrange(base(x),ofs,n)}.
\end{description}
The validity of a location, the \textsf{ACSL} predicate
\cinline{valid(l)} is translated as \whyinline{valid(ta,addr_of(l),n)} when
\whyinline{n} is the number of cells of the location \whyinline{l}.
The separation of two location, the \textsf{ACSL} predicate
\cinline{separated(l,l')} is translated by
\whyinline{separated(zone_of(l),zone_of(l'))}
\subsection{Variable scope}
The allocation table informs about how many cells have
been allocated for each address of base.
As said in section~\ref{ssec-store-addrg}, querying the
allocation table defines the validity of an address for a number of
cells. It can also informs about the scope of variables. An unallocated
\whyinline{base(x)} is associated to $0$ cell into the allocation
table. \par
Moreover, we need a property over \whyinline{base(x)} parametrized
by a store and a allocation to hang on the bound of the C variable $x$
scope. Hence, the property \whyinline{is_fresh(m,ta,b)} means that all
addresses such as their base is \whyinline{b}, cannot be loaded into the
store \whyinline{m} and cannot be valid into \whyinline{ta}. \par
During a WP computation, the scope of different kinds of variables
is specified as follows:
\begin{description}
\item Global variables are marked as they are already allocated into
the initial allocation table,
\item Formal parameters are specified as they were out of the scope
of the initial memory configuration. Their scopes are open before
the precondition,
\item The local variables scopes are open after the precondition and are
closed before the post-condition.
\end{description}
Lets consider the following piece of code:
\begin{ccode}
int X;
/*@ requires \valid(p);
assigns *p;
ensures *p == X;
*/
void f (int *p)
{
int * q;
q=p;
*q = X;
}
\end{ccode}
Running the WP computation with the Store model we get the
following environment :
\begin{whycode}
Global 'X'
wp_store_ex.c:1: int X ;
function X_X () : int = 2
Local 'p'
wp_store_ex.c:7: int* p ;
function X_p () : int = 1
Local 'q'
wp_store_ex.c:9: int* q ;
function X_q () : int = 3
Global 'X'
wp_store_ex.c:1: Global allocation table
axiom Alloc_X: forall ta:int farray.
global(ta)
-> (ta[X_X] = 1)
\end{whycode}
For each C variable, a base is defined \whyinline{X_X,X_p,X_q}. The
axiom \whyinline{Alloc_x} specifies the global scope of the variable
\whyinline{X}. If we get the scope mark \whyinline{global(ta)} then
\whyinline{X} is valid in \whyinline{ta} and the size associated is
\whyinline{1}.
The WP computation for the post-condition produces the formula:
\begin{whycode}
forall m_0:data farray.
forall ta_0:int farray.
global(ta_0)
-> (ta_0[X_p] = 0)
-> is_fresh(m_0, ta_0, X_p)
-> (let ta_0= ta_0[X_p->1] in
valid(ta_0, {m_0[addr(X_p,0)]}, 1)
-> (ta_0[X_q] = 0)
-> is_fresh(m_0, ta_0, X_q)
-> (let ta_0= ta_0[X_q->1] in
let m_1= m_0[addr(X_q,0)->{{m_0[addr(X_p,0)]}}] in
let m_2= m_1[{m_1[addr(X_q,0)]}->{{m_1[addr(X_X,0)]}}] in
let ta_0= ta_0[X_q->0] in
is_fresh(m_2, ta_0, X_q)
-> (let ta_0= ta_0[X_p->0] in
is_fresh(m_2, ta_0, X_p)
-> ({m_2[{m_0[addr(X_p,0)]}]} = {m_2[addr(X_X,0)]}))))
\end{whycode}
First, the {\it memory} and the allocation table are introduced.
The first hypothesis, \whyinline{global(ta_0)},
triggers the axiom \whyinline{Alloc_X} and we have \whyinline{X}
already allocated in the initial allocation table.
The two next hypotheses:
\begin{whycode}
(ta_0[X_p] = 0)
-> is_fresh(m_0, ta_0, X_p)
\end{whycode}
say that the formal parameter \whyinline{p} is out of the scope of the
initial memory configuration: its base of address is not valid in the
allocation table and it cannot been loaded in the initial memory.
As formal parameters are in the scope of the precondition,
the allocation table has to be updated before the precondition computation.
After the precondition translation, the two hypotheses
\begin{whycode}
(ta_0[X_q] = 0)
-> is_fresh(m_0, ta_0, X_q)
\end{whycode}
state that the local variable \whyinline{q} is out of the scope of
the precondition and then the allocation table is updated before
formulating the body of the function.
Before asserting the post-condition, the scope of the local variable
is closed: the allocation table is updated and its address cannot be
loaded in the final memory. On the contrary, the scope of the formal
parameter is still open, since the formal parameters are in the scope
of the post-condition.
\subsection{The store operations}
The store is an array of \whyinline{data} indexed by addresses
(see figure~\ref{fig:mem} and section~\ref{ssec-acsl-rec}
for the logic records).
\subsubsection{Data}\label{ssec-acsl-value}
The store is specified into logic array of
\whyinline{data}, indexed by addresses. The type \whyinline{data} is a
common type representation for all types of values supported by the
\textsf{ACSL}. That means a field of type $\tau$ contains an object
of type \whyinline{data} in the representation of the
record. However, the value of a field of type $\tau$ must be
specified by an object of type $\tau$.
\subsubsection{Loading and assignment of basic objects}
As basic type object only needs one cell to be stored in the Store
model, loading/writing a value of a basic type are translated in
simple access/update from the store, but this value has to be
encoded/decoded as defined in section~\ref{ssec-acsl-rec}. The format
for integers and floats are thus defined in section~\ref{ssec-acsl-rec},
for store address, we specify the special format
\whyinline{addr_format}.
\subsubsection{Loading and assignment of records and arrays}
In the Store model, it is possible to load or assign records or
arrays using the combination of two steps.
First, loading and assignment of a block of \whyinline{data} in
the memory:
\begin{description}
\item{\whyinline{access_range(m,z)}} loads in one time a zone
\whyinline{z} in the memory \whyinline{m} and returns a
\whyinline{data}. Note that \whyinline{z} has to be
\whyinline{zrange(b,ofs,n)} with \whyinline{n >0} to make sense.
This is what ensured the predicate \whyinline{is_block(z)}.
\item{\whyinline{update_range(m,z,v)}} updates in one operation
the zone \whyinline{z} by the \whyinline{data} \whyinline{v}
in the memory \whyinline{m}, with \whyinline{is_block(z)}.
\end{description}
Secondly, decoding/encoding the data (involved in the first step)
with the format of the type of the object.
The two following example illustrate this mechanism.
Suppose this simple function:
\begin{ccode}
int t[4];
/*@ assigns t[1];
ensures t == {\old(t) \with [1] = (int)3};
*/
void modif_array(void)
{ t[1] =3;}
\end{ccode}
The generated output in $\cal{L}$ defines, at first, how to update
and access to indexed values of the array of $4$ int:
\begin{whycode}
axiom Loaded_int_4_idx:
forall m:data farray.
forall p:int.
forall i:int.
(0 <= i)
-> (i < 4)
-> (decode(Afmt_int_4,access_range(m,zrange_of_addr_range(p,0,4)))[i]
= decode(int_format,m[addr_shift(p,i)]))
axiom Updated_int_4:
forall m:data farray.
forall i:int.
forall e:int.
forall p:int.
(0 <= i)
-> (i < 4)
-> Eqarr_int_4(
decode(Afmt_int_4,
access_range(m[addr_shift(p,i)<-encode(int_format,e)],
zrange_of_addr_range(p,0,4))),
decode(Afmt_int_4,access_range(m,zrange_of_addr_range(p,0,4)))[i<-e])
\end{whycode}
Notice that the update definition requires the equality of array of
$4$ int (definition \whyinline{Eqarr_int_4}) defined in the
\textsf{ACSL} model see section~\ref{ssec-acsl-eq}. \par
In the Store model, the access to the whole array \whyinline{t} is the
\whyinline{data} loaded from a block of the store \whyinline{m},
starting from the address \whyinline{(p,0)} over $4$ cells :
\whyinline {access_range(m,zrange_of_addr_range(p,0,4))}. This
\whyinline{data} is decoded as an array of $4$ int. The axiom
\whyinline{Loaded_int_4_idx} expresses that accessing to the $i^{nth}$
index of this array is the same that accessing to the address of the
beginning of the array \whyinline{p} shifted by $i$ times the size of
\whyinline{int} (i.e. $1$ since int is a basic type).
The update operation is defined in the same flavor. \par
The postcondition is formulated as:
\begin{whycode}
goal store_full_modif_array_post_1:
forall m:data farray.
Eqarr_int_4(
decode(Afmt_int_4,
access_range(m[addr(X_t,1)<-encode(int_format,3)],zrange(X_t,0,4))),
decode(Afmt_int_4,access_range(m,zrange(X_t,0,4)))[1
<-as_int(sint32_format,3)])
\end{whycode}
Informally, it is to say that the array \whyinline{t} loaded in the memory
after having updated the cell at the address \whyinline{addr(X_t,1)}
with the \whyinline{data} encoding of the int \whyinline{3} is equal
to the updated array loaded in the memory
\whyinline{decode(Afmt_int_4,access_range(m,zrange(X_t,0,4)))} at
index \whyinline{1} with the \whyinline{data} encoding of the int
\whyinline{3}.\par
\whyinline{Afmt_int_4} is the format of array of $4$ int for the Store
model. The model Store generated its own format for each array
and record type. \par
In the case of a record, the same kind of definitions occurs but this
time, instead of generalize over all bound indexed (\whyinline{0 <= i}
and \whyinline{i < 4}) an axiom for loading and another for
storing are defined for each field of the record. \par
\subsection{The assigns clause specification}
The WP computation needs two different specifications of an assigns
clause:
\subsubsection{Assigns as a memory operation}
The memory operation \whyinline{update_havoc(m,z,v)} returns a memory
where all addresses contains in the zone \whyinline{z} contains a
\whyinline{data}. This function is quite similar than
\whyinline{update_range} at first glance. In fact, they are
different, \whyinline{z} can be any zone and the stored
\whyinline{x} is never encoded or decoded.
\subsubsection{Assigns as a property between two memory states}
In the Store model there are two different ways to express the assigns clause
as a goal:
\begin{description}
\item{Relational:} the predicate
\whyinline{is_havoc(ta_init,m_init,z,ta_fin,m_fin)} holds if
from the memory configuration \whyinline{(ta_init,m_init)} to
\whyinline{(ta_fin,m_fin)} excluded all addresses in the zone
\whyinline{z} nothing has changed.
% \item{Zone inclusions:} TODO Loïc... \whyinline{included(z_c,z_a)}
\end{description}
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