Commit 9dad2791 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

change abstract, intro and overview using ATVA reviewers suggestions

parent 51ef5a2d
......@@ -32,7 +32,7 @@ Double Blind
}
\date{}
%\authorrunning{W. Su, Z. Wu and M. Sighireanu}
\authorrunning{D. Blind}
\authorrunning{Double Blind}
\setlength{\parskip}{0eX}
......
......@@ -13,7 +13,7 @@ These decision procedures mostly focused on separation logic fragments called \e
The SH fragments comprise existentially quantified formulas that are
conjunctions of atoms encoding
aliasing constraints $x = y$ and $x \neq y$ between pointers $x$ and $y$,
points-to constraints $x\pto v$ expressing that at the address $x$ is stored the value $v$,
points-to constraints $x\pto v$ expressing that the value $v$ is stored at the address $x$,
and predicate atoms $P(\vec{x})$ defining (usually unbounded) memory regions of a particular structure. The points-to and predicate atoms, also called spatial atoms,
are composed using the separating conjunction to specify the disjointness of memory blocks they specify.
......
%!TEX root = aplas2021.tex
\section{\slah, a separation logic fragment for heap-list}
\section{\slah: a separation logic fragment for heap lists}
\label{sec:logic-hls}
This section defines the syntax and the semantics of
......
......@@ -34,6 +34,9 @@ and ends before the header of the next chunk.
%% Example search size
%\input{fig-ex-rsz}
\newcommand{\ponce}{8-14} %{4-9}
\newcommand{\pinva}{9-15} %{5-10}
\begin{figure}[t]
{\small
\centering
......@@ -41,11 +44,16 @@ and ends before the header of the next chunk.
\vspace{6mm}% Hack!! But does do the job
\lstset{language=C,numbers=left,stepnumber=1,fontadjust=true}
\begin{lstlisting}
int* hbeg; // heap start
int* hend; // heap end
int* search(int rsz) {
int* t = hbeg;
while (t < hend) {
/*@ requires: pre
@ ensures: postT
@ or postF
@*/
int* search(int* b,
int* e,
int rsz) {
int* t = b;
while (t < e) {
/*@ invariant: I */
int sz = *t;
if (rsz <= sz)
return t;
......@@ -61,12 +69,12 @@ int* search(int rsz) {
\texttt{pre} \label{eq:over-pre}
& \triangleq & 0 < b < e : \hls{}(b,e)
\\[2mm]
\texttt{path}_{\texttt{4-9}} \label{eq:over-path-once}
& \triangleq & 0 < b < e \land b = t \land sz_0 < rsz
\texttt{path}_{\texttt{\ponce}} \label{eq:over-path-once}
& \triangleq & 0 < b < e \land b = t \land sz < rsz
\\
& \land & sz_0 = t_1 - t \land 2 \le t_1 - t
& \land & sz = t_1 - t \land 2 \le t_1 - t
\nonumber \\
& : & t \pto sz_0 \sepc \blk(t+1, t_1) \sepc \hls{}(t_1,e)
& : & t \pto sz \sepc \blk(t+1, t_1) \sepc \hls{}(t_1,e)
\nonumber \\[2mm]
I \label{eq:over-inv}
& \triangleq & 0 < b < e \land b \le t
......@@ -74,17 +82,28 @@ I \label{eq:over-inv}
\nonumber
& : & \hls{}(b,t; rsz-1) \sepc \hls{}(t,e)
\\[2mm]
\texttt{post}_{\texttt{5-10}}(I) \label{eq:over-inv-once}
& \triangleq & 0 < b < e \land b\le t_0 < e \\
& \land & 2 \le sz_0 < rsz \land t - t_0=sz_0
\texttt{post}_{\texttt{\pinva}}(I) \label{eq:over-inv-once}
& \triangleq & 0 < b \le t_0 < t \le e \\
& \land & 2 \le sz < rsz \land t - t_0=sz
\nonumber \\
& : & \hls{}(b,t_0;rsz-1) \sepc t_0 \pto sz_0
& : & \hls{}(b,t_0;rsz-1) \sepc t_0 \pto sz
\nonumber \\
& & \sepc\ \blk(t_0+1,t) \sepc \hls{}(t,e)
\nonumber
\\[2mm]
\texttt{postT}\label{eq:over-postT}
& \triangleq & 0 < b \le r < t' \le e \\
& \land & rsz \le sz \land t'-r=sz
\nonumber \\
& : & \hls{}(b,r;rsz-1) \sepc r \pto sz
\nonumber \\
& & \sepc\ \blk(r+1,t') \sepc \hls{}(t',e)
\nonumber \\
\texttt{postF}\label{eq:over-postT}
& \triangleq & r=0 < b < e ~:~ \hls{}(b,e,rsz-1)
\end{eqnarray}
\end{minipage}
\vspace{-2eX}
%\vspace{-2eX}
\caption{Searching a chunk in a heap list
and some of its specifications in \slah}
\label{fig:search}
......@@ -96,8 +115,7 @@ and some of its specifications in \slah}
The right part of Figure~\ref{fig:search} provides
several formulas in the logic \slah\ defined in Section~\ref{sec:logic-hls}.
The formula \texttt{pre} specifies the precondition of \lst{search},
i.e., there is a heap list from \lst{hbeg} to \lst{hend}
represented by the logic variables $b$ resp. $e$.
i.e., there is a heap list from \lst{b} to \lst{e}.
The pure part of \texttt{pre} (left side of ':') is a linear constraint
on the addresses. The spatial part of \texttt{pre} (right side of ':') employs the
predicate $\hls{}$ defined inductively by the last two rules below
......@@ -120,7 +138,8 @@ The inductive definition states that a heap list from $x$ to $y$ is
The chunk stores its size $z-x$ in the header
(atom $x\pto z-x$).
The chunk's body is specified by a memory block atom, $\blk(x+1,z)$, starting
after the header and ending before the next chunk.
after the header and ending before the next chunk;
because the body can not be empty, the chunk's size is constrained to be $\ge 2$\footnote{The value 2 is a minimum value; any constant $\ge 2$ could be used, such that it is the sum of the header size and the minimal accepted size of the body.}
%This predicate belongs to the class
% defined in Section~\ref{sec:logic-hls} (Equations~(\ref{eq:hlsv-emp})--(\ref{eq:hlsv-rec})),
% which allows predicates to specify
......@@ -131,12 +150,12 @@ The parameter $v$ is an upper bound on the size of all chunks in the list.
%By convention, $\hls{}(x,y)$ is a shorthand for $\hls{}(x,y;\infty)$, i.e,
%the chunks' sizes are unconstrained from above.
The formula $\texttt{path}_{\texttt{4-9}}$ is generated by
The formula $\texttt{path}_{\texttt{\ponce}}$ is generated by
the symbolic execution of \lst{search}
starting from \texttt{pre} and
executing the statements from line 4 to 9.
It's satisfiability means that the line 9 is reachable from
a state satisfying \texttt{pre}.
executing the statements \ponce.
Its satisfiability means that the line 14 %9
is reachable from a state satisfying \texttt{pre}.
% (We use the SSA representation for the program and
% extend it with the logic variables introduced by
% the unfolding of the $\hls{}$ predicate):
......@@ -168,23 +187,23 @@ their end address denoted by $\atomtail(a)$ (e.g., $x+1$ resp. $y$).
For the points-to atom, this constraint is true,
but for the $\blk(x,y)$ atom, the constraint is
$x = \atomhead(a) < \atomtail(a) = y$.
Therefore, the spatial part of $\texttt{path}_{\texttt{4-9}}$ is translated
into the \PbA\ formula $\texttt{pb}^\Sigma_{\texttt{4-9}}$:
Therefore, the spatial part of $\texttt{path}_{\texttt{\ponce}}$ is translated
into the \PbA\ formula $\texttt{pb}^\Sigma_{\texttt{\ponce}}$:
%
\begin{align*}
\underbrace{t+1 < t_1}_{\blk{}(t+1,t_1)} & \land
\underbrace{(t_1 = e \lor 2 < e-t_1)}_{\hls{}(t_1,e)}.
\end{align*}
%
Alone, $\texttt{pb}^\Sigma_{\texttt{4-9}}$ does not capture the semantics of
Alone, $\texttt{pb}^\Sigma_{\texttt{\ponce}}$ does not capture the semantics of
the separating conjunction in the spatial part.
For that, we add a set of constraints
expressing the disjointness of memory blocks occupied by the spatial atoms.
For our example, these constraints are
$\texttt{pb}^\sepc_{\texttt{4-9}} \triangleq t_1 < e \le t ~\lor~ t+1 < t_1 \le e$.
By conjoining the pure part of $\texttt{path}_{\texttt{4-9}}$ with
formulas $\texttt{pb}^\Sigma_{\texttt{4-9}}$ and
$\texttt{pb}^\sepc_{\texttt{4-9}}$,
$\texttt{pb}^\sepc_{\texttt{\ponce}} \triangleq t_1 < e \le t ~\lor~ t+1 < t_1 \le e$.
By conjoining the pure part of $\texttt{path}_{\texttt{\ponce}}$ with
formulas $\texttt{pb}^\Sigma_{\texttt{\ponce}}$ and
$\texttt{pb}^\sepc_{\texttt{\ponce}}$,
we obtain an equi-satisfiable existentially quantified {\PbA} formula
whose satisfiability is a NP-complete problem.
......@@ -231,16 +250,17 @@ To illustrate a non-trivial case of the matching procedure used
we consider the verification condition (VC)
for the inductiveness of $I$.
The antecedent of the VC is the formula
$\texttt{post}_{\texttt{5-10}}(I)$ in Figure~\ref{fig:search},
$\texttt{post}_{\texttt{\pinva}}(I)$ in Figure~\ref{fig:search},
obtained by symbolically executing the path including the statements
at lines 5--7 and 9 starting from $I$.
The \PbA\ abstraction of $\texttt{post}_{\texttt{5-10}}(I)$ is satisfiable
at lines \pinva and 14 %
9 starting from $I$.
The \PbA\ abstraction of $\texttt{post}_{\texttt{\pinva}}(I)$ is satisfiable
and entails the following ordering constraint on the terms used by the spatial atoms:
$0 < b \le t_0 < t_0+1 < t \le e$.
The spatial atoms used in the antecedent and consequent
are ordered using the order given by this contraint as follows:
are ordered using the order given by this constraint as follows:
\[\begin{array}{lcc}
\textrm{antecedent:} & \hls{}(b,t_0;rsz-1) \sepc\ t_0 \pto sz_0 \sepc\ \blk(t_0+1,t)
\textrm{antecedent:} & \hls{}(b,t_0;rsz-1) \sepc\ t_0 \pto sz \sepc\ \blk(t_0+1,t)
& \sepc\ \hls{}(t,e) \\
\textrm{consequent:} & \hls{}(b,t;rsz-1) & \sepc\ \hls{}(t,e)
\end{array}\]
......@@ -249,7 +269,7 @@ The matching procedure starts by searching
a prefix of the sequence of atoms in the antecedent
that matches the first atom in the consequent, $\hls{}(b,t;rsz-1)$, such that
the start and end addresses of the sequence are respectively $b$ and $t$.
The sequence found is $\hls{}(b,t_0;rsz-1) \sepc t_0 \pto sz_0 \sepc \blk(t_0+1,t)$
The sequence found is $\hls{}(b,t_0;rsz-1) \sepc t_0 \pto sz \sepc \blk(t_0+1,t)$
which also satisfies the condition (encoded in \PbA)
that it defines a contiguous memory block between $b$ and $t$.
The algorithm continues by trying to prove the matching found
......@@ -257,8 +277,8 @@ The algorithm continues by trying to prove the matching found
and the unfolding of the atom $\hls{}(t_0,t;rsz-1)$.
%ESOP 21: "one unfolding" what determines that one makes *one* unfolding here, in terms of the (automatic) procedure?
The \PbA\ abstraction of the antecedent is used to ensure that
$sz_0$ is the size of the heap list starting at $t_0$, i.e., $sz_0=t-t_0$
and the constraint $2 \le sz_0 \le rsz-1$ is satisfied.
$sz$ is the size of the heap list starting at $t_0$, i.e., $sz=t-t_0$
and the constraint $2 \le sz \le rsz-1$ is satisfied.
For this ordering of terms (i.e., $0 < b \le t_0 < t_0+1 < t \le e$),
the algorithm is able to prove the matching. Since this ordering is the only one compatible with the {\PbA} abstraction of the antecedent, we conclude that the entailment is valid.
%The procedure continues with the remaining cases, until
......
Markdown is supported
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