Commit af3ca9c5 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

revisit intro and overview

parent 46a6db52
...@@ -149,7 +149,7 @@ on a set of formulas originating from path conditions and verification condition ...@@ -149,7 +149,7 @@ on a set of formulas originating from path conditions and verification condition
We also randomly generate some formulas, in order to test the scalability of {\cspenp} further. We also randomly generate some formulas, in order to test the scalability of {\cspenp} further.
The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (0.05 seconds for satisfiability and 2.57 seconds for entailment in average). The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (0.05 seconds for satisfiability and 2.57 seconds for entailment in average).
To the best of our knowledge, this work presents the first decision procedure and automated solver for entailment problems in a separation logic fragment allowing pointer arithmetic inside inductive definitions. To the best of our knowledge, this work presents the first decision procedure and automated solver for decision problems in a separation logic fragment allowing both pointer arithmetic and memory blocks inside inductive definitions.
%As mentioned before, the logic ASL was introduced in~\cite{BrotherstonGK17}, but it contains no inductive predicates. %As mentioned before, the logic ASL was introduced in~\cite{BrotherstonGK17}, but it contains no inductive predicates.
%As mentioned before, an extension of ASL with the classic singly linked list $\ls{}$ was considered in~\cite{DBLP:journals/corr/abs-1802-05935} %As mentioned before, an extension of ASL with the classic singly linked list $\ls{}$ was considered in~\cite{DBLP:journals/corr/abs-1802-05935}
% where the only inductive predicate is the classic singly linked list $\ls{}$. % where the only inductive predicate is the classic singly linked list $\ls{}$.
......
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
This section illustrates the use of the logic $\slah$ for the specification This section illustrates the use of the logic $\slah$ for the specification
of programs manipulating heap lists and of programs manipulating heap lists and
give an overview of the ingredients used by the decision procedures gives an overview of the ingredients used by the decision procedures
we propose. we propose.
Figure~\ref{fig:search} presents the motivating example. Figure~\ref{fig:search} presents the motivating example.
...@@ -99,20 +99,22 @@ The formula \texttt{pre} specifies the precondition of \lst{search}, ...@@ -99,20 +99,22 @@ The formula \texttt{pre} specifies the precondition of \lst{search},
i.e., there is a heap list from \lst{hbeg} to \lst{hend} i.e., there is a heap list from \lst{hbeg} to \lst{hend}
represented by the logic variables $b$ resp. $e$. represented by the logic variables $b$ resp. $e$.
The pure part of \texttt{pre} (left side of ':') is a linear constraint The pure part of \texttt{pre} (left side of ':') is a linear constraint
on the addresses, while the spatial part (right side of ':') employs the on the addresses. The spatial part of \texttt{pre} (right side of ':') employs the
predicate $\hls{}$ defined inductively by the following two rules: predicate $\hls{}$ defined inductively by the last two rules below
and for which we define the following shorthand:
% Equations~(\ref{eq:hls-0})--(\ref{eq:hls-rec}). % Equations~(\ref{eq:hls-0})--(\ref{eq:hls-rec}).
\begin{align} \begin{align}
\label{eq:hlsv-infty}
\hls{}(x, y) & \equiv \hls{}(x,y;\infty) \mbox{ i.e., no upper bound on chunks' size, where}
\\
\label{eq:hlsv-emp} \label{eq:hlsv-emp}
\hls{}(x, y; v) & \Leftarrow x=y : \emp \\ \hls{}(x, y; v) & \Leftarrow x=y : \emp \\
\label{eq:hlsv-rec} \label{eq:hlsv-rec}
\hls{}(x, y; v) & \Leftarrow \exists z \cdot 2 \le z - x \le v : \hls{}(x, y; v) & \Leftarrow \exists z \cdot 2 \le z - x \le v :
x \pto z-x \sepc \blk(x+1,z) \sepc \hls{}(z,y; v) \\ x \pto z-x \sepc \blk(x+1,z) \sepc \hls{}(z,y; v)
\label{eq:hlsv-infty}
\hls{}(x, y) & \equiv \hls{}(x,y;\infty) \mbox{ i.e., no upper bound on chunks' sizes}
\end{align} \end{align}
stating that a heap list from $x$ to $y$ is The inductive definition states that a heap list from $x$ to $y$ is
either an empty heap if $x$ and $y$ are aliased, either an empty heap if $x$ and $y$ are aliased (Eq.~(\ref{eq:hlsv-emp})),
or a \emph{chunk} starting at address $x$ and ending at or a \emph{chunk} starting at address $x$ and ending at
address $z$ followed by a heap list from $z$ to $y$. address $z$ followed by a heap list from $z$ to $y$.
The chunk stores its size $z-x$ in the header The chunk stores its size $z-x$ in the header
...@@ -162,7 +164,7 @@ For the empty case, the summary is trivially $x=y$. ...@@ -162,7 +164,7 @@ For the empty case, the summary is trivially $x=y$.
The other spatial atoms $a$ (e.g., $x \pto v$ and $\blk(x,y)$) The other spatial atoms $a$ (e.g., $x \pto v$ and $\blk(x,y)$)
are summarized by constraints on are summarized by constraints on
their start address denoted by $\atomhead(a)$ (e.g., $x$) and their start address denoted by $\atomhead(a)$ (e.g., $x$) and
their end address $\atomtail(a)$ (e.g., $x+1$ resp. $y$). their end address denoted by $\atomtail(a)$ (e.g., $x+1$ resp. $y$).
For the points-to atom, this constraint is true, For the points-to atom, this constraint is true,
but for the $\blk(x,y)$ atom, the constraint is but for the $\blk(x,y)$ atom, the constraint is
$x = \atomhead(a) < \atomtail(a) = y$. $x = \atomhead(a) < \atomtail(a) = y$.
...@@ -179,7 +181,7 @@ Alone, $\texttt{pb}^\Sigma_{\texttt{4-9}}$ does not capture the semantics of ...@@ -179,7 +181,7 @@ Alone, $\texttt{pb}^\Sigma_{\texttt{4-9}}$ does not capture the semantics of
For that, we add a set of constraints For that, we add a set of constraints
expressing the disjointness of memory blocks occupied by the spatial atoms. expressing the disjointness of memory blocks occupied by the spatial atoms.
For our example, these constraints are For our example, these constraints are
$\texttt{pb}^\sepc_{\texttt{4-9}} \equiv t < t_1$. $\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 By conjoining the pure part of $\texttt{path}_{\texttt{4-9}}$ with
formulas $\texttt{pb}^\Sigma_{\texttt{4-9}}$ and formulas $\texttt{pb}^\Sigma_{\texttt{4-9}}$ and
$\texttt{pb}^\sepc_{\texttt{4-9}}$, $\texttt{pb}^\sepc_{\texttt{4-9}}$,
...@@ -233,7 +235,7 @@ To illustrate a non-trivial case of the matching procedure used ...@@ -233,7 +235,7 @@ To illustrate a non-trivial case of the matching procedure used
obtained by symbolically executing the path including the statements obtained by symbolically executing the path including the statements
at lines 5--7 and 9 starting from $I$. at lines 5--7 and 9 starting from $I$.
The \PbA\ abstraction of $\texttt{post}_{\texttt{5-10}}(I)$ is satisfiable The \PbA\ abstraction of $\texttt{post}_{\texttt{5-10}}(I)$ is satisfiable
and entails the following constraint on the terms used by the spatial atoms: 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$. $0 < b \le t_0 < t_0+1 < t \le e$.
The spatial atoms used in the antecedent and consequent 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 contraint as follows:
...@@ -255,9 +257,10 @@ The algorithm continues by trying to prove the matching found ...@@ -255,9 +257,10 @@ The algorithm continues by trying to prove the matching found
and the unfolding of the atom $\hls{}(t_0,t;rsz-1)$. 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? %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 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., $t-t_0$ $sz_0$ is the size of the heap list starting at $t_0$, i.e., $sz_0=t-t_0$
and the constraint $sz_0 \le rsz-1$ is satisfied. and the constraint $2 \le sz_0 \le rsz-1$ is satisfied.
For this ordering, the algorithm is able to prove the matching. Since this ordering is the only possible ordering compatible with the {\PbA} abstraction of the antecedent, we conclude that the entailment is valid. 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 %The procedure continues with the remaining cases, until
% either a matching fails (the entailment is invalid) % either a matching fails (the entailment is invalid)
% or cases led to a matching (the entailment is valid). % or cases led to a matching (the entailment is valid).
......
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