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

aplas: anonymisation and chunk size 2

parent 149444e4
......@@ -6,27 +6,27 @@
\label{sec:exp-hls}
\mypar{Implementation.}
The decision procedures presented are implemented as an extension of the \cspen\ solver~\cite{GuCW16}, called \cspenp, available at~\cite{CompSpenSite}.
Let us briefly recall some information about {\cspen}. {\cspen} is written in C++ and includes several decision procedures for symbolic heap fragments including
The decision procedures presented are implemented as an extension of the
\cspen\ solver~\cite{GuCW16},
called \cspenp, available at~\cite{CompSpenSite}.
%Let us briefly recall some information about {\cspen}.
{\cspen} is written in C++ and includes several decision procedures
for symbolic heap fragments including
(i) inductive predicates that are compositional~\cite{EneaSW15}
(the predicate $\ls{}(x,y)$ for list segments is a simple example)
and (ii) integer data constraints.
It uses SMT solvers (e.g., \textsc{Z3})
for solving linear integer arithmetic constraints.
\cspen\ ranked third among the eleven solvers in the general podium
of the last edition of SL-COMP, the competition of separation-logic solvers~\cite{SLCOMPsite}.
%\cspen\ ranked third among the eleven solvers in the general podium of
\cspen\ was ranked among the best solvers at
the last edition of SL-COMP, the competition of separation-logic solvers~\cite{SLCOMPsite}.
\cspenp\ %, as an extension of \cspen,
supports the new theory \slah.
%The \slah\ theory is defined by following the SMTLIB2 standard \cite{BarST-RR-10}.
% (the first one to our knowledge).
%Moreover, it allows a more general class of inductive definitions for $\hls{}$,
%where the chunk's header may include some information in a finite domain.
\cspenp\ supports the new theory \slah.
Internally, \cspenp\ parses the input file
which shall include the definition of $\hls{}$
(which fixes the size of the header to a constant which may be different from 2)
%ESOP 21 Reviewer 3: so this isn't built in specially? Or is it just that the tool expects the definition to be there because of the format? Does the definition have to be in syntactically exactly the form expected?
and the satisfiability or entailment queries in the SL-COMP format~\cite{SLCOMPsite}.
%~\cite{DBLP:conf/tacas/SighireanuPRGIR19}.
%
\begin{compactitem}
\item For satisfiability queries,
......@@ -82,8 +82,8 @@ classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as fo
\item MEM-SAT and MEM-ENT are satisfiability resp. entailment problems
generated by the verification of programs that are building blocks of heap-list based memory allocators, including:
create a heap-list with one element,
split a memory chunk into two consecutive memory chunks,
join two memory chunks,
split a memory chunk into two consecutive memory chunks (equivalent to cell insertion),
join two memory chunks (equivalent to cell delete),
search a memory chunk of size bigger than a given parameter (our running example),
or search an address inside a heap-list.
%
......@@ -93,7 +93,8 @@ classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as fo
we replace some $\hls{}$ atoms with their unfoldings in order to generate
formulas with more spatial atoms.
RANDOM-SAT includes also formulas where the atoms and their start
and end address terms are generated randomly. In addition, we generate some benchmarks manually.
and end address terms are generated randomly.
In addition, we generate some benchmarks manually.
This suite is motivated by testing the scalability of \cspenp.
%which usually contain more spatial atoms than those in MEM-SAT and MEM-ENT, motivated by testing the scalability of \cspenp.
\end{itemize}
......
......@@ -143,7 +143,7 @@ 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}.
We implemented the decision procedures on top of \cspen\footnote{We anonymize the name of the tool to comply with the double blind procedure.} 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.
......
......@@ -121,7 +121,7 @@ $s,h \models t_1 \pto t_2$ iff $\exists n\in\NN$ s.t.
\item
$s,h \models \hls{\ell+1}(t_1, t_2;t^\infty)$ iff
$s,h \models
\exists z\cdot 2 \le z-t_1 \land \Pi' : t_1\pto z-t_1\ \sepc
\exists z\cdot \kappa \le z-t_1 \land \Pi' : t_1\pto z-t_1\ \sepc
\blk(t_1+1,z) \sepc \hls{\ell}(z,t_2;t^\infty),
$
where if $t^\infty\equiv\infty$, then $\Pi'\equiv \top$, otherwise,
......@@ -149,8 +149,8 @@ Notice that the semantics of $\blk(x,y)$ differs from the one given in~\cite{Bro
because we consider that the location $y$ is the first after the last location in the memory block, as proposed in~\cite{CalcagnoDOHY06}.
%
Intuitively, an atom $\hls{}(x,y;v)$ with $v$ a variable
defines a heap lists where all chunks have sizes between $2$ and the value of $v$.
Notice that if $v < 2$ then the atom $\hls{}(x,y;v)$ has a model iff $x=y$.
defines a heap lists where all chunks have sizes between $\kappa$ and the value of $v$.
Notice that if $v < \kappa$ then the atom $\hls{}(x,y;v)$ has a model iff $x=y$.
%
With this semantics, the $\blk$ and $\hls{}$ predicates are compositional predicates~\cite{EneaSW15} and therefore they satisfy the following composition lemmas:
% \mihaela{r2 CADE}
......@@ -167,6 +167,9 @@ With this semantics, the $\blk$ and $\hls{}$ predicates are compositional predic
%with the absolute addressing $\blk(\ell,\ell')$ or
%with base-offset addressing $\blk(\ell, i, j)$ for the array from $\ell+i$ to $\ell+j-1$.
\noindent
For readability, we fix $\kappa=2$ in Eqns~(\ref{eq:hlsv-emp})--(\ref{eq:hlsv-infty}) in the remainder of the paper.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -128,7 +128,7 @@ and for which we define the following shorthand:
\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 :
\hls{}(x, y; v) & \Leftarrow \exists z \cdot \kappa \le z - x \le v :
x \pto z-x \sepc \blk(x+1,z) \sepc \hls{}(z,y; v)
\end{align}
The inductive definition states that a heap list from $x$ to $y$ is
......@@ -139,7 +139,7 @@ The inductive definition states that a heap list from $x$ to $y$ is
(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;
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.}
because the body can not be empty, the chunk's size is constrained to be $\ge \kappa$. For readability, we fix $\kappa=2$ in the following. Notice that 2 is the minimum value for the chunk's size of any heap list definition (i.e., the sum of sizes of the chunk's header and 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
......
......@@ -454,7 +454,7 @@ series = {ISMM 2020}
doi = {10.1007/978-3-319-41540-6_13}
}
@inproceedings{GuCW16,
@inproceedings{GuCW16X,
title = {A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints},
volume = {9706},
isbn = {978-3-319-40228-4 978-3-319-40229-1},
......@@ -510,17 +510,20 @@ series = {ISMM 2020}
}
@misc{CompSpenSite,
OPTauthor = {{CompSpen} github site},
title = {The {CompSpen} Solver},
OPTtitle = {The {CompSpen} Solver},
OPTyear = {2019},
note = {\url{https://github.com/suwy123/compspen2}}
OPTnote = {\url{https://github.com/suwy123/compspen2}},
title = {The XXX Solver},
note = {The GitHub address has been sent to chairs}
}
@misc{benchmark,
OPTauthor = {{CompSpen+} benchmarks},
title = {{CompSpen+} benchmarks},
OPTtitle = {{CompSpen+} benchmarks},
OPTyear = {2021},
note = {\url{https://github.com/suwy123/compspen2/tree/master/samples/PAsamples}}
OPTnote = {\url{https://github.com/suwy123/compspen2/tree/master/samples/PAsamples}},
title = {{XXX+} benchmarks},
note = {The GitHub address has been sent to chairs}
}
@inproceedings{EneaSW15,
......
......@@ -85,8 +85,10 @@
\newcommand{\fdom}{\mathtt{dom}}
\newcommand{\eub}{\mathtt{EUB}}
\newcommand{\cspen}{\textsc{CompSPEN}}
\newcommand{\cspenp}{\textsc{CompSPEN}$^+$}
%\newcommand{\cspen}{\textsc{CompSPEN}}
%\newcommand{\cspenp}{\textsc{CompSPEN}$^+$}
\newcommand{\cspen}{\textsc{XXX}}
\newcommand{\cspenp}{\textsc{XXX}$^+$}
%%%hide
\newcommand{\hide}[1]{ }
......
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