FIT BUT Technical Report Series
Kamil Dudka, Lukáš Holı́k, Petr Peringer,
Marek Trtı́k, and Tomáš Vojnar

Technical Report No. FIT-TR-2015-03
Faculty of Information Technology, Brno University of Technology
Last modified: October 28, 2015

arXiv:1510.07995v1 [] 27 Oct 2

From Low-Level Pointers
to High-Level Containers

NOTE: This technical report contains an extended version of the VMCAI’16 paper
with the same name.

From Low-Level Pointers to High-Level Containers
Kamil Dudka1 , Lukáš Holı́k1 , Petr Peringer1 , Marek Trtı́k2 , and Tomáš Vojnar1
1

FIT, Brno University of Technology

2

LaBRI, Bordeaux

Abstract. We propose a method that transforms a C program manipulating containers using low-level pointer statements into an equivalent program where the
containers are manipulated via calls of standard high-level container operations
like push back or pop front. The input of our method is a C program annotated
by a special form of shape invariants which can be obtained from current automatic shape analysers after a slight modification. The resulting program where
the low-level pointer statements are summarized into high-level container operations is more understandable and (among other possible benefits) better suitable
for program analysis since the burden of dealing with low-level pointer manipulations gets removed. We have implemented our approach and successfully tested
it through a number of experiments with list-based containers, including experiments with simplification of program analysis by separating shape analysis from
analysing data-related properties.

1

Introduction

We present a novel method that recognizes low-level pointer implementations of operations over containers in C programs and transforms them to calls of standard highlevel container operations, such as push back, insert, or is empty. Unlike the related
works that we discuss below, our method is fully automated and yet it guarantees preservation of the original semantics. Transforming a program by our method—or even just
the recognition of pointer code implementing container operations that is a part of our
method—can be useful in many different ways, including simplification of program
analysis by separating shape and data-related analyses (as we show later on in the paper), automatic parallelization [10], optimization of garbage collection [20], debugging
and automatic bug finding [2], profiling and optimizations [17], general understanding of the code, improvement of various software engineering tasks [6], detection of
abnormal data structure behaviour [11], or construction of program signatures [4].
We formalize the main concepts of our method instantiated for NULL-terminated
doubly-linked lists (DLLs). However, the concepts that we introduce can be generalized
(as we discuss towards the end of the paper) and used to handle code implementing other
kinds of containers, such as singly-linked lists, circular lists, or trees, as well.
We have implemented our method and successfully tested it through a number
of experiments with programs using challenging pointer operations. Our benchmarks
cover a large variety of program constructions implementing containers based on NULLterminated DLLs. We have also conducted experiments showing that our method can
be instantiated to other kinds of containers, namely circular DLLs as well as DLLs
with head/tail pointers (our implementation is limited to various kinds of lists due to

1

typedef struct
int x;
struct SNode
struct SNode
} Node;
#define NEW(T)

*f;
*b;

13

2

2 while (nondet()) {
3
Node*p=NEW(Node);
4
if (h==NULL)
5
h=p;
6
else
7
t->f=p;
8
p->f=NULL;
9
p->x=nondet();
10
p->b=t;
11
t=p;
12 }
...
13 Node *p=h;
14 while (p!=NULL) {
15
p->x=0;
16
p=p->f;
17 }

h t

h

t

h

t

L

nondet()

(T*)malloc(sizeof(T))

1 Node *h=0, *t=0;

(a)

h=
t=

SNode {

3

h t

L

p=malloc()

list L;

h t p

h==

while (nondet()) {
Node*p=NEW(Node);

h t p

h=p

h

t

h p

h

t

p

p->f=

L=push_back(L,p);

h p

h

t

p

h p

h

t

p

h

t

p

t

9
p->x=nondet()

t

10
p->b=t
t=p

p

L

t->f=p
8

p

L

7

p->x=nondet();

t
h

11
t

(b)

t

4
h!=

5

}
...
Node *p=front(L);
while (p!=NULL) {
p->x=0;
p=next(L,p);
}

h

p

L

L

(c)
Fig. 1. A running example. (a) A C code using low-level pointer manipulations. (b) The transformed pseudo-C++ code using container operations. (c) A part of the CFG of the low-level code
from Part (a) corresponding to lines 1-12, annotated by shape invariants.

limitations of the shape analyser used). We further demonstrate that our method can
simplify verification of pointer programs by separating the issue of shape analysis from
that of verification of data-related properties. Namely, we first obtain shape invariants
from a specialised shape analyser (Predator [7] in our case), use it within our method to
transform the given pointer program into a container program, and then use a tool that
specialises in verification of data-related properties of container programs (for which
we use the J2BP tool [14,15]).
Overview of the proposed method. We demonstrate our method on a running example
given in Fig. 1(a). It shows a C program that creates a DLL of non-deterministically
chosen length on lines 2–12 and then iterates through all its elements on lines 13–
17. Fig. 1(b) shows the code transformed by our method. It is an equivalent C++-like
program where the low-level pointer operations are replaced by calls of container operations which they implement. Lines 4–8, 10, and 11 are identified as push back (i.e.,
insertion of an element at the end of the list), line 13 as setting an iterator to the first
element of a list, and line 16 as a shift of the iterator.
The core of our approach is recognition of low-level pointer implementations of
destructive container operations, i.e., those that change the shape of the memory, such
as push back in our example. In particular, we search for control paths along which
pieces of the memory evolve in a way corresponding to the effect of some destructive
container operations. This requires(1) a control-flow graph with edges annotated by
2

an (over)approximation of the effect of program statements on the memory (i.e., their
semantics restricted to the reachable program configurations) and (2) a specification of
the operational semantics of the container operations that are to be searched for.
We obtain an approximation of the effect of program statements by extending current methods of shape analysis. These analyses are capable of inferring a shape invariant
for every node of the control-flow graph (CFG). The shape invariants are based on using various abstract objects to represent concrete or summarized parts of memory. For
instance, tools based on separation logic [13] use points-to and inductive predicates;
TVLA [19] uses concrete and summary nodes; the graph-based formalism of [7] uses
regions and list-segments; and sub-automata represent list-like or tree-like structures
in [8]. In all these cases, it is easy to search for configurations of abstract objects that
may be seen as having a shape of a container (i.e., a list-like container, a tree-like container, etc.) within every possible computation. This indicates that the appropriate part
of memory may be used by the programmer to implement a container.
To confirm this hypothesis, one needs to check that this part of memory is actually manipulated as a container of the appropriate type across all statements that work
with it. Additional information about the dynamics of memory changes is needed. In
particular, we need to be able to track the lifecycle of each part of the memory through
the whole computation, to identify its abstract encodings in successive abstract configurations, and by comparing them, to infer how the piece of the memory is changing. We
therefore need the shape analyser to explicitly tell us which abstract objects of a successor configuration are created from which abstract objects of a predecessor configuration
or, in other words, which abstract objects in the predecessor configuration denote parts
of the memory intersecting with the denotation of an object in the successor configuration. We say that the former objects are transformed into the latter ones, and we call the
relationship a transformation relation. A transformation relation is normally not output
by shape analysers, however, tools such as Predator [7] (based on SMGs), Slayer [1]
(based on separation logic), or Forester [8] (based on automata) actually work with it at
least implicitly when applying abstract transformers. We only need them to output it.
The above concepts are illustrated in Fig. 1(c). It shows a part of the CFG of the
program from Fig. 1(a) with lines annotated by the shape invariant in the round boxes
on their right. The invariant is expressed in the form of so-called symbolic memory
graphs (SMGs), the abstract domain of the shape analyser Predator [7], simplified to
a bare minimum sufficient for exposing main concepts of our method. The basic abstract objects of SMGs are shown as the black circles in the figure. They represent
continuous memory regions allocated by a single allocation command. Every region
has a next selector, shown as the line on its right-top leading into its target region on
the right, and prev selector, shown as a line on its left-bottom leading to the target region on the left. The ⊥ stands for the value NULL. Pairs of regions connected by the
represent the second type of abstract object, so called doubly-linked segments (DLS).
They represent doubly-linked lists of an arbitrary length connecting the two regions.
The dashed envelope indicates a memory that has the shape of a container, namely
of a NULL-terminated doubly-linked list. The transformation relation between objects of
successive configurations is indicated by the dashed lines. Making the tool Predator [7]
output it was easy, and we believe that it would be easy for other tools as well.
3

Further, we propose a specification of operational semantics of the container operations which has the same form as the discussed approximation of operational semantics
of the program. It consists of input and output symbolic configuration, with abstract objects related by a transformation relation. For example, Fig. 2 shows a specification of
push back as an operation which appends a region pointed by a variable y to a doublylinked list pointed by x. The left pair specifies the case when the input DLL is empty,
the right pair the case when it is not.
To find an implementation of thus specified push back,
y
y
semantic annotations of the CFG are searched for chains of
x
the transformation relation matching the specification. That
is, they start and end by configurations that include the inz
z
put and the output of the push back specification, resp., and
the composition of the transformation relation between these Fig. 2. Specification of
configurations matches the transformation relation specified. z = push back(x, y).
In Fig. 1(c), one of the chains implementing push back is shown as the sequence
of greyed configurations. It matches the case of the non-empty input DLL on the right
of Fig. 2. Destructive program statements within the chain implementing the found operation are candidates for replacement by a call of the container operation. In the figure,
lines 7, 8, 10 are candidates for replacement by L=push back(L,p). However, the replacement can be done only if a set of chains is found that together gives a consistent
image about a use of containers in the whole program. In our example, it is important
that on the left of the greyed chain, there is another chain implementing the case of
push back for empty DLLs (matching the left part of the specification in Fig. 2).
After identifying containers and destructive container operations as discussed above,
we search for implementations of non-destructive operations (like iterators or emptiness
tests). This leads to replacement of lines 13 and 16 in Fig. 1(a) by the initialization and
shift of the iterator shown on the same lines in Fig. 1(b). This step is much simpler,
and we will only sketch it in the paper. We then simplify the code using standard static
analysis. In the example, the fact that h and t become a dead variable until line 13 leads
to removing lines 4, 5, 6, and 11.
Our method copes even with cases when the implementation of a container operation is interleaved with other program statements provided that they do not interfere
with the operation (which may happen, e.g., when a manipulation of several containers
is interleaved). Moreover, apart from the container operations, arbitrary low-level operations can be used over the memory structures linked in the containers provided they
do not touch the container linking fields.
Related work. There have been proposed many dynamic analyses for recognition of
heap data structures, such as, e.g., [9,12,16,17,22,4]. These approaches are typically
based on observing program executions and matching observed heap structures against
a knowledge base of predefined structures. Various kinds of data structures can be
recognised, including various kinds of lists, red-black trees, B-trees, etc. The main purposes of the recognition include reverse engineering, program understanding, and profiling. Nevertheless, these approaches do not strive for being so precise that the inferred
information could be used for safe, fully automatic code replacement.
4

There exist static analyses with similar targets as the dynamic analyses above. Out
of them, the closest to us is probably the work [5]. Its authors do also target transformation of a program with low-level operations into high-level ones. However, their aim is
program understanding (design recovery), not generation of an equivalent “executable”
program. Indeed, the result does not even have to be a program, it can be a natural language description. Heap operations are recognised on a purely syntactical level, using
a graph representation of the program on which predefined rewriting rules are applied.
Our work is also related to the entire field of shape analysis, which provides the
input for our method. Due to a lack of space, we cannot give a comprehensive overview
here (see, e.g., [7,8,1] for references). Nevertheless, let us note that there is a line of
works using separation-logic-based shape analysis for recognition of concurrently executable actions (e.g., [18,21]). However, recognizing such actions is a different task
than recognizing low-level implementation of high-level container usage.
In summary, to the best of our knowledge, our work is the first one which targets
automatic replacement of a low-level, pointer-manipulating code by a high-level one,
with guarantees of preserving the semantics.

2

Symbolic Memory Graphs with Containers

We now present an abstract domain of symbolic memory graphs (SMGs), originally
introduced in [7], which we use for describing shape invariants of the programs being
processed. SMGs are a graph-based formalism corresponding to a fragment of separation logic capable of describing classes of heaps with linked lists. We present their
simplified version restricted to dealing with doubly-linked lists, sufficient for formalising the main concepts of our method. Hence, nodes of our SMGs represent either
concrete memory regions allocated by a single allocation statement or doubly-linked
list segments (DLSs). DLSs arise by abstraction and represent sets of doubly-linked
sequences of regions of an arbitrary length. Edges of SMGs represent pointer links.
In [7], SMGs are used to implement a shape analysis within the generic framework
of abstract interpretation [3]. We use the output of this shape analysis, extended with
a transformation relation, which provides us with precise information about the dynamics of the memory changes, as a part of the input of our method (cf. Section 4). Further,
in Section 3, we propose a way how SMGs together with a transformation relation can
be used to specify the container operations to be recognized.
Before proceeding, we recall that our use of SMGs can be changed for other domains common in the area of shape analysis (as mentioned already in the introduction
and further discussed in Section 7).
Symbolic memory graphs. We use > to explicitly denote undefined values of functions. We call a region any block of memory allocated as a whole (e.g., using a single
malloc() statement), and we denote by ⊥ the special null region. For a set A, we use
A⊥ , A> , and A⊥,> to denote the sets A ∪ {⊥}, A ∪ {>}, and A ∪ {⊥, >}, respectively.
Values stored in regions can be accessed through selectors (such as next or prev). To
simplify the presentation, we assume dealing with pointer and integer values only.
For the rest of the paper, we fix sets of pointer selectors S p , data selectors Sd ,
regions R, pointer variables V p , and container variables Vc (container variables do not
5

appear in the input programs, they get introduced by our transformation procedure to
denote parts of memory which the program treats as containers). We assume all these
sets to be pairwise disjoint and disjoint with Z⊥,> . We use V to denote the set V p ∪ Vc
of all variables, and S to denote the set S p ∪ Sd of all selectors.
A doubly-linked list segment (DLS) is a pair (r, r0 ) ∈ R × R of regions that abstracts
a doubly-linked sequence of regions of an arbitrary length that is uninterrupted by any
external pointer pointing into the middle of the sequence and interconnects the front
region represented by r with the back region r0 . We use D to denote the set of all DLSs
/ Both regions and DLSs will be called objects.
and assume that R ∩ D = 0.
To illustrate the above, the top-left part of Fig. 3 shows a memory layout with five regions (black circles), four of which form a NULL-terminated DLL. The bottom-left part
h
t
p
of Fig. 3 shows a sequence of three
doubly-linked regions abstracted into
L
a DLS (depicted as a pair of regions repre
t
h
p
linked via the “spring” ). Note that we
L
could also abstract all four doubly-linked
Fig. 3. A DLL and an SDLL, a PC and an SPC.
regions into a single DLS.
We can now define a symbolic memory graph (SMG) formally. It is a triple G =
(R, D, val) consisting of a set R ⊆ R of regions, a set D ⊆ R × R ⊆ D of DLSs, and a map
val defining the pointer and data fields of regions in R. It assigns to every pointer selector
sel p ∈ S p a function val(sel p ) : R → R⊥,> that defines the successors of every region
r ∈ R. Further, it assigns to every data selector seld ∈ Sd a function val(seld ) : R → Z>
that defines the data values of every region r ∈ R. We will sometimes abuse the notation
and write simply sel(r) to denote val(sel)(r). An SMG G0 = (R0 , D0 , val0 ) is a sub-SMG
of G, denoted G0  G, if R0 ⊆ R, D0 ⊆ D, and val0 (sel) ⊆ val(sel) for all sel ∈ S.
Container shapes. We now proceed to defining a notion of container shapes that we will
be looking for in shape invariants produced by shape analysis and whose manipulation
through given container operations we will be trying to recognise. For simplicity, we
restrict ourselves to NULL-terminated DLLs. However, in our experimental section, we
present results for some other kinds of list-shaped containers too. Moreover, at the end
of the paper, we argue that a further generalization of our approach is possible. Namely,
we argue that the approach can work with other types of container shapes as well as on
top of other shape domains.
A symbolic doubly-linked list (SDLL) with a front region r and a back region r0 is
an SMG in the form of a sequence of regions possibly interleaved with DLSs, interconnected so that it represents a DLL. Formally, it is an SMG G = (R, D, val) where
R = {r1 , . . . , rn }, n ≥ 1, r1 = r, rn = r0 , and for each 1 ≤ i < n, either next(ri ) = ri+1
and prev(ri+1 ) = ri , or (ri , ri+1 ) ∈ D and next(ri ) = prev(ri+1 ) = >. An SDLL which is
NULL-terminated, i.e., with prev(r) = ⊥ and next(r0 ) = ⊥, is called a container shape
(CS). We write csh(G) to denote the set of all CSs G0 that are sub-SMGs of an SMG G.
The bottom-right part of Fig. 3 contains an SDLL connecting a DLS and a region. It is
NULL-terminated, hence a CS, which is indicated by the dashed envelope .
Symbolic program configurations. A symbolic program configuration (SPC) is a pair
(G, σ) where G = (R, D, val) is an SMG and σ : (V p → R⊥,> ) ∪ (Vc → csh(G)> ) is
6

a valuation of the variables. An SPC C0 = (G0 , σ0 ) is a sub-SPC of an SPC C = (G, σ),
denoted C0  C, if G0  G and σ ⊆ σ0 . The bottom-right part of Fig. 3 depicts an SPC
with pointer variables h and t positioned next to the regions σ(h) and σ(t) they evaluate
to. The figure further shows a variable L positioned next to the CS σ(L) it evaluates to.
The top-right part of Fig. 3 is a PC as it has no DLSs. Examples of other SPCs are shown
in the annotations of program locations in Fig. 1(c) (and also Fig. 5 in Appendix E).
Additional notation. For an SMG or an SPC X, we write reg(X) to denote the set of its
regions, and obj(X) to denote the set of all its objects (regions and DLSs). A (concrete)
memory graph (MG), program configuration (PC), or doubly-linked list (DLL) is an
SMG, SPC, or DLL, respectively, whose set of DLSs is empty, i.e., no abstraction is
involved. A bijection π : R → R is called a region renaming. For an SMG, SPC, or
a variable valuation x, we denote by π(x) the structure arising from x by replacing each
occurrence of r ∈ R by π(r). A bijection λ : V → V is called a variable renaming, and
we define λ(x) analogous to π(x).
Abstraction and concretization. We now formalize the standard pair of abstraction and
concretization functions used in abstract interpretation for our domains of MGs and
SMGs. An SMG G is an abstraction of an MG g iff it can be obtained via the following
three steps: (i) Renaming regions of g by some region renaming π (making the semantics of an SMG closed under renaming). (ii) Removing some regions (which effectively
removes some constraint on a part of the memory, thus making its representation more
abstract). (iii) Folding some DLLs into DLSs (abstracting away some details of the
internal structure of the DLLs). In particular, a DLL l with a front region r and a back
region r0 may be folded into a DLS dl = (r, r0 ) by removing the inner regions of l (we say
that these regions get folded into dl ), removing the next-value of r and the prev-value of
r0 (unless r = r0 ), and adding dl into the set DG of DLSs of G.
Now, let g be a component of a PC (g, σ). The PC may be abstracted into an SPC
(G, σ0 ) by(a) forgetting values of some variables x ∈ dom(σ), i.e., setting σ0 (x) to >,
and (b) abstracting g into G by Steps (i–iii) above. Here, Step (i) is augmented by
redirecting every σ0 (x) to π(σ(x)), Step (ii) is allowed to remove only regions that are
neither in dom(σ0 ) nor in any CS that is in dom(σ0 ), and Step (iii) may fold a DLL into
a DLS only if none of its inner regions is in dom(σ0 ), redirecting values of container
variables from the original CSs to the ones that arise from it by folding.
The concretization of an SPC (SMG) X is then the set JXK of all PCs S
(MGs, resp.)
that can be abstracted to X. When X is a set of SPCs (SMGs), then JXK = X∈X JXK.
The left part of Fig. 3 shows an abstraction of an MG (top) into an SMG (bottom).
Step (i) renames all regions in the MG into the regions of the SMG, Step (ii) is not
applied, and Step (iii) folds three left-most regions of the DLL into a DLS. The repre
arrows show the so-called assignment of representing objects defined below.

3

Operations and their Specification

In this section, we introduce a notion of operations and propose their finite encoding in
the form of the so-called symbolic operations. Symbolic operations play a crucial role in
7

our approach since they are used to describe both of the two inputs of our algorithm for
recognition of high-level container operations in low-level code. In particular, on one
hand, we assume a (slightly extended) shape analyser to provide us with a CFG of the
program being processed annotated by symbolic operations characterizing the effect of
the low-level pointer statements used in the program (as discussed in Section 4). On the
other hand, we assume the high-level container operations whose effect—implemented
by sequences of low-level pointer statements—is to be sought along the annotated CFG
to be also described as symbolic operations. This can either be done by the users of
the approach (as discussed at the end of this section), or a library of typical high-level
container operations can be pre-prepared.
Below, we, in particular, concentrate on destructive container operations, i.e., those
container operations which change the shape of the heap. Non-destructive container
operations are much easier to handle, and we discuss them at the end of Section 5.
Operations and Symbolic Operations. We define an operation as a binary relation δ on
PCs capturing which input configurations are changed to which output configurations
by executing the operation. The individual pairs u = (c, c0 ) ∈ δ relating one input and
one output configuration are called updates. Operations corresponding to pointer statements or container operations relate infinitely many different input and output configurations, hence they must be represented symbolically. We therefore define a symbolic
update as a triple U = (C, ;,C0 ) where C = (G, σ), C0 = (G0 , σ0 ) are SPCs, and ;
is a binary relation over objects (regions and DLSs) called transformation relation.
A symbolic operation is then simply a (finite) set ∆ of symbolic updates.
Symbolic updates will be used to search for implementation of destructive container
operations based on changes of the SMGs labelling the given CFG. To be able to do
this with enough precision, symbolic updates must describe the “destructive” effect
that the operation has on the shape of the memory (addition/removal of a region or
a change of a selector value). For this, we require the semantics of a symbolic update
to be transparent, meaning that every destructive change caused by the operation is
explicitly and unambiguously visible in the specification of the operation (i.e., it cannot,
e.g., happen in an invisible way somewhere inside a DLS). On the other hand, we are not
interested in how the code modifies data values of regions. The semantics of a symbolic
update thus admits their arbitrary changes.
Semantics of symbolic updates. To define semantics of symbolic operations, we need to
distinguish abstract object (region or DLS) of an SPC C = (G, σ) representing a region
r of a PC c = (g, σ0 ) ∈ JCK. Recall that G arises by abstracting g by Steps (i–iii). Let π
be the region renaming used in Step (i). We define the representing object repre(r) of r
in C as(1) the region π(r) if π(r) ∈ reg(G), (2) > if π(r) is removed in G by Step (ii),
and (3) the DLS d if π(r) is folded into d ∈ obj(G) in Step (iii). We use c ∈repre JCK to
denote that the function repre is an assignment of representing objects of C to regions
of c. The inverse repre−1 (o) gives the set of all regions of c that are represented by the
object o ∈ obj(C). Notice that the way of how g is abstracted to G by Steps (i–iii) is not
necessarily unique, hence the assignment repre is not unique either. The right part of
Fig. 3 shows an example of abstraction of a PC c (top) to an SPC C (bottom), with the
assignment of representing objects repre shown via the top-down arrows.
8

Using this notation, the semantics of a symbolic update U = (C, ;,C0 ) can be defined as the operation JUK which contains all updates u = (c, c0 ) such that:

1. c ∈repre JCK and c0 ∈repre0 JC0 K.
2. An object o ∈ obj(C) transforms into an object o0 ∈ obj(C0 ), i.e., o ; o0 , iff the
denotations repre−1 (o) and (repre0 )−1 (o) share some concrete region, i.e., ∃r ∈
reg(c) ∩ reg(c0 ) : repre(r) = o ∧ repre0 (r) = o0 .
3. The semantics is transparent: (i) each selector change is explicit, i.e., if sel(r)
in c differs from sel(r) in c0 for a region r ∈ reg(c) ∩ reg(c0 ), then repre(r) ∈
reg(C) and repre0 (r) ∈ reg(C0 ) are regions such that sel(repre(r)) in C differs from
sel(repre0 (r)) in C0 ; (ii) every deallocation is explicit meaning that if a region r of
c is removed (i.e., it is not a region of c0 ), then repre(r) is a region (not a DLS) of
C; (iii) every allocation is explicit meaning that if a region r of c0 is added (i.e., it is
not a region of c), then repre0 (r) is a region of C0 .
S

The semantics of a symbolic operation ∆ is naturally defined as J∆K = U∈∆ JUK.
An example of a symbolic update is shown e.g. in Fig. 1(c), on the right of the
program edge between locations 3 and 4. It consists of the right-most SPCs attached to
these locations (denote them as C = (G, σ) and C0 = (G0 , σ0 ), and their DLSs as d and d 0 ,
respectively) and the transformation relation between their objects denoted by the dotted
vertical lines. The allocation done between the considered locations does not touch the
DLSs, it only adds a new region pointed to by p. This is precisely expressed by the
symbolic update U = (C, ;,C0 ) where ; = {(σ(L), σ0 (L))}. The relation ; (the dotted
line between objects σ(L) and σ0 (L)) says that, for every update from JUK, denotations
of the two DLSs d and d 0 share regions (by Point 2 above). By Point 3, there are no
differences in pointer links between the DLLs encoded by the two DLSs; the DLLs
encoded by d and the ones encoded by d 0 must be identical up to values of data fields.
The only destructive change that appears in the update is the addition of the freshly
allocated region σ0 (p) that does not have a ;-predecessor (due to Point 3(iii) above).
User Specification of Destructive Container Operations. As stated already above, we
first concentrate on searching for implementations of user-specified destructive container operations in low-level code. In particular, we consider non-iterative container
operations, i.e., those that can be implemented as non-looping sequences of destructive
pointer updates, region allocations, and/or de-allocations.1
We require the considered destructive container operations to be operations δy=op(x)
that satisfy the following requirements: (1) Each δy=op(x) is deterministic, i.e., it is
a function. (2) The sets x = x1 , ..., xn ∈ Vn and y = y1 , ..., ym ∈ Vm , n, m ≥ 0, are the
input and output parameters of the operation so that for every update ((g, σ), (g0 , σ0 )) ∈
δy=op(x) , the input PC has dom(σ) = {x1 , . . . , xn } and the output PC has dom(σ0 ) =
{y1 , . . . , ym }. (3) Since we concentrate on destructive operations only, the operation
1

Hence, e.g., an implementation of a procedure inserting an element into a sorted list, which
includes the search for the element, will not be understood as a single destructive container
operation, but rather as a procedure that calls a container iterator in a loop until the right place
for the inserted element is found, and then calls a destructive container operation that inserts
the given region at a position passed to it as a parameter.

9

does not modify data values, i.e., δy=op(x) ⊆ δconst where δconst contains all updates that
do not change data values except for creating an unconstrained data value or destroying
a data value when creating or destroying some region, respectively.
Container operations δy=op(x) of the above form can be specified by a user as symbolic operations, i.e., sets of symbolic updates, ∆y=op(x) such that δy=op(x) = J∆y=op(x) K∩
δconst . Once constructed, such symbolic operations can form a reusable library.
For instance, the operation δz=push back(x,y) can be specified as a symbolic operation
∆z=push back(x,y) which inputs a CS referred to by variable x and a region pointed to by y
and outputs a CS referred by z. This symbolic operation is depicted in Fig. 2. It consists
of two symbolic updates in which the user relates possible initial and final states of the
memory. The left one specifies the case when the input container is empty, the right one
the case when it is nonempty.

4

Annotated Control Flow Graphs

In this section, we describe the semantic annotations of a control-flow graph that our
procedure for recognizing implementation of high-level container operations in lowlevel code operates on.
Control-flow graph. A control flow graph (CFG) is a tuple cfg = (L, E, `I , `F ) where
L is a finite set of (control) locations, E ⊆ L × Stmts × L is a set of edges labelled by
statements from the set Stmts defined below, `I is the initial location, and `F the final
location. For simplicity, we assume that any two locations `, `0 are connected by at most
one edge h`, stmt, `0 i.
The set of statements consists of pointer statements stmt p ∈ Stmts p , integer data
statements stmtd ∈ Stmtsd , container statements stmtc ∈ Stmtsc , and the skip statement
skip, i.e., Stmts = Stmts p ∪ Stmtsd ∪ Stmtsc ∪ {skip}. The container statements and
the skip statement do not appear in the input programs, they are generated by our transformation procedure. The statements from Stmts are generated by the following grammar (we present a simplified minimalistic form to ease the presentation):
stmt p ::= p = (p | ps | malloc() | ⊥) | ps = p | free(p) | p == (p | ⊥) | p!= (p | ⊥)
stmtd ::= pd = (n | pd) | pd == pd | pd != pd

stmtc ::= y = op(x)

Above, p ∈ V p , s ∈ S p , d ∈ Sd , n ∈ Z, and x, y ∈ V∗ .
For each stmt ∈ Stmts p ∪ Stmtsd , let δstmt be the operation encoding its standard
C semantics. For example, the operation δx=y->next contains all updates (c, c0 ) where
c = (g, σ) is a PC s.t. σ(y) 6= > and c0 is the same as c up to the variable x that is
assigned the next-successor of the region pointed to by y. For each considered container
statement stmt ∈ Stmtsc , the operation δstmt is to be specified by the user. Let p =
e1 , . . . , en where ei = h`i−1 , stmti , `0i i, 1 ≤ i ≤ n, be a sequence of edges of cfg. We call p
a control flow path if `0i = `i for each 1 ≤ i < n. The semantics JpK of p is the operation
δstmtn ◦ · · · ◦ δstmt1 .
A state of a computation of a CFG cfg is a pair (l, c) where l is a location of cfg
and c is a PC. A computation of cfg is a sequence of states φ = (`0 , c0 ), (`1 , c1 ), . . .
of length |φ| ≤ ∞ where there is a (unique) edge ei = h`i , stmti , `i+1 i ∈ E such that
(ci , ci+1 ) ∈ δstmti for each 0 ≤ i < |φ|. The path e0 , e1 , . . . is called the control path of φ.
10

Semantic annotations. A semantic annotation of a CFG cfg consists of a memory
invariant mem, a successor relation I, and a transformation relation .. The quadruple (cfg, mem, I, .) is then called an annotated control-flow graph (annotated CFG).
A memory invariant mem is a total map that assigns to every location ` of cfg a set
mem(`) of SPCs describing (an overapproximation of) the set of memory configurations reachable at the given location. For simplicity, we assume that sets of regions of
any two different SPCs in img(mem) are disjoint. The successor relation is a binary relation on SPCs. For an edge e = h`, stmt, `0 i and SPCs C ∈ mem(`), C0 ∈ mem(`0 ), C I C0
indicates that PCs of JCK are transformed by executing stmt into PCs of JC0 K. The relation . is a transformation relation on objects of configurations in img(mem) relating
objects of C with objects of its I-successor C0 in order to express how the memory
changes by executing the edge e. The change is captured in the form of the symbolic
operation ∆e = {(C, .,C0 ) | (C,C0 ) ∈ I ∩ mem(`) × mem(`0 )}. For our analysis to be
sound, we require ∆e to overapproximate δstmt restricted to Jmem(`)K, i.e., J∆e K ⊇ δ`stmt
for δ`stmt = {(c, c0 ) ∈ δstmt | c ∈ Jmem(`)K}.
A symbolic trace of an annotated CFG is a possibly infinite sequence of SPCs Φ =
C0 ,C1 , . . . provided that Ci I Ci+1 for each 0 ≤ i < |Φ| ≤ ∞. Given a computation φ =
(`0 , c0 ), (`1 , c1 ), . . . of length |φ| = |Φ| such that ci ∈ JCi K for 0 ≤ i ≤ |φ|, we say that Φ
is a symbolic trace of computation φ.
A part of the annotated CFG of our running example from Fig. 1(a) is given in
Fig. 1(c), another part can be found in Fig. 5 in Appendix E. For each location `, the
set mem(l) of SPCs is depicted on the right of the location l. The relation . is depicted
by dotted lines between objects of SPCs attached to adjacent program locations. The
relation I is not shown as it can be almost completely inferred from .: Whenever objects
of two SPCs are related by ., the SPCs are related by I. The only exception is the Ichain of the left-most SPCs along the control path 1, 2, 3, 4 in Fig. 1(c).

5

Replacement of Low-Level Manipulation of Containers

With all the notions designed above, we are now ready to state our methods for identifying low-level implementations of container operations in an annotated CFG and for
replacing them by calls of high-level container operations. Apart from the very end of
the section, we concentrate on destructive container operations whose treatment turns
out to be significantly more complex. We assume that the destructive container operations to be sought and replaced are specified as sequences of destructive pointer updates,
region allocations, and/or de-allocations as discussed in the last paragraph of Sect. 3.
Given a specification of destructive container operations and an annotated CFG, our
algorithm needs to decide: (1) which low-level pointer operations to remove, (2) where
to insert calls of container operations that replace them and what are these operations,
and (3) where and how to assign the right values to the input parameters of the inserted
container operations. To do this, the algorithm performs the following steps.
The algorithm starts by identifying container shapes in the SPCs of the given annotated CFG. Subsequently, it looks for the so-called transformation chains of these
container shapes which capture their evolution along the annotated CFG. Each such
chain is a sequence of sub-SMGs that appear in the labels of a path of the given an11

notated CFG. In particular, transformation chains consisting of objects linked by the
transformation relation, meaning that the chain represents evolution of the same piece
of memory, and corresponding to some of the specified container operations are sought.
The algorithm then builds a so-called replacement recipe of a consistent set of transformation chains that interprets the same low-level code as the same high-level container operation for each possible run of the code. The recipe determines which code
can be replaced by which container operation and where exactly the container operation is to be inserted within the sequence of low-level statements implementing it. This
sequence can, moreover, be interleaved with some independent statements that are to
be preserved and put before or after the inserted call of a container operation.
The remaining step is then to find out how and where to assign the right values of
the input parameters of the inserted container operations. We do this by computing a socalled parameter assignment relation. We now describe the above steps in detail. For
the rest of Sect. 5, we fix an input annotated CFG cfg and assume that we have specified
a symbolic operation ∆stmt for every container statement stmt ∈ Stmtsc .
5.1

Transformation Chains

A transformation chain is a sequence of sub-SMGs that describes how a piece of memory evolves along a control path. We in particular look for such transformation chains
whose overall effect corresponds to the effect of some specified container operation.
Such transformation chains serve us as candidates for code replacement.
Let p = h`0 , stmt1 , `1 i, . . . , h`n−1 , stmtn , `n i be a control flow path. A transformation
chain (or simply chain) with the control path p is a sequence τ = τ[0] · · · τ[n] of SMGs
such that, for each 0 ≤ i ≤ n, there is an SPC Ci = (Gi , σi ) ∈ mem(`i ) with τ[i]  Gi
and the relation Iτ = {(Ci−1 ,Ci ) | 1 ≤ i ≤ n} is a subset of I, i.e., Ci is the successor
of Ci−1 for each i. We will call the sequence C0 , . . . ,Cn the symbolic trace of τ, and we
let .iτ = . ∩ (obj(τ[i − 1]) × obj(τ[i])) for 1 ≤ i ≤ n denote the transformation relation
between the objects of the i − 1th and ith SMG of τ.
An example of a chain, denoted as τpb below, is the sequence of the six SMGs that
are a part of the SPCs highlighted in grey in Fig. 1(c). The relation Iτpb links the six
SPCs, and the relation .τpb consists of the pairs of objects connected by the dotted lines.
Let ∆ be a specification of a container operation. We say that a transformation chain
τ implements ∆ w.r.t. some input/output parameter valuations σ/σ0 iff JUτ K ⊆ J∆K for the
symbolic update Uτ = ((τ[0], σ), .nτ ◦ · · · ◦ .1τ , (τ[n], σ0 )). Intuitively, Uτ describes how
MGs in Jτ[0]K are transformed into MGs in Jτ[n]K along the chain. When put together
with the parameter valuations σ/σ0 , Uτ is required to be covered by ∆.
In our example, by taking the composition of relations .5τpb ◦ · · · ◦ .1τpb (relating objects from location 4 linked by dotted lines with objects at location 11), we see that the
chain τpb implements the symbolic operation ∆z=push back(x,y) from Fig 2, namely, its
symbolic update on the right. The parameter valuations σ/σ0 can be constructed as L and
p correspond to x and y at location 4, respectively, and L corresponds to z at location 11.
Let τ be a chain implementing ∆ w.r.t. input/output parameter valuations σ/σ0 . We
define implementing edges of τ w.r.t. ∆, σ, and σ0 as the edges of the path p of τ that are
labelled by those destructive pointer updates, region allocations, and/or deallocations
12

that implement the update Uτ . Formally, the i-th edge ei of p, 1 ≤ i ≤ n, is an imple/ ., (τ[i], 0))K
/ ∩ δconst is not an identity (the update
menting edge of τ iff J((τ[i − 1], 0),
does not talk about values of variables, hence the empty valuations).
For our example chain τpb , the edges (7,8), (8,9), and (10,11) are implementing.
Finding transformation chains in an annotated CFG. Let ∆stmt be one of the given symbolic specifications of the semantics of a destructive container statement stmt ∈ Stmtsc .
We now sketch our algorithm for identifying chains that implement ∆stmt . More deb
tails can be found in Appendix A. The algorithm is based on pre-computing sets U
of so-called atomic symbolic updates that must be performed to implement the effect
of each symbolic update U ∈ ∆stmt . Each atomic symbolic update corresponds to one
pointer statement that performs a destructive pointer update, a memory allocation, or
b can be computed by looking at the differences in the selector
a deallocation. The set U
values of the input and output SPCs of U. The algorithm then searches through symbolic traces of the annotated CFG cfg and looks for sequences of sub-SMGs present
b (in any permutation) or
in them and linked by the atomic symbolic updates from U
by identity (meaning that a statement irrelevant for stmt is performed). Occurrences of
atomic updates are found based on testing entailment between symbolic atomic updates
and symbolic updates annotating subsequent CFG locations. This amounts to checking
entailment of the two source and the two target SMGs of the updates using methods
of [7], augmented with testing that the transformation relation is respected. Soundness
of the procedure depends on the semantics of symbolic updates being sufficiently precise, which is achieved by transparency of their semantics.
For example, for the container statement z=push back(x,y) and the symbolic upb will consist
date U corresponding to an insertion into a list of length one or more, U
of (i) symbolic updates corresponding to the pointer statements assigning y to the nextselector of the back region of x, (ii) assigning the back region of x to the prev-selector
of y, and (iii) assigning ⊥ to the next-selector of y. Namely, for the chain τpb in Fig. 1(c)
b consists of three
and the definition of the operation ∆z=push back(x,y) in Fig. 2, the set U
symbolic updates: from location 7 to 8 by performing Point (i), then from location 8 to 9
by performing (iii), and from location 10 to 11 by performing (ii).
5.2

Replacement Locations

A replacement location of a transformation chain τ w.r.t. ∆, σ, and σ0 is one of the
locations on the control path p of τ where it is possible to insert a call of a procedure
implementing ∆ while preserving the semantics of the path. In order to formalize the
notion of replacement locations, we call the edges of p that are not implementing (do
not implement the operation—e.g., they modify data) and precede or succeed the replacement location as the prefix or suffix edges, and we denote pp/s/i the sequences of
edges obtained by removing all but prefix/suffix/implementing edges, respectively. The
replacement location must then satisfy that Jpp · pi · ps K Jmem(` )K = JpK Jmem(` )K where
0

0

the notation δ S stands for the operation δ restricted to updates with the source configurations from the set S. The prefix edges are chosen as those which read the state of the
container shape as it would be before the identified container operation, the suffix edges
13

as those which read its state after the operation. The rest of not implementing edges is
split arbitrarily. If we do not find a splitting satisfying the above semantical condition,
τ is discarded from further processing.
For our example chain τpb , the edges (4,7) and (9,10) can both be put into the prefix
since none of them saves values of pointers used in the operation (see Fig. 1(c)). The
edge (9,10) is thus shifted up in the CFG, and the suffix remains empty. Locations 8–11
can then be used as the replacement locations.
5.3

Replacement Recipes

A replacement recipe is a map ϒ that assigns to each chain τ of the annotated CFG cfg
out
a quadruple ϒ(τ) = (∆τ , σin
τ , στ , `τ ), called a replacement template, with the following
meaning: ∆τ is a specification of a container operation that is to be inserted at the reout
placement location `τ as a replacement of the implementing edges of τ. Next, σin
τ /στ
are input/output parameter valuations that specify which parts of the memory should be
passed to the inserted operation as its input parameters and which parts of the memory
correspond to the values of the output parameters that the operation should return.
For our example chain τpb , a replacement template ϒ(τpb ) can be obtained, e.g., by
taking ∆τpb = ∆z=push back(x,y) , `τpb = 11, σin
τpb (x) = στpb [0] (L) denoting the CS in the
gray SPC of loc. 4, σin
(y)
=
σ
(p)
denoting
the right-most region of the gray SPC
τpb [0]
τpb
out
of loc. 4, and στpb (z) = στpb [5] (L) denoting the CS in the gray SPC of loc. 11.
We now give properties of replacement recipes that are sufficient for the CFG cfg0
generated by our code replacement procedure, presented in Sect. 5.5, to be semantically
equivalent to the original annotated CFG cfg.
Local consistency. A replacement recipe ϒ must be locally consistent meaning that
out
(i) every τ ∈ dom(ϒ) implements ∆τ w.r.t. σin
τ and στ and (ii) `τ is a replacement locain
out
tion of τ w.r.t. ∆τ , στ , and στ . Further, to enforce that τ is not longer than necessary,
we require its control path τ to start and end by an implementing edge. Finally, implementing edges of the chain τ cannot modify selectors of any object that is a part of a CS
which is itself not at the input of the container operation.
Global consistency. Global consistency makes it safe to replace the code w.r.t. multiple
overlapping chains of a replacement recipe ϒ, i.e., the replacements defined by them do
not collide. A replacement recipe ϒ is globally consistent iff the following holds:
1. A location is a replacement location within all symbolic traces passing it or within
none. Formally, for each maximal symbolic trace Φ passing the replacement location `τ of a chain τ ∈ dom(ϒ), there is a chain τ0 ∈ dom(ϒ) s.t. `τ0 = `τ and the
symbolic trace of τ0 is a sub-sequence of Φ passing `τ .
2. An edge is an implementing edge within all symbolic traces passing it or within
none. Formally, for each maximal symbolic trace Φ passing an implementing edge
e of a chain τ ∈ dom(ϒ), there is a chain τ0 ∈ dom(ϒ) s.t. e is its implementing edge
and the symbolic trace of τ0 is a sub-sequence of Φ passing e.
14

3. For any chains τ, τ0 ∈ dom(ϒ) that appear within the same symbolic trace, the following holds: (a) If τ, τ0 share an edge, then they share their replacement location,
i.e., `τ = `τ0 . (b) Moreover, if `τ = `τ0 , then τ is an infix of τ0 or τ0 is an infix of τ. The
latter condition is technical and simplifies the proof of correctness of our approach.
4. Chains τ, τ0 ∈ dom(ϒ) with the same replacement location `τ = `τ0 have the same
operation, i.e., ∆τ = ∆τ0 .
5. An edge is either implementing for every chain of dom(ϒ) going through that edge
or for no chain in dom(ϒ) at all.
Notice that Points 1, 2, and 3 speak about symbolic traces. That is, they do not have to
hold along all control paths of the given CFG cfg but only those which appear within
computations starting from Jmem(`I )K.
Connectedness. The final requirement is connectedness of a replacement recipe ϒ. It
reflects the fact that once some part of memory is to be viewed as a container, then
destructive operations on this part of memory are to be done by destructive container
operations only until the container is destroyed by a container destructor. Note that
this requirement concerns operations dealing with the linking fields only, the rest of
the concerned objects can be manipulated by any low-level operations. Moreover, the
destructive pointer statements implementing destructive container operations can also
be interleaved with other independent pointer manipulations, which are handled as the
prefix/suffix edges of the appropriate chain.
Connectedness of ϒ is verified over the semantic annotations by checking that in
the .-future and past of every container (where a container is understood as a container
shape that was assigned a container variable in ϒ), the container is created, destroyed,
and its linking fields are modified by container operations only. A formal description
can be found in Appendix B.
Computing recipes. The algorithm for building a replacement recipe ϒ starts by looking for chains τ of the annotated CFG cfg that can be associated with replacement
out
templates ϒ(τ) = (∆τ , σin
τ , στ , `τ ) s.t. local consistency holds. It uses the approach described in Sect. 5.1. It then tests global consistency of ϒ. All the five sub-conditions
can be checked straightforwardly based on their definitions. If ϒ is found not globally consistent, problematic chains are pruned it until global consistency is achieved.
Testing for connectedness is done by testing all Ics -paths leading forward from output
parameters of chains and backward from input parameters of chains. Testing whether
J(S, ., S0 )K ∩ δconst or J(S0 , ., S)K ∩ δconst is an identity, which is a part of the procedure,
can be done easily due to the transparency of symbolic updates. Chains whose container
parameters contradict connectedness are removed from ϒ. The pruning is iterated until
ϒ is both globally consistent and connected.
5.4

Parameter Assignment

To prevent conflicts of names of parameters of the inserted container operations, their
calls are inserted with fresh parameter names. Particularly, given a replacement recipe
15

ϒ, the replacement location `τ of every chain τ ∈ dom(ϒ) is assigned a variable renaming λ`τ that renames the input/output parameters of the symbolic operation ∆τ , specifying the destructive container operation implemented by τ, to fresh names. The renamed
parameters of the container operations do not appear in the original code, and so the
code replacement algorithm must insert assignments of the appropriate values to the
parameters of the operations prior to the inserted calls of these operations. For this,
we compute a parameter assignment relation ν containing pairs (`, x := y) specifying
which assignment x := y is to be inserted at which location `. Intuitively, ν is constructed so that the input parameters of container operations take their values from the
output container parameters of the preceding container operations or, in case of pointer
variables, directly from the access paths (consisting of a pointer variable v or a selector value vs) that are used in the original program to access the concerned memory
regions. More details are given in Appendix C. Let us just note that if we fail to find
a parameter assignment, we remove some chains from ϒ and restart the search.
5.5

Code Replacement

The input of the replacement procedure is the annotated CFG cfg, a replacement recipe ϒ,
a variable renaming λ` for every replacement location ` of ϒ, and a parameter assignment relation ν. The procedure produces a modified CFG cfg0 . It first removes all implementing edges of every chain τ ∈ dom(ϒ) and adds instead an edge with a call to
λ` (∆` ) at `τ , and then adds an edge with the assignment x := y at ` for every pair
(`, x := y) ∈ ν. The edge removal is done simply by replacing the statement on the
given edge by the skip statement whose semantics is identity. Given a statement stmt
and a location `, edge addition amounts to: (1) adding a fresh location `• , (2) adding
a new edge h`, stmt, `• i, (3) replacing every edge h`, stmt0 , `0 i by h`• , stmt0 , `0 i. Intuitively, edge removal preserves all control paths going through the original edge, only
the statement is now “skipped”, and edge addition inserts the given statement into all
control paths containing the given location.
After replacing destructive container operations, we replace non-destructive container operations, including, in particular, usage of iterators to reference elements of
a list and to move along the list, initialisation of iterators (placing an iterator at a particular element of a list), and emptiness tests. With a replacement recipe ϒ and an assignment relation ν at hand, recognizing non-destructive operations in the annotated CFG
cfg is a much easier task than that of recognizing destructive operations. Actually, for
the above operations, the problem reduces to analysing annotations of one CFG edge at
a time. We refer an interested reader to Appendix E for more details.
Preservation of semantics. It can now be proved (cf. Appendix D) that under the assumption that the replacement recipe ϒ is locally and globally consistent and connected
and the parameter assignment relation ν is complete, our code replacement procedure
preserves the semantics. In particular, computations of the CFG cfg are surjectively
mapped to computations of the CFG cfg0 that are equivalent in the following sense.
They can be divided into the same number of segments that are in the computation of
cfg delimited by borders of the chains that it passes through. The two computations
agree on the final PCs of the respective segments. Note also that the transformation
16

preserves memory safety errors—if they appear, the related containers will not be introduced due to violation of connectedness.

6

Implementation and Experimental Results

We have implemented our approach as an extension of the Predator shape analyser [7]
and tested it through a number of experiments. Our code and experiments are publicly available at http://www.fit.vutbr.cz/research/groups/verifit/tools/
predator-adt.
The first part of our experiments concentrated on how our approach can deal with
various low-level implementations of list operations. We built a collection of 18 benchmark programs manipulating NULL-terminated DLLs via different implementations of
typical list operations, such as insertion, iteration, and removal. Moreover, we generated
further variants of these implementations by considering various legal permutations of
their statements. We also considered interleaving the pointer statements implementing
list operations with various other statements, e.g., accessing the data stored in the lists.2
Finally, we also considered two benchmarks with NULL-terminated Linux lists that heavily rely on pointer arithmetics. In all the benchmarks, our tool correctly recognised
list operations among other pointer-based code and gave us a complete recipe for code
transformation. On a standard desktop PC, the total run time on a benchmark was almost
always under 1s (with one exception at 2.5s), with negligible memory consumption.
Next, we successfully applied our tool to multiple case studies of creating, traversing, filtering, and searching lists taken from the benchmark suite of Slayer [1] (modified
to use doubly-linked instead of singly-linked lists). Using a slight extension of our prototype, we also successfully handled examples dealing with lists with head/tail pointers
as well as with circular lists. These examples illustrate that our approach can be generalized to other kinds of containers as discussed in Section 7. These examples are also
freely available at the link above. Moreover, in Appendix F, we present an example how
we deal with code where two container operations are interleaved.
Further, we concentrated on showing that our approach can be useful to simplify
program analysis by separating low-level pointer-related analysis from analysing other,
higher-level properties (like, e.g., sortedness or other data-related properties). To illustrate this, we used our approach to combine shape analysis implemented in Predator
with data-related analysis provided by the J2BP analyser [14]. J2BP analyses Java programs, and it is based on predicate abstraction extended to cope with containers.
We used 4 benchmarks for the evaluation. The first one builds an ordered list of
numerical data, inserts another data element into it, and finally checks sortedness of the
resulting list, yielding an assertion failure if this is not the case (such a test harness must
be used since J2BP expects a closed program and verifies absence of assertion failures).
The other benchmarks are similar in that they produce lists that should fulfill some
property, followed by code that checks whether the property is satisfied. The considered
properties are correctness of the length of a list, the fact that certain inserted values
appear in a certain order, and correctness of rewriting certain values in a list. We used
2

In practice, there would typically be many more such statements, seemingly increasing the size
of the case studies, but such statements are not an issue for our method.

17

our tool to process the original C code. Next, we manually (but algorithmically) rewrote
the result into an equivalent Java program. Then, we ran J2BP to verify that no assertion
failures are possible in the obtained code, hence verifying the considered data-related
properties. For each benchmark, our tool was able to produce (within 1 sec.) a container
program for J2BP, and J2BP was able to complete the proof. At the same time, note that
neither Predator nor J2BP could perform the verification alone (Predator does not reason
about numerical data and J2BP does not handle pointer-linked dynamic data structures).

7

Possibilities of Generalizing the Approach

Our method is built around the idea of specifying operations using a pair of abstract configurations equipped with a transformation relation over their components. Although we
have presented all concepts for the simple abstract domain of SMGs restricted to NULLterminated DLLs, the main idea can be used with abstract domains describing other
kinds of lists, trees, and other data structures too. We now highlight what is needed for
that. The abstract domain to be used must allow one to define a sufficiently fine-grained
assignment of representing objects, which is necessary to define symbolic updates with
transparent semantics. Moreover, one needs a shape analysis that computes annotations
of the CFG with a precise enough invariant, equipped with the transformation relation,
encoding pointer manipulations in a transparent way. However, most shape analyses do
actually work with such information internally when computing abstract post-images
(due to computing the effect of updates on concretized parts of the memory). We thus
believe that, instead of Predator, tools like, e.g., Slayer [1] or Forester [8] can be modified to output CFGs annotated in the needed way.
Other than that, given an annotated CFG, our algorithms searching for container operations depend mostly on an entailment procedure over symbolic updates (cf. Sec. 5.1,
App. A). Entailment of symbolic updates is, however, easy to obtain as an extension of
entailment over the abstract domain provided the entailment is able to identify which
parts of the symbolic shapes encode the same parts of the concrete configurations.

8

Conclusions and Future Work

We have presented and experimentally evaluated a method that can transform in a sound
and fully automated way a program manipulating NULL-terminated list containers via
low-level pointer operations to a high-level container program. Moreover, we argued
that our method is extensible beyond the considered list containers (as illustrated also
by our preliminary experiments with lists extended with additional pointers and circular
lists). A formalization of an extension of our approach to other kinds of containers,
a better implementation of our approach, as well as other extensions of our approach
(including, e.g., more sophisticated target code generation and recognition of iterative
container operations) are subject of our current and future work.
Acknowledgement. This work was supported by the Czech Science Foundation project
14-11384S.
18

References
1. J. Berdine, B. Cook, and S. Ishtiaq. SLAyer: Memory Safety for Systems-Level Code. In
Proc. of CAV’11, volume 6806 of LNCS, pages 178–183. Springer, 2011.
2. T. M. Chilimbi, M. D. Hill, and J. R. Larus. Cache-Conscious Structure Layout. In Proc. of
PLDI’99, pages 1–12. ACM, 1999.
3. P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis
of Programs by Construction or Approximation of Fixpoints. In Proc. of POPL’77, pages
238–252. ACM, 1977.
4. A. Cozzie, F. Stratton, H. Xue, and S. T. King. Digging for Data Structures. In Proc. of
USENIX’08, pages 255–266. USENIX Association, 2008.
5. R. Dekker and F. Ververs. Abstract Data Structure Recognition. In Proc. of KBSE’94, pages
133–140, 1994.
6. B. Demsky, M. D. Ernst, P. J. Guo, S. McCamant, J. H. Perkins, and M. C. Rinard. Inference
and Enforcement of Data Structure Consistency Specifications. In Proc. of ISSTA’06, pages
233–244. ACM, 2006.
7. K. Dudka, P. Peringer, and T. Vojnar. Byte-Precise Verification of Low-Level List Manipulation. In Proc. of SAS’13, volume 7935 of LNCS, pages 215–237. Springer, 2013.
8. P. Habermehl, L. Holı́k, A. Rogalewicz, J. Simácek, and T. Vojnar. Forest Automata for
Verification of Heap Manipulation. Formal Methods in System Design, 41(1):83–106, 2012.
9. I. Haller, A. Slowinska, and H. Bos. MemPick: High-Level Data Structure Detection in
C/C++ Binaries. In Proc. of WCRE’13, pages 32–41, 2013.
10. L. J. Hendren and A. Nicolau. Parallelizing Programs with Recursive Data Structures. IEEE
Trans. Parallel Distrib. Syst., 1(1):35–47, 1990.
11. M. Jump and K. S. McKinley. Dynamic Shape Analysis via Degree Metrics. In Proc. of
ISMM’09, pages 119–128. ACM, 2009.
12. C. Jung and N. Clark. DDT: Design and Evaluation of a Dynamic Program Analysis for
Optimizing Data Structure Usage. In Proc. of MICRO’09, pages 56–66. ACM, 2009.
13. P. O’Hearn, J. Reynolds, and H. Yang. Local Reasoning about Programs that Alter Data
Structures. In Proc. of CSL’01, volume 2142 of LNCS, pages 1–19. Springer, 2001.
14. P. Parı́zek. J2BP. http://plg.uwaterloo.ca/˜{}pparizek/j2bp.
15. P. Parı́zek and O. Lhoták. Predicate Abstraction of Java Programs with Collections. In Proc.
of OOPSLA’12, pages 75–94. ACM, 2012.
16. S. Pheng and C. Verbrugge. Dynamic Data Structure Analysis for Java Programs. In Proc.
of ICPC’06, pages 191–201. IEEE Computer Society, 2006.
17. E. Raman and D. I. August. Recursive Data Structure Profiling. In Proc. of MSP’05, pages
5–14. ACM, 2005.
18. M. Raza, C. Calcagno, and P. Gardner. Automatic Parallelization with Separation Logic. In
Proc. of ESOP’09, pages 348–362. Springer, 2009.
19. S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric Shape Analysis via 3-valued Logic.
TOPLAS, 24(3), 2002.
20. R. Shaham, E. K. Kolodner, and S. Sagiv. On the Effectiveness of GC in Java. In Proc. of
ISMM’00, pages 12–17. ACM, 2000.
21. V. Vafeiadis. RGSep Action Inference. In Proc. of VMCAI’10, pages 345–361. Springer,
2010.
22. D. H. White and G. Lüttgen. Identifying Dynamic Data Structures by Learning Evolving
Patterns in Memory. In Proc. of TACAS’13, volume 7795 of LNCS, pages 354–369. Springer,
2013.

19

A

Finding transformation chains in an annotated CFG

In this appendix, we provide a detailed description of our algorithm that can identify
chains which implement—w.r.t. some input/output valuations—the symbolic operations
∆stmt of a destructive container statement stmt ∈ Stmtsc in a given annotated CFG. For
b of the so-called atomic
that, as we have already said in Sect. 5.1, we pre-compute sets U
symbolic updates that must be performed to implement the effect of each symbolic
update U ∈ ∆stmt . Each atomic symbolic update corresponds to one pointer statement
which performs a destructive pointer update, a memory allocation, or a deallocation.
b can be computed by looking at the differences in the selector values of the
The set U
input and output SPCs of U.
The algorithm identifying chains τ in the given annotated CFG iterates over all
symbolic updates U = (C, ;,C0 ) ∈ ∆stmt where stmt ∈ Stmtsc is a destructive container
statement. For each of them, it searches the annotated CFG for a location ` that is labelled by an SPC (G, σ) ∈ mem(`) for which there is a sub-SMG H  G and a valuation
σ0 such that J(H, σ0 )K ⊆ JC0 K. The latter test is carried out using an entailment procedure on the abstract heap domain used. If the test goes through, the first point of a new
chain τ[0] = H and the input valuation σ = σ0 are constructed.
b The algorithm
The rest of the chain τ is constructed as follows using the set U.
investigates symbolic traces C = C0 ,C1 , . . . starting from the location `. At each Ci , i > 0,
it attempts to identify τ[i] as a sub-SMG of Ci that satisfies the following property for
some valuation σi : Objects of τ[i] are the .-successors of objects of τ[i − 1] in Ci , and for
the symbolic update Ui = J(τ[i − 1], σi−1 ), ., (τ[i], σi )K, it either holds that JUi K ∩ δconst
is an identity, or JUK ⊆ JUa K for some atomic pointer change Ua . This is, τ[i − 1] does
either not change (meaning that the implementation of the sought container operation is
interleaved with some independent pointer statements), or it changes according to some
of the atomic symbolic updates implementing the concerned container operation. In the
latter case, the i-th edge of the control path of τ is an implementing edge of τ. We note
that both of the tests can be carried out easily due to the transparency of the semantics
of symbolic updates (cf. Section 3), which makes all pointer changes specified by U,
Ui , and Ua “visible”.
If τ[i] and σi satisfying the required property are not found, the construction of τ
along the chosen symbolic trace fails, otherwise the algorithm continues extending it.
b is associated with
The chain τ is completed when every atomic symbolic update from U
some implementing edge. That means that all steps implementing U have appeared, no
other modifications to τ[0] were done, and so τ[0] was modified precisely as specified
by U. Finally, an output valuation σ0 is chosen so that τ implements ∆ w.r.t. σ and σ0 .
Note that since one of the conditions for τ[i] is that its objects are images of objects
of τ[i − 1], operations that allocate regions would never be detected because a newly
allocated region cannot be the image of any object. The construction of chains implementing such operations is therefore done in the opposite direction, i.e., it starts from
C0 and continues against ..

B

Connectedness

The below formalized requirement of connectedness of a replacement recipe ϒ reflects
the fact that once some part of memory is to be viewed as a container, then destruc20

tive operations on this part of memory are to be done by destructive container operations only, until the container is destroyed by a container destructor. Note that this
requirement concerns operations dealing with the linking fields only, the rest of the
concerned objects can be manipulated by any low-level operations. Moreover, recall
that destructive pointer statements implementing destructive container operations can
be interleaved by other independent pointer manipulations, which are handled as the
prefix/suffix edges of the appropriate chain.
Let C,C0 ∈ dom(mem). The successor CS of a CS S  C is a CS S0  C0 s.t. obj(S0 ) =
obj(C0 ) ∩ .(obj(S)). The CS S is then called the predecessor CS of S0 in C, denoted S Ics
S0 . The successor set of a CS S is defined recursively as the smallest set succ(S) of CSs
that contains S and each successor CS S00 of each CS S0 ∈ succ(S) that is not obtained
by a statement that appears in the path of some chain in dom(ϒ). Symmetrically, for
a CS S which is the input of some chain in dom(ϒ), we define its predecessor set as
the smallest set predτ (S) of CSs that contains S and each predecessor S00 of each CS in
S0 ∈ predτ (S) that is not obtained by a statement that appears in the path of some chain
in dom(ϒ).
Using the notions of successor and predecessor sets, ϒ is defined as connected iff it
satisfies the following two symmetrical conditions: (1) For every CS S0 in the successor
set of a CS S that is the output of some chain in dom(ϒ), S0 is either the input of
some chain in dom(ϒ) or, for all successors S00 of S0 , J(S0 , ., S00 )K ∩ δconst is an identity.
(2) For every CS S0 in the predecessor set of a CS S that is the input of some chain in
dom(ϒ), S0 is either the output of some chain in dom(ϒ) or, for all predecessors S00 of
S0 , J(S00 , ., S0 )K ∩ δconst is an identity. Intuitively, a CS must not be modified in between
of successive destructive container operations.

C

Parameter Assignment

Let ϒ be a replacement recipe. Further, for the replacement location ` of every chain τ ∈
dom(ϒ), let λ` be the variable renaming that renames the input/output parameters of the
symbolic operation ∆τ , specifying the destructive container operation implemented by
τ, to fresh names. Below, we describe a method that computes a parameter assignment
relation ν containing pairs (`, x := y) specifying which assignments are to be inserted at
which location in order to appropriately initialize the renamed input/output parameters.
As said already in Sect. 5.4, ν is constructed so that input container parameters take
their values from variables that are outputs of preceding container operations.
In particular, for an input container parameter x and an output container parameter y (i.e., x, y ∈ Vc ), a location where x can be identified with y is s.t. every element
of pred(Sx ) at the location is in succ(Sy ) and it is not in succ(Sy0 ) of any other output
parameter y0 . Here Sv denotes the (unique) container shape that is the value of the container parameter defined in ϒ . The parameters must be properly assigned along every
feasible path leading to `. Therefore, for every replacement location ` and every input
container parameter x of λ` (∆` ), we search backwards from ` along each maximal Ics path p leading to x. We look for a location ` on p where x can be identified with y. If we
find it, we add (`, x := y) to ν. If we do not find it on any of the paths, ν is incomplete.
τ is then removed from dom(ϒ), and the domain of ϒ is pruned until it again becomes
21

globally consistent. The computation of ν is then run anew. If the search succeeds for
all paths, then we call ν complete.
Region parameters are handled in a simpler way, using the fact that the input regions are usually sources or targets of modified pointers (or they are deallocated within
the operation). Therefore, in the statements of the original program that perform the
corresponding update, they must be accessible by access paths (consisting of a pointer
variable v or a selector value vs). These access paths can then be used to assign the
appropriate value to the region parameters of the inserted operations. Let τ be a chain
in dom(ϒ) with an input region parameter x ∈ V p . For every control path p leading to
`τ , taking into account that `τ can be shared with other chains τ0 , we choose the location `0 which is the farthest location from `τ on p s.t. it is a starting location of a chain
τ0 ∈ dom(ϒ) with `τ0 = `τ . We then test whether there is an access path a (i.e., a variable y or a selector value ys) s.t. all SPCs of mem(`0 ) have a region r which is the
.-predecessor of input region x of the chain τ0 and which is accessible by a. If so, we
put to ν the pair (`, x := a). Otherwise, τ is removed from ϒ, and the whole process of
pruning ϒ and computing the assignments is restarted.

D

Correctness

We now argue that under the assumption that the replacement recipe ϒ is locally and
globally consistent and connected and the parameter assignment relation ν is complete,
our code replacement procedure preserves the semantics of the input annotated CFG
cfg. We show that computations of cfg and of the CFG cfg0 obtained by the replacement
procedure are equivalent in the sense that for every computation φ of one of the annotated CFGs, there is a computation in the other one, starting with the same PC, such that
both computations can be divided into the same number of segments, and at the end of
every segment, they arrive to the same PCs. The segments will be delimited by borders
of chains that the computation in cfg passes through.
Formally, the control path of every computation φ of cfg is a concatenation of segments s1 s2 · · · . There are two kinds of segments: (1) A chain segment is a control path
of a chain of ϒ, and it is maximal, i.e., it cannot be extended to either side in order to
obtain a control path of another chain of ϒ. (2) A padding segment is a segment between
two chain segments such that none of its infixes is a control path of a chain.
We define the image of an edge e = h`1 , stmt1 , `2 i of cfg as the edge e0 = h`1 , stmt01 , `2 i
of cfg0 provided no new edge f = h`2 , stmt2 , `•2 i is inserted to cfg0 . Otherwise, the image
is the sequence of the edges e0 f . The image of a path p of cfg is then the sequence of
images of edges of p, and p is called the origin of p0 . Similarly to computations of cfg,
every computation φ0 of cfg0 can be split into a sequence of chain and padding segments.
They are defined analogously, the only difference is that instead of talking about control
paths of chains, the definition talks about images of control paths of chains.
We say that a PC c = (g, σ) of a computation of cfg is equivalent to a PC c0 =
0
(g , σ0 ) of a computation of cfg0 iff g = g0 and σ ⊆ σ0 . That is, the PCs are almost the
same, but c0 can define more variables (to allow for equivalence even though c0 defines
values of parameters of container operations). A computation φ of cfg is equivalent
to a computation φ0 of cfg0 iff they start with the same PC, have the same number of
22

segments, and the configurations at the end of each segment are equivalent. This is
summarised in the following theorem.
Theorem 1. For every computation of cfg starting with (`I , c), c ∈ Jmem(`I )K, there is
an equivalent computation of cfg0 , and vice versa.
For simplicity, we assume that every branching in a CFG is deterministic (i.e., conditions on branches starting from the same location are mutually exclusive).
In order to prove Theorem 1, we first state and prove several lemmas.
Lemma 1. Let φ be a computation of an annotated CFG cfg over a control path p and
a symbolic trace Φ = C0 ,C1 , · · · . Then:
1. There is precisely one way of how to split it into segments.
2. If the i-th segment is a chain segment which spans from the j-th to the k-th location
of p, then C j , . . . ,Ck is a symbolic trace of some chain τi of ϒ.
3. Every replacement point and implementing edge on p belong to some τi .
Proof. Let φ = (`0 , c0 ), (`1 , c1 ), . . .. Let the i-th segment be a chain segment that spans
from the j-th to the k-th location of φ. We start by Point 2 of the lemma.
Due to consistency, it holds that C j , . . . ,Ck is a symbolic trace of some chain τ ∈
dom(ϒ). Particularly, it can be argued as follows: The control path of a chain segment
is by definition a control path of some chain τ of ϒ but there is no chain of ϒ with the
control path that is an infix of p and larger than the one of τ. The control path of τ
contains the replacement location of τ. Let it be `l , j ≤ l ≤ k, and let e and e0 be the
extreme edges of the control path of τ. By local consistency, e and e0 are implementing.
By Point 2 of global consistency, the extreme edges are also implementing edges of
some chains τ0 and τ00 with the symbolic traces being infixes of Φ. By Point 3(b) of
global consistency, since control paths of τ0 and τ00 overlap with that of τ, they share the
replacement location with it, and hence, by Point 3(a) of global consistency, the control
path of one of them is an infix of the control path of the other. The larger of the two thus
spans from the j-th to the k-th location (not more since the control path of τ is maximal
by definition). Hence, the longer of the two chains τ0 , τ00 can be taken as τi .
Point 3 of the lemma is also implied by consistency. If there was a contradicting
implementing edge or replacement location, Points 1 or 2 of global consistency, respectively, would imply that it belongs to a chain τ ∈ dom(ϒ) such that its symbolic trace is
an infix of Φ. The control path of τ cannot be an infix of a padding segment since this
would contradict the definition of a padding segment. Moreover, the control path of τ
cannot overlap with the control path of any τi . By Point 3(b) of global consistency, it
would share the replacement location with τi , hence by Point 3(a) and by the maximality of τi , τ would be an infix of τi , and by Point 5 of global consistency, its implementing
edges would be implementing edges of τi .
Finally, Point 1 of the lemma is easy to establish using the above reasoning.
t
u
Lemma 2. A computation of an annotated CFG cfg over a control path p is equivalent
to a computation over the image of p of the CFG cfg0 obtained from cfg by the procedure
for replacing destructive pointer operations.
23

Proof. Let φ = (`0 , c0 ), (`1 , c1 ), . . . be a computation of cfg. The equivalent computation
φ0 of cfg0 can be constructed by induction on the number n of segments of φ.
Take the case n = 0 as the case when φ consists of the initial state (`I , c0 ) only.
The claim of the lemma holds since both φ and φ0 are the same. A computation φ with
n + 1 segments arises by appending a segment to a prefix φn of a computation φ which
contains its n first segments, for which the claim holds by the induction hypothesis. That
is, assuming that φn ends by (`, c) there is a prefix of a computation φ0n of cfg0 which is
equivalent to φn and ends by (`0 , c0 ) where c and c0 are equivalent, and the control path
of φ0n is the image of the control path of φn .
Let the (n + 1)-th segment of φ be a padding one. Then the (n + 1)-th segment of
cfg0 is an infix of a computation that starts by (`0 , c0 ) and continues along the image of
the control path of the (n + 1)-th segment of φ. The paths are the same up to possibly
inserted assignment of parameters of container operations in the control of φ0n since, by
Lemma 1, a padding segment does not contain replacement points and implementing
instructions. Assignments of the parameters of container operations do not influence
the semantics of the path (modulo the values of the parameters) since the path does not
contain any calls of operations and the parameters are not otherwise used. Hence the
two configurations at the ends of the (n + 1)-th segments of φ and φ0 must be equivalent.
Let the (n+1)-th segment of φ be a chain segment. Let Φ = C0 ,C1 , . . . be a symbolic
trace of φ. By Lemma 1, we know that the infix of Φ that corresponds to the (i +
1)-th segment is a symbolic trace of some τi of ϒ, and that the control path of the
segment does not contain any replacement points other than the one of τi , and that all
implementing edges in it are implementing edges of τi . Let pi be the control path of τi
(and of the i + 1th segment). The control path pi is hence exactly p0i = pp .estmt .ps where
stmt is the statement calling the container operation δstmt of τi with parameters renamed
by λ`τi , and pp and ps are the prefix and suffix edges of τi . This means that under the
assumption that parameters of the operation stmt are properly assigned at the moment
of the call, p0i modifies the configuration c0 in the same way as pi modifies c, modulo
assignment of parameters, and hence the resulting configurations are equivalent. The
parameters are properly assigned since ν was complete.
t
u
Lemma 3. The control path of every computation of the annotated CFG cfg0 obtained
by the procedure for replacing destructive pointer operations from a CFG cfg is an
image of a control path of a computation in cfg.
Proof. By contradiction. Assume that the control path p0 of a computation φ0 of cfg0
is not an image of a control path of a computation in cfg. Take the longest prefix p00
of p0 such that there exists a computation φ of cfg with a prefix that has a control path
p and p00 is the image of p. p00 is a sequence of n images of segments of p ended by
an incomplete image of the (n + 1)-th segment of p. By Lemma 2, the configurations
of φ and φ0 at the end of the n-th segment and its image, respectively, are equivalent.
The computation φ0 then continues by steps within the image of the (n + 1)-th segment
of φ until a point where its control path diverges from it. The (n + 1)−th segment of
φ cannot be a padding segment since edges of padding segments and their images do
not differ (up to assignments of parameters of container operations, which are irrelevant
here). The (n + 1)-th segment of φ is thus a chain segment. By equivalence of semantics
24

of control paths of chains and their images (Section 5.1), φ0 must have had a choice to
go through the image of the (n + 1)-th segment until reaching its ending location with
a configuration equivalent to the one of φ. However, this means that branching of cfg0
is not deterministic. Since the code replacement procedure cannot introduce nondeterminism, it contradicts the assumption of the branching of cfg being deterministic.
t
u
The proof of Theorem 1 is now immediate.
Proof (Theorem 1). Straightforward by Lemma 2 and Lemma 3.

E

t
u

Replacement of Non-destructive Container Operations

We now discuss our way of handling non-destructive container operations, including,
in particular, a use of iterators to reference elements of a list and to move along the
list, initialisation of iterators (placing an iterator at a particular element of a list), and
emptiness tests. With a replacement recipe ϒ and an assignment relation ν at hand, recognizing non-destructive operations in an annotated CFG is a much easier task than that
of recognizing destructive operations. Actually, for the above operations, the problem
reduces to analysing annotations of one CFG edge at a time.
We first present our handling of non-destructive container operations informally by
showing how we handle some of these operations in the running example of Sect. 1. For
convenience, the running example is repeated in Fig. 43 . Fig. 5 then shows the annotated
CFG corresponding to lines 13–17 of the running example. In the figure, some of the
CSs are assigned the container variable L. The assignment has been obtained as follows:
We took the assignment of the chain input/output parameters defined by templates of
ϒ, renamed it at individual locations using renamings λ` , and propagated the obtained
names of CSs along Ics .
Clearly, the pointer assignment on the edge h13, p=h, 14i can be replaced by the
iterator initialisation p=front(L) because on line 13, the variable h is either at the
front region of the CS L, or in the case L is empty, it equals ⊥. This is exactly what
f ront(L) does: it returns a pointer to the front region of L, and if L is empty, it returns ⊥.
The pointer statement of the edge h16, p=p->f, 14i can by replaced by the list iteration
p=next(L,p) because in all SPCs at line 16, p points to an element of the CS L and
next is the binding pointer of L.
In the following four paragraphs, we present detailed definitions of common and
frequently used non-destructive container operations.
Go-to-front. Let e be an edge of an analysed CFG labelled by either p0 =p, p0 =ps,
or p0 s0 =p where p, p0 ∈ V p and s, s0 ∈ S p . This edge is a go-to-front element nondestructive container operation if there is a variable L ∈ Vc s.t. for each symbolic update (C, ·, ·) ∈ ∆e the following holds true: If C does not contain any container shape,
3

Actually, Fig. 4(c) contains a bit more complex version of the annotated CFG than the one
shown in Fig. 1(c). The reason is that Fig. 4(c) shows the actual output of Predator whereas
Fig. 1(c) has been slightly optimized for simplicity of the presentation. The optimization has
been based on that a DLL consisting of one region is subsumed by the set of DLLs represented
by a DLS—this subsumption is, however, not used by Predator.

25

typedef struct
int x;
struct SNode
struct SNode
} Node;
#define NEW(T)

SNode {
1

*f;
*b;

h=
t=
12

(T*)malloc(sizeof(T))

1 Node *h=0, *t=0;

1

2

h t

3

h t

while (nondet()) {
Node*p=NEW(Node);

p->x=nondet();

7

t

p

L
h

p

t

p

L

L

t->f=p
8

h p

h t

p

h

t

p

h p

h t

p

h

t

p

h p

h t

p

h

t

p

p

h

t

p

t

9
t

p->x=nondet()

}
...
Node *p=front(L);
while (p!=NULL) {
p->x=0;
p=next(L,p);
}

L
h

L

p->f=

L=push_back(L,p);

t

p

h t

h t p

h=p

(a)

4
h!=

5

h

L
h t

h t p

h==

t

L

h t

p=malloc()

2 while (nondet()) {
3
Node*p=NEW(Node);
4
if (h==NULL)
5
h=p;
6
else
7
t->f=p;
8
p->f=NULL;
9
p->x=nondet();
10
p->b=t;
11
t=p;
12 }
...
13 Node *p=h;
14 while (p!=NULL) {
15
p->x=0;
16
p=p->f;
17 }

h

L

nondet()

list L;

2

h t

10
t

p->b=t
t=p
11
p=

h

p

h t

t

L

L

1

L
2

(c)

(b)

Fig. 4. The running example from Sect. 1. (a) A C code using low-level pointer manipulations.
(b) The transformed pseudo-C++ code using container operations. (c) A part of the CFG of the
low-level code from Part (a) corresponding to lines 1-12, annotated by shape invariants (in the
form obtained from the Predator tool).

13

p

p=h
p==

17

p!=

h t

h t
4
h

t

h t
p

p

15
p

L

p->x=0

p

L

p

L

L

L

p
t

p

L

L

p

t

L

p
h

t

L

h t

t
p

h

t
p

h

t

L

p

h

h

t

h

1

5

7

6

t

L

p
h

h t

t

p
h

h

L

p

16

L

h t

ht

p

2

14

h

h t

h t

L

3
p

h

t

2

p

L

L
4

L

t
p

L

p=p->f
1

5

6 7

6 7

5

3

Fig. 5. The annotated CFG corresponding to lines 13–17 of the C code depicted in Fig. 4(a).

then either σC (p) = ⊥ or sC (σC (p)) = ⊥ according to whether the first or the second
syntactical form of the edge implementing the go-to-front operation is used. Otherwise,
σC (L) 6= > and, according to the syntactical form used, either σC (p) or sC (σC (p)) is the
front region of σC (L), respectively. We replace the label of each go-to-front edge, according to the syntactical form used, by p0 =front(L), p0 =front(L), or p0 s0 =front(L),
respectively.
26

Go-to-next. Let e be an edge of an analysed CFG labelled by p0 =ps where p, p0 ∈ V p
and s ∈ S p . This edge is a go-to-next element non-destructive container operation if
there is a variable L ∈ Vc s.t. for each symbolic update (C, ·, ·) ∈ ∆e there is σC (L) 6= >,
s corresponds to the next selector, and σC (p) belongs to σC (L). We replace the label of
each go-to-next edge by p0 =next(L, p).
End-reached? Let e = h`, stmt, ·i be an edge of an analysed CFG s.t. stmt is either
p==(p0 | ⊥) or p!=(p0 | ⊥) where p, p0 ∈ V p . Let p00 ∈ V p be a fresh variable s.t. for
each SPC C ∈ mem(`) either σC (p00 ) = σC (p0 ) or σC (p00 ) = ⊥, according to the syntactical form used. The edge e is an end-reached non-destructive container query operation if there is a variable L ∈ Vc , two different variables x, y ∈ {p, p00 }, two SPCs
C0 ,C00 ∈ mem(`) s.t. σC0 (L) 6= >, σC0 (x) = ⊥, σC00 (L) 6= >, σC00 (x) 6∈ {⊥, >}, and for
each symbolic update (C, ·, ·) ∈ ∆e , the following holds true: σC (y) = ⊥ and if C contains no container shape, then σC (x) = ⊥. Otherwise, σC (L) 6= > and σC (x) is either ⊥
or it belongs to σC (L). We replace the label stmt of each end-reached edge by x==end(L)
or x!=end(L), according to the syntactical form used, respectively.
Is-empty? Let e = h`, stmt, ·i be an edge of an analysed CFG s.t. stmt is either in the
form p==(p0 | ⊥) or p!=(p0 | ⊥) where p, p0 ∈ V p . Let p00 ∈ V p be a fresh variable s.t. for
each SPC C ∈ mem(`), either σC (p00 ) = σC (p0 ) or σC (p00 ) = ⊥, according to the syntactical form used. This edge is an is-empty non-destructive container query operation
if there is a variable L ∈ Vc , C0 ∈ mem(`) s.t. σC0 (L) 6= > and there are two different variables x, y ∈ {p, p00 } s.t. for each symbolic update (C, ·, ·) ∈ ∆e , the following
holds true: σC (y) = ⊥ and if C contains no container shape, then σC (x) = ⊥; otherwise,
σC (L) 6= > and σC (x) belongs to σC (L). We replace the label stmt of each is-empty
edge by 0==is empty(L) or 0!=is empty(L), according to the syntactical form used,
respectively.
We have omitted definitions of non-destructive container operations go-to-previous
and go-to-back since they are analogous to definitions of operations go-to-next and
go-to-front, respectively. There are more non-destructive container operations, such as
get-length. We have omitted them since we primarily focus on destructive operations in
this paper.
We now show how the definitions above apply to the edges of the annotated CFG cfg
corresponding to lines 13–17 of our running example from Fig. 4(a), which is depicted
in Fig. 5. Let us start with the edge h13, p=h, 14i. Clearly, according to the syntax of
the statement, the edge may be a go-to-front edge only. We can see in the figure that
the leftmost SPC at location 13 does not contain any container shape and σ(h) = ⊥. In
all the remaining SPCs at that location there is defined a container variable L and σ(h)
always references the front region of σ(L). Therefore, we replace p=h by p=front(L).
Next, we consider the edge h14, p!=⊥, 15i. According to the syntax of the statement,
it can either be an is-empty or an end-reached edge. Since variable p does not belong to
the container shape referenced by L in the rightmost SPC at location 14, the edge cannot
be an is-empty one. Nevertheless, it satisfies all properties of an end-reached edge. In
particular, whenever L is present in an SPC, then p references either a region of L or it is
⊥, and both of these cases occur at that location (for two different SPCs). Moreover, the
27

p
1

q

Y

X

p->f=q

q

p
2

Y

q->f->b=
p

q

3

Y'

q->b=p
p

q

p

q

4
q->f=

Y'

5

X'

Y'

Fig. 6. A fraction of an annotated CFG depicting interleaved operations push back and
pop front applied on CSs X and Y and the region q.

leftmost SPC at location 13 does not contain any container shape and σ(h) is indeed ⊥.
Therefore, we replace p!=⊥ by p!=end(L). The discussion of the edge h14, p==⊥, 17i
is similar to the last one, so we omit it.
The statement p->x=0 of the only outgoing edge from location 15 does not syntactically match any of our non-destructive container operations, so the label of this edge
remains unchanged.
Finally, the edge h16, p=p->f, 14i can be either a go-to-front or a go-to-next edge,
according to the syntax of its statement. However, since p does not reference the front
region of L in the rightmost SPC at location 16, the edge cannot be a go-to-front one. On
the other hand, we can easily check that L is defined at each SPC attached to location
16, f represents the next selector of L, and p always references a region of L. So, this
edge is a go-to-next edge, and we replace its label by p=next(L, p).

F

An Example of an Interleaved Use of Container Operations

We now provide an example illustrating that our approach can handle even the case
when a programmer interleaves the code implementing some container operations—in
our case, push back and pop front. The example is depicted in Fig. 6. The implementing edges of the push back operation are (1, 2), (3, 4), and (4, 5). A non-implementing
edge is (2, 3) because it operates on the pointer qf b of the region qf , which is not
included in the specification of the operation. The edge (2, 3) is an implementing edge
of the operation pop front.
From the point of view of the push back operation, one can see that the nonimplementing edge (2, 3) can be safely moved before the edge (1, 2). From the point
of view of the pop front operation, this move is also possible since (1, 2) is nonimplementing, i.e., it can be moved after the implementing edge (2, 3). Our algorithm
considers this rearrangement of edges and so it transforms this C code into the equivalent sequence of operations: (Y 0 ,q) = pop front(Y); X 0 = push back(X, q).
28

