Commit 85467b42 authored by ehilin02's avatar ehilin02
Browse files
parents fa95ba29 b71b8f52
......@@ -4,14 +4,16 @@
Pointer arithmetic is widely used in low-level programs, e.g. memory allocators.
%
%The verification of such programs usually requires simultaneous reasoning about pointer arithmetic and unbounded heap regions.
The verification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. heap lists, in memory allocators.
The specification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. heap lists in memory allocators.
%
In this work, we investigate a separation logic SLAH that allows pointer arithmetic inside inductive definitions, thus capable of specifying properties of programs manipulating heap lists.
In this work, we investigate decision problems for SLAH, a separation logic fragment
that allows pointer arithmetic inside inductive definitions,
thus enabling specification of properties for programs manipulating heap lists.
%a common data structure used in memory allocators.
%
Pointer arithmetic inside inductive definitions is challenging for automated reasoning.
%
We propose some new ideas to tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas.
We tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas.
%
The crux of our decision procedure for satisfiability is to compute summaries of inductive definitions. We show that although the summary is naturally expressed as an existentially quantified non-linear arithmetic formula, it can actually be transformed into an equivalent linear arithmetic formula.
%
......
......@@ -6,9 +6,9 @@
\mypar{Context.}
Separation Logic (SL, \cite{Reynolds:2002,OHearn19}), an extension of Hoare logic, is a well-established formalism for the verification of heap manipulating programs. SL features a \emph{separating conjunction operator} and \emph{inductive predicates}, which allow to express how data structures are laid out in memory in an abstract way. Since its introduction, various verification tools based on separation logic have been developed. A notable one among them is the INFER tool \cite{CD11}, which was acquired by Facebook in 2013 and has been actively used in its development process \cite{CDD+15}.
Decision procedures and constraint solvers for separation logic formulas are vital for the automation of the verification process.
Decision procedures for separation logic formulas are vital for the automation of the verification process.
%
These decision procedures and solvers mostly focused on separation logic fragments called \emph{symbolic heaps} (SH)~\cite{BerdineCO04}, since they provide a good compromise between expressivity and tractability.
These decision procedures mostly focused on separation logic fragments called \emph{symbolic heaps} (SH)~\cite{BerdineCO04}, since they provide a good compromise between expressivity and tractability.
%
The SH fragments comprise existentially quantified formulas that are
conjunctions of atoms encoding
......@@ -18,7 +18,7 @@ and predicate atoms $P(\vec{x})$ defining unbounded memory regions of a particul
are composed using the separating conjunction to specify the disjointness of memory blocks they specify.
Let us briefly summarize the results on the SH fragments in the sequel.
For the SH fragment with the list-segment predicate, arguably the simplest SH fragment, its satisfiability and entailment problems have been shown to be in PTIME~\cite{CookHOPW11} and efficient solvers have been developed for it~\cite{SLCOMPsite}.
For the SH fragment with the singly linked list-segment predicate, arguably the simplest SH fragment, its satisfiability and entailment problems have been shown to be in PTIME~\cite{CookHOPW11} and efficient solvers have been developed for it~\cite{SLCOMPsite}.
%
The situation changes for more complex inductive predicates:
The satisfiability problem for the SH fragment with a class of general inductive predicates was shown to be EXPTIME-complete~\cite{DBLP:conf/csl/BrotherstonFPG14}. On the other hand, the entailment problem for the SH fragment with slightly less general inductive predicates was shown to be 2-EXPTIME-complete~\cite{KatelaanMZ19,DBLP:conf/lpar/EchenimIP20}.
......@@ -143,13 +143,13 @@ The ordered entailment problem is then decided by matching each spatial atom in
Splitting a spatial atom into multiple ones in the antecedent is attributed to pointer arithmetic and unnecessary for SH fragments with nominal addresses.
%Moreover, the availability of $\hls{}$ makes the splitting more involved.
We implemented the decision procedures on top of \cspen\ solver~\cite{GuCW16,CompSpenSite}.
We evaluate the performance of the new solver, called {\cspenp},
We implemented the decision procedures on top of \cspen\ solver~\cite{GuCW16}.
We evaluate the performance of the new solver, called {\cspenp}~\cite{CompSpenSite},
on a set of formulas originating from path conditions and verification conditions of programs working on heap lists in memory allocators.
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).
To the best of our knowledge, this work presents the first decision procedures and automated solvers for separation logic fragments 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, 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{}$.
......
......@@ -20,7 +20,7 @@ and symbolic heaps $\varphi$ is given by the following grammar:
\begin{array}{l l l r}
t & ::= x \mid n \mid t+t &\ \ \ & \mbox{terms}
\\
\Pi & ::= t=t \mid t \ne t \mid t \leq t \mid t < t \mid \Pi \land \Pi &\ \ \ & \mbox{pure formulas}
\Pi & ::= \top \mid \bot \mid t=t \mid t \ne t \mid t \leq t \mid t < t \mid \Pi \land \Pi &\ \ \ & \mbox{pure formulas}
\\
\Sigma & ::= \emp \mid t \pto t \mid \blk(t, t) \mid \hls{}(t, t; t^\infty) \mid \Sigma \sepc \Sigma &\ \ \ & \mbox{spatial formulas}
\\
......@@ -42,7 +42,7 @@ the rules in Equations~(\ref{eq:hlsv-emp}) and (\ref{eq:hlsv-rec}),
where $v$ is a variable interpreted over $\NN\cup\{\infty\}$.
%Here we assume that $c \ge 2$ since $x \pto x'-x \sepc \blk(x+1,x')$ occurs in the body of Rule~(\ref{eq:hlsv-rec}).
An atom $\hls{}(x,y;\infty)$ is also written $\hls{}(x,y)$;
$\top$ and $\bot$ are shorthands for $x=x$ and $x\ne x$ atoms..
%$\top$ and $\bot$ are shorthands for $x=x$ and $x\ne x$ atoms..
Whenever one of $\Pi$ or $\Sigma$ is empty, we omit the colon.
We write $\fv(\varphi)$ for the set of free variables occurring in $\varphi$.
If $\varphi = \exists\vec{z}\cdot\Pi:\Sigma$,
......@@ -92,6 +92,7 @@ The satisfaction relation $s,h\models \varphi$,
where $s$ is a stack, $h$ a heap, and $\varphi$ a \slah\ formula,
is defined by: % structural induction on $\varphi$ as follows:
\begin{itemize}
\item $s,h \models \top$ always and never $s,h \models \bot$,
\item $s,h \models t_1 \sim t_2$ iff
$s(t_1) \sim s(t_2)$, where $\sim\in\{=,\ne,\le,<\}$,
%
......@@ -138,7 +139,7 @@ $s,h \models \exists\vec{z}\cdot\Pi:\Sigma$ iff $\exists \vec{n}\in\NN^{|\vec{z
\end{definition}
%\vspace{-2mm}
We write $A \models B$ for $A$ and $B$ sub-formula in \slah\ to mean
We write $A \models B$ for $A$ and $B$ (sub-)formula in \slah\ to mean
that $A$ entails $B$, i.e., that for any model $(s,h)$ such that $s,h\models A$
then $s,h\models B$.
......
......@@ -5,7 +5,7 @@
This section illustrates the use of the logic $\slah$ for the specification
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.
Figure~\ref{fig:search} presents the motivating example.
......@@ -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}
represented by the logic variables $b$ resp. $e$.
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
predicate $\hls{}$ defined inductively by the following two rules:
on the addresses. The spatial part of \texttt{pre} (right side of ':') employs the
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}).
\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}
\hls{}(x, y; v) & \Leftarrow x=y : \emp \\
\label{eq:hlsv-rec}
\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) \\
\label{eq:hlsv-infty}
\hls{}(x, y) & \equiv \hls{}(x,y;\infty) \mbox{ i.e., no upper bound on chunks' sizes}
x \pto z-x \sepc \blk(x+1,z) \sepc \hls{}(z,y; v)
\end{align}
stating that a heap list from $x$ to $y$ is
either an empty heap if $x$ and $y$ are aliased,
The inductive definition states that a heap list from $x$ to $y$ is
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
address $z$ followed by a heap list from $z$ to $y$.
The chunk stores its size $z-x$ in the header
......@@ -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)$)
are summarized by constraints on
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,
but for the $\blk(x,y)$ atom, the constraint is
$x = \atomhead(a) < \atomtail(a) = y$.
......@@ -179,12 +181,12 @@ Alone, $\texttt{pb}^\Sigma_{\texttt{4-9}}$ does not capture the semantics of
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}} \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
formulas $\texttt{pb}^\Sigma_{\texttt{4-9}}$ and
$\texttt{pb}^\sepc_{\texttt{4-9}}$,
we obtain an equi-satisfiable existentially quantified {\PbA} formula
whose satisfiability is NP-complete.
whose satisfiability is a NP-complete problem.
\smallskip
\noindent
......@@ -233,7 +235,7 @@ To illustrate a non-trivial case of the matching procedure used
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
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$.
The spatial atoms used in the antecedent and consequent
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
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., $t-t_0$
and the constraint $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.
$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.
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
% either a matching fails (the entailment is invalid)
% 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