Commit adfeda69 authored by ehilin02's avatar ehilin02
Browse files

section 5.2

parent 8d34b17a
......@@ -13,13 +13,13 @@ From~(\ref{eq:order}) and the definition of $\abs$, we have that
$C_\preceq \land \abs(\varphi)$ implies $\Pi'$,
so we simplify this entailment to deciding:
\begin{align*}
C_\preceq \wedge \Pi: a_1 \sepc \cdots \sepc a_m \models_\preceq b_1,
\Pi: a_1 \sepc \cdots \sepc a_m \models_\preceq b_1,
\end{align*}
where, the atoms $a_i$ ($i\in [m]$) and $b_1$ represent \emph{non-empty} heaps,
and the start and end addresses of atoms $a_i$ as well as those of $b_1$ are totally ordered by $C_\preceq$.
and the addresses $\atomhead(a_i)$ and $\atomtail(a_i)$ as well as $\atomhead(b_1)$ and $\atomtail(b_1)$ are totally ordered by $C_\preceq$.
Because $b_1$ defines a continuous memory region,
the procedure checks the following necessary condition in \PbA:
Since $b_1$ is either a points-to atom, or a block atom, or a $\hls{}$ atom, from their semantics, we know that $b_1$ defines a continuous memory region.
Therefore, the decision procedure checks the following necessary condition for the validity of $\Pi: a_1 \sepc \cdots \sepc a_m \models_\preceq b_1$:
%for the entailment $\varphi \models_\preceq \psi$ is
{\small
\begin{align*}
......@@ -44,7 +44,7 @@ $b_1 \equiv \hls{}(t_1, t_2; t_3)$, we distinguish between $m=1$ or not.
\myfpar{$a_1 \equiv t'_1 \pto t'_2$}
Then $\varphi \models_\preceq \psi$ does not hold, since a nonempty heap
modeling $b_1$ has to contain at least two memory cells.
modeling $b_1 \equiv \hls{}(t_1, t_2; t_3)$ has to contain at least two memory cells.
\myfpar{$a_1 \equiv \blk(t'_1, t'_2)$}
Then the entailment $\varphi \models_\preceq \psi$ does not hold
......@@ -69,7 +69,7 @@ Consider $x < y \wedge y -x = 4: \hls{}(x, y; 3) \models \hls{}(x, y; 2)$. The
The reason behind this seemly counterintuitive fact is that when we unfold $ \hls{}(x, y; 3)$ to meet the constraint $y - x = 4$, it is impossible to have a memory chunk of size $3$. (Actually every memory chunk is of size $2$ during the unfolding.)
\end{example}
We are going to show how to tackle this issue in the sequel.
We are going to show how to tackle this seemly counter-intuitive issue.
\begin{definition}[Unfolding scheme of a predicate atom and effective upper bound]
Let $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$ be an {\slah} formula and $s: \cV \rightarrow \NN$ be a stack such that $s \models \abs(\varphi)$ and $s(t'_2) - s(t'_1) \ge 2$.
......@@ -83,7 +83,7 @@ The \emph{effective upper bound} of $\varphi$ w.r.t. $s$, denoted by $\eub_\varp
Let $\varphi \equiv x < y: \hls{}(x, y; 3)$ and $s$ be a store such that $s(x)= 1$ and $s(y) = 7$. Then there are two unfolding schemes of $\varphi$ w.r.t. $s$, namely, $(2, 2, 2)$ and $(3,3)$, whose chunk size upper bounds are $2$ and $3$ respectively. Therefore, $\eub_\varphi(s)$, the effective upper bound of $\varphi$ w.r.t. $s$, is $3$.
\end{example}
The following lemma (proved in the appendix) states that
The following lemma (see proof in the appendix) states that
the effective upper bounds of chunks in heap lists atoms of $\varphi$
with respect to stacks %\mihaela{r3: not clear}
can be captured by a {\qfpa} formula.
......@@ -92,7 +92,7 @@ can be captured by a {\qfpa} formula.
For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a {\qfpa} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$ and $s[z \gets n] \not \models \xi_{eub,\varphi}(z)$ for all $n \neq \eub_\varphi(s)$.
\end{lemma}
The following lemma (proof in the appendix) provides the correct test used
The following lemma (see proof in the appendix) provides the correct test used
for the case $a_1 \equiv \hls{}(t'_1, t'_2; t'_3)$.
%for deciding the ordered entailment $\Pi: \hls{}(t'_1, t'_2; t'_3) \models_\preceq \hls{}(t_1, t_2; t_3)$ .
\begin{lemma}\label{lem-hls-hls}
......
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