Verifying Pointer Safety for Programs with
Unknown Calls
Chenguang Luo, Florin Craciun, Shengchao Qin, Guanhua He
Durham University, Durham DH1 3LE, UK

Wei-Ngan Chin
National University of Singapore

Abstract
We study the automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls. Given a Hoare-style partial correctness specification S ={Pre} C {Post} in separation logic, where the program C contains calls to some unknown procedure U , we infer a specification SU for the unknown procedure U from the calling contexts.
We show that the problem of verifying the program C against the specification S can be safely
reduced to the problem of proving that the procedure U (once its code is available) meets thederived specification SU . The expected specification SU for the unknown procedure U is automatically calculated using an abduction-based shape analysis. We have also implemented a
prototype system to validate the viability of our approach. Preliminary results show that the
specifications derived by our tool fully capture the behaviors of the unknown code in many cases.
Key words: Inference, verification, abduction, separation logic

1.

Introduction

While automated verification of memory safety remains a big challenge [14, 21], especially for substantial system software such as the Linux distribution and device drivers,
significant advances have been seen recently on the automated verification of pointersafety for such software [6, 22]. The abduction-based compositional shape analysis [6]is able to calculate the pre/post specifications for procedures in a bottom-up approach,based on the call-dependency graph. It can verify the pointer safety of a large portion
Email addresses: {chenguang.luo, florin.craciun, shengchao.qin, guanhua.he}@durham.ac.uk(Chenguang Luo, Florin Craciun, Shengchao Qin, Guanhua He), chinwn@comp.nus.edu.sg (Wei-NganChin).

Preprint submitted to Elsevier

16 April 2010

of the Linux kernel and many device drivers manipulating shared mutable data structures. One issue that has not been dealt within their work is unknown procedure calls. In
their SpaceInvader tool, unknown calls are currently ignored and replaced by the empty
statement skip during the verification. This may lead to imprecise or unsound results ingeneral. Our work here is to investigate this issue carefully and provide a better solution
to the verification of pointer safety of programs with unknown calls.
Automated program verifiers usually require to have access to the entire given program, which in practice may not be completely available for various reasons. For instance,some programs (e.g. in C) may contain unknown calls that correspond to function pointers, some programs (e.g. in OO) may contain calls to interface methods whose actual
implementations may not be available statically, or some programs may have calls to
library procedures whose code is not available during verification. Other possible scenarios can be found in remote procedure calls such as COM/DCOM [20], mobile code andsoftware upgrading, where program fragments may be unavailable at verification time. To
deal with the verification of programs with unknown procedure calls, current automatedprogram verifiers either• ignore the unknown procedure calls, e.g. replacing them by skip [6], which can beunsound in general; or• assume that the program and the unknown procedure have disjoint memory footprints
so that the unknown call can be safely ignored due to the hypothetical frame rule [18];however, this assumption does not hold in many cases; or• use specification mining [1] to discover possible specifications for the (unknown part ofthe) program, which is performed dynamically by observing the execution traces andis not likely to be exhaustive for all possible program behaviors; or• take into account all possible implementations for the unknown procedure [10, 12].
In general, there can be too many such candidates, making the verification almost
impossible at compile time; or• simply stop at the first unknown procedure call and provide an incomplete verification,
which is obviously undesirable.
Approach and contributions. We propose a different approach in this paper tothe verification of programs with unknown procedure calls. Given a specification S ={Pre} C {Post} for the program C containing calls to an unknown procedure U, our solution is to proceed with the verification for the known fragments of C, and at the sametime infer a specification SU that is expected for the unknown procedure U based on
the calling context(s). The problem of verifying the program C against the specification
S can now be safely reduced to the problem of verifying the procedure U against theinferred specification SU , provided that the verification of the known fragments does notcause any problems. The inferred specification is subject to a later verification when an
implementation or a specification for the unknown procedure becomes available (e.g. atloading time in Java).
The intuition of our method to infer the unknown procedure’s specification can be divided into two steps. The first step is to analyze the code before the unknown procedure
call to discover its precondition. The second is to analyze the code after the unknown
call in order to discover its postcondition. For the second step, one might suggest to use
a deductive backwards analysis, starting from the postcondition of the program being
verified, to derive an expected postcondition for the unknown procedure. We cannot follow this suggestion due to a technical challenge: backwards reasoning over the separation2

domain is simply too costly to implement ([6]). Therefore, we exploit an abductive forwards reasoning [6, 11] to derive the unknown procedure’s postcondition, and in this way
the verification can be accomplished.
Our paper makes the following technical contributions:• We propose a novel framework in separation logic for the verification of pointer safety
for programs with unknown calls.
• The top-down feature of our approach can potentially benefit the general softwaredevelopment process. Given the specification for the caller procedure, it can be used
to infer the specification for the callee procedures. This is a potentially beneficial
complement for current bottom-up approaches ([13]).
• We have enhanced the abduction mechanism, resulting in an improved algorithm forthe verification use. Compared with bi-abductive analysis [6] we have added additional
reasoning rules (e.g. for the list tail matching) such that the use of inaccurate reasoning
rules (like the “missing” rule) is avoided in many cases. We have also introduced a morepractical partial order to judge the quality of different solutions for abduction.
• We have successfully incorporated the call-by-reference mechanism into the forward
analyses in the separation domain.
• We have built a prototype system to test the viability and performance of our approach,and we have conducted some initial experimental studies to evaluate the precision of
the results and the scalability of our system. Preliminary results show that our tool
can derive expressive specifications which fully capture the behaviors of the unknown
code in many cases.
Outline. Section 2 employs a motivating example to informally illustrate our main approach. Section 3 presents the programming language and the abstract domain for ouranalysis. Section 4 introduces our abductive reasoning. Section 5 defines two abstract
semantics used in our verification. Section 6 depicts our verification algorithms. Experimental results are shown in Section 7, followed by some concluding remarks.
2.

A Motivating Example

In this section we illustrate informally, via an example, how our analysis infers the
specification for an unknown procedure. Our analysis makes use of a separation domain
similar to the one used in the SpaceInvader tool [6, 9]. To keep the presentation simple, we
use a small imperative language with both call-by-value and call-by-reference parameters
for procedures. Formal details about the abstract domain and the language will be given
in Section 3.
Example 1. Our goal is to verify the procedure findLast against the given pre/post
specifications shown in Figure 1. The data structure node { int data; node next }defines a node in a linked list. The predicate ls(x, y) used in the pre/post specifications aswell as other places denotes a (possibly empty) list segment referred to by x and ended
with the pointer y (i.e., y denotes the next field of the last node). Its formal definitionis given in page 7.
According to the given specification, the procedure findLast takes in a non-empty
linked list x and stores a reference to the last node of the list in the call-by-reference
parameter z. Here we group call-by-value and call-by-reference parameters together anduse semicolon ; to separate them. Note that findLast calls an unknown procedure
unkProc at line 4.
2

3

// Given Specification:// PrefindLast := ls(x, null) ∧ x6=null// PostfindLast := ls(x, z) ∗ z7→null
void findLast(node x; ref node z) {0
node w, y;
0a// ∆ := PrefindLast∆ ` x6=null
1
w := x.next;
1a// ∆ := x7→w ∗ ls(w, null) ∧ x6=null
2
if (w == null) z := x;2a// ∆ := x7→w ∧ x6=null ∧ w=null ∧ z=x
2b// ∃w, y · ∆ ` PostfindLast
3else {
3a// ∆ := x7→w ∗ ls(w, null) ∧ x6=null ∧ w6=null
3b// H := Local(∆, {x, y}) := x7→w ∗ ls(w, null) ∧ x6=null ∧ w6=null
3c// R0 := Frame(∆, {x, y}) := emp ∧ x6=null ∧ w6=null
4
unkProc(x; y);4a// ∆ := R0 ∗ M0
M0 := (emp ∧ x=a ∧ y=b)
M := M04b// ∆ 0 [y/x] PrefindLast
4c// ∆ ∗ [M1 ] . [y/x] PrefindLast (s.t. ∆ ∗ M1 ` [y/x] PrefindLast ∗ true)4d// M1 := ls(y, null) ∧ y6=null
M := M ∗ M1
4e// ∆ ∗ M1 ` [y/x] PrefindLast ∗ R1
R1 := emp ∗ x=a ∧ y=b
5
findLast(y; z);5a// ∆ := ([y/x] PostfindLast ) ∗ R1
5b// ∆ 0 PostfindLast
5c// ∆ ∗ [M2 ] . PostfindLast
M2 := ls(x, y)M := M ∗ M26
} }6a // PreunkProc := ∃w · [a/x, b/y] H
6b // PostunkProc := [a/x, b/y] M
Fig. 1. Verification of findLast calling an unknown procedure unkProc.

For this example, the unknown call to unkProc performs essential modification to a
local variable, so it can neither be regarded as skip nor dealt with using the hypotheticalframe rule. The candidate implementations of unkProc are not available, preventing averification against all possible candidates. However our approach is still applicable here
as described below.
We conduct a symbolic execution ([4, 16]) on the procedure body starting with theprecondition PrefindLast (line 0a). The results of our analysis (e.g. the abstract states) aremarked as comments in the code. The analysis carries on as a standard forward shapeanalysis until the unknown procedure call at line 4.
At line 3, the current symbolic heap ∆ is split into two disjoint parts: the local part
H (line 3b) that is dependent on, and possibly mutated by, the unknown procedure; andthe frame part R0 (line 3c) that is not accessed by the unknown procedure. Intuitively,
the local part of a symbolic heap w.r.t. a set of variables X is the part of the heap4

reachable from variables in X (together with the aliasing information); while the framepart denotes the unreachable heap part (together with the aliasing information). For
example, for a symbolic heap ls(x, w) ∗ ls(y, z) ∗ ls(z, null) ∧ w=z, its local part w.r.t.
{x} is ls(x, w) ∗ ls(z, null) ∧ w=z, and its frame part w.r.t. {x} is ls(y, z) ∧ w=z. We will
have their formal definitions in Section 6.
We take H (line 3b) as a crude precondition for the unknown procedure, since it
denotes the symbolic heap that is accessible, and hence potentially usable, by the unknown call. The frame part R0 is not touched by the unknown call and will remain in
the post-state, as shown in line 4a.
At line 4a, the abstract state after the unknown call consists of two parts: one isthe aforesaid frame R0 not accessed by the call, and the other is due to the procedure’s
postcondition which is unfortunately not available. Our next step is to discover the
postcondition by examining (the requirements of) the code fragment after the unknown
call by doing abductive reasoning (line 4a to 5c).
Initially, we assume the unknown procedure having an empty heap M0 as its postcondition 1 , and gradually discover the missing parts of the postcondition during the symbolic
execution of the code fragment after the unknown call. To do that, our analysis keeps
track of a pair (∆, M) at each program point, where ∆ refers to the current heap state,
and M denotes the expected postcondition discovered so far for the unknown procedure.
The notations Mi are used to represent parts of the discovered postcondition.
At line 5, the procedure findLast is called recursively. Since the current heap state
does not satisfy the precondition of findLast (as shown in line 4b), the verification
fails. However, this is not necessarily due to a program error; it may be due to the factthat the unknown call’s postcondition is still unknown. Therefore, our analysis performs
an abductive reasoning (line 4c) to infer the missing part M1 for ∆ such that ∆ ∗ M1
entails the precondition of findLast w.r.t. some substitution [y/x]. As shown in line
4d, M1 is inferred to be ls(y, null) ∧ y6=null, which is accumulated into M as part ofthe expected postcondition of the unknown procedure. (We will explain the details for
abductive reasoning in Sec 4.) Now the heap state combined with the inferred M1 meetsthe precondition of the procedure findLast, and also generates a residual frame heap
R1 (line 4e).
The heap state ∆ immediately after the recursive call (line 5a) is formed by findLast’s
postcondition and the frame R1 , and it is expected to establish the postcondition offindLast for the overall verification to succeed. However, it does not (as shown in line5b). Again this might be due to the fact that part of the unknown call’s postcondition
is still missing. Therefore, we perform another abductive reasoning (line 5c) to infer the
missing M2 as follows:ls(y, z) ∗ z7→null ∧ x=a ∧ y=b ∗ [M2 ] . ls(x, z) ∗ z7→nullsuch that ∆ ∗ M2 entails PostfindLast . In this case, our abductor returns M2 :=ls(x, y) as
the result which is then added into M by separation conjunction, as shown in line 5c.
Finally, we generate the expected pre/post-specification for the unknown procedure(lines 6a and 6b). The precondition is obtained from the local pre-state of the unknown
call, H, by replacing all variables that are aliases of a (or b) with the formal parameter a (or b). The postcondition is obtained from the accumulated abduction result, M,
1

Note that we introduce fresh logical variables a and b to record the value of x and y when unkProc
returns.

5

after performing the same substitution. Our discovered specification for the unknown
procedure unkProc(a;b) is:
PreunkProc := ∃w · a7→w ∗ ls(w, null) ∧ a6=null ∧ w6=null
PostunkProc := ls(a, b) ∗ ls(b, null) ∧ b6=null
The entire program is correct if unkProc meets the derived specification.
3.

Programming Language and Abstract Domain

In this section, we first depict the syntax of a language in which programs may invoke
unknown procedures, and then present the abstract domain for our analysis.
To focus only on key issues, we use a simple imperative language:E=df x | nullb

=df E1 =E2 | E1 6=E2

A[E] =df [E] := E1 | dispose(E) | x := [E]A=df x := E | x := new(E) | skip

C

=df A[E] | A | f (x; y) | C1 ; C2 |if b then C1 else C2 fi | while b do C od

U

=df unkFn(x; y) | { unkFn(x0 ; y0 ); C1 ;unkFn(x1 ; y1 ); C2 ; . . . ; Cn−1 ; unkFn(xn ; yn )} |if b then V else C fi | if b then C else V fi |if b then V1 else V2 fi | while b do V od

V=df { C1 ; U(x1 ;y1 ) ; C2 }(x0 ;y0 )P=df · | P ; f (x; ref y) { local z; C } |P ; f (x; ref y) { local z; V }Note that expressions (E) are program variables to record memory locations in the heap,
and all program variables are assumed of the same type, reference. The language has bothheap sensitive (A[E]) and heap insensitive (A) atomic commands. The former requires
access to the heap location referred to by E, while the latter does not. The command
C contains calls to known procedures only, while the commands U and V comprise
unknown procedure calls. Note also that our language allows both call-by-value andcall-by-reference parameters for procedures, and for convenience, we group call-by-value
parameters on the left and call-by-reference ones on the right, separated by a semicolon.
The unknown commands U and V specify the possible scenarios in which an unknown
call (unkFn(x; y)) may occur. Note that U and V may be annotated with two sets of variables, e.g. (x0 , y0 ) in the definition of V , where x0 denotes variables that can be accessed,
but cannot be modified by V , and where y0 denotes variables that may be mutated by
V . The same annotation applies to U . These annotations can be obtained automatically
via a pre-processing phase of the analysis, by recording all the variables appearing in V
as the right(left)-value of an assignment, and/or as a call-by-value(reference) parameterof a procedure invocation [17].

6Example 2 (Unknown procedure and unknown block). The parse tree of findLast’s
body (omitting local variable definition) in our motivating example is as in Figure 2. 2
V ({...}(x;w,y,z)
XX)XXX
gggg
XXXXX
g
g
g
g
g
XXXXX
ggggg
U(x,w;y,z)C(w := x.next)C(skip)if (w == null) then C(z := x)celse
ccV ({...}(x;y,z) )cccccggcgcgcgggg
c
c
c
c
c
c
c
c
g
ccccccggggg
ccccccccUc
C(skip)c
C(findLast(y, z))(x;y) (unkProc(x; y))Fig. 2. The parse tree of findLast’s body.

A program P is composed of several procedures (with one of them as the entry
method). A procedure can be totally known to the verifier (so that its body is composed by C), or it may contain an unknown block V .
We use a memory model similar to the standard one for separation logic [19]:Stack =dfVal
=df
Heap =df
State =df

(Var ∪ LVar ∪ SVar) → Val
Loc ∪ {null}Loc * Val
Stack × Heap

The slight difference is that we have three (disjoint) set of variables: a finite set ofprogram variables Var = {x, y, ..}, logical variables LVar = {x0 , y 0 , ..}, and the special(logical) variables SVar = {a, b, ..}, with the last set reserved for unknown proceduresfor specification purpose. As usual, Loc is a countably infinite set of locations, subsumed
by the set of values Val. The function Heap denotes a partial mapping from locations tovalues and a program state is a pair of stack and heap.
An abstract (program) state in our analysis is a symbolic heap representing a set ofconcrete heaps. It is defined as follows:E=df x | x0 | aΠ=df E1 =E2 | E1 6=E2 | true | Π1 ∧Π2 Pure formulae

Expressions

B(E1 , E2 ) =df E1 7→E2 | ls(E1 , E2 )Basic separation predicatesΣ=df B(E1 , E2 ) | true | emp | Σ1 ∗ Σ2 Separation formulae∆=df Π ∧ Σ

Quantifier-free symbolic heapsH=df ∃x.∆Symbolic heaps

The expressions (x, x0 and a) correspond to the three kinds of variables (program, logicaland special ones). Pure formulae Π express the aliasing information among expressions.
The basic separation predicate B(E1 , E2 ) denotes either a singleton heap or a list segment [6, 9, 16]. A (possibly empty) list segment is inductively defined as follows:ls(E1 , E2 ) =df (emp ∧ E1 =E2 ) ∨ (∃E3 · E1 7→E3 ∗ ls(E3 , E2 ))Here the list segment predicate is regarded as a built-in predicate in our abstract domain,as our abstract semantics and abduction are fine tuned for it. According to SpaceInvader [6] we may extend it with other predicates. A symbolic heap H is composed of a7

pure formula Π and a separation formula Σ, possibly with existential quantifications overthem. The separation formula Σ is formed by the predicates B(E1 , E2 ), true (arbitrary
heaps) and emp (an empty heap) via separation conjunction [19]. We use SH to denotethe set of all symbolic heaps and we will use the two terms “symbolic heap” and “abstractstate” interchangeably.
The semantics of a symbolic heap H [3, 4] is defined by the satisfaction relationship(s, h) |= H between a pair of stack and heap states (s, h) and H, where s ∈ Stack andh ∈ Heap:|[x]|s =df s(x)|[null]|s =df null(s, h) |= E1 =E2 =df |[E1 ]|s = |[E2 ]|s(s, h) |= E1 6=E2 =df |[E1 ]|s 6= |[E2 ]|s(s, h) |= Π1 ∧ Π2 =df (s, h) |= Π1 and (s, h) |= Π2(s, h) |= true
=df always(s, h) |= emp=df h = ∅(s, h) |= E1 7→E2 =df h = {|[E1 ]|s7→|[E2 ]|s}(s, h) |= Σ1 ∗ Σ2 =df h = h1 ∪ h2 and (s, h1 ) |= Σ1 and (s, h2 ) |= Σ2
where h1 and h2 are domain-disjoint
and the semantics of ls(E1 , E2 ) can be obtained from its inductive definition over theabstract domain. Based on such semantics, the entailment relationship between two symbolic heaps H1 and H2 is straightforward:
H1 ` H2 =df ∀s, h · (s, h) |= H1 implies (s, h) |= H2
which is used to check whether one symbolic heap is stronger than another in our analysis.
4.

Abduction

As shown in Example 1 (Section 2), when analyzing the code after an unknown call,due to the lack of information about the unknown procedure, it is possible that thecurrent state is too weak to meet the required precondition for the next instruction. As
a consequence, the symbolic execution fails. A technique called abduction (or abductive
reasoning) [6, 11] can be used to discover a symbolic heap M to make the entailment∆ ∗ M ` H ∗ R succeed, when the entailment ∆ ` H ∗ R fails. Here R denotes the(automatically computed) frame part. For instance, the entailments at line 4b and line
5b failed in Example 1, and in both cases, the abduction algorithm was called to find themissing M .
One problem in abduction is that there can be many solutions of M for the entailment∆ ∗ M ` H ∗ R to succeed. For instance, false can be a solution but should be avoided
where possible. As another example, for the entailment ls(y, z) ∗ M ` ls(x, z) ∗ R (asimilar one was at line 5c in Example 1 in Sec 2), an abductive reasoning may return,for example, two different solutions: M = ls(x, y) with R = emp or M = ls(x, z) with
R = ls(y, z). A partial order ¹ over symbolic heaps was given by Calcagno et al. [6] tomake the selection from different solutions:
M ¹ M0 =df (M0 ` M ∗ true ∧ M 0 M0 ∗ true) ∨(M0 ` M ∗ true ∧ M ` M0 ∗ true ∧ M0 ` M)

8

Intuitively speaking, consider two symbolic heaps M and M0 , if M0 entails M (possibly
extended by some frame), then M is less than M0 under ¹. For example, we have ls(x, y) ¹
ls(x, y) ∗ ls(y, z), and emp ∨ ∃x, y.ls(x, y) ¹ emp.
With such partial order ¹, we can judge the quality of different solutions for abduction
by always choosing the least one according to ¹.
Two solutions can not be distinguished when they are not comparable under thispartial order. However, we may still prefer one solution over another in this case, as will
be discussed in Section 6. We would expect that the solution to incur as few free variables
as possible in the frame part (R). For this reason, we define a new order as follows:
0
0
0
0
M ¹∆
H M =df M¹M ∨ (MM ∧ M M ∧∆ ∗ M ` H ∗ R ∧ ∆ ∗ M0 ` H ∗ R0 ∧|fv(R)| ≤ |fv(R0 )|)Note that our partial order is defined over the set of solutions for one abduction. Intuitively, given two solutions which are not comparable w.r.t. ¹, our partial order may still
be able to compare them, if one incurs fewer free variables in the frame R than the other.
To ensure that the abductor will choose the former, but not the latter, we enrich theabductor [6] with some new rules (right column below) so that it attempts to introduce
less free variables in the frame, where possible:∆ ∗ [M] . ∆0 ∆ ∗ B(E, E 0 ) 0 false(E0 =E1 ∧ ∆) ∗ [M] . ∃y0 .∆0missingt-match000∆ ∗ [M ∗ B(E, E )] . ∆ ∗ B(E, E )∆ ∗ E0 7→E ∗ [∃x0 .E0 =E1 ∧ M].
0 0
0∃x y .∆ ∗ E1 7→E
E6=E0 ∧ ∆ ∗ ls(E0 , x0 ) ∗ [M] . ∃y0 .∆0t-left∆ ∗ ls(E0 , E) ∗ [E0 6=E ∧ M].
0 0
00∃x y .∆ ∗ x 7→E(E6=E0 ∧ ∆ ∗ ls(x, E0 )) ∗ [M] . ∆0h-left∆ ∗ ls(E, E0 ) ∗ [E6=E0 ∧ M] .
0∃x.∆ ∗ E7→x

∆ ∗ [M] . ∆0 ∗ ls(E0 , E1 )∆ ∗ [M] . ∃x0 .∆0 ∗ ls(E0 , E1 )h-right
t-right0∆ ∗ B(E, E0 ) ∗ [M] . ∆ ∗ ls(E, E1 )∆ ∗ B(E0 , E) ∗ [M] . ∃x0 .∆0 ∗ B(E1 , E)
where the rules from Calcagno et al. [6] are on the left and our new ones are on the right.
Compared with their work, when the matching from the head of a list segment fails, ourabductor also tries to match from the tail, instead of directly applying missing rule tointroduce a new separation predicate, which could bring in more free variables in theframe. In our case, the rule t-match introduces aliasing information between two headsof pointing-to relationships in the premise and conclusion of the abduction, respectively.
The last two rules try to match from the end of a basic separation predicate; if thematching succeeds then the matched part will be dropped from both sides to reducethe complexity of the predicates. For instance, in Example 1 in Section 2, for the last
abduction∃y . ls(y, z) ∗ z7→null ∗ [M] . ls(x, z) ∗ z7→null
their abductor will return ls(x, z) as M, by trying to match the heads of the list segments
on both sides of ., and adding the missing heap part to the left hand side once thematching fails. This solution is not optimal in the light that it introduces a free variable
z in the frame. Comparatively, our abduction tries to match also from the tail of a list
segment, finding ls(x, y) as the result for the aforesaid abduction, which is a minimal
solution under our partial order ¹∆
H.

9

We prefer to find solutions that are (potentially locally) minimal with respect to¹∆
H and consistent. However, such solutions are generally not easy to compute and can
incur excess cost (with additional disjunction in the analysis). Therefore, our abductive
inference is designed more from a practical perspective to discover anti-frames that should
be suitable as specifications for unknown procedures, and the order ¹∆
H is to state thedecision choices of our implementation of the abduction. This is proven in Sec 7 with theexperiments we conduct.
5.

Abstract Semantics

This section introduces two kinds of abstract semantics we use to analyze the program:an underlying semantics from the local shape analysis ([9]) and another semantics basedon both the first one and abduction from the composite shape analysis ([6]).
We denote the specifications of a procedure f (x; y) as a subset of SH × (SH ∪ {>})
(where > stands for a fault abstract state). Note that for a call-by-reference parameter x,
both old(x) and x may occur in a postcondition with the former referring to the value ofx in the pre-state (as in JML [15]).To illustrate, a postcondition ls(old(x), x) means that
there is a list segment beginning with the initial value of x (present in the precondition)
to the final x when the procedure returns. The set of all specifications for all proceduresis defined as
AllSpec =df P(Name × P(SH × (SH ∪ {>})))
where Name refers to the set of all function names. Then our underlying abstract semantics’ type is defined as|[C]| : AllSpec → P > (SH) → P > (SH)where P > (SH) stands for P(SH ∪ {>}). Given a program C, a specification table T ∈AllSpec, a set of abstract states S, |[C]|T S returns another set of abstract states.
Example 3 (Underlying semantics). For the findLast in our motivating example, suppose the specification table T is{(findLast(a, b), {(ls(a, null) ∧ a6=null, ls(a, b) ∗ b7→null)})}Then we know the symbolic execution |[findLast(x, y)]|T {ls(x, null) ∧ x6=null} will give{ls(x, y) ∗ y7→null} as result.
2
The basic transition functions below form the foundation of the first underlying semantics. With one symbolic heap as input, they return either another symbolic heap or
a set of symbolic heaps:
rearr(E)=df SH → P > (SH[E])

Rearrangement

exec(A[E]) =df SH[E] → SH ∪ {>} Heap-sensitive execution
exec(A)=df SH → SH

Heap-insensitive executionabs=df SH → SH

Abstraction

where SH[E] denotes a set of symbolic heaps in which each element has E exposed as
the head in one of its pointing-to conjuncts (E7→F ). Here rearr(E) attempts to unroll

10the shape beginning with E to expose it as the head of a pointing-to predicate, say,
E points to another expression. (If such unrolling fails then it will return {>}.) Thisis a preparation for the second transition function exec(A[E]), as it tries to perform
some dereference of E. The third function, like the semantics for stack-based variableassignment and heap allocation, does not require such exposure of E, and thus is called
heap-insensitive compared with the second one. The last transition function conducts arolling over the shapes, to eliminate unimportant cutpoints to ensure termination for ourverification.
The rules for the basic transition functions are adopted from Distefano et al. [9], where
the logical variable x00 is always fresh.
Below are the rules for rearrangement, where we try to find an explicit pointing-to
beginning with the expression E to be unrolled (or its alias). If such unrolling fails then{>} is returned.
rearr(E) (∃x0 .Π∧∆ ∗ ls(G, F )) =df if Π ` G=E then{∃x0 .Π∧E=F ∧∆, ∃x0 .Π∧∆ ∗ E7→F,∃x0 , x00 .Π∧∆ ∗ E7→x00 ∗ ls(x00 , F )} else {>}| (∃x0 .Π∧∆ ∗ G7→F ) =df if Π ` G=E then{∃x0 .Π∧∆ ∗ E7→F } else {>}| (∃x0 .Π∧∆) =df {>}Below are rules for symbolic execution to reflect the effects, over heap or not, of atomic
commands.
exec (x := E)(∃x0 .Π∧∆) =df ∃x0 .x=[x00 /x]E ∧ [x00 /x](Π∧∆)
exec (x := [E])(∃x0 .Π∧∆ ∗ E7→F ) =df ∃x0 .x=[x00 /x]F ∧ [x00 /x](Π∧∆ ∗ E7→F )| (∃x0 .Π∧∆) =df >exec ([E] := G)(∃x0 .Π∧∆ ∗ E7→F ) =df ∃x0 .Π∧∆ ∗ E7→G| (∃x0 .Π∧∆) =df >exec (x := new(E))(∃x0 .Π∧∆) =df ∃x0 .[x00 /x](Π∧∆) ∗ x7→[x00 /x]E
exec (dispose(E))(∃x0 .Π∧∆ ∗ E7→F ) =df ∃x0 .Π∧∆| (∃x0 .Π∧∆) =df >Below are definitions of rules for abstraction. Their rationale is to remove any heap
garbage from the current state and eliminate logical cutpoints that are neither shared nor
essential in denoting a cyclic list over the heap. In our semantics, when the abstraction is
actually performed, the six rules are applied several rounds, with each round from the top
one to the bottom, until the abstracted state does not change any more. Its termination11

is discussed later in Section 6.2.
∃z0 . E=x0 ∧ Π ∧ Σ Ã ∃z0 . [E/x0 ]Π ∧ ΣEquality

x0 ∈LVar(Σ)/
Disequality∃z0 . E6=x0 ∧ Π ∧ Σ Ã ∃z0 . Π ∧ Σ
x0 ∈LVar(Π,
/
Σ)
Junk1
0
0
∃z . Π ∧ Σ ∗ B(x , E) Ã ∃z0 . Π ∧ Σ ∗ true
x0 , y 0 ∈LVar(Π,
/
Σ)
Junk2
∃z . Π ∧ Σ ∗ B(x , y 0 ) ∗ B(y 0 , x0 ) Ã ∃z0 . Π ∧ Σ ∗ true00/
Σ, E, F )
Π ` F =null
x0 ∈LVar(Π,
Abs1
0
0
0
∃z . Π ∧ Σ ∗ B1 (E, x ) ∗ B(x , F ) Ã ∃z0 . Π ∧ Σ ∗ ls(E, null)x0 ∈LVar(Π,/Σ, E, F, E1 , F1 )

Π ` F =E1

∃z0 . Π ∧ Σ ∗ B1 (E, x0 ) ∗ B(x0 , F ) ∗ B(E1 , F1 ) Ã ∃z0 . Π ∧ Σ ∗ ls(E, F ) ∗ B(E1 , F1 )Abs2

A lifting function p† is defined over partial functions on symbolic heaps to lift their
domains and ranges to a powerset of SH, plus >:p† S =df {> | > ∈ S} ∪ {p H | H ∈ S \ {>}}and this function is overloaded for rearr only to lift its domain to P > (SH):[rearr(E)† S =df {>|>∈S} ∪ (rearr(E) H)
H∈S\{>}

The following function, filt, is to filter out any symbolic heap that does not satisfy thegiven aliasing constraint:
filt (E=F )(H) =df if H 0 E6=F then H ∧ E=F else undefined
filt (E6=F )(H) =df if H 0 E=F then H ∧ E6=F else undefined
and the program constructors’ semantics are based on the atomic ones defined above:|[b]|T S=df filt(b)† S|[A[E]]|T S=df abs† ◦ exec(A[E])† ◦ rearr(E)† S|[A]|T S=df abs† ◦ exec(A)† S|[C1 ; C2 ]|T S=df |[C2 ]|T ◦ |[C1 ]|T S|[if b then C1 else C2 fi]|T S =df |[b; C1 ]|T S ∪ |[¬b; C2 ]|T S|[while b do C od]|T S=df |[¬b]|T (lfix λS0 .S ∪ |[b; C]|T S0 )12Finally we need to adapt the underlying abstract semantics to procedure invocation:|[f (x; y)]|T S =df {[x/a, y/b, y0 /old(b)]Post ∗ [y0 /y]R | ∆∈S ∧(Pre, Post)∈Specf ∧ ∆ ` [x/a, y/b]Pre ∗ R}
where (f, Specf ) ∈ T and y0 are freshwhere T is an element of AllSpec. We assume here the formal parameters in f ’s specifications are expressed in terms of a, b and old(b), respectively. We first check whether theprocedure’s precondition is satisfied by the current state (subject to substitution), andthen replace it with the (substituted) postcondition to indicate the effect of the procedure
call.
Next we define the abstract semantics with abduction used in our verification to
discover the effect of unknown procedure calls.
A

|[C]|

: AllSpec → P > (SH × SH) → P > (SH × SH)

Here P > (SH × SH) denotes P((SH ∪ {>}) × (SH ∪ {>})). Given a specification tableA
T ∈ AllSpec, each element of the input (or output) for |[C]|T is a pair of two symbolic
heaps, of which the first denotes the current program state, and the second stands for theabduction result. In our framework, this semantics is used to accumulate the discovered
effect of unknown procedure calls into the second symbolic heap in the pair.
Example 4 (Abstract semantics with abduction). Consider the same setting for findLast
A
in Example 3. For the semantics with abduction |[findLast(x, y)]|T {ls(x, null)}, we will
have {(ls(x, y) ∗ y7→null, x6=null)} as result. Here in order to obtain the first componentof the pair as the final state (ls(x, y) ∗ y7→null), the second component (x6=null) must
be added to its corresponding input state ls(x, null).
2
This semantics also consists of the basic transition functions which composes theatomic instructions’ semantics and then the program constructors’ semantics. Here thebasic transition functions are lifted as follows:
Rearr(E)(H, M) =df
let H=rearr(E)(H) and S={(H 0 , M)|H 0 ∈ H ∩ SH}
in if (> ∈/ H) then S
else if (H ` E=a for some a ∈ SVar) and (M 0 a7→x0 for fresh x0 ∈ LVar)then S ∪ {(H ∗ E7→x0 , M ∗ a7→x0 )} else S ∪ {>}Exec(A)(H, M) =df let H=exec(A)(H)in {(H 0 , M)|H 0 ∈ H} ∪ {>|> ∈ H}
where A is [E] := G or dispose(E)Exec(x := E)(∃x0 .Π∧∆, M) =df (∃x0 .x=σE ∧ σ(Π∧∆), σM)
Exec(x := [E])(∃x0 .Π∧∆ ∗ E7→F ) =df (∃x0 .x=σF ∧ σ(Π∧∆ ∗ E7→F ), σM)| (∃x0 .Π∧∆) =df if ∃x0 .Π∧∆ ∗ E7→F ` false then (>, σM)else (∃x0 .x=σF ∧ σ(Π∧∆ ∗ E7→F ), σ(M ∗ E7→F ))Exec(x := new(E))(∃x0 .Π∧∆) =df (∃x0 .σ(Π∧∆) ∗ x7→σE, σM)
Abs(H, M) =df (abs(H), abs(M))

13

In the lifted Rearr, in case of a rearrangement failure, we utilize abduction to discovera pointing-to in the current heap, followed by another attempt of rearrangement. If it
succeeds, then the abduction result is confirmed and added to the current state. Note thatin the definition of Exec we need to treat variable assignments specifically. As can be seenin the rules, when x is assigned to a new value, the original value is still preserved in a fresh
logical variable x00 with a substitution σ = [x00 /x]. This allows us to keep the connection
among the history values of a variable and its latest value, which may be essential asa link from the unknown procedure’s postcondition to its caller’s postcondition. Thisis because the unknown procedure’s postcondition may refer to one of such variable’s
historical values, and its caller’s postcondition can count on that variable’s final value. Inthat case, the recorded values in the abduction results will serve as a connection among
these abstract states. Abs simply performs abstraction over both H and M.
The filter function Filt now only works on the first symbolic heap of a pair:Filt(b)(H, M) =df (filt(b)(H), M)
and the abstract semantics for the program constructors is as follows:A=df Filt(b)† S|[b]|T S
A=df Abs† ◦ Exec(A[E])† ◦ Rearr(E)† S|[A[E]]|T S
A=df Abs† ◦ Exec(A)† S|[A]|T S
A

A|[C1 ; C2 ]|T S

A=df |[C2 ]|T ◦ |[C1 ]|T S
AAA|[if b then C1 else C2 fi]|T S =df |[b; C1 ]|T S ∪ |[¬b; C2 ]|T S
A|[while b do C od]|T S

AA=df |[¬b]|T (lfix λS0 .S ∪ |[b; C]|T S0 )Same as above, at last is the semantics for procedure invocation with abduction:A|[f (x; y)]|T S =df {([x/a, y/b, y0 /old(b)]Post ∗ [y0 /y]R, [y0 /y]M) | (∆, M)∈S ∧(Pre, Post)∈Specf ∧ ∆ ` [x/a, y/b]Pre ∗ R} ∪{([x/a, y/b, y0 /old(b)]Post ∗ [y0 /y]R, [y0 /y](M ∗ M0 )) |(∆, M)∈S ∧ (Pre, Post)∈Specf ∧ ∆0[x/a, y/b]Pre ∗ R ∧∆ ∗ [M0 ] . [x/a, y/b]Pre}
where (f, Specf ) ∈ T and y0 are freshwhere T is an element of AllSpec. We also use a, b and old(b) for formal parameters inthe specification. This rule distinguishes two cases: 1. the current state in S is sufficiently
strong to entail Pre subject to some substitutions, and corresponding postcondition isestablished; 2. the current state does not entail substituted Pre, and abduction is appliedwith further requirements on the current state accumulated (M0 ). It will combine theresults from both cases to update the state after the procedure invocation and continue
with the symbolic execution.

14

6.

Verification

Based on the abstract semantics defined in the last section, we present in this section
our algorithms for the verification of programs with unknown calls.
6.1.

Main Verification Algorithm

1. Main algorithm. Our verification algorithm given in Figure 3 attempts to verify the
body of the current procedure (the third input, comprising an unknown command U )against the given specifications (the second input). The first input gives a set of known
procedure specifications, which are necessary as the current procedure may invoke known
procedures apart from unknown ones. If the verification succeeds, it returns specifications
that are expected for all unknown procedures invoked within U for the whole verification
to succeed. If it fails, we know that the current procedure cannot meet one or more
given specifications, no matter what specifications are given to the invoked unknown
procedures. Returned specifications will be expressed using special variables a, b, etc. asin the earlier example.
For each specification (Pre, Post) to verify against (line 2), the algorithm works inthree steps. Based on the underlying semantics mentioned earlier, it first computes thepost-states of C1 (i.e. S0 ) from Pre (line 3), from which it extracts the preconditions forU(x;y) using the function Local. Intuitively, it extracts the part of each ∆1 reachable fromthe variables that may be accessed by U , namely, x and y (line 6). Here fv(∆) stands for
all free (program and logical) variables occurring in ∆. The function Local(Π ∧ Σ, {x})is defined as follows:
Local(Π∧Σ, {x}) =df ∃fv(Π∧Σ) \ ReachVar(Π∧Σ, {x}) ·Π ∗ ReachHeap(Π∧Σ, {x})where ReachVar(Π∧Σ, {x}) is the minimal set of variables reachable from {x}:{x} ∪ {z2 | ∃z1 , Π1 · z1 ∈ReachVar(Π∧Σ, {x}) ∧ Π=(z1 =z2 ) ∧ Π1 } ∪{z2 | ∃z1 , Σ1 · z1 ∈ReachVar(Π∧Σ, {x}) ∧ Σ=B(z1 , z2 ) ∗ Σ1 } ⊆ ReachVar(Π∧Σ, {x})where B(z1 , z2 ) stands for either z1 7→z2 or ls(z1 , z2 ). And the formula ReachHeap(Π∧Σ,{x}) denotes the part of Σ reachable from {x} and is formally defined as the ∗-conjunctionof the following set of formulae:{Σ1 | ∃z1 , z2 , Σ2 · z1 ∈ReachVar(Π∧Σ, {x}) ∧ Σ=Σ1 ∗Σ2 ∧ Σ1 =B(z1 , z2 )}The second step is to symbolically execute C2 , using the abstract semantics with
abduction, to discover the postconditions for U(x;y) (lines 8–10). At line 8, since we know
nothing about U , we take emp as the post-state of U . Therefore, the initial state for thesymbolic execution of C2 is simply the frame part of state not touched by U . Here Frame
is formally defined as
Frame(Π∧Σ, {x}) =df Π ∧ UnreachHeap(Π∧Σ, {x})where UnreachHeap(Π∧Σ, {x}) is the formula consisting of all ∗-conjuncts from Σ which
are not in ReachHeap(Π∧Σ, {x}).
Note that x=a ∧ y=b ∧ z=c are used to record the snapshot of variables associatedwith U using the special variables a, b and c. The symbolic execution of C2 at line 815Verify : AllSpec × P(SH × SH) × V * AllSpec ∪ {fail}
Algorithm Verify(T , SpecV , {C1 ; U(x;y) ; C2 }(x0 ;y0 ) )1 SpecU := ∅2 foreach (Pre, Post) ∈ SpecV do
3 S0 := |[C1 ]|T {Pre ∧ y0 =old(y0 )}4 if > ∈ S0 then return fail endif
5 foreach ∆1 ∈ S0 do
6
PreU := Local(∆1 , {x, y})7
Denote z = fv(PreU ) \ {x, y}A
8
S := |[C2 ]|T {([old(b)/y] Frame(∆1 , {x, y}) ∧x=a ∧ y=b ∧ z=c, emp ∧ x=a ∧ y=b ∧ z=c)}
S0 := { (∆, M) | (∆, M)∈S ∧ ∆ ` Post ∗ true } ∪9{ (∆ ∗ M0 , M ∗ M0 ) | (∆, M)∈S ∧∆ 0 Post∗true ∧ ∆∗[M0 ] . Post }10
if ∃(∆, M)∈S0 . fv(M) * ReachVar(∆, {a, b})then return (fail, M) endif
11
foreach (∆, M) ∈ S0 do
PreU := [a/x, b/y, c/z]PreU
12
13
PostU := sub alias(M, {a, b, c})
14g := (fv(PreU ) ∩ fv(PostU )) ∪ {a, b}
15
SpecU := SpecU ∪ {(∃(fv(PreU )\g) · PreU , PostU )}16
end foreach17 end foreach18 end foreach
19 TU := CaseAnalysis(T , SpecU , U )20 Post Check(T ]TU , SpecV , {C1 ; U ; C2 })21 return T ]TU
end Algorithm
Fig. 3. The main verification algorithm.

returns a set S of pairs (∆, M) where ∆ is a possible post state of C2 and M records
the discovered effect of U . At line 9, we check whether or not each ∆ can establish thepostcondition Post for the whole procedure. If not, another abduction ∆∗[M0 ] . Post is
invoked to discover further effect M0 which is then added into M.
There can be some complication here. Note that there can be a potential bug in the
program, or the given specification is not sufficient. As a consequence of that, the result
M returned by our abductor may contain more information than what can be expectedfrom U , in which case we cannot simply regard the whole M as the postcondition of U .
For example, consider the code fragment unknown(x); z:=y.next with the precondition
x7→null. Before the second instruction (dereference of y.next) we use abduction to get
y6=null. However, noting the fact y ∈ReachVar(∆,/{x}) where ∆ = emp∧y6=null is thestate immediately after the unknown call plus the abduction result, we know that fromthe unknown call’s parameters (x), y is not reachable, and hence the unknown call will
never establish a state where y6=null. In that case we are assured that the procedure
being verified cannot meet the specification.

16

To detect such a situation, we introduce the check in line 10. It tests whether the whole
abduction result is reachable from variables accessed by U . If not, then the unreachable
part cannot be expected from U , which indicates a possible bug in the program or someinconsistency between the program and its specification. In such cases, the algorithm
returns an additional formula that can be used by a further analysis to either identify
the bug or strengthen the specification. Recall the example presented in the previous
paragraph: since y6=null cannot be established by the unknown call, if we add it to theprecondition of the code fragment (to form a new precondition x7→null ∧ y6=null), thenthe verification with the new specification can move on and will potentially succeed. We
will exemplify this later with experimental results.
The third step (lines 11–16) is to form the derived specifications for U in terms ofvariables a, b and g, where g denotes logical variables not directly accessed by U , but
occurring in both pre- and postconditions. The formula sub alias(M, {a, b, c}) is obtained
from M by replacing all variables with their aliases in {a, b, c}. It is defined as
sub alias(M, {x}) =df ({[x/x0 ] | x∈{x} ∧ x0 ∈aliases(M, x)} M)∧
V{x = x0 | x, x0 ∈{x} ∧ x0 ∈aliases(M, x)}
where a set of substitutions before a formula M denotes the result of applying all those
substitutions to M, and aliases(M, x) returns all the aliases of x in M.
Finally, at line 19, the obtained specifications SpecU for U are passed to the caseanalysis algorithm (given in Figure 4) to derive the specifications of unknown procedures
invoked in U . At line 20, we conduct a post analysis for soundness purpose.
2. Case analysis algorithm. In order to discover specifications for unknown procedures
invoked in U , the algorithm in Figure 4 conducts a case analysis according to the structureof U . In the first case (line 2), U is simply an unknown call. In this situation, the algorithm
simply returns all the pre-/postcondition pairs from SpecU as the unknown procedure’s
specifications.
In the second case (line 4), U is an if construct and each branch contains an unknown
block. The algorithm uses the main algorithm to verify the two branches separately withpreconditions Pre∧b and Pre∧¬b respectively, where Pre is one of the preconditions of
the whole if. The results obtained from the two branches are then combined using the ]operator:
R1 ] R2 =df {(f, Refine(Spec1f ∪ Spec2f )) | (f, Spec1f )∈R1 ∧ (f, Spec2f )∈R2 }where Refine is defined as
Refine (∅)=df ∅Refine ({(Pre, Post)} ∪ Spec) =df if ∃(Pre0 , Post0 )∈Spec · Pre0 ¹Pre ∧ Post¹Post0
then Refine(Spec)else {(Pre, Post)} ∪ Refine(Spec)The intuition of Refine is to eliminate any specification (Pre0 , Post0 ) from a set if there
exists a “stronger” one (Pre, Post) such that Pre¹Pre0 and Post0 ¹Post. ] is to refine theunion of two specification sets.

17

CaseAnalysis : AllSpec × P(SH × SH) × U * AllSpec ∪ {fail}
Algorithm CaseAnalysis(T , SpecU , U )1 switch U
2 case unkFn(x; y)3
return {(unkFn, SpecU )}4 case if b then V1 else V2 fi
5
SpecT := {(Pre∧b, Post) | (Pre, Post) ∈ SpecU }6
SpecF := {(Pre∧¬b, Post) | (Pre, Post) ∈ SpecU }7
R1 := Verify(T , SpecT , V1 )8
R2 := Verify(T , SpecF , V2 )9return R1 ] R2
10 case if b then V else C fi
11
SpecT := {(Pre∧b, Post) | (Pre, Post) ∈ SpecU }12
R := Verify(T , SpecT , V )13
if ∃(Pre, Post) ∈ SpecU , ∆ ∈ |[C]|T {Pre ∧ ¬b} ·∆=> ∨ ∆ 0 Post∗true then return fail14
else return R endif
15 case if b then C else V fi (Similar to the previous case)
16 case while b do V od
Denote V as {C1 ; U(x1 ;y1 ) ; C2 }(x;y)
1718Define loop(x; y){ if b then V ; loop(x; y) fi}
19
T 0 := T ] { (loop, SpecU ) }20
return Verify(T 0 , SpecU , {if b then V ; loop(x; y) fi}(x;y) )21 case unkFn(x0 ; y0 ); { ; Ci ; unkFn(xi ; yi )}ni=122
return {(unkFn, SeqUnkCalls(T , SpecU , U ))}end Algorithm
Fig. 4. The case analysis algorithm.

The third and fourth cases (line 10 and 15) are for if constructs which contain one
unknown block in one branch. This is handled in a similar way as in the second case.
The only difference is that, for the branch without unknown blocks, we need to verify itwith the underlying semantics (line 13).
The fifth case is the while loop. In the motivating example in Section 2, we haveshown that our approach is able to handle the verification of a tail-recursive function
provided with both pre- and postconditions, our solution here is to translate the while
loop into a tail-recursive function to verify it. As can be seen in lines 16 – 20, the algorithm
generates a new function loop for the while loop, and takes the variables accessed by V tobe its parameters. Note that the read-only variables (x) become call-by-value parameters
and other possibly mutable ones (y) become call-by-reference parameters (which is one
reason for us to introduce call-by-reference parameters in our language). The algorithm
then adds the specifications found for the while loop as loop’s specifications into table T ,verifying it, and at the same time obtaining specifications for the unknown procedure in
the while loop, using the main algorithm Verify.
In the last case (line 21), where U consists of multiple unknown procedure calls insequence, the algorithm invokes another algorithm, SeqUnkCalls, to deal with it.

18

3. Verifying sequential unknown calls. To handle the most complicated case, unknown procedure calls in sequence, we still need the SeqUnkCalls algorithm. First we
illustrate the brief idea using two sequential unknown procedure calls as an example,
followed by the general algorithm.
Suppose we have{Pre} {unkFn1 (x0 ; y0 ); C; unkFn2 (x1 ; y1 )} {Post}
where C is the only known code fragment within the block. Our current solution attempts
to find a common specification to capture both unknown procedures’ behaviors.
The algorithm works in three steps. In the first step, it extracts the precondition for
the first procedure, say PreU , from the given precondition Pre by extracting the part ofheap that may be accessed by the call via x0 and y0 , which is similar to the first step of
the main algorithm Verify. Aiming at a general specification for both unknown calls, itthen assumes that the second procedure has a similar precondition PreU . In the second
step, it symbolically executes the code fragment C with the help of the abductor, todiscover a crude postcondition, say Post0U , expected from the first unknown call. This issimilar to the second step of the main algorithm Verify, except that the postcondition
for C is now assumed to be PreU . In the third step, the algorithm takes Post0U (withappropriate variable substitutions) as the postcondition of the second unknown call, andchecks whether or not the derived post (Post0U ) satisfies Post. If not, it invokes anotherabduction to strengthen Post0U to obtain the final postcondition PostU for the unknown
procedures. Note that this strengthening does not affect soundness: the strengthened
PostU can still be used as a general postcondition for both unknown procedures.
Figure 5 presents the algorithm to infer specifications for n (n ≥ 2) unknown calls in sequence. As aforementioned, given a block of (n+1) unknown procedure calls with n piecesof known code blocks sandwiched among them (unkFn(x0 ; y0 ) {; Ci ; unkFn(xi ; yi )}ni=1 inline 1), and the specification (Pre, Post) (line 3) for such a block, our approach generally
works in three steps: first, to compute a precondition for the unknown calls; second, toverify each code fragment Ci (i = 1, ..., n) with abduction to collect expected behavior of
the unknown calls (as part of their postcondition); third, to guarantee that the collected
postcondition satisfies Post. If not, then another abduction is conducted to strengthen
the gained postcondition to ensure this.
The first step is completed by lines 4 to 6. The local part of Pre is extracted w.r.t.
the first unknown call’s parameters x0 and y0 . Other free variables are distinguished asz0 , which may be ghost variables. Finally the precondition is found in terms of special
logical variables a, b and c.
The second step is performed over each Ci ; unkFn(xi ; yi ). Its main idea is to take thepostcondition generated for the last unknown call (Posti−1 ), plus the frame part during
the entailment check against Prei−1 , as the post-state of unkFn(xi−1 ; yi−1 ), and try toverify Ci beginning with such a state, using abduction when necessary (line 9). Afterthe verification we get Si containing abstract states before unkFn(xi ; yi ), and we wantthose states to satisfy its precondition PreU subject to substitution. Note that during theverification of Ci and the last satisfaction checking we may use abduction to strengthen
the program state, whose results reflect the expected behavior of unkFn(xi−1 ; yi−1 ) andare accumulated as its expected postcondition. Hence we achieve a sufficiently strong
postcondition for each unknown call.

19

SeqUnkCalls : AllSpec × P(SH × SH) × U * P(SH × (SH ∪ {>}))
Algorithm SeqUnkCalls(T , SpecU , U )1 Denote U as unkFn(x0 ; y0 ) {; Ci ; unkFn(xi ; yi )}ni=1
2 R := ∅3 foreach (Pre, Post) ∈ SpecU do
PreU := Local(Pre, {x0 , y0 })45
Denote z0 = fv(PreU ) \ {x0 , y0 }6
PreU := [a/x0 , b/y0 , c/z0 ]PreU
7
S00 := {(Pre ∧ y0 =old(y0 ), emp ∧ a=x0 ∧ b=y0 ∧ c=z0 )}8for i := 1 to n doA
Si := |[Ci ]|T { (Posti−1 ∗[old(b)/yi−1 ] Frame(∆i−1 , {xi−1 , yi−1 }), Posti−1 ) |9(∆i−1 , Mi−1 )∈S0i−1 ∧ Posti−1 = ([xi−1 /a, yi−1 /b, zi−1 /c] sub alias(
Mi−1 , {a, b, c})) ∧ a=xi−1 ∧ b=yi−1 ∧ c=zi−1 } where zi−1 is fresh
10
S0i := {(∆, M) | (∆, M)∈Si ∧ σ∆ ` ∃c · PreU ∗true} ∪ {(∆ ∗ M0 , M ∗ M0 ) |(∆, M)∈Si ∧ σ∆ 0 ∃c · PreU ∗true ∧ σ∆∗[M0 ] . ∃c · PreU }where σ=[a/xi , b/yi ]11
if ∃(∆, M)∈S0i · fv(M) * ReachVar(∆, {a, b}) thenreturn (fail, Local(M, {x0 , old(y0 )})) endif
12
end for13
Sn+1 := { (Postn ∗[old(b)/yn ]Frame(∆n , {xn , yn }), Postn ) | (∆n , Mn )∈S0n ∧Postn = ([xn /a, yn /b, zn /c] sub alias(Mn , {a, b, c})) ∧a=xn ∧ b=yn ∧ c=zn } where zn is fresh
14
S0n+1 := {(∆, M) | (∆, M)∈Sn+1 ∧ ∆ ` Post∗true} ∪ {(∆ ∗ M0 , M ∗ M0 ) |(∆, M)∈Sn+1 ∧ ∆ 0 Post∗true ∧ ∆∗[M0 ] . Post}
015
if ∃(∆, M)∈Sn+1 · fv(M) * ReachVar(∆, {a, b}) thenreturn (fail, Local(M, {x0 , old(y0 )})) endif
foreach (∆, M) ∈ S0n+1 do
16
17
PostU := sub alias(M, {a, b, c})18g := fv(PreU ) ∩ fv(PostU ) \ {a, b}
19
R := Refine(R ∪ {(∃fv(PreU ) \ (g ∪ {a, b}) · PreU , PostU )})20
end foreach21 end foreach
22 return R
end Algorithm
Fig. 5. Algorithm for sequential unknown calls.

The third step is similar to the first algorithm: it checks whether the final abstractstate entails the postcondition of the whole block, and strengthens the final abstractstate with abduction if it cannot. Then the ghost variables are recognized and processedanalogously to the first algorithm. Finally the strongest specifications discovered for thoseunknown procedures are returned.
Note that our current solution tries to find a common specification (Pre, Post) suitable
for all the unknown procedures. Generally we may allow the unknown procedures tohave different specifications. In theory, this can be achieved by a more in-depth analysis

20

which examines the known code fragments in between those unknown calls. That is,by analyzing the code fragment Ci we would hopefully obtain a postcondition for the(i−1)-th procedure and a precondition for the i-th. In the case of two unknown calls
unkFn0 (x0 ; y0 ); C1 ; unkFn1 (x1 ; y1 ), the precondition for unkFn0 and the postcondition for
unkFn1 can be obtained as usual (by analyzing the code before unkFn0 and after unkFn1
respectively). To derive the postcondition Post0 for unkFn0 and the precondition Pre1 for
unkFn1 , we initialize Post0 to be emp to start a forward analysis over C1 with abduction,to accumulate (via abduction) the expected behavior of unkFn0 (for C1 to be verified)
as Post0 , and extract a formula (which is relevant to the footprint of unkFn1 ) from theabstract state at the end of C1 as Pre1 . However, our initial experiments show that, unlessthe fragment C1 is sufficiently complex to expose enough information expected fromunkFn0 , the derived Post0 and Pre1 can be rather weak. As a consequence, the derived
specification for unkFn0 can be too weak (with a weak postcondition) and the one for
unkFn1 can be too strong (with a weak precondition). It remains an open problem how
we might tune the derived results to obtain more reasonable specifications. We conjecturethat certain heuristics might help and we will explore this further in our future work.
6.2.

Soundness and Termination

Informally, in the presence of unknown procedure calls, the soundness of the verification signifies that, a program is successfully verified against its specifications, if all
the unknown procedures that it invokes conform to the specifications discovered by theverification algorithm. Therefore, the correctness of the program depends on a (possible)
further verification for the unknown procedures.
The soundness of our verification algorithm is guaranteed at line 20 in the algorithm
Verify. Upon return, the algorithm conducts another forward verification on the whole
program, assuming that the unknown procedures are already verified against the discovered specifications. As in Calcagno et al. [6], this final check rules out any potentiallyunsound pre/post pairs (due to the use of abstraction); therefore, it ensures the soundnessof our verification.
The termination of our verification algorithms is based on two facts: the finiteness ofverification input (program and its specifications), and the termination of our semantics.
Firstly, all the loops and (recursive) algorithm invocations in the three verification algorithms are performed over the input program and specifications to be verified, where
each time of iteration deals with part of the specifications/states and each invocation
processes part of the input program structurally. Therefore, as long as all such processing terminates, the whole verification will terminate. This fact is further guaranteed withthe termination of our abstract semantics, which can be proved by claiming the finiteness of program and logical variables, and hence the finiteness of all possible abstractstates [9]. Hence we can conclude that our verification algorithm terminates with resultsof either fail or successfully returned specifications that the unknown procedures must
conform.
7.

Experiments and Evaluation

We have implemented the two abstract semantics and the verification algorithms with
Objective Caml and evaluated them over some list processing programs to test their21

viability and precision. The results are in Table 1. The first and second columns denote theprograms used for evaluation [5, 8] and their time consumption, respectively. We manuallyhide some code in the original programs as calls to unknown procedures, for which wetry to discover specifications during the verification process. The third column shows thepartial specification for each program that is provided as input to our algorithm. The
last column exhibits the discovered specifications for unknown procedures inside those
programs. The programs are listed in Figure 6.
ProgramTime(s)Program Specification

findLast(x; z)

0.00135

Pre := ls(x, null) ∧ x6=null
Post := ls(x, z) ∗ z7→null

append(y; x)

0.00216

copy(x; y)0.00204

revCopy(x; y)

0.00107

clear(; x)0.00239

appendThree(y, z; x)0.00315

towardsLast(x; y)

0.00428

iWillFail(x, y; )0.00066

Discovered Unknown Specification
Pre:= ∃w · a7→w ∗ ls(w, null)∧
a6=null ∧ w6=null
Post:= ls(a, b)∗ls(b, null)∧b6=null
Pre := ls(a, null)
Post := ls(a, b) ∗ ls(b, null)
Pre := ls(a, null)
Post := ls(a, null)
Pre := true
Post := true
Pre := a7→b ∗ ls(b, null)
Post := ls(b, null)

Pre := ls(x, null)∗ls(y, null)
Post := ls(x, y) ∗ ls(y, null)
Pre := ls(x, null)
Post := ls(x, null)∗ls(y, null)
Pre := ls(x, null)
Post := ls(x,null)∗ls(y,old(y))
Pre := ls(x, null)
Post := emp ∧ x=null
Pre:= ls(x, null)∗ls(y, null)∗
Pre := ls(a, null) ∗ ls(b, null)ls(z, null)
Post := ls(a, null)
Post:= ls(x, null)
Pre:= ls(x, null) ∧ x6=null
Pre:= ls(a, null) ∧ a6=null
Post:= ls(x, y) ∗ ls(y, null)∧
Post:= ls(a, null) ∗ ls(b, null)∧
x6=null
a6=null ∧ b6=null
Pre:= ls(x, null)(fail, ls(y, null))
Post:= ls(x, null) ∗ ls(y, null)

Table 1. Experimental results for simple list processing programs.

Here we note down two observations on the experimental results. The first is that thediscovered specifications for the unknown procedures are more general than we would
have expected. Bear in mind that we have replaced some code from those programs withunknown calls. We have compared the inferred specifications for those unknown callswith the original code. The results show that the specifications derived by our algorithm
not only fully capture the behaviors of the replaced code, but also suggest other possible
implementations. A case in point is our motivating example findLast given in Sec 2,
where the original code replaced by unknown call is y := x.next with the post-state
x7→y ∗ ls(y, null) ∧ y6=null. According to our result, the post-state can be more general,
namely, ls(x, y) ∗ ls(y, null) ∧ y6=null. This suggests that as long as y is not null, theunknown call can traverse any number of nodes towards the tail of the list.
The second observation is about the last program listed in the table, a procedure
called iWillFail, whose code is given as follows:
void iWillFail(node x, node y; ) { unknown(x; ) }22

findLast(x; ref z) {node w := [x], y;
if w = null then z := xelse
unknown(x; y);findLast(y; z)fi}append (y; ref x) {if x = null then x := yelse
unknown(x; w);
if w = null then [x] := yelse append(y; w)fifi}

copy(x; ref y) {if x = null then y := nullelse
w := [x];copy (w; y);unknown(; y);fi}

revCopy(x; ref y) {if x = null then skip
else
unknown(; y);w := [x];revCopy (w; y)fi}clear(; ref x) {if x = null then skipelse
w := [x];unknown(x, w; );x := w;
clear(; x)fi}appendThree(y, z; ref x) {unknown(x, y; );unknown(x, z; )}towardsLast(x; y) {unknown(; x);unknown(x; y)}iWillFail(x, y; ) {unknown(x; )}Fig. 6. Code of experimental examples.

This program is expected to be verified against the specification (Pre = ls(x, null),
Post = ls(x, null) ∗ ls(y, null)). Our verification fails and returns an additional formulals(y, null) from our abduction process. A further analysis reveals that the failure is actually due to the given specification where the precondition Pre is too weak for the program
to establish the postcondition Post: since y is not reachable from the parameters of the unknown call, no implementation of the unknown call can establish the postcondition Post
involving y. The returned formula from our verification can then be used to strengthen thegiven specification. In this case, if we add ls(y, null) into Pre via separation conjunction,
the verification will succeed with the specification (Preu = ls(x, null), Postu = ls(x, null))discovered for the procedure unknown.

23

We have also conducted some experiments to test our approach’s performance andscalability. The results are shown in Table 2.
ProgramLines of code

Time(s)Memory(Mb)Specs discovered

list.hlist.c

474

0.2

14.54

4

tasks.htasks.c

3150

11.2

17.9724

wd-stat.h wd-stat.cctrins.h ctrins.c

1404

1.232

16.66410

kr-db.hkr-db.c

1674

1.837

16.63612

krbid.h krbid.c
krpage.h krpage.c

2873

6.44

16.67611

kdbadapt.h kdbadapt.c
kdbview.h kdbview.c

3208

7.88

17.54

13

Table 2. Experimental results for performance.

These results were achieved with an Intel Core 2 Quad CPU 2.66GHz with 8Gb
memory. The verified programs are either source code from FreeRTOS [2] (list.c andtasks.c), or some working code created by the author (wd-stat.c, ctrins.c, kr-db.c,
krbid.c, krpage.c, kdbadapt.c and kdbview.c). All these programs mainly deal withpointer-based linear data structures, such as singly-linked and/or doubly-linked lists.
For example, list.c provides functions to initialize and modify lists, while tasks.ccalls those functions to manipulate several lists during runtime. The other programs,
wd-stat.c, ctrins.c, kr-db.c, krbid.c, krpage.c, kdbadapt.c and kdbview.c maintain some list-based vectors for runtime data storage, or hashtables implemented with aseries of linked lists. Meanwhile, these programs have many function calls in them, like
invocation of library functions or calls of other functions in the project.
As for verification purpose, we provide each function to be verified with its specification
and run our algorithm over it. The unknown functions are manually assigned, such as
library function calls which mainly consist of memory allocation functions like malloc,
and functions that reside in other programs of the project. Since we only consider pointersafety of linked data structures at the moment, we did some modification to the programs
to revise the code not relevant to our verification (like data types int and char for
instance), such that the programs can be successfully verified.
The experimental results suggest that our approach might be able to scale up as averification system for pointer safety, albeit we are trying to do more experiments, as well
as optimize the algorithm, to justify this. What is more, we have tested the top-downfeature of our abductive based verification system in the experiments. For instance, thespecifications gained for “unknown” functions being invoked in tasks.c cohere with theones for the corresponding callee functions in list.c. The same situation also applies toother test cases. Based on such results, we will investigate more towards this direction to
uncover the power of a top-down abductive-based system as a viable alternative to thecurrent bottom-up approaches [6, 13].

24

8.

Conclusion

It is a challenging problem to automatically verify (even pointer safety of) heapmanipulating imperative programs with unknown procedure calls. We propose a novel
approach to this problem, which infers expected specifications for unknown proceduresfrom their calling contexts during the verification process. The program is proven correct
subject to the condition that the invoked unknown procedures meet the inferred specifications. We employ a forward shape analysis with separation logic and an enhanced
abductive reasoning mechanism to synthesize both pre- and postconditions of the unknown procedure. As a proof of concept, we have also implemented a prototype system
to test the viability of the proposed approach.
There are two possible future directions. One is to explore a more general solution
for unknown calls in sequence as discussed, e.g., it might be possible for us to invent
some heuristics to strengthen the postcondition for the first unknown call, so that theprecondition of the second can be strengthened accordingly, to achieve more reasonablespecifications for both. Another direction is to extend this method to an abstract domain
combining separation and numerical information [7], so that more general properties, suchas memory safety and functional correctness, can be specified and verified. We envisage
that, with the combined domain, the abstract semantics and analysis algorithms willremain conceivably the same, but the abduction will be redefined to discover the antiframes for the newly introduced numerical features.
Acknowledgement
This work was supported in part by the EPSRC (Engineering and Physical Sciences
Research Council) projects [EP/E021948/1 and EP/G042322/1]. We thank Hongseok
Yang for his encouragement and invaluable comments and Dino Distefano for very useful
discussions. We also acknowledge the precious insights from the anonymous reviewers.
References
[1]

[2]
[3]

[4]

[5]

[6]

Glenn Ammons, Rastislav Bodik, and James R. Larus. Mining specifications. In Proc.
of 29th Principles of Programming Languages (POPL), New York, NY, USA, pages 4–16.
ACM Press, 2002.
Richard Barry. FreeRTOS Reference Manual — API Functions and Configuration Options.
Real Time Engineers Ltd, 2009.
Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. A decidable fragment of separation logic. In Proc. of Foundations of Software Technology and Theoretical Computer
Science (FSTTCS), Chennai, India, LNCS 3328, pages 97–109. Springer, December 2004.
Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. Symbolic execution with separation logic. In Proc. of 3rd Asian Symposium on Programming Languages and Systems(APLAS), Tsukuba, Japan, LNCS 3780, pages 52–68. Springer, 2005.
Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. Footprint
analysis: A shape analysis that discovers preconditions. In Proc. of 14th International
Symposium on Static Analysis (SAS), Denmark, LNCS 4634, pages 402–418. Springer,
2007.
Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. Compositional
shape analysis by means of bi-abduction. In Proc. of 36th Principles of Programming
Languages (POPL), Savannah, Georgia, USA, pages 289–300. ACM Press, January 2009.

25

[7]

Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. Automated verification of shape, size and bag properties. In Proc. of 12th International Conference on
Engineering of Complex Computer Systems (ICECCS), Auckland, New Zealand, pages
307–320. IEEE, 2007.
[8] Florin Craciun, Chenguang Luo, Guanhua He, Shengchao Qin, and Wei-Ngan Chin. Discovering specifications for unknown procedures (work in progress). In Proc. of Workshop
of Invariant Generation (WING), pages 30–44, March 2009.
[9] Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. A local shape analysis based on
separation logic. In Proc. of 12th Tools and Algorithms for the Construction and Analysis
of Systems (TACAS), Vienna, Austria, LNCS 3920, pages 287–302. Springer, 2006.
[10] Maryam Emami, Rakesh Ghiya, and Laurie J. Hendren. Context-sensitive interprocedural
points-to analysis in the presence of function pointers. In Proc. of Programming Language
Design and Implementation (PLDI), New York, NY, USA, pages 242–256. ACM Press,
1994.
[11] Roberto Giacobazzi. Abductive analysis of modular logic programs. In Proc. of the International Symposium on Logic Programming (ISLP), pages 377–391. The MIT Press,
1994.
[12] Denis Gopan and Thomas Reps. Low-level library analysis and summarization. In Proc.
of 19th Computer Aided Verification (CAV), Berlin, Germany, LNCS 4590, pages 68–81.
Springer, 2007.
[13] Bhargav S. Gulavani, Supratik Chakraborty, Ganesan Ramalingam, and Aditya V. Nori.
Bottom-up shape analysis. In Proc. of 16th International Symposium on Static Analysis(SAS), Los Angeles, CA, USA, LNCS 5673, pages 188–204. Springer, 2009.
[14] Cliff Jones, Peter W. O’Hearn, and Jim Woodcock. Verified Software: A Grand Challenge.
IEEE Computer, 39(4):93–95, April 2006.
[15] Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular specification of frame
properties in JML. In Concurrency and Computation: Practice and Experience, 15:117–154,
2003.
[16] Huu Hai Nguyen, Cristina David, Shengchao Qin, and Wei-Ngan Chin. Automated verification of shape and size properties via separation logic. In Proc. of 8th Verification, Model
Checking, and Abstract Interpretation (VMCAI), Nice, France, LNCS 4349, pages 251–266.
Springer, 2007.
[17] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis.
Springer, 2005.
[18] Peter W. O’Hearn, Hongseok Yang, and John C. Reynolds. Separation and information
hiding. In Proc. of 31st Principles of Programming Languages (POPL), Venice, Italy, pages
268–280. ACM Press, January 2004.
[19] John C. Reynolds. Separation logic: a logic for shared mutable data structures. In Proc.
of 17th IEEE Symposium on Logic in Computer Science (LICS), Copenhagen, Denmark,pages 55–74. IEEE, 2002.
[20] Roger Sessions. COM and DCOM: Microsoft’s vision for distributed objects. John Wiley& Sons, Inc., New York, NY, USA, 1998.
[21] Jim Woodcock. Verified software grand challenge. In Proc. of 14th International Symposium
on Formal Methods (FM), Hamilton, Canada, LNCS 4085, pages 617–617. Springer, 2006.
[22] Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter W. O’Hearn. Scalable shape analysis for systems code. In Proc. of 20thComputer Aided Verification (CAV), Princeton, NJ, USA, LNCS 5123, pages 385–398.
Springer, April 2008.

26