# Verifying Heap-Manipulating Programs using Constrained Horn Clauses

Quang Loc Le  Singapore University of Technology and Design  ,  Jun Sun
Singapore University of Technology and Design  and  Shengchao Qin  School of
Computing, Teesside University- UK

###### Abstract.

Constrained Horn Clause (CHC) has recently emerged as a promising intermediate
language for program verification. Existing approaches focus only on non-
dynamic-heap programs and provide little support for reasoning about
dynamically linked data structures. In this work, we propose a CHC-based
system for verifying or falsifying safety properties of heap-manipulating
programs. Given a sequential C program annotated with assertions, our system
automatically generates a set of verification conditions for memory safety and
correctness of the assertions. These conditions are systematically encoded as
CHCs which are based on separation logic. Different from existing work, our
system is based on small-block encoding which effectively allows us to produce
concrete counterexamples as witness of safety violation. Furthermore, we
develop a novel decision procedure for satisfiability checking in order to
discharge the verification conditions. We have implemented our proposed
verification system and applied it to a set of heap-based benchmarks. The
experimental results show that our system is effective and efficient when
compared with state-of-the-art verifiers.

Software Verification ⋅ Constrained Horn Clauses ⋅ Satisfiability Solver ⋅
Separation Logic

††journalyear: 2017

##  1\. Introduction

Recently, there has been an increasing interest in logic-based systems
(Hoder:CAV:2011; Nikolaj:SMT:2012; DBLP:conf/birthday/BjornerGMR15;
export:180055; Grebenshchikov:PLDI:2012; Gurfinkel:CAV:2015), which provides a
genuine compound of multiple program verification techniques. The main benefit
is the separation of concerns, i.e., the same system can be extended to
support different programming language syntaxes, operational semantics or
verification algorithms. Given a program, a logic-based system partitions the
verification process into two phases: (1) generating verification condition
(VC) in the form of Constrained Horn Clause (CHC) from the source code and (2)
checking the satisfiability of the VC using logic-based decision procedures.
Different from other approaches (Cousot:POPL:1977; Clarke:1981:DSS;
King:1976:SEP), verification algorithms in logic-based systems are embedded in
the decision procedure. As a result, logic-based systems can automatically
take advantage of rapidly developing satisfiability checking engines,
especially Satisfiability Modulo Theory (SMT) solvers (Barrett:CAV:2011;
TACAS08:Moura). For examples, the logic-based systems reported in
(export:180055; Grebenshchikov:PLDI:2012; Gurfinkel:CAV:2015) have been shown
to effectively and efficiently verify a range of systems including Linux
device drivers and avionics software.

However, these logic-based systems provide little or no support for reasoning
about dynamically allocated data structures so far. Fundamentally, this is
because they rely on SMT solvers which are primarily based on first-order
logic and have not catered to the needs of heap-oriented logics. Automatically
verifying memory safety of heap-manipulating programs has been a core
challenge in software verification due to its high complexity. Loops and
recursive procedures in these programs may allocate (inherently) infinite sets
of reachable heaps which may form complex inductively linked data structures.
It is even more challenging when the program correctness additionally depends
on pure (non-heap) properties and data values stored in the allocated
structures.

There has been considerable progress on automated verification of heap-
manipulating programs over the past decades. Broadly speaking, existing
approaches can be classified into two categories. The first category of
verification tools, based on under-approximation, aims for bug identification,
i.e., they search for a witness which shows that a program is erroneous.
Example approaches in this category include program testing
(Herbert:SEFM:2015), symbolic execution (Braione:FSE:2015) and bounded model
checking (Wei:VMCAI:2014; Chalupa:TACAS:2016). The second category of
verification tools, based on over-approximation, aims for program
verification, i.e., they search for a proof of unsatisfiability to show that a
program is error-free. Techniques used in these tools include data flow
analysis (Sui:ISSTA:2012), abstract interpretation (CAV08:Yang;
Dudka:CAV:2011; Bouajjani:PLDI:2011), and deductive verification
(Cristiano:POPL:09; Chin:SCP:12; Loc:CAV:2014). Recently, there have been some
efforts to support both program verification and bug identification for heap-
manipulating programs. For examples, the work on spatial interpolant
(Aws:ESOP:2015), which assumes that a shape abstraction is given, constructs
an over-approximation and an under-approximation of the abstraction at the
same time. In addition, there are techniques based on hardwired abstraction
predicates which work only for specific data structures (e.g., list
(Itzhaky:CAV:2014; Aleksandr:CAV:2015; Ruzica:TACAS:2014;
Navarro:APLAS:2013)). These techniques are not designed for arbitrary data
structures.

In this work, we propose $\tt S2_{td}$, a fully-automated logic-based
verification system for verifying or falsifying arbitrary heap-manipulating
programs. Similar to existing approaches (Hoder:CAV:2011; Nikolaj:SMT:2012;
DBLP:conf/birthday/BjornerGMR15; export:180055; Grebenshchikov:PLDI:2012;
Gurfinkel:CAV:2015), $\tt S2_{td}$ proceeds in two phases. In the first phase,
it precisely transforms an input program into an intermediate representation
using a newly designed symbolic executor. In particular, we extend CHC to
support a fragment of separation logic (Ishtiaq:POPL01; Reynolds:LICS02) and
serve as the language for the intermediate representation. Separation logic is
a well-established formalism for reasoning about heap-manipulating programs.
It provides concise and precise notations for specifying pointer-based
programs and their data structures. Different from the work presented in
(Loc:CAV:2016; Gurfinkel:CAV:2015) where large-block encoding
(Dirk:FMCAD:2009) is used, our approach employs small-block encoding to
support not only program verification but also bug identification.

One particular challenge of using separation logic to encode VC of heap-
manipulating programs is that the negation operator over spatial formulae in
separation logic is not well defined. Consider, for instance, that a given
program contains a statement $\tt if(COND)~{}{\small{\tt ERROR();}}$ where
$\tt COND$ could be like “$x$ has not been allocated”, our symbolic executor
needs to generate VC for both memory safety (in which case the negation of
$\tt COND$ is satisfied) and the erroneous condition (in which case $\tt COND$
is satisfied). Since the negation operator over spatial formulae in separation
logic is not well defined, the VC may not be determined. Our remedy to the
problem is based on the observation that safety on memory properties (e.g.,
null pointer de-referencing or pointer double-free) is often evaluated on
individual pointers. Hence, to overcome the aforementioned problem we define
the negation operator over size-1-heap formulae (i.e. those formulae with heap
size at most one). Given that a pointer-typed variable is either allocated and
points to an object, or is assigned to $\tt NULL$, or has neither been
allocated nor been de-allocated (and not assigned $\tt NULL$) in a program, it
always refers to at most one object at any time. Our novel proposal on
negating size-1-heap formulae is thus sufficient to encode memory safety
properties.

After the first phrase, $\tt S2_{td}$ has reduced the verification problem
into a satisfiability problem. In the second phase, $\tt S2_{td}$ solves the
satisfiability problem using a novel decision procedure, called
$\tt{S2SAT_{eSL}}$. $\tt{S2SAT_{eSL}}$ supports a combination of multiple
techniques: under-approximation, over-approximation, and induction reasoning.
$\tt{S2SAT_{eSL}}$ is sound for both satisfiability ($\tt SAT$) and
unsatisfiability ($\tt UNSAT$) checking. To check the satifiability of a
formula, $\tt{S2SAT_{eSL}}$ iteratively constructs a series of unfolding trees
by unfolding the inductive predicates in the formula. After each unfolding,
$\tt{S2SAT_{eSL}}$ attempts to establish that the formula is $\tt SAT$ by
showing that an under-approximation of the formula is $\tt SAT$, or to
establish that the formula is $\tt UNSAT$ by showing that an over-
approximation is $\tt UNSAT$. Moreover, it actively searches for a cyclic
proof so that no further unfolding is necessary. For efficiency, we enhance
$\tt{S2SAT_{eSL}}$ with memorization and slicing at the logical level
(Chin:CAV:2011). We prove that $\tt{S2SAT_{eSL}}$ always terminates for a
fragment of separation logic where the constraints over arithmetical
parameters of inductive predicates are restricted to periodic relations
(Marius:CAV:2010; Makoto:APLAS:2016). As a result, $\tt{S2SAT_{eSL}}$ is shown
to be a decision procedure. We remark that $\tt{S2SAT_{eSL}}$ is useful for
other program analysis tasks as well, e.g., frame inference
(Loc:2016:S2ENT:TR) and termination analysis (Brotherston-Gorogiannis:14).

### Contribution

In short, we make the following main contributions in this work.

  * •

We propose a new approach to verifying or falsifying safety properties of
heap-manipulating programs, based on automatically encoding VC in CHC. We
generate counter-examples to witness a falsified property.

  * •

We present a satisfiability solver $\tt{S2SAT_{eSL}}$ for CHC. We show that
$\tt{S2SAT_{eSL}}$ always terminates for formulae where the arithmetic
properties over parameters of inductive predicates are restricted to periodic
relations.

  * •

We have implemented our approach in a prototype system and have evaluated it
on a set of heap-manipulating programs.

### Organization

The remainders of the paper are organized as follows. Section 2 defines an
assertion language. Section 3 illustrates our approach using an example.
Section 4 then shows the first part of our approach, i.e., encoding VC in CHC.
Section 5 then presents a decision procedure for solving the VC. Section 6
contains correctness analysis of our approach. Section 7 presents an
implementation of our approach and evaluates its effectiveness. Section 8
discusses related work and we conclude in Section 9. Proofs of lemmas and
theorems in this paper are presented in the Appendix.

##  2\. Assertion Language

In this section, we present the intermediate language used to encode programs
as CHC. This language is base on separation logic (Ishtiaq:POPL01;
Reynolds:LICS02) and supports inductive predicates and arithmetic.

In the concrete heap models, we assume there are a fixed finite collection of
data structures Node, a fixed finite collection of fields Fields, a disjoint
set Loc of locations (heap addresses), a set of non-address values Val, such
that ${{\small{\tt null}}}{\in}{\textit{Val}}$ and Val $\cap$ Loc
=$\emptyset$. In addition, we assume a finite set of inductive predicates
$\tt\mathcal{P}$. The syntax is presented in Figure 1. A formula $\Phi$ is a
disjunction of symbolic heap $\Delta$ where each disjunct is used to model one
program path derived from branching statements, e.g. $\tt if$ and $\tt while$.
A symbolic heap $\Delta$ is an existentially quantified formula which consists
of a spatial constraint $\kappa$ and a pure (non-heap) constraint $\pi$. It
may be annotated with $@\overline{{\tt E}}$ to state that the heap of the
formula is not empty. All free variables are implicitly universally quantified
at the outermost level.

$\begin{array}[]{rcl}\Phi&{~{}::=}&{\small{\tt true}}\,~{}|~{}{\small{\tt
false}}\,\mid\Delta\mid\Phi_{1}{\vee}\Phi_{2}\\\
\Delta&{~{}::=}&\exists\bar{v}{\cdot}~{}(\kappa{\wedge}\pi)~{}|~{}\exists\bar{v}{\cdot}~{}(\kappa{\wedge}\pi)@\overline{{\tt
E}}\\\ \kappa&{~{}::=}&{\tt
emp}~{}|~{}{x}{{\scriptsize\mapsto}}c(f_{i}{:}v_{i})~{}|~{}{\small{\tt
P}}(\bar{v})~{}|~{}\kappa_{1}{*}\kappa_{2}\\\
\pi&{~{}::=}&\pi_{1}{\wedge}\pi_{2}~{}|~{}\pi_{1}{\vee}\pi_{2}~{}|~{}\neg\pi_{1}\mid\exists
v{\cdot}~{}\pi_{1}\mid\textit{b}\mid\alpha\mid\phi~{}|x{\not\hookrightarrow}\\_\\\
\textit{b}&{~{}::=}&{\small{\tt true}}\,~{}|~{}{\small{\tt false}}\,\mid
v\mid\textit{b}_{1}{=}\textit{b}_{2}\\\
\alpha&{~{}::=}&v_{1}{=}v_{2}~{}|~{}v{=}{{\small{\tt null}}}\\\
\phi&{~{}::=}&a_{1}{=}a_{2}\mid a_{1}{\leq}a_{2}\\\
a&{~{}::=}&~{}k^{{\small{\tt int}}}\mid v\mid k^{{\small{\tt
int}}}{\times}a\mid
a_{1}{+}a_{2}\mid-a\mid\textit{max}(a_{1},\\!a_{2})\mid\textit{min}(a_{1},\\!a_{2})\\\
\end{array}$ Figure 1. Fragment of Separation Logic

A spatial formula is either the predicate ${\tt emp}$, a points-to predicate
${x}{{\scriptsize\mapsto}}c(f_{i}{:}v_{i})$ (where $c{\in}{\textit{Node}}$ and
$f_{i}{\in}{\textit{Fields}}$), an inductive predicate instance ${\small{\tt
P}}(\bar{v})$ \- an occurrence of the inductive predicate $\tt P$ where
${\small{\tt P}}{\in}{\small{\tt\mathcal{P}}}$ \- or their spatial
conjunction. Predicate ${\tt emp}$ asserts an empty heap. Predicate
${x}{{\scriptsize\mapsto}}c(f_{i}{:}v_{i})$ asserts that the pointer $x$
points to singly allocated heap typed $c$ with content $f_{i}{:}v_{i}$. When
there is no ambiguity, we discard $f_{i}$ and simply write the short form
${x}{{\scriptsize\mapsto}}c(v_{i})$. The predicate instance ${\small{\tt
P}}(\bar{v})$ is an instance of a user-defined predicate $\tt P$. Intuitively,
it represents an (infinite) set of allocated objects which are defined by
predicate $\tt P$. We note that each predicate instance is used to encode a
method invocation; and to capture the ordering of those invocations, our
system automatically annotates each instance a superscript $o$ and subscript
$u$ as ${\small{\tt P}}(\bar{v})^{o}_{u}$. These annotations are for context-
and flow- sensitive analysis; where $o$ captures the ordering of method
invocation, and $u$ captures the unfolding number of a method. While $o$ is
annotated by the symbolic execution engine, $u$ is initially annotated (with
0) by the engine and updated by the satisfiability solver. The spatial
conjunction $\kappa_{1}{*}\kappa_{2}$ asserts that a given heap can be
decomposed into two disjoint regions and the formulas, $\kappa_{1}$ and
$\kappa_{2}$, hold respectively and separately in the two memory regions.

A pure formula can be a boolean formula $b$, an equality constraint $\alpha$,
a formula in Presburger arithmetic $\phi$, a pointer constraint
$x{\not\hookrightarrow}\\_$, or a boolean combination of them. The predicate
$x{\not\hookrightarrow}\\_$ states that $x$ is a dangling pointer, i.e., $x$
is not yet allocated or is already deallocated. We use $v_{1}{\neq}v_{2}$
(resp., $v{\neq}{{\small{\tt null}}}$) as short forms for
$\neg(v_{1}{=}v_{2})$ (resp., $\neg(v{=}{{\small{\tt null}}})$). ${\tt res}$
is a reserved variable to denote the returned value of each procedure. A
formula defined in Fig. 1 is said to be a base formula if it does not contain
any inductive predicates. Note that in our definition, a pure formula, which
could be a pointer constraint $x{\not\hookrightarrow}\\_$, can be negated.
This is necessary in order to encode the VC of a given program. The negation
of spatial formula in separation logic is in general not well defined. We
observe that a pointer $x$ always satisfies one of the following three
predicates: $x{=}null$, $x{\not\hookrightarrow}\\_$ (i.e., $x$ is dangling),
and ${x}{{\scriptsize\mapsto}}c(f_{i}{:}v_{i})$ (i.e., it points to some heap
object). Based on the above observation, we define the negation for pointer
constraints (i.e., size-1-heap formulae) as follows.

$\begin{array}[]{rcl}\neg({x}{{\scriptsize\mapsto}}c(f_{i}{:}v_{i}))&{\equiv}&x{=}{{\small{\tt
null}}}~{}{\vee}~{}x{\not\hookrightarrow}\\_\\\ \neg(x{=}{{\small{\tt
null}}})&{\equiv}&{x}{{\scriptsize\mapsto}}c(f_{i}{:}v_{i})~{}{\vee}~{}x{\not\hookrightarrow}\\_\\\
\neg(x{\not\hookrightarrow}\\_)&{\equiv}&x{=}{{\small{\tt
null}}}~{}{\vee}~{}{x}{{\scriptsize\mapsto}}c(f_{i}{:}v_{i})\end{array}$

In our assertion language, we allow user-defined inductive predicate of the
form ${\small{\tt P}}(\bar{t})$. In general, ${\small{\tt P}}(\bar{t})$ is
defined as: ${\tt pred}~{}{\small{\tt
P}}(\bar{t})~{}{\equiv}\bigvee^{n}_{i=1}({\exists}\bar{w_{i}}{\cdot}~{}\Delta_{i}{:}l_{i})$
where $\bar{t}$ is a set of formal parameters;
$\exists\bar{w_{i}}{\cdot}\Delta_{i}{:}l_{i}$ (i $\in$ 1…n}) are definition
rules (branches), $l_{i}$ are path labels of the rules; Each inductive
predicate is generated automatically an over-approximated invariant, a pure
constraint representing a superset of all possible models of the predicate.
Each branch corresponds to a path in the program. The path label $l_{i}$ is a
sequence of controls at the branching statements. This label $l_{i}$ is used
to generate the witness for program errors. We use 1 to label the branch which
satisfies conditions of branching statements (e.g., $\tt then$ branch) and use
2, otherwise (e.g., $\tt else$ branch). In each definition rule, we require
that variables that are not formal parameters must be existentially
quantified, i.e. $\forall
i{\in}\\{1...n\\}{\cdot}\textit{FV}({\Delta_{i}}){=}\bar{t}$ and
$\bar{w_{i}}{\cap}\bar{t}{=}\emptyset$ where $\textit{FV}({\Delta})$ are all
free variables in the formula $\Delta$. In the following, we apply the
language to model AVL trees ($\tt avl$) with the data structure $\tt node2$
declared as: $\tt struct$ $\tt
node2~{}\\{{~{}node2~{}{*}left};{~{}node2~{}{*}right};\\}$

$\begin{array}[]{lcl}{\small{\tt pred}}~{}{\small{\tt avl({\tt
root}{,}n{,}h)}}&\equiv&{\small{\tt{\tt emp}}}\wedge{\small{\tt{\tt
root}{=}{{\small{\tt null}}}}}\wedge{\small{\tt n{=}0}}\wedge{\small{\tt
h{=}0:[1]}}~{}~{}{\vee}\\\
&&{\small{\tt~{}{\exists}~{}l,r,n_{1},n_{2},h_{1},h_{2}{\cdot}{\tt
root}{\mapsto}node2(l,r)*avl(l,n_{1},h_{1})*avl(r,n_{2},h_{2})\wedge}}\\\
&&\qquad{\small{\tt n{=}n_{1}{+}n_{2}{+}1\wedge
h{=}max(h_{1}{,}h_{2}){+}1\wedge{-}1{\leq}h_{1}{-}h_{2}{\leq}1:[2]}}\end{array}$

### Semantics

Formulas of our separation logic fragment are interpreted over pairs ($s$,$h$)
where $s$ models the program stack and $h$ models the program heap. Formally,
we define:

$\begin{array}[]{lcllcl}{\textit{Heaps}}&{\overset{\text{\scriptsize{def}}}{=}}&{\textit{Loc}}{\rightharpoonup_{fin}}({\textit{Node}}~{}{\rightarrow}~{}\textit{Fields}~{}{\rightarrow}~{}\textit{Val}\cup\textit{Loc})\\\
{\textit{Stacks}}&{\overset{\text{\scriptsize{def}}}{=}}&{\textit{Var}}~{}{\rightarrow}~{}\textit{Val}\cup\textit{Loc}\end{array}$

The semantics of a formula $\Phi$ is defined by a satisfaction relation:
$s,h\models\Phi$ that forces the stack $s$ and heap $h$ to satisfy the
constraint $\Phi$ where $s\in{\textit{Stacks}}$ and $h\in{\textit{Heaps}}$. In
our system, pure domains include integer domain ($\tt Ints$), and boolean. The
evaluation for pure expressions are determined by valuations as follows:

${s}(a)~{}{\in}~{}{\small{\tt
Ints}}\qquad{s}(\textit{b})~{}{\in}~{}\\{{\small{\tt true}}\,,{\small{\tt
false}}\,\\}$

The semantics is presented in Fig. 2 where the semantics for pure formulas is
omitted.

$\begin{array}[]{rcl}s,h{\models}{\tt emp}&{\small{\tt
iff}}{}&h{=}\emptyset\\\
s,h{\models}{v}{{\scriptsize\mapsto}}c(f_{1}{:}v_{1},..,f_{n}{:}v_{n})&{\small{\tt
iff}}{}&l{=}s(v),\text{dom}(h){=}\\{l\\}{\wedge}h(l){=}r\mbox{ and
}r(c{,}f_{i}){=}s({v_{i}})\mbox{ for }1{\leq}i{\leq}n\\\ s,h\models{\small{\tt
P}}(\bar{t})&\small{\tt iff}{}&s,h\models{\small{\tt P}}(\bar{t})^{m}\text{
for some }m{\geq}0\\\ s,h\models{\small{\tt P}}(\bar{t})^{k{+}1}&\small{\tt
iff}{}&s,h\models\Delta[{\small{\tt P}}(\bar{t})^{k}/P(\bar{t})]\text{ for
some definition branch }\Delta\text{ of {\small{$\tt P$}}}\\\
s,h\models{\small{\tt P}}(\bar{t})^{0}&\small{\tt iff}{}&\mbox{never}\\\
s,h{\models}\kappa_{1}*\kappa_{2}&{\small{\tt iff}}{}&\exists
h_{1},h_{2}{\cdot}~{}h_{1}{\\#}h_{2}\mbox{ and }h{=}h_{1}{\cdot}h_{2}\mbox{
and }s,h_{1}\models\kappa_{1}\mbox{ and }s{,}h_{2}\models\kappa_{2}\\\
s,h\models{\small{\tt true}}&{\small{\tt iff}}{}&\mbox{always}\\\
s,h\models{\small{\tt false}}&{\small{\tt iff}}{}&\mbox{never}\\\
s,h\models\exists v_{1}..v_{n}{\cdot}(\kappa{\wedge}\pi)&{\small{\tt
iff}}{}&\exists{\nu_{1}}..{\nu_{n}}{\cdot}{s}[{v_{1}}{{\scriptsize\mapsto}}{\nu_{1}},..,{v_{n}}{{\scriptsize\mapsto}}{\nu_{n}}]{,}h\models{\kappa}\text{
and
}{s}[{v_{1}}{{\scriptsize\mapsto}}{\nu_{1}},..,{v_{n}}{{\scriptsize\mapsto}}{\nu_{n}}]\models{\pi}\\\
s,h\models\Phi_{1}\vee\Phi_{2}&{\small{\tt iff}}{}&s,h\models\Phi_{1}\mbox{ or
}s,h\models\Phi_{2}\\\ \end{array}$ Figure 2. Semantics. $dom(f)$ is the
domain of the function $f$; $h_{1}{\\#}h_{2}$ denotes that heaps $h_{1}$ and
$h_{2}$ are (domain) disjoint, i.e.,
$\text{dom}(h_{1}){\cap}\text{dom}(h_{2}){=}\emptyset$; and
$h_{1}{\cdot}h_{2}$ denotes the union of two disjoint heaps.
${s}[{v_{1}}{{\scriptsize\mapsto}}{\nu_{1}},..,{v_{n}}{{\scriptsize\mapsto}}{\nu_{n}}](v)={s}(v)$
for $v{\notin}\\{v_{1},..,v_{n}\\}$, and
${s}[{v_{1}}{{\scriptsize\mapsto}}{\nu_{1}},..,{v_{n}}{{\scriptsize\mapsto}}{\nu_{n}}](v_{i})=\nu_{i}$
for $1{\leq}i{\leq}n$.

We define numeric and spatial projection functions. These projections are
critical for computing back-links of our decision procedure. We use $\bar{x}$
to denote a sequence of variables and ${x_{i}}$ to denote its $i^{th}$
element. We write $\bar{x}^{N}$ and $\bar{x}^{S}$ to denote the sequence of
integer variables and pointer variables in $\bar{x}$, respectively. For each
$c\in{\textit{Node}}$, we assume node symbol $\tt c^{S}$ for its spatial
projection. $\tt c^{S}$ is a sequence of fields similarly to $c$ except that
non-pointer fields are replaced by the $\\_$ fields.

###### Definition 1 (Spatial Projection).

The spatial projection $(\Phi)^{S}$ is defined inductively as follows.

$\vspace{-2mm}\begin{array}[]{ll}\begin{array}[]{lcl}(\Delta_{1}\vee\Delta_{2})^{S}&\equiv&(\Delta_{1})^{S}\vee(\Delta_{2})^{S}\\\
(\exists\bar{x}\cdot\Delta)^{S}&\equiv&\exists\bar{x}^{S}\cdot(\Delta)^{S}\\\
(\kappa{\wedge}\alpha{\wedge}\phi)^{S}&\equiv&(\kappa)^{S}{\wedge}\alpha\\\
\end{array}&\qquad\begin{array}[]{lcl}(\kappa_{1}{*}\kappa_{2})^{S}&\equiv&(\kappa_{1})^{S}{*}(\kappa_{2})^{S}\\\
({\small{\tt P}}(\bar{v}))^{S}&\equiv&{\small{\tt P^{S}}}(\bar{v}^{S})\\\
({x}{{\scriptsize\mapsto}}c(\bar{v}))^{S}&\equiv&{x}{{\scriptsize\mapsto}}c^{S}(\bar{v}^{S})\\\
({\tt emp})^{S}&\equiv&{\tt emp}\\\ \end{array}\end{array}$

For each inductive predicate ${\tt pred}~{}{\small{\tt
P}}(\bar{t})~{}{\equiv}~{}\bigvee^{n}_{i=1}({\exists}\bar{w_{i}}{\cdot}~{}\Delta_{i}:l_{i});$,
we assume the inductive predicate symbols $\tt P^{S}$ and predicate
${\small{\tt P^{S}}}(\bar{t}^{S})$ for its spatial projection satisfying ${\tt
pred}~{}{\small{\tt
P}}^{S}(\bar{t}^{S})~{}{\equiv}~{}\bigvee^{n}_{i=1}({\exists}\bar{w_{i}}{\cdot}~{}\Delta_{i})^{S}:l_{i};$.

###### Definition 2 (Numeric Projection).

The numeric projection $(\Phi)^{N}$ is defined inductively as follows.

$\vspace{-2mm}\begin{array}[]{ll}\begin{array}[]{lcl}(\Delta_{1}\vee\Delta_{2})^{N}&\equiv&(\Delta_{1})^{N}\vee(\Delta_{2})^{N}\\\
(\exists\bar{x}\cdot\Delta)^{N}&\equiv&\exists\bar{x}^{N}\cdot(\Delta)^{N}\\\
(\kappa{\wedge}\alpha{\wedge}\phi)^{N}&\equiv&(\kappa)^{N}{\wedge}\phi\\\
\end{array}&\qquad\begin{array}[]{lcl}(\kappa_{1}{*}\kappa_{2})^{N}&\equiv&(\kappa_{1})^{N}{\wedge}(\kappa_{2})^{N}\\\
({\small{\tt P}}(\bar{v}))^{N}&\equiv&{\small{\tt P^{N}}}(\bar{v}^{N})\\\
({x}{{\scriptsize\mapsto}}c(\bar{v}))^{N}{\equiv}({\tt
emp})^{N}&\equiv&{\small{\tt true}}\\\ \end{array}\end{array}$

For each inductive predicate ${\tt pred}~{}{\small{\tt
P}}(\bar{t})~{}{\equiv}~{}\bigvee^{n}_{i=1}({\exists}\bar{w_{i}}{\cdot}~{}\Delta_{i}:l_{i});$,
we assume the inductive predicate symbols $\tt P^{N}$ and predicate
${\small{\tt P^{N}}}(\bar{t}^{N})$ for its numeric projection satisfying ${\tt
pred}~{}{\small{\tt
P}}^{N}(\bar{t}^{N})~{}{\equiv}~{}\bigvee^{n}_{i=1}({\exists}\bar{w_{i}}{\cdot}~{}\Delta_{i})^{N}:l_{i};$.

##  3\. Overall Approach

$\begin{array}[]{c}\begin{array}[]{ll}1&{\small{\tt
struct~{}node{*}~{}sll(int~{}i)\\{}}\\\ 2&{\small{\tt\quad\quad
if(i{==}0)~{}return~{}{\small{\tt NULL}};}}\\\ 3&{\small{\tt\quad\quad
else~{}\\{}}\\\ 4&{\small{\tt\quad\quad\quad\quad
struct~{}node~{}{*}n{=}(struct~{}node{*})~{}malloc(sizeof(struct~{}node));}}\\\
5&{\small{\tt\quad\quad\quad\quad
n{\texttt{-\\!>}}val{=}i;~{}n{\texttt{-\\!>}}next{=}sll(i{-}1);}}\\\
6&{\small{\tt\quad\quad\quad\quad return~{}n;}}\\\
7&{\small{\tt\quad\quad\\}}}\\\ 8&{\small{\tt\\}}}\\\ &\\\ 9&{\small{\tt
int~{}main(int~{}n)\\{}}\\\ 10&{\small{\tt\quad\quad
struct~{}node~{}{*}x;}}\\\ 11&{\small{\tt\quad\quad
if(n{<}0)~{}return~{}0;}}\\\ 12&{\small{\tt\quad\quad x{=}sll(n);}}\\\
13&{\small{\tt\quad\quad while(x)\\{}}\\\ 14&{\small{\tt\quad\quad\quad\quad
struct~{}node~{}{*}tmp{=}x;}}\\\ 15&{\small{\tt\quad\quad\quad\quad
if(x{\texttt{-\\!>}}val{<}0)~{}ERROR();}}\\\
16&{\small{\tt\quad\quad\quad\quad x{=}x{\texttt{-\\!>}}next;}}\\\
17&{\small{\tt\quad\quad\quad\quad free~{}tmp;}}\\\ 18&\quad\quad\\}\\\
19&{\small{\tt\quad\quad return~{}1;}}\\\ 20&\\}\\\ &\\\ 21&{\small{\tt
struct~{}node~{}\\{int~{}val;}}\quad{\small{\tt
struct~{}node~{}{*}next;\\}}}\end{array}\end{array}$
Figure 3. An illustrative example

In this section, we use the C program shown in Fig. 3 to illustrate our
approach. This program allocates a null-terminated singly-linked list using
the recursive procedure $\tt sll$ at line 12. This list contains a list of
decreasing non-negative integer numbers. The loop from line 13 to 18 traverses
the list to check if any number stored in the list is negative. The user
supplies an assertion at line 15. For each node, it reports an error (via $\tt
ERROR()$) if the number is negative. If this is not the case, it de-allocates
each node before moving to the next. Given this program, our system
automatically verifies whether: (i) the method $\tt ERROR()$ at line 15 is
never called; and (ii) this program is memory safe, i.e., no error caused by
de-reference pointers (at line 5, 15 and 16) and free pointers (at line 17),
and (iii) there is no memory leak.

$\tt S2_{td}$ has three main components: a front-end parser, a middle-end
encoder and a back-end SAT solver. The parser takes the C program as input and
transforms it into a normalized form in the core language (whose syntax is
presented in Fig. 5). Specifically, it uses CIL (Necula:CC:2002) to parse the
C program into an Abstract Syntax Trees (AST). After that, it transforms the
AST as follows: it converts the program into a static single assignment (SSA)
form; it internalizes global variables, and it rewrites $\tt switch$
statements into $\tt if{-}then{-}else$ statements.

### Encoding

The encoder then generates (i) one inductive predicate as an encoding of each
procedure in the program, (ii) verification conditions to prove the absence of
memory errors and (iii) one verification condition to verify that the method
$\tt ERROR()$ is never called. The arguments of each predicate generated
include the set of parameters of the procedure and two reserved variables:
${\tt res}$ and $\varepsilon$. For instance, the encoding of the procedure
$sll($) shown in Figure 3 is as follows.

$\begin{array}[]{rcl}{\tt pred}~{}sll(i{,}{\tt res}{,}\varepsilon)&\equiv&{\tt
emp}{\wedge}{\tt res}{=}{{\small{\tt
null}}}{\wedge}i{=}0{\wedge}\varepsilon{=}0{:}[1]{\vee}\\\
&&{\exists}~{}i_{1}{,}r{\cdot}~{}{\tt
res}{\mapsto}node(i{,}r){*}sll(i_{1}{,}r{,}\varepsilon)^{0}{\wedge}i{\neq}0{\wedge}i_{1}{=}i{-}1{:}[2]\end{array}$

where $res$ is a special variable denoting the return value of the procedure
and $\varepsilon$ is a special value which explicitly captures the state of
the procedure. That is, $\varepsilon$ has two possible values: $0$ denoting a
safe state and $1$ denoting an error state. The encoding is based on the
Control Flow Graph (CFG) of the procedure. For instance, the first disjunct of
the encoding corresponds to the if-branch (with the path trace [1]) in Figure
3, whereas the second disjunct corresponds to the else-branch (with the path
trace [2]). The occurrence of the predicate $sll$ in the second disjunct is
also annotated with the ordering number 0.

In our system, a CHC $\sigma$ is a rule of the form
$\Delta_{b}{\rightarrow}P(\bar{x})$ or a query $\Delta_{q}$ where:
$\bar{x}{\subseteq}\bar{X}$, $\bar{X}$ is the set of global variables.
$\Delta_{b}$ and $P(\bar{x})$ are called body and head respectively.
Semantically, a CHC $\forall\bar{v}{\cdot}~{}\Delta\rightarrow P(\bar{x})$
($\bar{x}\subseteq\bar{v}$) is valid iff $\forall s,h~{}{\models}~{}\Delta$
then $s,h~{}{\models}~{}P(\bar{x})$. A set of CHCs $\mathcal{R}$ is
satisfiable if there exists an interpretation $\Gamma$ of the predicate
symbols $\mathcal{P}$ such that each constraint $\sigma{\in}\mathcal{R}$ is
true under $\Gamma$. Next, the encoder groups CHCs with the same head into an
inductive predicate:
$(\Delta_{b_{1}}{\rightarrow}P(\bar{x}))~{}{\vee}~{}(\Delta_{b_{2}}{\rightarrow}P(\bar{x}))$
is grouped into $\Delta_{b_{1}}{\vee}\Delta_{b_{2}}~{}{\equiv}~{}P(\bar{x})$.
As a result, those rules generated from the same loop or a procedure have the
same head and are thus grouped together. Moreover, whenever a memory error
$\bot_{m}$ is detected, the engine stops executing and reports the error.

While our symbolic execution engine encodes an input program locally i.e., it
encodes each method separately, the verification of memory safety must be done
globally (a memory cell may be allocated by one method and is accessed by
another method). To bridge this gap, our system marks the memory access
locally and processes the sequence of these accesses globally. To encode a
sequence of memory accesses, we introduce two new predicates into pure
constraints: the predicate ${\small{\tt LD}}({x}{.}f_{i}{,}v{,}k)$ for memory
reads and the predicate ${\small{\tt ST}}({x}{.}f_{i}{,}v{,}k)$ for memory
writes. The predicate ${\small{\tt LD}}({x}{.}f_{i}{,}v{,}k)$ (resp.,
${\small{\tt ST}}({x}{.}f_{i}{,}v{,}k)$) states the load from (resp., store
into) field $f_{i}$ of the pointer $x$ at logic level where $k$ is a non-
negative integer to capture the order of load/store sequence on heaps. These
predicates are checked globally (after the symbolic execution) by the
satisfiability solver. To detect memory errors, our systems generates the
following verification conditions to check the presence of null-deference
errors at line 5 of this method.

$\begin{array}[]{rcl}VC_{m_{5_{1}}}&{\equiv}&n{\mapsto}node(\\_\,{,}\\_\,){\wedge}i{\geq}0{\wedge}i{\neq}0{\wedge}n{=}{{\small{\tt
null}}}\\\
VC_{m_{5_{2}}}&{\equiv}&n{\mapsto}node(\\_\,{,}\\_\,){\wedge}i{\geq}0{\wedge}i{\neq}0{\wedge}n{\not\hookrightarrow}\\_\\\
VC_{m_{5_{3}}}&{\equiv}&n{\mapsto}node(i{,}\\_\,){\wedge}i{\geq}0{\wedge}i{\neq}0{\wedge}n{=}{{\small{\tt
null}}}\\\
VC_{m_{5_{4}}}&{\equiv}&n{\mapsto}node(i{,}\\_\,){\wedge}i{\geq}0{\wedge}i{\neq}0{\wedge}n{\not\hookrightarrow}\\_\\\
\end{array}$

If any of these conditions is satisfied, there is a memory error and our
encoder halts with state $\bot_{m}$. These conditions state that there is an
error if the pointer $n$ either is ${{\small{\tt null}}}$ ($VC_{m_{5_{1}}}$
and $VC_{m_{5_{3}}}$) or has not allocated ($VC_{m_{5_{2}}}$ and
$VC_{m_{5_{4}}}$) before the memory is accessed. Similarly, the encoding of
the procedure $\tt main$ is as follows.

$\begin{array}[]{rcl}{\tt pred}~{}main(n{,}{\tt
res}{,}\varepsilon)&\equiv&{\tt emp}{\wedge}n{<}0{\wedge}{\tt
res}{=}0{\wedge}\varepsilon{=}0{:}[1]{\vee}\\\ &&\exists
x{,}x^{\prime}{,}\varepsilon_{1}{,}\varepsilon_{2}{\cdot}sll(n{,}x{,}\varepsilon_{1})^{0}{*}loop_{13}(x{,}x^{\prime}{,}\varepsilon_{2})^{1}{\wedge}n{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon{=}1{:}[2]{\vee}\\\
&&\exists
x{,}x^{\prime}{,}\varepsilon_{1}{,}\varepsilon_{2}{\cdot}sll(n{,}x{,}\varepsilon_{1})^{0}{*}loop_{13}(x{,}x^{\prime}{,}\varepsilon_{2})^{1}{\wedge}n{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}0{\wedge}\varepsilon{=}0{:}[2]{\vee}\\\
&&\exists
x{,}x^{\prime}{,}\varepsilon_{1}{,}\varepsilon_{2}{\cdot}sll(n{,}x{,}\varepsilon_{1})^{0}{*}loop_{13}(x{,}x^{\prime}{,}\varepsilon_{2})^{1}{\wedge}n{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}0{\wedge}\varepsilon{=}1@\overline{{\tt
E}}{:}[2]\\\ {\tt pred}~{}loop_{13}(x{,}x^{\prime}{,}\varepsilon)&\equiv&{\tt
emp}{\wedge}x{=}{{\small{\tt
null}}}{\wedge}x^{\prime}{=}x{\wedge}\varepsilon{=}0{:}[2]{\vee}\\\ &&\exists
v_{1}{\cdot}{\tt
emp}{\wedge}{\neg}x{\not\hookrightarrow}\\_{\wedge}x{\neq}{{\small{\tt
null}}}{\wedge}{\small{\tt
LD}}({x}{.}val{,}v_{1}{,}0){\wedge}v_{1}{<}0{\wedge}\varepsilon{=}1{:}[1;1]{\vee}\\\
&&\exists
v_{1}{,}x_{1}{\cdot}loop_{13}(x_{1}{,}x^{\prime}{,}\varepsilon)^{0}{\wedge}{\neg}x{\not\hookrightarrow}\\_{\wedge}x{\neq}{{\small{\tt
null}}}{\wedge}{\small{\tt
LD}}({x}{.}val{,}v_{1}{,}0){\wedge}v_{1}{\geq}0{\wedge}{\small{\tt
LD}}({x}{.}next{,}x_{1}{,}0){:}[1;2]\end{array}$

While the first disjunct encodes the if-branch at line 11, the second disjunct
encodes the else-branch at line 11 and the assertion at line 15 is violated,
the third disjunct encodes the else branch at line 11 and the assertion at
line 15 is not violated and memory is not leaked at exit, and the last
disjunct encodes the else-branch at line 11 and memory is leaked. We note that
in the second, third and fourth disjuncts, the occurrences of $sll$ and
$loop_{13}$ are ordered; the satisfiability solver always unfolds the former
(whose ordering number is 0) before the latter (whose ordering number is 1).
This mechanism ensures that if a pointer is allocated before accessed, our
system discharges this scenario as memory safe. Otherwise, it detects a memory
error. Using variable $\varepsilon$, we can encode when error occurs. For
instance, in the encoding of the procedure $\tt main$, the fourth branch
captures the memory leakage, i.e., the program has a memory leak if there
exists an execution whose heap is not empty (encoded by $@\overline{{\tt E}}$)
upon termination. The user-supplied assertion at line 15 is encoded similarly.
We note that the loop from 13 to 18 is encoded as a separate inductive
predicate, i.e., $loop_{13}$ where 13 is the starting line number of the loop.
The list of arguments of this predicate include input parameters, output
parameters and the $\varepsilon$. Input parameters are those variables
occurring in the $\tt while$ condition or the body of the $\tt while$ loop;
output parameters are a subset of the input parameters and contain those
variables that are modified within the loop body.

Similarly, we generate VCs which are necessary to detect memory safety
violation at lines 15-17. For examples, to detect whether a memory error at
line 15 happens, we generate the following VCs

$\begin{array}[]{rcl}VC_{m_{15_{1}}}&{\equiv}&\exists
x{,}\varepsilon_{1}{,}{\cdot}sll(n{,}x{,}\varepsilon_{1})_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}}^{0}{\wedge}n{\geq}0{\wedge}x{\neq}{{\small{\tt
null}}}{\wedge}\varepsilon_{1}{=}0{\wedge}x{\not\hookrightarrow}\\_\\\
VC_{m_{15_{2}}}&{\equiv}&\exists
x{,}\varepsilon_{1}{,}{\cdot}sll(n{,}x{,}\varepsilon_{1})_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}}^{0}{\wedge}n{\geq}0{\wedge}x{\neq}{{\small{\tt
null}}}{\wedge}\varepsilon_{1}{=}0{\wedge}x{=}{{\small{\tt null}}}\end{array}$

If either $\Delta_{m_{15_{1}}}$ or $\Delta_{m_{15_{2}}}$ is satisfiable, our
engine returns $\bot_{m}$. We remark that unfolding numbers of these predicate
instances in these VCs are initially assigned to 0 and updated by the
satisfiability solver while unfolding.

After inductive definitions are generated, we automatically infer their (over-
approximated) invariants using the technique presented in (Loc:CAV:2016).
These invariants facilitate our analysis later on. For example, the invariant
of the predicate $\tt sll$ is $i{\geq}0{\wedge}\varepsilon{=}0$, which is
generated through the following three steps. First, we assume the invariant of
$\tt sll$ to be a pure unknown predicate ${\small{\tt P}}(i{,}{\tt
res}{,}\varepsilon)$ and generate an induction hypothesis as: $\forall
i{,}{\tt res}{,}\varepsilon{\cdot}{\small{\tt sll}}(i{,}{\tt
res}{,}\varepsilon){\implies}{\small{\tt P}}(i{,}{\tt res}{,}\varepsilon)$.

Secondly, in the induction step, we unfold the predicate $\tt sll$ in the
left-hand side prior to substituting the occurrence of the predicate $\tt sll$
with its corresponding induction hypothesis to obtain the following.

$\begin{array}[]{l}({\tt emp}{\wedge}{\tt res}{=}{{\small{\tt
null}}}{\wedge}i{=}0{\wedge}\varepsilon{=}0~{}~{}{\vee}~{}~{}{\exists}~{}r{\cdot}~{}{\tt
res}{\mapsto}node(i{,}r)~{}{*}~{}{\small{\tt
P}}(i{-}1{,}r{,}\varepsilon){\wedge}i{\neq}0){\implies}{\small{\tt
P}}(i{,}{\tt res}{,}\varepsilon)\end{array}$

Lastly, we over-approximate the heap to obtain:

$({\tt emp}{\wedge}{\tt res}{=}{{\small{\tt
null}}}{\wedge}i{=}0{\wedge}\varepsilon{=}0~{}~{}{\vee}~{}~{}{\exists}~{}r{\cdot}~{}{\tt
res}{\neq}{{\small{\tt null}}}{\wedge}{\small{\tt
P}}(i{-}1{,}r{,}\varepsilon){\wedge}i{\neq}0){\implies}{\small{\tt
P}}(i{,}{\tt res}{,}\varepsilon)$

After that, we pass this non-heap constraint to the analyzer $\tt LFP$
presented in (Trinh:APLAS:2013) to compute the fixed point for $\tt P$. We
similarly generate invariant $0{\leq}{\tt res}{\leq}1$ for $\tt main$ and
invariant $0{\leq}\varepsilon{\leq}1$ for $\tt loop_{13}$.

After encoding every procedure, we encode the following verification condition
(VC) for our example.

$\Delta_{0}{\equiv}main(n_{0}{,}{\tt
res}_{0}{,}\varepsilon_{0})^{0}_{0}{\wedge}\varepsilon_{0}{=}1$

Intuitively, this VC asks whether it is possible to invoke $\tt main$ with
symbolic input $n_{0}$ such that an error occurs. Note that based on our
encoding, an error occurs if the user-supplied assertion is violated i.e., the
method $\tt ERROR()$ is invoked.

We notice that our symbolic execution engine prunes beforehand any infeasible
CHC whose body is unsatisfiable. For instance, while encoding the procedure
$\tt main$, the engine detects and prunes the following CHC $\sigma_{1}$:

$\vspace{-1mm}\exists\varepsilon_{1}{\cdot}sll(n{,}x{,}\varepsilon_{1})_{\\_}^{0}{\wedge}n{\geq}0{\wedge}\varepsilon_{1}{=}1{\wedge}\varepsilon{=}1{\rightarrow}main(n{,}{\tt
res}{,}\varepsilon)$

This unsatisfiability comes from the inconsistency of the over-approximated
invariant of the predicate $sll$ (i.e., $\varepsilon_{1}{=}0$) with the sub-
formula $\varepsilon_{1}{=}1$ of the body of $\sigma_{1}$.

### Satisfiability Checking

After generating the VCs, we reduce the verification problem into
satisfiability checking problems i.e., whether any of $VC_{m_{\\_\,}}$ and
$\Delta_{0}$ is satisfiable or not. In our approach, the satisfiability
checking is based on a procedure named $\tt{S2SAT_{eSL}}$, which is an
instantiation of the general satisfiability procedure $\tt{S2SAT}$ previously
presented in (Loc:CAV:2016). In the following, we illustrate how
$\tt{S2SAT_{eSL}}$ decides the formula $\Delta_{0}$.

$\Delta_{0}$$\Delta_{11}$$\Delta_{12}^{\bigstar}$$\Delta_{13}$$\Delta_{14}^{\dagger}$$\Delta_{21}$$\Delta_{22}$$\Delta_{51}$$\Delta_{52}$$\Delta_{31}$$\Delta_{32}$$\Delta_{33}$$\Delta_{41}$$\Delta_{42}$$\Delta_{43}^{\bigstar}$$\Delta_{61}$$\Delta_{62}$$\Delta_{63}$$\Delta_{71}$$\Delta_{72}$$\Delta_{73}^{\dagger}$
Figure 4. Unfolding Tree ${\mathcal{T}}$.

Given the formula, $\tt{S2SAT_{eSL}}$ constructs an unfolding tree, which
contains a single root node $\Delta_{0}$. Given an unfolding tree,
$\tt{S2SAT_{eSL}}$ attempts either to prove that the unfolding tree is
satisfiable (e.g., there is a counter-example satisfying the VC) or it is
unsatisfiable. In our example, since $\tt{S2SAT_{eSL}}$ cannot conclude that
whether the only node $\Delta_{0}$ in the tree is $\tt SAT$ or $\tt UNSAT$,
$\tt{S2SAT_{eSL}}$ grows the unfolding tree by unfolding the predicate
instance $main$ in $\Delta_{0}$. As a result, the node $\Delta_{0}$ is now
connected to four leaf nodes $\Delta_{11}$, $\Delta_{12}$, $\Delta_{13}$ and
$\Delta_{14}$, which are defined as follows.

$\begin{array}[]{rcl}\Delta_{11}&{\equiv}&{\tt
emp}{\wedge}n_{0}{<}0{\wedge}{\tt
res}_{0}{=}0{\wedge}\underline{\varepsilon_{0}{=}0}{\wedge}\underline{\varepsilon_{0}{=}1}\\\
\Delta_{12}&{\equiv}&sll(n_{0}{,}x{,}\varepsilon_{1})_{1}^{0}{*}loop_{13}(x{,}x^{\prime}{,}\varepsilon_{2})_{1}^{1}{\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1\\\
\Delta_{13}&{\equiv}&sll(n_{0}{,}x{,}\varepsilon_{1})_{1}^{0}{*}loop_{13}(x{,}x^{\prime}{,}\varepsilon_{2})_{1}^{1}{\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}0{\wedge}\underline{\varepsilon_{0}{=}0}{\wedge}\underline{\varepsilon_{0}{=}1}\\\
\Delta_{14}&{\equiv}&sll(n_{0}{,}x{,}\varepsilon_{1})_{1}^{0}{*}loop_{13}(x{,}x^{\prime}{,}\varepsilon_{2})_{1}^{1}{\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}0{\wedge}{\varepsilon_{0}{=}0}@\overline{{\tt
E}}\end{array}$

Note that existentially quantified variables are skolemized for simplicity and
path traces (the labels to mark program paths for witness generation) are
discarded. We note that unfolding number of an occurrence of a predicate in
the unfolded formulas is increased by one from the unfolding number of the
occurrence $main$ in $\Delta_{0}$. Next, $\tt{S2SAT_{eSL}}$ attempts to prove
that either the unfolding tree is satisfiable or it is unsatisfiable. In
particular, if a leaf node does not contain any instance of recursive
predicates, $\tt{S2SAT_{eSL}}$ checks whether it is satisfiable; otherwise,
$\tt{S2SAT_{eSL}}$ checks whether it can be proven unsatisfiable. In
particular, $\tt{S2SAT_{eSL}}$ first checks whether $\Delta_{11}$ is
satisfiable and concludes that it is unsatisfiable. Note that the unsat core
is underlined for readability. Afterwards, $\tt{S2SAT_{eSL}}$ tries to see
whether $\Delta_{12}$, $\Delta_{13}$ or $\Delta_{14}$ is unsatisfiable.
$\tt{S2SAT_{eSL}}$ concludes that $\Delta_{13}$ is unsatisfiable but fails to
prove that $\Delta_{12}$ or $\Delta_{14}$ is unsatisfiable. $\tt{S2SAT_{eSL}}$
then moves on to grow the tree, by unfolding instances of recursive predicates
in $\Delta_{12}$.

Note that there are two recursive predicates in $\Delta_{12}$: $sll$ and
$loop_{13}$. For a flow-sensitive analysis, $\tt{S2SAT_{eSL}}$ unfolds
occurrences of inductive predicates in a breadth-first and top-down manner. To
do so, $\tt{S2SAT_{eSL}}$ chooses the predicate instance which has the
smallest unfolding number and the smallest sequence number first. In this
example, it chooses $sll$ first and grows the node $\Delta_{12}$ with two new
leaves $\Delta_{21}$ and $\Delta_{22}$ which are defined as follows.

$\begin{array}[]{rcl}\Delta_{21}&{\equiv}&x{=}{{\small{\tt
null}}}{\wedge}n_{0}{=}0{\wedge}\varepsilon_{1}{=}0{\wedge}loop_{13}(x{,}x^{\prime}{,}\varepsilon_{2})_{1}^{1}{\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1\\\
\Delta_{22}&{\equiv}&x{\mapsto}node(n_{1}{,}r_{2}){*}sll(n_{1}{,}r_{2}{,}\varepsilon_{1})_{2}^{0}{*}loop_{13}(x{,}x^{\prime}{,}\varepsilon_{2})_{1}^{1}{\wedge}n_{0}{\neq}0{\wedge}n_{1}{=}n_{0}{-}1{\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1\end{array}$

Since $\tt{S2SAT_{eSL}}$ cannot prove that $\Delta_{21}$ is unsatisfiable, it
grows node $\Delta_{21}$ with the following leaves, by unfolding $loop_{13}$.

$\begin{array}[]{rcl}\Delta_{31}&{\equiv}&{\tt emp}{\wedge}x{=}{{\small{\tt
null}}}{\wedge}n_{0}{=}0{\wedge}\varepsilon_{1}{=}0{\wedge}x{=}{{\small{\tt
null}}}{\wedge}x^{\prime}{=}x{\wedge}\underline{\varepsilon_{2}{=}0}{\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\underline{\varepsilon_{2}{=}1}{\wedge}\varepsilon_{0}{=}1\\\
\Delta_{32}&{\equiv}&{\tt emp}{\wedge}\underline{x{=}{{\small{\tt
null}}}}{\wedge}n_{0}{=}0{\wedge}\varepsilon_{1}{=}0{\wedge}{\neg}x{\not\hookrightarrow}\\_{\wedge}\underline{x{\neq}{{\small{\tt
null}}}}{\wedge}{\small{\tt
LD}}({x}{.}val{,}v_{1}{,}0){\wedge}v_{1}{<}0{\wedge}n_{0}{\geq}0{\wedge}\\\
&&\qquad\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1\\\
\end{array}$

$\begin{array}[]{rcl}\Delta_{33}&{\equiv}&\underline{x{=}{{\small{\tt
null}}}}{\wedge}n_{0}{=}0{\wedge}\varepsilon_{1}{=}0{\wedge}loop_{13}(x_{1}{,}x^{\prime}{,}\varepsilon_{2})_{2}^{0}{\wedge}{\neg}x{\not\hookrightarrow}\\_{\wedge}\underline{x{\neq}{{\small{\tt
null}}}}{\wedge}{\small{\tt
LD}}({x}{.}val{,}v_{1}{,}0){\wedge}v_{1}{\geq}0{\wedge}\\\ &&\qquad{\small{\tt
LD}}({x}{.}next{,}x_{1}{,}0){\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1\end{array}$

$\tt{S2SAT_{eSL}}$ proves $\Delta_{31}$, $\Delta_{32}$, and $\Delta_{33}$ are
unsatisfiable (as there are no recursive predicates). Similarly, since
$\tt{S2SAT_{eSL}}$ cannot prove that $\Delta_{22}$ is unsatisfiable, it grows
the node $\Delta_{22}$ with the following leaves, by unfolding $loop_{13}$.

$\begin{array}[]{rcl}\Delta_{41}&{\equiv}&x{\mapsto}node(n_{1}{,}r_{2}){*}sll(n_{1}{,}r_{2}{,}\varepsilon_{1})_{2}^{0}{\wedge}x{=}{{\small{\tt
null}}}{\wedge}x^{\prime}{=}x{\wedge}\underline{\varepsilon_{2}{=}0}{\wedge}n_{0}{\neq}0{\wedge}n_{1}{=}n_{0}{-}1{\wedge}n_{0}{\geq}0{\wedge}\\\
&&\qquad\varepsilon_{1}{=}0{\wedge}\underline{\varepsilon_{2}{=}1}{\wedge}\varepsilon_{0}{=}1\\\
\Delta_{42}&{\equiv}&x{\mapsto}node(n_{1}{,}r_{2}){*}sll(n_{1}{,}r_{2}{,}\varepsilon_{1})_{2}^{0}{\neg}x{\not\hookrightarrow}\\_{\wedge}x{\neq}{{\small{\tt
null}}}{\wedge}{\small{\tt
LD}}({x}{.}val{,}v_{1}{,}0){\wedge}v_{1}{<}0{\wedge}\underline{\varepsilon_{1}{=}1}{\wedge}n_{0}{\neq}0{\wedge}\\\
&&\qquad
n_{1}{=}n_{0}{-}1{\wedge}n_{0}{\geq}0{\wedge}\underline{\varepsilon_{1}{=}0}{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1\\\
\Delta_{43}&{\equiv}&x{\mapsto}node(n_{1}{,}r_{2}){*}sll(n_{1}{,}r_{2}{,}\varepsilon_{1})_{2}^{0}{*}loop_{13}(x_{1}{,}x^{\prime}{,}\varepsilon_{2})_{2}^{1}{\wedge}{\neg}x{\not\hookrightarrow}\\_{\wedge}x{\neq}{{\small{\tt
null}}}{\wedge}v_{1}{\geq}0{\wedge}\\\ &&\qquad{\small{\tt
LD}}({x}{.}val{,}v_{1}{,}0){\wedge}{\small{\tt
LD}}({x}{.}next{,}x_{1}{,}0){\wedge}n_{0}{\neq}0{\wedge}n_{1}{=}n_{0}{-}1{\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1\\\
\end{array}$

$\tt{S2SAT_{eSL}}$ proves $\Delta_{41}$ and $\Delta_{42}$ are unsatisfiable.
Furthermore, $\tt{S2SAT_{eSL}}$ detects that $\Delta_{43}$ (after
normalization which we will explain in Section 5) is _subsumed_ by
$\Delta_{12}$. $\tt{S2SAT_{eSL}}$ then adds a back-link from $\Delta_{43}$ to
$\Delta_{12}$ to form a partial pre-proof (Loc:CAV:2016). Intuitively, this
back-link means that although the path from $\Delta_{12}$ to $\Delta_{43}$ can
be infinitely unfolded, there is no counterexample generated this way and
therefore we can stop unfolding $\Delta_{43}$. Note that in order to guarantee
that a back-link is sound (i.e., stopping unfolding the node will not lead to
miss out a counterexample), additional well-formedness conditions must be
checked, as we will explain in detail in Section 5.

We similarly grow $\Delta_{14}$ with children and their children until either
$\tt{S2SAT_{eSL}}$ proves a newly grown node is satisfiable (in which case a
counterexample is identified) or it is unsatisfiable (in which case we stop
unfolding the node) or it is linked-back to an existing node (in which case we
stop unfolding the node). The resultant unfolding tree is shown in Figure 4.
Note that every leaf of the tree is either proven unsatisfiable or linked-
back. As a result, $\tt{S2SAT_{eSL}}$ concludes that the VC $\Delta_{0}$ is
unsatisfiable and thus discharged. We remark that the unfolding tree shown in
Figure 4 can be viewed as cyclic proof of the unsatisfiability of
$\Delta_{0}$. After showing that every VC is unsatisfiable, our system proves
that the program is safe.

##  4\. CHC Encoding

In this section, we present details on how we encode programs into VCs.

$\begin{array}[]{rcl}\textit{prog}&::=&\textit{datat}^{*}~{}\textit{meth}^{*}\\\
\textit{datat}&::=&{\tt data}~{}c~{}\\{~{}\textit{field;}^{*}~{}\\}\\\
\textit{meth}&::=&t~{}\textit{mn}~{}((t~{}v)^{*})~{}\\{e\\}\\\
\textit{field}&::=&t~{}v\\\ t&::=&c~{}|~{}\tau\hfill\text{user-defined types
or primitive types}\\\ \tau&::=&{\small{\tt int}}~{}|~{}{\small{\tt
bool}}~{}|~{}{\small{\tt void}}\hfill\text{primitive types}\\\
e&::=&{{\small{\tt null}}}~{}|\hfill\text{NULL}\\\
&&k^{\tau}~{}|\hfill\text{an arithmetic expression}\\\ &&v~{}|\hfill\text{a
variable}\\\ &&v~{}{:=}~{}e~{}|\hfill\text{an assignment}\\\
&&t~{}v~{}|\hfill\text{a variable declaration}\\\
&&\textit{mn}(v_{1},..,v_{n})~{}|\hfill\text{a procedure invocation}\\\
&&{\small{\tt assume({\pi}}})~{}|\hfill\text{an assume-statement}\\\
&&v{\texttt{-\\!>}}f~{}|\hfill\text{memory read}\\\ &&{\tt
new}~{}c(v_{1},..,v_{n})~{}|\hfill\text{building a new object}\\\ &&{\tt
free}~{}v~{}|\hfill\text{free an object}\\\
&&v_{1}{\texttt{-\\!>}}f{:=}v_{2}~{}|\hfill\text{memory write}\\\
&&e_{1};e_{2}~{}|\hfill\text{sequential composition}\\\ &&{\small{\tt
if}}~{}v~{}{\small{\tt then}}~{}e_{1}~{}{\small{\tt
else}}~{}e_{2}~{}|\qquad\qquad\qquad\qquad\hfill\text{conditional branch}\\\
&&{\small{\tt while}}(v){\small{\tt\\{}}e\\}\hfill\text{while-loop}\\\
\end{array}$ Figure 5. A core language: $t$ is a type name; $v$ is a variable
name

The first step is to systematically translate a given program into a
normalized form which we call a core program. The syntax of a core program
prog is defined in Figure 5. In general, a core program consists of multiple
data structures and procedures. Each data structure datat is composed of
multiple fields. Each field field is composed of a type $t$ and a variable
name $v$. In this work, we restrict the types to be either $int$ or $bool$.
Each procedure meth is composed of a return type $t$, a method name $mn$,
multiple parameters (each of which has a type and a name) and a command $e$.
Furthermore, all function calls of the method $\tt ERROR()$ are replaced by
the statement: $\tt assume(\varepsilon^{\prime}{=}1)$. The syntax of command
$e$ is shown in Figure 5. We assume there is a special procedure called $\tt
main$ which is the entry point of the program. We skip the details on
translating a program (e.g., in the C syntax) to a core program, as it is
standard (Necula:CC:2002; Gurfinkel:CAV:2015).

${\bf\scriptstyle[ASSUME]}\frac{\begin{array}[]{c}\rho{=}\circ\\{v^{\prime}/v~{}|~{}v\in\textit{FV}(\pi)\\}\end{array}}{\\_\,{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}{\small{\tt
assume}}~{}\pi){\leadsto}(\Delta{\wedge}(\pi[\rho])){:}l}\qquad{\bf\scriptstyle[LOCAL-
PTR]}\frac{\begin{array}[]{c}t{\in}Node~{}~{}\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{*}v^{\prime}{\not\hookrightarrow}\\_{:}l{,}e){\leadsto}\Delta_{1}{:}l_{1}\end{array}}{\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}\\{t~{}v;~{}e\\}){\leadsto}\exists\,v,v^{\prime}{\cdot}\Delta_{1}{:}l_{1}}$

${\bf\scriptstyle[IF]}\frac{\begin{array}[]{c}\begin{array}[]{c}\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{\wedge}v^{\prime}{:}(l{::}1){,}e_{1}){\leadsto}\Delta_{1}{:}l_{1}\quad\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{\wedge}{\neg}v^{\prime}{:}(l{::}2){,}e_{2}){\leadsto}\Delta_{2}{:}l_{2}\end{array}\end{array}}{\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}{\small{\tt if}}~{}v~{}{\small{\tt
then}}~{}e_{1}~{}{\small{\tt
else}}~{}e_{2}){\leadsto}\Delta_{1}{:}l_{1}{\vee}\Delta_{2}{:}l_{2}}\qquad{\bf\scriptstyle[VAR]}\frac{\begin{array}[]{c}\Delta_{1}{=}(\Delta{\wedge}{\tt
res}{=}v^{\prime})\end{array}}{\\_\,{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}v){\leadsto}\Delta_{1}{:}l}$

${\bf\scriptstyle[SEQ]}\frac{\begin{array}[]{c}\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}e_{1}){\leadsto}\Delta_{1}{:}l_{1}\quad\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta_{1}{:}l_{1}{,}e_{2}){\leadsto}\Delta_{2}{:}l_{2}\end{array}}{\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}e_{1};e_{2}){\leadsto}\Delta_{2}{:}l_{2}}\qquad{\bf\scriptstyle[NEW]}\frac{\begin{array}[]{c}\Delta_{1}{=}(\Delta\,{*}\,{{\tt
res}}{{\scriptsize\mapsto}}c(v^{\prime}_{1}{,}..{,}v^{\prime}_{n}))\end{array}}{\\_\,{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}{\tt new}~{}c(v_{1},..,v_{n})){\leadsto}\Delta_{1}{:}l}$

${\bf\scriptstyle[ASSIGN]}\frac{\begin{array}[]{c}\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}e){\leadsto}\Delta_{1}{:}l_{1}~{}~{}\Delta_{2}{=}\exists{\tt
res}{,}r{\cdot}(\Delta_{1}[r/v^{\prime}]{\wedge}v^{\prime}{=}{\tt
res})~{}~{}\textit{fresh}~{}r\end{array}}{\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}v{:=}e){\leadsto}\Delta_{2}{:}l_{1}}\qquad{\bf\scriptstyle[CONST]}\frac{\begin{array}[]{c}\Delta_{1}{=}(\Delta{\wedge}\textit{eq}_{\tau}({\tt
res},k))\end{array}}{\\_\,{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}k^{\tau}){\leadsto}\Delta_{1}{:}l}$

${\bf\scriptstyle[CALL]}\frac{\begin{array}[]{c}t_{0}~{}mn(t_{1}~{}v_{1},..,t_{n}~{}v_{n})~{}\\{e_{b}\\}{\in}\textit{prog}\\\
{\small{\tt if}}~{}(\text{mn has not been processed})~{}{\small{\tt
then}}~{}\vdash{(\Delta_{c}[v_{1}/x_{1};...;v_{n}/x_{n}]{*}\Delta)}{:}~{}t_{0}~{}\textit{mn}(t_{1}~{}v_{1},..,t_{n}~{}v_{n})~{}\\{e_{b}\\}\\\
\textit{fresh}~{}e_{mn}\qquad\Delta_{1_{i}}{=}\exists
e{\cdot}\Delta{*}\textit{mn}(v_{1}^{\prime}{,}..{,}v^{\prime}_{n}{,}{\tt
res}{,}e_{mn})^{n_{i}}{\wedge}e_{mn}{=}i{\wedge}\varepsilon^{\prime}{=}i{:}l\qquad
i{\in}\\{0{,}1\\}\qquad\text{ increase
}n_{i}\end{array}}{\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}mn(x_{1},..,x_{n})){\leadsto}\Delta_{1_{0}}~{}{\vee}~{}\Delta_{1_{1}}}$

${\bf\scriptstyle[FREE]}\frac{\begin{array}[]{c}\textit{VC}{=}\textit{VC}\cup\\{\Delta_{c}{*}\Delta{\wedge}x^{\prime}{=}{{\small{\tt
null}}};\Delta_{c}{*}\Delta{\wedge}x^{\prime}{\not\hookrightarrow}\\_\\}\qquad\textit{fresh}~{}w\quad\Delta_{1}{=}\Delta[w/x^{\prime}]{\wedge}{\neg
w{\not\hookrightarrow}\\_}{\wedge}w{\neq}{{\small{\tt
null}}}\end{array}}{\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}{\small{\tt free}}~{}x){\leadsto}\Delta_{1}{:}l}$

${\bf\scriptstyle[LOAD]}\frac{\begin{array}[]{c}\textit{VC}{=}\textit{VC}\cup\\{\Delta_{c}{*}\Delta{\wedge}x^{\prime}{=}{{\small{\tt
null}}};\Delta_{c}{*}\Delta{\wedge}x^{\prime}{\not\hookrightarrow}\\_\\}\qquad\pi_{load}{=}{\neg
v^{\prime}{\not\hookrightarrow}\\_}{\wedge}v^{\prime}{\neq}{{\small{\tt
null}}}{\wedge}{\small{\tt LD}}({v^{\prime}}{.}f_{i}{,}{\tt
res}{,}k_{g})\quad\text{ increase }k_{g}\end{array}}{{\small{\tt
exec}}(\Delta{:}l{,}v{\texttt{-\\!>}}f_{i}){\leadsto}\Delta{\wedge}\pi_{load}{:}l}$

${\bf\scriptstyle[STORE]}\frac{\begin{array}[]{c}\textit{VC}{=}\textit{VC}\cup\\{\Delta_{c}{*}\Delta{\wedge}x^{\prime}{=}{{\small{\tt
null}}};\Delta_{c}{*}\Delta{\wedge}x^{\prime}{\not\hookrightarrow}\\_\\}\qquad\pi_{store}{=}{\neg
v^{\prime}{\not\hookrightarrow}\\_}{\wedge}v^{\prime}{\neq}{{\small{\tt
null}}}{\wedge}{\small{\tt
ST}}({v^{\prime}}{.}f_{i}{,}v^{\prime}_{0}{,}k_{g})\quad\text{ increase
}k_{g}\end{array}}{\Delta_{c}{:}~{}{\small{\tt
exec}}(\Delta{:}l{,}v{\texttt{-\\!>}}f_{i}{:=}v_{0}){\leadsto}\Delta{\wedge}\pi_{store}{:}l}$

Figure 6. Encoding VC via Symbolic Execution

Our encoding is built upon forward symbolic execution for separation logic
(Berdine:APLAS05; Chin:SCP:12). Our approach works similarly to a Strongest
Post Condition Calculus; it naturally and precisely generates CHCs like those
VCs obtained from Dijkstra’s weakest liberal precondition calculus
(Dijkstra:CACM:1975), but works the other way around. CHCs correspond to
liberal datalog, which in turn is equivalent to existential fixed point logic
(DBLP:journals/corr/abs-0811-0977). While existential fixed point logic would
be well-suited to capture total correctness (Blass:1987), we focus on safety
properties in this work and leave termination analysis in future work.

The proposed engine takes a program as input. It symbolically executes each
command starting from a $\tt main$ function. The engine produces a set of
verification conditions VC for the verification of memory safety as well as a
set of CHCs to encode the verification of user-supplied assertions. The
forward verification rule for each command $\tt e$ is formalized as a
quadruple $\Delta_{c}{:}~{}{\small{\tt exec}}(\Delta_{1}{,}{\it
e}){\leadsto}\Delta_{2}$ where $\Delta_{1}$ and $\Delta_{2}$ are its
precondition and postcondition respectively, $\Delta_{c}$ is its calling
context. The calling context is used for memory error detection. Furthermore,
we assume that the engine maintains a pair $n_{l}$ and $k_{g}$ where $n_{l}$
is the next function call number (used to locally order the function calls)
and $k_{g}$ is the next memory access number (used to globally order the
memory accesses over the heaps). The engine halts when it detects either an
erroneous state in the precondition, i.e. $\\_{:}~{}{\small{\tt
exec}}(\Delta{\wedge}\varepsilon^{\prime}{=}1{,}{\it e}){\leadsto}\\_$ or a
memory error in the postcondition, i.e. $\\_{:}~{}{\small{\tt
exec}}(\\_{,}{\it e}){\leadsto}\bot_{m}$. Verification conditions to detect
memory errors are accumulated into a global set VC which is initially set to
empty. In our implementation, whenever a verification condition is generated,
our engine invokes the solver for satisfiability checking. If it is the case,
it immediately halts with the state $\bot_{m}$. Note that in our system, each
state (e.g. $\Delta_{1}$, $\Delta_{2}$) may contain both unprimed and primed
versions of program variables (e.g. $x$, $x_{i}$ ($i{\geq}0$), $x^{\prime}$),
where $x$ represents the initial value of the variable, $x_{i}$ represent the
intermediate values of the variable through updates, $\tt x^{\prime}$
represents the value of the variable at the next step. The use of both primed
and unprimed versions of program variables is critical for the symbolic
execution of loops. The variable ${\tt res}$ is used to denote the return
value of each command (if applicable) in the post-condition.

Some rules for forward symbolic execution are presented in Fig. 6. We discuss
the rest of the rules below one-by-one. A procedure $\tt mn$ is encoded by the
predicate $mn$ as:

$\vspace{-1mm}\frac{\begin{array}[]{c}V{=}\\{v_{1}{,}..{,}v_{n}{,}{\tt
res}{,}\varepsilon\\}\qquad\Delta_{c}{:}~{}{\small{\tt exec}}({\tt
emp}{\wedge}\textit{initV}(V){:}[]{,}e){\leadsto}\bigvee\Delta_{i}{:}l_{i}\\\
\Delta_{i}^{e}{=}{\small{\tt
encodeL}}(\Delta_{i})\qquad\textit{W}{=}\textit{prime}(V)\qquad{\tt
pred}~{}\textit{mn}(v_{1}{,}..{,}v_{n}{,}{\tt
res}{,}\varepsilon^{\prime}){\equiv}{(\bigvee~{}{\exists}\textit{W}{\cdot}\Delta_{i}^{e}{:}l_{i})}\end{array}}{\vdash\Delta_{c}{:}~{}t_{0}~{}\textit{mn}(t_{1}~{}v_{1},..,t_{n}~{}v_{n})~{}\\{e\\}}$

The list of arguments of the predicate $mn$ includes the set of parameters of
$\tt mn$ and two reserved variables: ${\tt res}$ for output and
$\varepsilon^{\prime}$ for error status. Each program path in $\tt mn$
corresponds to a disjunct constituting the predicate $mn$. The function
$\textit{prime}(V)$ returns the primed form of all variables in $V$. The
function $\textit{initV}(V)$ returns a formula asserting that the unprimed and
primed versions of each variable in $V$ are equal. For the entry procedure
$\tt main$, $k_{g}$ is initially assigned to $0$, the calling context is ${\tt
emp}{\wedge}{\small{\tt true}}\,$, and every pointer parameter ${v_{i}}$ is
initially set to be dangling, with the constraint
$v^{\prime}_{i}{\not\hookrightarrow}\\_$ spatially conjoined ($*$) with the
precondition before executing. After symbolic execution, a disjunctive formula
($\bigvee\Delta_{i}$) precisely encoding the input program is obtained. The
function $\tt encodeL$ is used to post-process this encoding. For each safe
path, i.e. $\Delta_{i}$ which does not include $\varepsilon^{\prime}{=}1$,
$\tt encodeL$ generates the following disjunct
$\Delta_{i}{\wedge}\varepsilon^{\prime}{=}0$. Especially, for the entry
procedure $\tt main$, $\tt encodeL$ generates another disjunct to encode the
leak errors: $\Delta_{i}{\wedge}\varepsilon^{\prime}{=}1@\overline{{\tt E}}$.

We notice that the primed version of a variable works as either the final
value (to be read from) or the next value (to be written to) of a variable.
For example, in the rule $\tt[VAR]$, we assign primed version to $res$ to
obtain the final value of the variable $v$ instead of the unprimed one. The
equality operator $\tt eq_{\tau}$ (rule $\tt[CONST]$) converts boolean
constants and ${{\small{\tt null}}}$ to their corresponding integer values.
Every local pointer variable $v$ (rule $\tt[LOCAL-PTR]$) is initially set to
dangling ($v^{\prime}{\not\hookrightarrow}\\_$).

A function call mn (the rule $\tt[CALL]$) is encoded as an inductive predicate
instance with an increasing ordering number $n_{l}$. This predicate instance
is spatially conjoined ($*$) into the precondition. The correctness of $*$ is
as follows. If mn allocates new heaps, the spatial conjunction states
correctly the separation between the new heaps and the heap in the
precondition. Otherwise, mn includes only pure constraint (e.g., ${\tt
emp}{\wedge}\pi$), the correctness is ensured by the axiom (Reynolds:LICS02):
$(\kappa_{1}{\wedge}\pi_{1}){*}({\tt
emp}{\wedge}\pi)\Leftrightarrow\kappa_{1}{\wedge}\pi_{1}{\wedge}\pi$. The
ordering number $n_{i}$ captures the order of function calls and is essential
for flow-sensitive analysis; it is used by $\tt{S2SAT_{eSL}}$ to choose a
predicate instance for unfolding. For each method, the execution engine
maintains one $n_{i}$ (initially assigned to 0) to encode the order of
function calls within the method. Moreover, if the body of mn has not been
processed, the engine generates a new ordering variable $n_{j}$ (initially
assigned to 0) and a new calling context prior to executes the source code of
mn.

A $\tt while$ loop is encoded as function call of a tail recursive procedure
through the two following steps. (i) First, the encoding of the loop body is
similar to the encoding of a procedure. (ii) Second, the loop invariant is
combined into the current states like the encoding of the procedure call.

The command $\tt new$ allocates and combines a new points-to predicate into
the precondition. The command $\tt free$ is encoded in a way such that it aids
for both safety and double free error discovery. Essentially, $\tt{free}~{}x$
is erroneous if the precondition $\Delta$ implies that either $\tt x$ is
either a dangling pointer $x^{\prime}{\not\hookrightarrow}\\_$ or
$x^{\prime}{=}{{\small{\tt null}}}$. $\tt{free}~{}x$ is safe if $\Delta$
implies that $\tt x$ has been allocated i.e.
${x^{\prime}}{{\scriptsize\mapsto}}c(...)$. The key point to detect double
free errors is that the post-condition of the command $\tt free~{}x$ must
ensure that the latest value of $\tt x$ points to a dangling heap, i.e.
$x^{\prime}{\not\hookrightarrow}\\_$. We notice that the contraction rule in
separation logic (i.e. $\kappa~{}{\implies}~{}\kappa{*}\kappa$), is not sound
for the spatial conjunction $*$, but sound for the non-heap formula (i.e.
$\pi~{}{\implies}~{}\pi{*}\pi$) (Ishtiaq:POPL01). Hence, while we could
conjoin the pure constraints (e.g., $x^{\prime}{=}{{\small{\tt null}}}$) to
encode the errors, we could not spatially conjoin
${x^{\prime}}{{\scriptsize\mapsto}}c(...)$ into $\Delta$ to encode the safety.

For memory safety of free and field access commands (field load and field
store) over a pointer, we delegate the binding to the logic layer where
symbolic path traces include explicit points-to predicates. In these rules,
${\small{\tt{\sc{{\small{\tt{S2SAT_{eSL}}}}}}}}(\Delta)$ checks whether
$\Delta$ is satisfiable (${\sc{{\small{\tt SAT}}}}$) or unsatisfiable
(${\sc{{\small{\tt UNSAT}}}}$). We note that
${\Delta{\wedge}(\pi_{1}\vee\pi_{2})}$ will be normalized into
$(\Delta{\wedge}\pi_{1})\vee(\Delta{\wedge}\pi_{2})$ prior to
${\small{\tt{\sc{{\small{\tt{S2SAT_{eSL}}}}}}}}(...)$ procedure being invoked
to process these disjuncts separately. Memory errors are detected through
verification conditions generated and stored in VC. In the cases of memory
safety, we add predicates with explicit binding notation (${\small{\tt
LD}}({x}{.}f_{i}{,}v{,}k)$ for field load and ${\small{\tt
ST}}({x}{.}f_{i}{,}v{,}k)$ for field store) into program states and postpone
the binding to the normalization of the satisfiability solver. Constraints
used to encode safety and pointer dereference errors are analogous to the
encoding of the $\tt free$ command. We remark that existing verification
systems based on separation logic like (Berdine:APLAS05; Chin:SCP:12;
Ruzica:TACAS:2014; Qiu:PLDI:2013) typically perform the binding while
symbolically executing programs by looking for its corresponding points-to
predicate in the precondition. Unlike these systems which are based on
entailment verification conditions, our system is based on satisfiability
solving.

To sum up, our symbolic execution engine transforms a program into a CHC
presented as a system of user-defined predicates. Finally, if no memory error
has been detected, the safety of the program is reduced to satisfiability of
the following query: ${\small{\tt
main}}(v_{1}{,}..{,}v_{n}{,}\varepsilon{,}{\tt
res})^{0}_{0}{\wedge}\varepsilon{=}1$. The generated verification condition is
solved by the $\tt{S2SAT_{eSL}}$ solver which is presented in the next
section.

##  5\. Solving Verification Conditions

In this section, we present the satisfiability procedure $\tt{S2SAT_{eSL}}$ in
detail. An overview of $\tt{S2SAT_{eSL}}$ is presented in Algorithm 1.
$\tt{S2SAT_{eSL}}$ takes a VC $\Delta$, which is a formula in our assertion,
as well as a place holder $[]$ for a counterexample as inputs. It outputs two
possible outcomes (if it terminates): $\tt SAT$ with a counterexample $\xi$ or
$\tt UNSAT$ with a proof. If it does not terminate some threshold time units,
we conclude the result is $\tt UNKNOWN$.

At line 1, an unfolding tree with only one root node $\Delta$ is constructed.
The loop (lines 2-11) then iteratively grows the tree while attempts to
establish an $\tt SAT$ proof or an $\tt UNSAT$ proof. In particular, at line
3, it checks whether any leaf node of the tree is $\tt SAT$ using a function
$\tt{\small{\tt UA_{eSL}}}$(${\mathcal{T}}$). Note that function $\tt
UA_{eSL}$ focuses on those leaf nodes which do not contain inductive
predicates, which we refer to as base formulas. If one of the leaf nodes is
proved to be satisfiable, the algorithm returns $\tt SAT$ at line 4 together
with the satisfiable node (obtained by using function $\tt get\\_sat$) as a
counterexample. Otherwise, any leaf node which is proved to be $\tt UNSAT$ is
marked so at line 5, using a function $\tt OA_{eSL}$. Afterwards, every
remaining leaf node is checked to see if it can be linked-back (to another
node in the tree) through function $\tt link\\_back_{eSL}$. At line 7, it
checks whether the tree is closed and returns $\tt UNSAT$ if so. Note that the
tree is considered closed if all leaf nodes are either proved $\tt UNSAT$ or
can be linked-back. Otherwise, at line 8, it chooses a leaf which is neither
marked $\tt UNSAT$ nor linked-back and grows the tree by unfolding the
inductive predicate in the node using function $\tt{\small{\tt
unfold_{eSL}}}$. Afterwards, the same process is repeated until either $\tt
SAT$ or $\tt UNSAT$ is returned or a timeout occurs.

1

input : ($\Delta$:[])

output : ($\tt SAT$, $\xi$) or $\tt UNSAT$

2 ${\mathcal{T}}{\leftarrow}\\{(\Delta{:}[])\\}$ build the unfolding tree with
only the root node

3while  _ ${\small{\tt true}}\,$ _ do

4 ($\tt is\\_sat$,${\mathcal{T}}$) $\leftarrow$ $\tt{\small{\tt
UA_{eSL}}}$(${\mathcal{T}}$); mark any leaf node of the tree satisfiable if it
is proven so

5 if $\tt is\\_sat$ then  return _( ${{\sc{{\small{\tt SAT}}}}}$, $\tt
get\\_sat$(${\mathcal{T}}$))_;

6 ${\mathcal{T}}{\leftarrow}{\small{\tt{\small{\tt
OA_{eSL}}}}}({\mathcal{T}});$ mark any leaf node of the tree unsatisfiable if
it is proven so

7 ${\mathcal{T}}{\leftarrow}{\small{\tt{\small{\tt
link\\_back_{eSL}}}}}({\mathcal{T}});$ check if any leaf node of the tree can
be linked back

8 if $\tt is\\_closed$(${\mathcal{T}}$) then  return _$\tt UNSAT$ _ check if
the tree is closed

9 else

10

11 ${\mathcal{T}}{\leftarrow}{\small{\tt{\small{\tt
unfold_{eSL}}}}}({\mathcal{T}})$; select a leaf and grow it with new leaves

12 end if

13

14 end while

Algorithm 1 $\tt{S2SAT_{eSL}}$ Satisfiability Procedure

### Function $\tt{\small{\tt UA_{eSL}}}$

Given an unfolding tree ${\mathcal{T}}$, function $\tt{\small{\tt UA_{eSL}}}$
identifies every leaf node of the tree which is a base formula and checks
whether the formula is satisfiable or unsatisfiable using a decision
procedure. If any of the formulas is satisfiable, function $\tt{\small{\tt
UA_{eSL}}}$ returns true; otherwise it returns false. Let ${\Delta^{b}}$ be a
base formula defined in our assertion language. The satisfiability of
${\Delta^{b}}$ is decided through four steps.

The first step is to normalize ${\Delta^{b}}$. The normalization of
${\Delta^{b}}$ to $\Delta$ is denoted as
${\parallel}{{\Delta^{b}}}{\parallel}$ ${\leadsto}$ $\Delta$. The
normalization process works as follows. First, we check whether there exists a
non-empty heap to ensure the absence of memory leaks. That is, there is no
memory leakage if the formula includes an empty heap. Formally,
${\parallel}{{\exists}\bar{w}{\cdot}{\tt emp}{\wedge}\pi@\overline{{\tt
E}}}{\parallel}~{}{\leadsto}~{}{\small{\tt false}}\,$. Next, we apply the
calculus on negation for size-1-heap formulae. We exhaustively detect
inconsistency on each individual pointer $x$ which appears in dangling
predicates $x{\not\hookrightarrow}\\_$, by applying the following.

$\begin{array}[]{l}\begin{array}[]{rclrcl}{\parallel}{{\exists}\bar{w}{\cdot}\Delta{\wedge}x{\not\hookrightarrow}\\_{\wedge}x{=}{{\small{\tt
null}}}}{\parallel}&{\leadsto}&{\small{\tt
false}}&{\parallel}{{\exists}\bar{w}{\cdot}\Delta{\wedge}\neg
x{\not\hookrightarrow}\\_{\wedge}x{\not\hookrightarrow}\\_}{\parallel}&{\leadsto}&{\small{\tt
false}}\\\
{\parallel}{{\exists}\bar{w}{\cdot}\Delta{*}{x}{{\scriptsize\mapsto}}c(\bar{v_{i}}){\wedge}x{\not\hookrightarrow}\\_}{\parallel}&{\leadsto}&{\small{\tt
false}}&{\parallel}{{\exists}\bar{w}{\cdot}\Delta{*}{x}{{\scriptsize\mapsto}}c(\bar{v_{i}}){\wedge}x{=}{{\small{\tt
null}}}}{\parallel}&{\leadsto}&{\small{\tt false}}\\\ \end{array}\\\
\begin{array}[]{rcl}{\parallel}{{\exists}\bar{w}{\cdot}\Delta{*}{x}{{\scriptsize\mapsto}}c(\bar{v_{i}}){\wedge}\neg
x{\not\hookrightarrow}\\_{\wedge}x{\neq}{{\small{\tt
null}}}}{\parallel}&{\leadsto}&{\parallel}{{\exists}\bar{w}{\cdot}\Delta{*}{x}{{\scriptsize\mapsto}}c(\bar{v_{i}})}{\parallel}\end{array}\end{array}$

Lastly, we bind the fields with the corresponding variables and remove all
explicit bindings $\tt load$ and $\tt store$ in ${\Delta^{b}}$ as follows. For
a sequence of load/store updates on the same field of a pointer, we perform
the following update in sequence. For a load ${\small{\tt
LD}}({z}{.}f_{i}{,}y{,}k)$, we bind y to the variable corresponding to the
field $f_{i}$ of the points-to predicate $x$ where $\pi\Rightarrow x{=}z$:

$\begin{array}[]{l}||{\exists}\bar{w}{\cdot}\kappa{*}{x}{{\scriptsize\mapsto}}c(f_{1}{:}v_{1}{,}..{,}f_{i}{:}v_{i}{,}...{,}f_{n}{:}v_{n}){\wedge}{\small{\tt
LD}}({z}{.}f_{i}{,}y{,}k){\wedge}\pi||~{}{\leadsto}~{}{\exists}\bar{w}{\cdot}\kappa{*}{x}{{\scriptsize\mapsto}}c(f_{1}{:}v_{1},..,f_{i}{:}v_{i},...f_{n}{:}v_{n}){\wedge}y{=}v_{i}{\wedge}\pi\\\
\end{array}$

Note that, if the points-to predicate
${x}{{\scriptsize\mapsto}}c(f_{i}{:}v_{i})$ does not exist, either
$x{\not\hookrightarrow}\\_$ or $x{=}{{\small{\tt null}}}$ must hold and,
hence, this formula must have been normalized to ${\small{\tt false}}\,$ in
the above step. For an update ${\small{\tt ST}}({z}{.}f_{i}{,}y{,}k)$, we
generate a refresh variable (e.g.,$v_{f}$) and then bind y to the primed
variable (e.g., $v_{i}^{\prime}$) corresponding to the field $f_{i}$ of the
points-to predicate $x$ where $\pi{\Rightarrow}x{=}z$:

$\begin{array}[]{l}||{\exists}\bar{w}{\cdot}\kappa{*}{x}{{\scriptsize\mapsto}}c(f_{1}{:}v_{1},..,f_{i}{:}v_{i},...f_{n}{:}v_{n}){\wedge}{\small{\tt
ST}}({z}{.}f_{i}{,}y{,}k){\wedge}\pi||~{}{\leadsto}~{}{\exists}\bar{w}{\cdot}(\kappa{*}{x}{{\scriptsize\mapsto}}c(f_{1}{:}v_{1},..,f_{i}{:}v_{i},...f_{n}{:}v_{n}){\wedge}\pi)[v_{f}/v_{i}^{\prime}]{\wedge}v^{\prime}_{i}{=}y\\\
\end{array}$

For example, in the motivating example in Sec 3, $\Delta_{43}$ is normalized
to $\Delta_{43}^{\prime}$ as follows. First, the solver binds the pointer x to
the corresponding point-to predicate. Next, it unifies fields: $\tt LD$
predicates of $x.next$ ($x_{1}$ is substituted by $r_{2}$) and $x.val$
($v_{1}$ is substituted by $n_{1}$). Afterward, the solver removes $\neg
x{\not\hookrightarrow}\\_$. The normalized formula $\Delta_{43}^{\prime}$ is:

$\begin{array}[]{lcl}\Delta^{\prime}_{43}&{\equiv}&{\parallel}{\Delta_{43}}{\parallel}{\equiv}x{\mapsto}node(n_{1}{,}r_{2}){*}sll(n_{1}{,}r_{2}{,}\varepsilon_{1})_{2}^{0}{*}loop_{13}(r_{2}{,}x^{\prime}{,}\varepsilon_{2})_{2}^{1}{\wedge}x{\neq}{{\small{\tt
null}}}{\wedge}\\\
&&n_{0}{\neq}0{\wedge}n_{1}{=}n_{0}{-}1{\wedge}n_{1}{\geq}0{\wedge}n_{0}{\geq}0{\wedge}\varepsilon_{1}{=}0{\wedge}\varepsilon_{2}{=}1{\wedge}\varepsilon_{0}{=}1\\\
\end{array}$

The second step is to reduce the normalized formula into a first-order logic
formula. Let $\Delta$ be the normalized formula. We first discard the
$@\overline{{\tt E}}$ annotation and dangling predicates in $\Delta$ since
they become redundant after normalization. After that, we transform the
resultant formula into a first-order logic formula through a reduction
function ${\bf{\scriptstyle eXPure}}$ which is defined as follows.

$\begin{array}[t]{l}{\bf{\scriptstyle
eXPure}}(\exists\bar{w}{\cdot}~{}{x_{1}}{{\scriptsize\mapsto}}c_{1}(\bar{v}_{1}){*}...{*}{x_{n}}{{\scriptsize\mapsto}}c_{n}(\bar{v}_{n})~{}{\wedge}~{}\pi)~{}~{}{\equiv}~{}~{}{\small{\tt\exists}}~{}\bar{w}{\cdot}~{}{\bigwedge}\\{x_{i}{\neq}{{\small{\tt
null}}}\mid i{\in}\\{1..n\\}\\}~{}{\wedge}~{}\bigwedge\\{x_{i}{\neq}x_{j}\mid
i,j{\in}\\{1..n\\}\text{ and }i{\neq}j\\}~{}{\wedge}~{}\pi\end{array}$

Intuitively, function $\tt{\bf{\scriptstyle eXPure}}$ generates first-order
constraints to ensure that each points-to predicate is allocated (not equal to
${{\small{\tt null}}}$) and two points-to predicates connected by separating
conjunction $*$ are not aliasing. The following lemma establishes the
correctness of the reduction.

###### Lemma 5.1 ((Loc:CAV:2016)).

For all ${\Delta^{b}}$ such that $\tt{\bf{\scriptstyle
eXPure}}$(${\parallel}{{\Delta^{b}}}{\parallel}$) ${\leadsto}$ $\Delta$,
${\small{\tt{\bf{\scriptstyle eXPure}}}}(\Delta)$ and $\Delta$ are equi-
satisfiable. $\square$

The third step is to eliminate existential quantifiers $\bar{w}$ using a
projection function $\Pi$. Function ${\Pi}(\pi,\bar{w})$ eliminates the
existential quantifiers on variables $\bar{w}$ where $\bar{w}$ are pointer-
typed. It is defined as follows.

$\begin{array}[]{l}\begin{array}[]{rclrcl}{\Pi}({\small{\tt
true}}\,,\bar{w})&=&{\small{\tt
true}}&\qquad\qquad{\Pi}(v_{1}{\not=}v_{1}{\wedge}\pi_{1},\bar{w})&=&{\small{\tt
false}}\\\ \end{array}\\\
\begin{array}[]{rcl}{\Pi}(v_{1}{=}v_{2}{\wedge}\pi_{1},\bar{w})&=&\begin{cases}{\Pi}(\pi_{1}[v_{1}/v_{2}],\bar{w})&\quad\text{if
}v_{1}\in\bar{w}\\\ {\Pi}(\pi_{1}[v_{2}/v_{1}],\bar{w})&\quad\text{if
}v_{2}\in\bar{w}\text{ and }v_{1}\not\in\bar{w}\\\
v_{1}{=}v_{2}{\wedge}{\Pi}(\pi_{1},\bar{w})&\quad\text{otherwise}\end{cases}\\\
{\Pi}(v_{1}{\not=}v_{2}{\wedge}\pi_{1},\bar{w})&=&\begin{cases}v_{1}{\not=}v_{2}{\wedge}{\Pi}(\pi_{1},\bar{w})&\quad\text{if
}v_{i}{\not\in}\bar{w},i{=}\\{1,2\\}\\\
{\Pi}(\pi_{1},\bar{w})&\quad\text{otherwise}\end{cases}\end{array}\end{array}$

For soundness, we assume that $\pi$ is sorted s.t. equality conjuncts are
processed before dis-equality ones.

###### Lemma 5.2.

${\Pi}(\pi_{i},\bar{w})$ and $\pi_{i}$ are equi-satisfiable. $\square$

The proof which is based on a structural induction on the number of
(dis)equalities is presented in App. A.

Lastly, we invoke an existing decision procedure for first-order logic formula
(e.g., Z3 (TACAS08:Moura)) to decide the resultant formula. If the formula is
decided to be satisfiable, the function $\tt{\small{\tt UA_{eSL}}}$ returns
true.

### Function $\tt{\small{\tt OA_{eSL}}}$

Given the unfolding tree ${\mathcal{T}}$, the function $\tt{\small{\tt
OA_{eSL}}}$ checks every leaf node. If the leaf is a base formula, the same
decision procedure used in the function $\tt{\small{\tt UA_{eSL}}}$ is applied
to check whether it is $\tt UNSAT$. If the leaf is a formula containing
inductive predicates, it is transformed such that every occurrence of those
inductive predicates is substituted by its over-approximated invariant.
Afterwards, the same decision procedure used in the function $\tt{\small{\tt
UA_{eSL}}}$ is applied to check whether it is $\tt UNSAT$. Any time a formula
is proved to be $\tt UNSAT$, the corresponding leaf node is marked $\tt
UNSAT$.

### Function $\tt{\small{\tt link\\_back_{eSL}}}$

The function $\tt link\\_back_{eSL}$ checks every leaf node $\Delta^{bud}$
which is not marked $\tt UNSAT$ and checks whether there exists an interior
node $\Delta^{comp}$ such that the spatial part of $\Delta^{bud}$ is subsumed
by the spatial part of $\Delta^{comp}$ and the numeric part of all base
formulas generated by $\Delta^{bud}$ are unsatisfiable. In particular, $\tt
link\\_back_{eSL}$ checks whether there exists a well-founded ordering
relation $R$ between $\Delta^{bud}$ and $\Delta^{comp}$ so as to form an
infinite path following the path between these two nodes. For global
infinitary soundness (Brotherston:APLAS:12; Loc:CAV:2016), $\tt
link\\_back_{eSL}$ only considers those $\Delta^{bud}$ and $\Delta^{comp}$ of
the following form.

$\begin{array}[]{rcl}\Delta^{comp}&{\equiv}&\exists\bar{w}_{1}{\cdot}\kappa_{b_{1}}{*}{\small{\tt
P_{1}}}(\bar{t}_{1})_{m}^{0}{*}...{*}{\small{\tt
P_{i}}}(\bar{t_{i}})_{m}^{i}{\wedge}\pi_{1}\\\
\Delta^{bud}&{\equiv}&\exists\bar{w}_{2}{\cdot}\kappa_{b_{2}}{*}{\small{\tt
P_{1}}}(\bar{t}_{1}^{\prime})_{n}^{0}{*}...{*}{\small{\tt
P_{i}}}(\bar{t_{k}^{\prime}})_{n}^{k}{\wedge}\pi_{2}\end{array}$

where $\tt k{\geq}i$, $\tt n{>}m$, $\kappa_{b_{1}}$ and $\kappa_{b_{2}}$ are
base formulas. The constraint $\tt n{>}m$ implies that every occurrence of
inductive predicate must be unfolded at least once. In particular,
${{\small{\tt link\\_back_{eSL}}}}(\Delta^{bud}{,}\Delta^{comp})$ is
implemented as follows.

  1. (1)

Firstly, load $\tt LD$ and store $\tt ST$ predicates are normalized.

  2. (2)

Secondly, free points-to predicates are exhaustively matched. For every
${x_{j}}{{\scriptsize\mapsto}}c_{j}(\\_\,)\in\kappa_{b_{1}}$ and
$x_{j}\notin\bar{w}_{1}$, there exists
${x^{\prime}_{j}}{{\scriptsize\mapsto}}c_{j}(\\_\,)\in\kappa_{b_{2}}$ such
that $\pi_{2}\Rightarrow x_{j}^{\prime}{=}x_{j}$; and vice versa, for every
${x_{j}}{{\scriptsize\mapsto}}c_{j}(\\_\,)\in\kappa_{b_{2}}$ and
$x_{j}\notin\bar{w}_{2}$, there exists
${x^{\prime}_{j}}{{\scriptsize\mapsto}}c_{j}(\\_\,)\in\kappa_{b_{1}}$ such
that $\pi_{1}\Rightarrow x_{j}^{\prime}{=}x_{j}$.

  3. (3)

Thirdly, occurrences of inductive predicates are exhaustively matched. First,
we replace every existentially quantified argument of inductive predicates in
$\kappa_{b_{1}}$ and $\kappa_{b_{2}}$ by $\\_\,$. After that for every
${\small{\tt P_{j}}}(\bar{t}_{j})_{m}^{\\_}\,\in\kappa_{b_{1}}$, there exists
${\small{\tt P_{j}}}(\bar{t}_{j})_{n}^{\\_}\,\in\kappa_{b_{2}}$ and vice
versa. We remark that this matching considers equality constraints in
$\pi_{1}$ and $\pi_{2}$.

  4. (4)

Fourthly, (in)quality over pointers are matched. Let $\pi_{1}^{\prime}$
($\pi_{2}^{\prime}$) be the set of spatial constraints of $\pi_{1}$
($\pi_{2}$, respectively). Let
$\pi_{1}^{\prime\prime}{=}{\Pi}({\bf{\scriptstyle
eXPure}}(\exists\bar{w_{1}}{\cdot}\kappa_{b_{1}}){\wedge}\pi_{1},\bar{w_{1}})$
and $\pi_{2}^{\prime\prime}{=}{\Pi}({\bf{\scriptstyle
eXPure}}(\exists\bar{w_{1}}{\cdot}\kappa_{b_{1}}){\wedge}\pi_{1},\bar{w_{2}})$.
Check whether $\pi_{1}^{\prime\prime}\Rightarrow\pi_{2}^{\prime\prime}$ and
$\pi_{2}^{\prime\prime}\Rightarrow\pi_{1}^{\prime\prime}$.

  5. (5)

Lastly, we compute a disjunctive set of possible base formulas generated by
the bud. Back-link is decided if all disjuncts of this set are unsatisfiable.
The set is a conjunction of a disjunctive set of base formulas over the
spatial part and the invariant (fixed point) over the numeric part.

    1. (a)

The set of all base formulas is collected from base leaf nodes (after applying
the spatial projection) in the subtree rooted by the companion
$\Delta^{comp}$.

    2. (b)

The invariant is obtained by first applying numeric projection over all
inductive predicates in the bud $\Delta^{bud}$ and then conjoining the fixed
points of these numeric predicates.

Intuitively, steps 2-4 show that the set of base leaf nodes over spatial
projection generated by the bud is subsumed by the set generated by the
companion. Step 5 computes the set of all possible base leaf nodes by
combining the set of base leaf nodes over spatial projection with invariants
of the numeric projections. If all these nodes are unsatisfiable, there is no
counter-example following the bud. Thus, it is safe to mark the bud closed.

### Function $\tt{\small{\tt unfold_{eSL}}}$

The function $\tt unfold_{eSL}$finds the first leaf node $\Delta$ in the tree
which is neither marked $\tt UNSAT$ nor linked-back in the breath-first-search
order. It then unfolds an inductive predicate in $\Delta$ to form children of
the node. If $\Delta$ contains multiple occurrences of inductive predicates,
an occurrence ${\small{\tt P}}(\bar{v})_{u}^{o}$ is selected if $\tt u$ is the
smallest number of unfoldings. If there are more than one occurrences that
have the same smallest number of unfoldings, the one selected if its $\tt o$
is the smallest. In general, $\Delta$ is a formula in the form of
${\exists}\bar{w}_{0}{\cdot}~{}\kappa{*}{\bigvee}(\Delta_{i}~{}\tau_{i})(\wedge)\pi$.
The set of new leaves are:
$\\{{({\exists}\bar{w}_{0}{\cdot}\kappa{*}\Delta_{i}{\wedge}\pi){:}(l{::}({\small{\tt
P}}{,}\tau_{i}))}\\}$. $\tt{\small{\tt unfold_{eSL}}}$ is implemented as
follows. $\tt{\small{\tt unfold_{eSL}}}$ takes a formula
${\exists}\bar{w}_{0}{\cdot}~{}\kappa{*}{\small{\tt
P}}(\bar{v})_{u}^{o}{\wedge}\pi$ labeled with path trace $l$ as input. It
unfolds the predicate instance $\tt P$ by spatially conjoining branches of the
instance ${\small{\tt P}}(\bar{v})$ into the formula. This step also combines
the path traces of the branches with the present path trace. For instance, the
interprocedural path corresponding to the leaf $\Delta_{33}$ of the motivating
example is $\tt[(main,[2]);(sll,[1]);[(inv_{12},[1;1])]]$. This trace captures
the program path from the entry of the procedure $\tt main$ to the $\tt else$
branch, call function $\tt sll$ once ($\tt if$ branch) and to the body of the
$\tt while$ loop once ($\tt else$ branch). We remark that if $\Delta_{i}$
includes load/store predicates, its sequence number must be set to be an
increasing number. Moreover, the unfolding and ordering numbers are updated as
follows. Let ${\small{\tt Q}}(\bar{t})^{o_{l}}$ be an occurrence of an
inductive predicate in a branch of the definition of $\tt P$. Its unfolding
number is set to $\tt u{+}1$ and its sequence number is set to $o_{l}{+}o$.

##  6\. Soundness and Termination

### Soundness

Given a program defined in our core language shown in Figure 5, the program
has an error if and only if there is a satisfiable VC; and the program has no
error if and only if all VCs are unsatisfiable. The soundness of our symbolic
execution follows the systems presented in (Berdine:APLAS05; Chin:SCP:12). In
the following, we analyze the soundness and complexity of our decision
procedure. $\tt{S2SAT_{eSL}}$ is a non-trivial instantiation of the general
satisfiability procedure $\tt{S2SAT}$ presented in (Loc:CAV:2016).
$\tt{S2SAT}$ is designed for deciding a sound and complete base theory
$\mathcal{L}$ augmented with inductive predicates. Furthermore, the base
theory $\mathcal{L}$ must satisfy the following properties: (i) $\mathcal{L}$
is closed under propositional combination and supports boolean variables; (ii)
there exists a complete decision procedure for $\mathcal{L}$. It is easy to
check that $\tt{S2SAT_{eSL}}$ inherits the soundness of the $\tt{S2SAT}$
framework. As an instantiation of $\tt{S2SAT}$ framework, $\tt{S2SAT_{eSL}}$
is sound for both $\tt SAT$ and $\tt UNSAT$. Its soundness is ensured under
the following assumptions: the base logic is both sound and complete, and
functions $\tt{\small{\tt UA_{eSL}}}$, $\tt{\small{\tt OA_{eSL}}}$ and $\tt
link\\_back_{eSL}$ are sound.

### Termination

Our encoding is always terminating. By following the results proved in
(Loc:CAV:2016), we know that $\tt{S2SAT_{eSL}}$ always terminates if a VC is
$\tt SAT$ and may not terminate if a VC is $\tt UNSAT$. In the following, we
show that $\tt{S2SAT_{eSL}}$ terminates (and thus becomes a decision
procedure) for a fragment, which we refer to as ${\small{\tt SLA^{P}}}$ in the
following.

${\small{\tt SLA^{P}}}$ is a language which supports all the syntax shown in
Figure 1 except that inductive predicates are restricted as follows. An
inductive predicate ${\small{\tt P}}(\bar{t})$ in ${\small{\tt SLA^{P}}}$
either does not contain a recursive branch or its numeric projection is in the
form of:

${\tt pred}~{}{\small{\tt
P^{N}}}(\bar{t}^{N}){\equiv}\pi_{0}\vee{\exists}\bar{w}{\small{\tt
P^{N}}}(\bar{v}_{1}^{N}){*}...{*}{\small{\tt
P^{N}}}(\bar{v}_{l}^{N}){\wedge}\pi_{r}$

where $\pi_{0}$ is a disjunction of pure formulas without occurrences of
inductive predicates, and $\pi_{r}$ is a conjunction of either arithmetical
constraints over data fields or constraints over arithmetical parameters of
periodic relations $R$ (Marius:CAV:2010; Makoto:APLAS:2016) which is defined
as follows. Given an inductive predicate ${\small{\tt P^{N}}}(\bar{x})$ where
$\bar{x}$ is the sequence of $m$ integer parameters. Let ${\small{\tt
P^{N}}}(\bar{v}_{i})$ ($i\in\\{1...l\\}$) be any sub-term in one of its
recursive branches. $R\in Z^{m}\times Z^{m}$ is an integer relation over
variables $\bar{x}$ and $\bar{v}_{i}$, its transitive closure is written as
$R^{+}{=}\bigcup_{i{=}1}^{\infty}$ where $R^{1}{=}R$ and
$R^{i{+}1}{=}R^{i}{\circ}R$ for all $i{\geq}1$. The relation $R$ is defined as
one of the following two forms.

  * •

Octagonal relation (Marius:CAV:2010). An octagonal relation is a finite
conjunction of the form
$R(x_{1}{,}x_{2}){\equiv}\underline{+}x_{1}\underline{+}x_{2}{\leq}k$ where
$k$ is an integer constant,
$x_{1}{,}x_{2}{\in}(\bar{x}{\cup}\bar{v}_{1}\cup...\cup\bar{v}_{l})$.

  * •

DPI relation (Makoto:APLAS:2016). A DPI relation is a finite conjunction of
constraints of the form $R(\bar{y}){\equiv}y_{i}+f(\bar{z}){\leq}k_{1}$, or
$R(\bar{y}){\equiv}y_{i}+f(\bar{z}){\geq}k_{2}$ where
$\bar{y}\subseteq\bar{x}{\cup}\bar{x}^{\prime}$,
$y_{i}\in\bar{x}{\cup}\bar{x}^{\prime}$,
$\bar{z}\subseteq(\bar{x}{\cup}\bar{v}_{1}\cup...\cup\bar{v}_{l})$, $k_{1}$
and $k_{2}$ are integer numbers and

$\vspace{-2mm}f(\bar{z}){\equiv}z_{i}~{}|~{}min(f(\bar{z_{1}}),f(\bar{z_{2}}))~{}|~{}max(f(\bar{z_{1}}),f(\bar{z_{2}}))$

(Marius:CAV:2010) and (Makoto:APLAS:2016) show that the transitive closure of
these periodic relations is Presburber-definable and effectively computable.

In the following, we prove that $\tt{S2SAT_{eSL}}$ terminates for
unsatisfiable ${\small{\tt SLA^{P}}}$ formulas. We prove that for each leaf
(respectively a bud) of the unfolding tree derived for an unsatisfiable
formula if it has not been classified as $\tt UNSAT$ yet, it must be linked
back to an interior node (respectively a corresponding companion) to form a
cyclic proof in finite steps. We remark that in the following, we only
consider companions which are descendant of a bud. We recap that a bud is
linked to a companion if free pointer variables of points-to predicates and
predicate instances are exhaustively matched and fixed points of all numeric
projections of buds are computable. In addition, the function $\tt
link\\_back_{eSL}$ does not rely on constraints over data fields. We use
$\pi^{df}$ to denote the constraint on variables of data fields of points-to
predicates. We show $\tt{S2SAT_{eSL}}$ always terminates for ${\small{\tt
SLA^{P}}}$ through three steps. First, we show that the termination of
$\tt{S2SAT_{eSL}}$ does not rely on the pure constraints over data fields of
points-to predicates.

###### Lemma 6.1.

Given a bud
$\Delta_{bud}{\equiv}\exists\bar{w}_{2}\cdot\Delta_{2}{\wedge}\pi^{df}_{2}$ if
there exists a companion
$\Delta_{comp}{\equiv}\exists\bar{w}_{1}\cdot\Delta_{1}{\wedge}\pi^{df}_{1}$
such that the subformula $\exists\bar{w}_{2}\cdot\Delta_{2}$ can be linked
back to the subformula $\exists\bar{w}_{1}\cdot\Delta_{1}$, then
$\Delta_{bud}$ can be linked back to $\Delta_{comp}$.

The proof is presented in App. B.

Secondly, we prove that $\tt{S2SAT_{eSL}}$ terminates for formulae including
spatial-based inductive predicates, those predicates whose parameters are
pointer-typed. The quantifier elimination of function ${\small{\tt\bf
sat}}({\Delta^{b}})$ implies that the satisfiability problem in this fragment
does not rely on existentially quantified variables. In other words, this
problem is based on free variables. As the number of these free variables in a
formula is finite, checking satisfiability in this fragment is decidable.

###### Lemma 6.2.

$\tt{S2SAT_{eSL}}$ terminates for a system of spatial-based inductive
predicates.

Lastly, we show that $\tt{S2SAT_{eSL}}$ always terminates for formulas which
contain inductive predicates with shape, pure constraints over data fields and
periodic relations over arithmetical parameters. We show that given a formula
in ${\small{\tt SLA^{P}}}$, $\tt{S2SAT_{eSL}}$ can always construct a cyclic
proof in finite time.

###### Theorem 6.1.

$\tt{S2SAT_{eSL}}$ terminates for ${\small{\tt SLA^{P}}}$.

This theorem immediately follows from lemma 6.1, lemma 6.2 and the results in
(Marius:CAV:2010; Makoto:APLAS:2016) which state that the transitive closure
of these periodic relations is Presburber-definable and effectively
computable.

##  7\. Implementation and Evaluation

We have implemented our approach in a prototype tool named $\tt S2_{td}$ for
reasoning about heap-based programs. $\tt S2_{td}$ is programmed in Ocaml and
uses Z3 (TACAS08:Moura) for checking satisfiability of first-order logic
formulae. It is known that forward-based strongest postcondition calculus in
separation logic is incomplete in the presence of $\tt free$ statements
(Berdine:APLAS05). Hence, in the presence of an erroneous trace, $\tt S2_{td}$
produces a counterexample annotated with a stack record of function calls
$\xi$ leading to the error. Each function call includes an intra-procedural
path trace label. From this counter example, we extract the error location and
generate error witnesses (Beyer:FSE:2015) in GraphXML
(DBLP:conf/gd/BrandesEHHM00). These witnesses can be validated independently
to validate the errors. Furthermore, they are useful for debugging and can be
validated by other validation tools, e.g., (Heizmann:CAV:13; Dirk:CAV:2015).

Table 1. Experimental Results Tool | #s$\surd$ | #e$\surd$ | #unk | #s✗ | #e✗ | pts | mins
---|---|---|---|---|---|---|---
PredatorHP (Predator:SV:16) | 37 | 46 | 35 | 14 | 0 | -104 | 49
Cascade (Wei:VMCAI:2014) | 0 | 8 | 124 | 0 | 0 | 8 | 50
SeaHorn (Gurfinkel:CAV:2015) | 59 | 58 | 5 | 10 | 0 | 16 | 19
ESBMC (Cordeiro:2011:ICSE) | 36 | 41 | 52 | 0 | 3 | 17 | 115
UAutomizer (Heizmann:CAV:13) | 27 | 30 | 75 | 0 | 0 | 84 | 113
CPA-Seq (Beyer:CAV:2007) | 54 | 46 | 31 | 0 | 1 | 122 | 79
CBMC (Clarke:TACAS:2004) | 44 | 51 | 36 | 1 | 0 | 123 | 142
Smack-Corral (Haran:TACAS:2015) | 44 | 50 | 38 | 0 | 0 | 138 | 125
$\tt S2_{td}$ | 59 | 57 | 16 | 0 | 0 | 175 | 38

We conduct an experiment on verifying a set of heap-based programs which
requires reasoning over both shape and arithmetic domains in order to
establish their correctness. We focus on programs containing at least one loop
or one recursive method call. Our test subjects include 132 programs where 24
of them are taken from Heap Data Structures category in the SV-COMP benchmark
repository (Dirk:SVCOMP:2016), 98 of them are from Recursive category in the
repository (Dirk:SVCOMP:2016) and the rest 10 are generated by us. The
programs in the last group manipulate complex data structures (e.g. trees
whose leaves are linked as a list (Loc:CAV:2014)), which are not yet to be
included in (Dirk:SVCOMP:2016). Furthermore, each program has at least one
pure assertion. Timeout is set to 180 seconds. We compare our verification
system $\tt S2_{td}$ with the state-of-the-art verification tools participated
in the SV-COMP2016 competition. The readers are referred to Sec. 8 for details
on these systems. The experiments were performed on a machine with an Intel
i7-6500U (2.5GHz) processor and 4 GB of RAM with Ubuntu 14.04 (64 bit) OS. The
results are reported in Table 1. The first column shows the verification
systems. Note that we apply the same binaries and settings as they were used
in the SV-COMP (Dirk:SVCOMP:2016). The next three columns show the number of
correct safe (s$\surd$), correct error (e$\surd$) and unknown. The next two
columns capture the number of false positives (s✗) and false negatives (e✗).
We rank these tools based on their points (pts column). Following the SV-COMP
2016 competition, we gave +2 for one s$\surd$, +1 for one e$\surd$, 0 for unk
and -16 for one s✗ and -32 for one e✗. The last column shows the total time in
minutes. The results show that CHC-based tools, SeaHorn and $\tt S2_{td}$, are
the most efficient. SeaHorn was the fastest. However, it produced 10 false
positives on programs taken from Heap Data Structures category. We suspect
that this incompleteness problem comes from the lack of a CHC encoding for
heap-manipulating programs. These experimental results also imply that $\tt
S2_{td}$ is effective and efficient; it achieved the best score within a short
time.

### Limitation

The current implementation of $\tt{S2SAT_{eSL}}$ has not yet supported the
reasoning on pointer arithmetic, string, arrays, and (non)termination.
Moreover, our front-end supports only a limited fragment of C programs, e.g.,
with no $\tt enum$ and $\tt goto$ commands nested in loops.

##  8\. Related Work

Closest to our work are CHC-based verification systems, e.g. Duality
(export:180055), HSF (Grebenshchikov:PLDI:2012), SeaHorn (Gurfinkel:CAV:2015)
and $\mu$Z (Hoder:CAV:2011). In the last few years, Rybalchelko et. al.
developed a framework to support for a new verification methodology which uses
CHC as an intermediate language. The CHC encodes both safety and error
properties of the input programs. Details on these systems based on CHC were
summarized in (Nikolaj:SMT:2012; DBLP:conf/birthday/BjornerGMR15). As
mentioned above, these systems focus on non-heap programs whereas we target
heap-based programs.

Verification systems support for both verifying and falsifying safety
properties over lists-based data structures include property-directed
reachability (PDR) (Itzhaky:CAV:2014; Aleksandr:CAV:2015), interpolation
(Aws:ESOP:2015), and separation logic (Berdine:APLAS05; Ruzica:TACAS:2014;
Navarro:APLAS:2013). PDR is a sound and relatively complete framework for
shape analysis using abstraction predicates. Given a safety property and an
abstract domain, this approach could either verify, or generate a concrete
counterexample or report that the abstract domain is not expressive enough to
establish the proof. Spatial interpolation (Aws:ESOP:2015) takes shape
analysis and a property as inputs. It defines a bounded abduction and refines
this bound based on interpolation of non-heap domains until it can verify the
safety or detect a bug. Smallfoot (Berdine:APLAS05) is among the first
verifiers which provided foundation for separation logic field (a decidable
fragment, symbolic execution rules) and a practical system. GRASShopper
(Ruzica:TACAS:2014) and Asterix (Navarro:APLAS:2013) encode the verification
conditions of list-based programs into an SMT supported form. While this SMT-
based approach efficiently supports for the combination of heap and pure
domains, the encoding is limited. Our encoding is expressive as it precisely
captures the program semantics and was not fixed into any predefined
abstraction. Moreover, VCs generated by the existing verification systems
based on separation logic rely on entailments and their completeness is
limited to simply linked data structures. In contrast, VCs generated by our
system are satisfiability queries; the expressiveness of the decidable
fragment which includes complex data structures is promising to advance the
completeness of the verification system.

Software verification systems based on Bounded Model Checking (BMC) have been
implemented for falsification, e.g. (Clarke:TACAS:2004; Wei:VMCAI:2014;
Herbert:SEFM:2015; Morse:TACAS:2013; Martin:SAS:2015). These systems under-
approximate input programs to confirm error with a concrete counterexample.
For example, Cascade (Wei:VMCAI:2014) eliminates loops by using bounded loop
unfolding; Map2Check (Herbert:SEFM:2015) generates and checks unit tests for C
programs. To extend BMC to verification, ESBMC (Morse:TACAS:2013) combines BMC
with k-induction. Even more, 2LS (Martin:SAS:2015) was designed to unify BMC,
k-induction and abstract interpretation. However, it is unclear how these
systems could verify and falsify properties of heap-based programs like $\tt
S2_{td}$.

Safety verification systems based on abstract interpretation have been
developed for verification (not falsification), e.g. (Chin:SCP:12; CAV08:Yang;
Dudka:CAV:2011; Holik:CAV:2013; Loc:CAV:2014). These systems over-approximate
input programs to verify the absence of errors. To extend these systems to
falsification, one can run these tools and those based on under-approximation
in parallel. For an example, PredatorHP (Predator:SV:16) runs several
instances of Predator (Dudka:CAV:2011) in parallel and composes the results
into a final verification verdict. One of them soundly over-approximates the
behaviour of the input program; the rest of them under-approximates the input
program with bounded depth-first search while traversing the state space. As
information can not be exchanged among these Predator instances, this
combination implies a mixture rather than a genuine compound like $\tt
S2_{td}$.

Decision procedures for satisfiability problems in separation logic have been
well developed. Initial approaches like Smallfoot (Berdine:APLAS05), Asterix
(NavarroPerez:PLDI:2011), (Cook:CONCUR:2011) and SPEN (Enea:APLAS:2014) focus
on linked lists and (in)equalities over pointer-typed variables.
(DBLP:conf/cade/IosifRS13) extends the decidable fragment with tree width
structures. SLSAT (Brotherston:LISC:14) proposes a decision procedure for
arbitrary inductive definitions. For arithmetic, SMT-based procedures,
GRASShoper (Piskac:CAV:2013) and Asterix (Navarro:APLAS:2013), are among the
first decision procedures for decidable fragments for which shape definitions
are restricted in linked lists. The decidable fragment including shape and
arithmetic has been recently widened in extended GRASShoper
(Ruzica:TACAS:2014), CompSPEN (Gu:IJCAR:2016), $\tt S2SAT_{SL}$ (Loc:CAV:2016)
and (Makoto:APLAS:2016). While CompSPEN extends the graph-based algorithm
(Cook:CONCUR:2011) to doubly-linked list, $\tt S2SAT_{SL}$ is an instantiation
of a cyclic-proof-based framework $\tt SLSAT$ (Loc:CAV:2016). Our proposed
procedure $\tt{S2SAT_{eSL}}$ is another instantiation of $\tt SLSAT$. Compared
with $\tt S2SAT_{SL}$, $\tt{S2SAT_{eSL}}$ has two main differences. First, it
additionally supports a fragment of separation logic for memory safety
verification. In particular, $\tt{S2SAT_{eSL}}$ provides the normalization to
support dangling pointers and load/store predicates. Second, it supports a new
back-link function in which the subsumption between a bud and a companion is
checked by first linking spatial part back and then computing the fixed point
for the arithmetic part. By doing so, it extends the expressiveness of the
decidable fragment. While (Loc:CAV:2016) supports for a fragment restricted in
both shape and arithmetic, $\tt{S2SAT_{eSL}}$ supports arbitrary inductive
definitions with periodic relations over arithmetical parameters. The decision
procedure in (Makoto:APLAS:2016) reduces the satisfiability problem of an
inductive predicate into the satisfiability problem of its numeric part. The
reduction requires that the spatial part of its recursive branch is
existentially quantified. In contrast, our decision procedure here creates
back-links to obtain all base formulas over the spatial part and thus it can
support arbitrary spatial-based inductive predicates.

##  9\. Conclusion and Future Work

This work advocates the approach to automatic verification of heap-based
programs using CHC. We have presented $\tt S2_{td}$, a CHC-based verification
system using separation logic. Given a C program, our system transforms it
into CHCs and invokes a novel satisfiability solver $\tt{S2SAT_{eSL}}$ to
solve these CHCs. $\tt{S2SAT_{eSL}}$ examines under-approximation (so as to
prove $\tt SAT$), over-approximation (so as to prove $\tt UNSAT$), or
constructs a cyclic proof (so as to prove $\tt UNSAT$). We have also
implemented a prototype and evaluated it on a set of heap-manipulating
programs. The experimental results shows that CHC-based approach is promising
for software verification. For future work, we may extend the system to verify
array-based programs. (Non)Termination analysis using CHCs might be another
future work.

##  Appendix A Proof of Lemma 5.2

While Lemma A.1 states the “if” direction, Lemma A.2 states the “only if”
direction.

###### Lemma A.1.

Let $\exists\bar{w}{\cdot}\alpha$ be a (dis)equality conjunction. If
$s\models\alpha$ then $s\models{\Pi_{{\small{\tt SH}}}}(\alpha,\bar{w})$

Proof We prove lemma A.1 by induction on size of $\alpha$. The proof for this
lemma is based on semantics of $\wedge$.

  * •

Case $\alpha{\equiv}{\small{\tt true}}\,$. Trivially.

  * •

Case $\alpha{\equiv}v_{1}{=}v_{2}{\wedge}\alpha_{1}$ and $v_{1}\in\bar{w}$.

$\begin{array}[]{ll}&s\models\alpha\\\ \Longleftrightarrow&s\models
v_{1}{=}v_{2}\text{ and }s\models\alpha_{1}~{}~{}(\text{semantics of
}\wedge)\\\ \Longrightarrow&s\models\alpha_{1}[v_{2}/v_{1}]\\\ \end{array}$

  * •

Case $\alpha{\equiv}v_{1}{=}v_{2}{\wedge}\alpha_{1}$ and
$v_{1}\not\in\bar{w}$, $v_{2}\in\bar{w}$.

$\begin{array}[]{ll}&s\models\alpha\\\ \Longleftrightarrow&s\models
v_{1}{=}v_{2}\text{ and }s\models\alpha_{1}~{}~{}(\text{semantics of
}\wedge)\\\ \Longrightarrow&s\models\alpha_{1}[v_{1}/v_{2}]\\\ \end{array}$

  * •

Other cases are similar

###### Lemma A.2.

Let $\exists\bar{w}{\cdot}\alpha$ be a satisfiable (dis)equality conjunction.
If $s\models{\Pi_{{\small{\tt SH}}}}(\alpha,\bar{w})$ $\exists
s^{\prime}{\cdot}s\subseteq s^{\prime}\text{ and }s^{\prime}\models\alpha$

Proof By induction on size of $\alpha$.

  1. (1)

Case $\alpha{\equiv}{\small{\tt true}}\,$. Trivially.

  2. (2)

Case $\alpha{\equiv}v_{1}{=}v_{2}{\wedge}\alpha_{1}$ and $v_{1}\in\bar{w}$.

By assumption, $s\models{\Pi_{{\small{\tt SH}}}}(\alpha_{1},\bar{w})$. By
induction, there exists a stack $s_{1}$ such that $s\subseteq s_{1}$ and
$s_{1}\models{\alpha_{1}}$. We examines four subcases:

    1. (a)

Case $s_{1}(v_{1})$ and $s_{2}(v_{2})$ are both defined. Never.

    2. (b)

Case $s_{1}(v_{1})$ is defined and $s_{1}(v_{2})$ is undefined. We define
$s_{2}(v_{2})$ such that $s_{2}(v_{2}){=}s_{1}(v_{1})$. This implies
$s_{1}\cup s_{2}\models v_{1}{=}v_{2}$. Thus, $(s_{1}\cup
s_{2})\models\alpha$.

    3. (c)

Case $s_{1}(v_{2})$ is defined, $s_{1}(v_{1})$ is undefined and both are
undefined are similar.

  3. (3)

Case $\alpha{\equiv}v_{1}{=}v_{2}{\wedge}\alpha_{1}$ and
$v_{1}\not\in\bar{w}$, $v_{2}\in\bar{w}$.

By assumption, $s\models{\Pi_{{\small{\tt SH}}}}(\alpha_{1},\bar{w})$. By
induction, there exists a stack $s_{1}$ such that $s\subseteq s_{1}$ and
$s_{1}\models\alpha_{1}$. We examines two subcases:

    1. (a)

Case $s_{1}(v_{1})$ is defined. As $v_{2}\in\bar{w}$, $v_{2}$ has been
substituted already. Thus, $s_{1}(v_{2})$ is undefined. We define
$s_{2}(v_{2})$ such that $s_{2}(v_{2}){=}s_{1}(v_{1})$. This implies
$s_{1}\cup s_{2}\models v_{1}{=}v_{2}$. Thus, $(s_{1}\cup
s_{2})\models\alpha$.

    2. (b)

Case $s_{1}(v_{1})$ is undefined. Never.

  4. (4)

Case $\alpha{\equiv}v_{1}{=}v_{2}{\wedge}\alpha_{1}$ and
$v_{1}\not\in\bar{w}$, $v_{2}\not\in\bar{w}$. By assumption,
$s\models{\Pi_{{\small{\tt SH}}}}(\alpha_{1},\bar{w})$. By induction, there
exists a stack $s_{1}$ such that $s\subseteq s_{1}$ and
$s_{1}\models{\alpha_{1}}$. As $v_{1}\not\in\bar{w}$ and
$v_{2}\not\in\bar{w}$, $s_{1}(v_{1})$ and $s_{1}(v_{2})$ are both defined. As
$\alpha$ is satisfiable, $s_{1}(v_{1}){=}s_{1}(v_{2})$. This implies
$s_{1}\models v_{1}{=}v_{2}$. Thus, $s_{1}\models\alpha$.

  5. (5)

Case $\alpha{\equiv}v_{1}{\not=}v_{2}{\wedge}\alpha_{1}$ and
$v_{1}\in\bar{w}$, $v_{2}\in\bar{w}$.

By assumption, $s\models{\Pi_{{\small{\tt SH}}}}(\alpha_{1},\bar{w})$. By
induction, there exists a stack $s_{1}$ such that $s\subseteq s_{1}$ and
$s_{1}\models{\alpha_{1}}$. As $v_{1}\in\bar{w}$ and $v_{2}\in\bar{w}$,
$s_{1}(v_{1})$ and $s_{2}(v_{2})$ are both undefined. We define $s_{2}(v_{1})$
and $s_{2}(v_{2})$ such that $s_{2}(v_{2}){\not=}s(v_{2})$ (As domain of
integer is infinite, we always find a such value for $v_{1}$ and $v_{2}$) This
implies $s_{1}\cup s_{1}v_{1}{\not=}v_{2}$. Thus, $(s_{1}\cup
s_{2})\models\alpha$.

  6. (6)

Case $\alpha{\equiv}v_{1}{\not=}v_{2}{\wedge}\alpha_{1}$ and
$v_{1}\in\bar{w}$, $v_{2}\not\in\bar{w}$. Similar to Case 5.

  7. (7)

Case $\alpha{\equiv}v_{1}{=}v_{2}{\wedge}\alpha_{1}$ and
$v_{1}\not\in\bar{w}$, $v_{2}\in\bar{w}$. Similar to Case 5.

  8. (8)

Case $\alpha{\equiv}v_{1}{=}v_{2}{\wedge}\alpha_{1}$ and
$v_{1}\not\in\bar{w}$, $v_{2}\not\in\bar{w}$. By assumption,
$s\models{\Pi_{{\small{\tt SH}}}}(\alpha_{1},\bar{w})$. By induction, there
exists a stack $s_{1}$ such that $s\subseteq s_{1}$ and
$s_{1}\models{\alpha_{1}}$. As $v_{1}\not\in\bar{w}$ and
$v_{2}\not\in\bar{w}$, $s_{1}(v_{1})$ and $s_{1}(v_{2})$ are both defined. As
$\alpha$ is satisfiable, $s_{1}(v_{1}){\not=}s_{1}(v_{2})$. This implies
$s_{1}\models v_{1}{\not=}v_{2}$. Thus, $s_{1}\models\alpha$.

##  Appendix B Proof of Lemma 6.1

Proof We assume $\exists\bar{w}_{2}\cdot\Delta_{2}$ can be linked back to
$\exists\bar{w}_{1}\cdot\Delta_{1}$. As so, the heap in bud can be weakened
and matched with the heap in the companion with some substitutions $\rho$. And
$\pi^{df}_{2}$ after weakened and substituted to become $\pi^{\prime df}_{2}$,
at the last step we need to prove $\pi^{\prime df}_{2}{\implies}\pi^{df}_{1}$.
Suppose that $\pi^{\prime df}_{2}{\equiv}\pi^{\prime
df}_{21}{\wedge}\pi^{\prime df}_{22}$ where $\textit{FV}(\pi^{\prime
df}_{21}){\in}w_{2}$ and $\textit{FV}(\pi^{\prime df}_{22})$ are observable
variables. Similarly, suppose that $\pi^{\prime df}_{1}{\equiv}\pi^{\prime
df}_{11}{\wedge}\pi^{\prime df}_{12}$ where $\textit{FV}(\pi^{\prime
df}_{11}){\in}w_{1}$ and $\textit{FV}(\pi^{\prime df}_{12})$ are observable
variables.

As $\Delta_{comp}$ is still open (it is not unsatisfiable) and $\pi^{\prime
df}_{11}$ is in a decidable fragment, there exists $s$ such that
$s{\models}\pi^{\prime df}_{11}$. This implies that there exists $s_{1}$ such
that $s{\subseteq}\Gamma_{1}$,
$s_{1}{\models}\exists\bar{w}_{1}{\cdot}\pi^{\prime df}_{11}$. This means
${\small{\tt true}}\,{\implies}{\exists}\bar{w}_{1}{\cdot}\pi^{\prime
df}_{11}$ (1).

Note if $\Delta_{comp}$ is a descendant of $\Delta_{bud}$, $\pi^{\prime
df}_{22}$ must be of the form $\pi^{\prime
df}_{22}{\equiv}\pi^{df}_{12}{\wedge}\pi^{df}_{12}{\wedge}...{\wedge}\pi^{df}_{12}$.
Thus, $\pi^{\prime df}_{22}\implies\pi^{df}_{12}$ (2).

From (1) and (2), we have $\pi^{\prime df}_{2}\implies\pi^{df}_{1}$. $\square$