sat-hls.tex 10.1 KB
Newer Older
1
%!TEX root = atva2021.tex
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181

\section{Satisfiability problem of {\slah}}
\label{sec:sat-hls}

The satisfiability problem for an \slah\ formula $\varphi$ is to decide
whether there is a stack $s$ and a heap $h$ such that $s,h \models \varphi$.
In this section, we propose a decision procedure for the satisfiability problem, 
thus showing that the satisfiability problem is NP-complete.

\begin{theorem}\label{thm-sat}
The satisfiability problem of {\slah} is NP-complete.
\end{theorem}
The NP lower bound follows from that of ASL in \cite{BrotherstonGK17}. The NP upper bound is achieved by encoding the satisfiability problem of {\slah} as that of an existentially quantified Presburger arithmetic formula. The rest of this section is devoted to the proof of the NP upper bound.

Presburger arithmetic (\PbA) is the first-order theory with equality
of the signature $\langle 0,1,+, <\rangle$ interpreted over the
domain of naturals $\NN$ with `$+$' interpreted as the addition and 
`$<$' interpreted as the order relation.\footnote{%
Although `$<$' may be encoded using existential quantification in \PbA\ over naturals,
we prefer to keep it in the signature of \PbA\ to obtain quantifier free formulas.%
}
%The relations $\neq$, $\leq$ and $<$ may be encoded (using existential quantification) as well as multiplication by a constant.
%Reviewer 2 ESOP'21: < is not needed for PA over natural numbers, 
%as it can be derived: x < y iff exists z . x+z=y ^ x =/= y . 
% It would be needed for integers.
\PbA\ is a useful tool for showing complexity classes because its 
satisfiability problem belongs to various complexity classes depending
on the number of quantifier alternations~\cite{Haase2018ASG}.
Here, we employ the $\mathsf{\Sigma}_1$-fragment of \PbA, which
contains existentially quantified Presburger arithmetic formulas (abbreviated as \EPbA). The satisfiability problem of {\EPbA} is NP-complete.
%When the number of existentially quantified variables is fixed, 
%the problem is P-complete.
%Moreover, the existential fragment of \PbA\  
%extended with a divisibility relation ($\PbA_{\%}$) is still 
%decidable~\cite{Lipshitz78,Lipshitz81}, and known to be NP-hard and in NEXP.


%The pure part of \slah\ formulas is in \EPbA. %,
%Brotherston and Kanovich~\cite{BrotherstonK18} showed that even if 
%the pure formulas are difference constraints and
%the spatial formulas contain only points-to atoms,
%the satisfiability of ASL is still NP-complete.
%
%The NP upper bound of ASL is obtained by the encoding
%ASL formulas into equi-satisfiable {\EPbA} formulas.

We basically follow the same idea as ASL to build 
an {\EPbA} abstraction of a \slah\ formula $\varphi$, denoted by $\abs(\varphi)$,
that encodes its satisfiability: 
\begin{compactitem}
\item At first, points-to atoms $t_1 \pto t_2$ are transformed into $\blk(t_1, t_1+1)$. 
\item Then, the block atoms $\blk(t_1, t_2)$ are encoded by the constraint $t_1 < t_2$.
\item Also, the predicate atoms $\hls{}(t_1, t_2; t_3)$ are encoded by a formula in {\EPbA}, $\abs^+(\hls{}(t_1, t_2; t_3))$. 
\item Lastly, the separating conjunction is encoded by an {\EPbA} formula constraining the address terms of spatial atoms. 
\end{compactitem}
The Appendix~\ref{app:sat-hls} provides more details.
%
The crux of this encoding and 
its originality with respect to the ones proposed for ASL in~\cite{BrotherstonGK17}
is the computation of $\abs^+(\hls{}(t_1, t_2; t_3))$, 
which are the least-fixed-point summaries in \EPbA\ for $\hls{}(t_1, t_2; t_3)$.
In the sequel, we show how to compute them.

%Moreover, $\abs(\varphi)$ will be used as a basic ingredient of the entailment procedure in Section~\ref{sec:ent}. 

%We tackle this challenge by showing that an {\EPbA} formula can be computed for this purpose, although the summary is a non-linear formula at the first sight.

%by that we recall for self-containment here.
%	First, the spatial atoms other than block atoms are translated into $\blk{}$ atoms.
%	Second, the non-emptiness and the separation of block atoms is translated
%	into an {\EPbA} formula over the boundary terms in $\blk{}$ atoms.
%To exploit this idea, we have to encode the inductive predicate $\hls{}$ as
%	a block atom and an additional {\EPbA} formulas, which
%	poses the following challenge for the encoding: 
%	How to compute a least-fixed-point summary of the inductive definition of $\hls{}$.
%We tackle this challenge by showing that an {\EPbA} formula can be computed for this purpose, although the summary is a non-linear formula at the first sight.

%The crux of the aforementioned encoding is to compute $\abs^+(\hls{}(t_1, t_2; t_3))$, which are the least-fixed-point summaries of $\hls{}(t_1, t_2; t_3)$.

%
%ESOP'21 Reviewer 3: 4.1 could use a little "closing" text to summarise where we are now: I felt as though we had perhaps already seen the key idea behind the submission (of course, there is more to come); maybe you could reflect on the significance of the Lemma and lead into the next part.
%

%\subsection{{\EPbA} summary of $\hls{}$ atoms}
%\label{ssec:sat-hls-abs}
\smallskip
Intuitively, the abstraction of the predicate atoms $\hls{}(t_1, t_2; t_3)$
	shall summarize the relation between $t_1$, $t_2$ and $t_3$ 
	for all $k \ge 1$ unfoldings of the predicate atom.
From the fact that the pure constraint in the inductive rule of $\hls{}$ is $2 \le x' - x \le v$, it is easy to observe that 
for each $k \ge 1$, $\hls{k}(t_1, t_2; t_3)$ can be encoded by $2 k \le t_2-t_1 \le k t_3$. It follows that $\hls{}(t_1, t_2; t_3)$ can be encoded by $\exists k.\ k \ge 1 \wedge 2k \le t_2 - t_1 \le k t_3$.
If $t_3 \equiv\infty$, then $\exists k.\ k \ge 1 \wedge 2 k \le t_2-t_1 \le k t_3$ is equivalent to  $\exists k.\ k \ge 1 \wedge 2k \le t_2 - t_1$, thus an {\EPbA} formula.
Otherwise, $2 k \le t_2-t_1 \le k t_3$ is a non-linear formula since $k t_3$ is a non-linear term if $t_3$ contains variables. 
The following lemma states that 
%In the sequel, we are going to show that 
$\exists k.\ k \ge 1 \wedge 2 k \le t_2 - t_1 \le k t_3$ can actually be turned into an equivalent {\EPbA} formula.

\begin{lemma}[Summary of $\hls{}$ atoms]
Let $ \hls{}(x, y; z)$ be an atom in \slah\
representing a non-empty heap, where $x, y, z$ are three distinct variables in $\cV$.
%Then there is an {\EPbA} formula, denoted by $\abs^+(\hls{}(x,y; z))$, 
We can construct in polynomial time an {\EPbA} formula $\abs^+(\hls{}(x,y; z))$
which summarizes $\hls{}(x, y; z)$, namely we have 
for every stack $s$, $s \models \abs^+(\hls{}(x,y; z))$ iff 
there exists a heap $h$ such that $s, h \models \hls{}(x, y, z)$. 
%Similarly for $ \hls{}(x, y; \infty)$ and $ \hls{}(x, y; d)$ with $d \in \NN$.
\end{lemma}

\begin{proof}
The constraint that the atom represents a non-empty heap means that 
the inductive rule defining $\hls{}$ in Equation~(\ref{eq:hlsv-rec})
should be applied at least once. As explained above,
%we prove by induction (see Appendix~\ref{app:sat-hls})
%Notice that the semantics of this rule
%defines, at each inductive step,
%a memory block starting at $x$ and ending before $x'$ of size $x'-x$.
%By induction on $k \ge 1$, we obtain that $\hls{k}(x, y; z)$ defines
%a memory block of length $y-x$ such that 
%$2 k \le y-x \le k z$. Then 
$\hls{}(x, y; z)$ is summarized by the formula $\exists k.\ k \ge 1 \wedge 2k \le y -x \le kz$, which is a non-linear arithmetic formula.
%
However, the previous formula
%The formula $\exists k.\ k \ge 1 \wedge 2k \le y -x \le kz$ 
is actually equivalent to the disjunction of the two formulas corresponding to the following two cases:
\begin{compactitem}
\item If $2 = z$,  then $\abs^+(\hls{}(x, y; z))$ has as disjunct 
		$\exists k.\ k \ge 1 \land y -x = 2k$.
%
\item If $2 < z$, then we consider two sub-cases:
(a) If $k = 1$ 
	then $\abs^+(\hls{}(x, y; z))$ contains 
		$2 \leq y-x \le z$ as a disjunct.
(b) If $k \ge 2$ then we observe that the intervals 
	$[2k, k z]$ and $[2(k+1), (k+1) z]$
	overlap, 
	and consequently $\bigcup_{k \ge 2} [2k, kz] = [4, \infty)$.
	Therefore, $\abs^+(\hls{}(x, y; z))$ contains $4 \le y-x$ as a disjunct.
    %Therefore, $\bigcup \limits_{k \ge 2} [2k, kz] = [4, \infty)$, 
    %It follows that the formula 
    %$\exists k.\ k \ge 2 \land 2k \le y-x \le k z$ 
    %is equivalent to $4 \le y-x$. 
    %Therefore, $\abs^+(\hls{}(x, y; z))$ contains $4 \le y-x$ as a disjunct.
    Thus we obtain $2 < z ~\land~ \big(2 \leq y-x \le z \lor 4 \le y-x  \big)$, which can be simplified into $2 < z  ~\land~ 2 \le y - x$.
\end{compactitem}
To sum up, we obtain
\begin{align*}
\abs^+(\hls{}(x, y; z)) & \triangleq 
          \big(2 = z 
				 \land \exists k.\ k \ge 1 \land 2k = y-x \big) %\\
   %& \lor & \big(2 < z 
   ~\lor~ \big(2 < z
            \land 2 \le y - x
                          \big).
\end{align*}
\vspace{-2eX}\qed
\end{proof}

The formula $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1 \equiv r \bmod n$; the satisfiability of such formulas is still NP-complete. 
%We are using $\abs^+(\hls{}(x, y; z))$ defined above 
%to obtain in polynomial time an equi-satisfiable \EPbA\ abstraction for a symbolic heap $\varphi$, denoted by $\abs(\varphi)$.
Therefore, the satisfiability problem of \slah\ is in NP. 
%
% ESOP'21, Reviewer 3: At the end of page 10, when discussing the abstraction idea, I wondered to what extent this is related to the decision procedures for ASL itself; is the overall approach new, or is it a similar approach with suitable extensions?
%For this reason, we leave 
%the definition of $\abs(\varphi)$ and the proof of its correctness 
%stated by the following proposition 
%to Appendix~\ref{app:sat-hls}.
%
The correctness of $\abs(\varphi)$ is guaranteed by the following result.

%\vspace{-2mm}
\begin{proposition}\label{prop-sat-correct}
A \slah\ formula $\varphi$ is satisfiable iff $\abs(\varphi)$ is satisfiable.
\end{proposition}
%\vspace{-2mm}

%Notice that $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1 \equiv r \bmod n$. The satisfiability of such formulas is still NP-complete. 
From now on, we shall assume that {\bf $\abs(\varphi)$ is a quantifier-free \PbA\ formula containing modulo constraints}. This enables using the off-the-shelf SMT solvers, e.g. Z3, to solve the satisfiability problem of \slah\ formulas.