Automatic verification of imperative programs that destructively manipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, and trees inductively as solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications.
In this paper we show how to reason effectively about pointer programs using automatic first-order theorem provers. Common approaches to such reasoning rely on transitiveclosure to express reachability in linked data structures. However, first-order theorem provers cannot handle transitive closure accurately, because there is no finite firstorder axiomatisation. Instead, various approximations have been proposed for proving (non-)reachability in linked data structures. Yet, there is no universal scheme for approximating transitive closure — the choice of approximation depends on the data structure and on the type of (non-)reachability problem at hand.
We propose a different approach to reasoning about pointer programs. Instead of reasoning about reachability, we reason about the extension of heap data structures, i. e., about sets of heap cells. This is sufficient to express many (non-)reachability problems, e. g., “x is reachable from the head of the list”, or “the lists pointed to by x and y are separate”.
We define common data structures, including acyclic lists, cyclic lists, sorted lists, and binary trees, as logic programs. More precisely, the logic programs define shape types, i. e., monadic predicates capturing the extension (set of heap cells) of the given data structure. These logic programs, if viewed as universal first-order theories, have many models, some of which will contain junk, i. e., unreachable heap cells; see Fig 3, showing a shape type for a singly linked list containing junk. The issue of junk models can be avoided if we confine ourselves to least models, i. e., to inductive reasoning. We approximate this inductive least model reasoning by first-order verification conditions. The main contributions of this paper are the following: – We present logic programs defining a number of common shape types (Section 2).
The programs are carefully chosen to harness the power of automatic
resolutionbased theorem provers (in our case study SPASS [
2.1
We work in the framework of many-sorted first-order logic with equality, assuming familiarity with the basic syntactic and semantic concepts.
Notation. A signature Σ declares finite sets of sorts ΣS , function symbols ΣF and relation symbols ΣR. Function symbols f and relation symbols R have associated arities, usually written as R ⊆ T1 × · · · × Tm resp. f : T1 × · · · × Tn → T0 (or f : T if f is a constant). Given signatures Σ and Δ, their union ΣΔ is a signature. We call Δ an extension of Σ if Δ = ΣΔ; we call the extension relational if additionally ΔS = ΣS and ΔF = ΣF .
A Σ-algebra A interprets sorts T ∈ ΣS as carriers T A, function symbols f ∈ ΣF as functions f A, and relation symbols R ∈ ΣR as relations RA. We call B a Δextension (or simply extension) of A if Δ is an extension of Σ and B is a Δ-algebra whose Σ-reduct B|Σ is A.
First-order formulas over Σ are constructed by the usual logical connectives (including the equality predicate =). We write A, α |= φ to denote that formula φ is true in Σ-algebra A under variable assignment α; we may drop α if φ is closed. Logical model of program state. We consider programs in a subset of the programming language C. With regard to the heap, these programs may allocate and free records (structs in C terminology) on the heap, and they may dereference and update pointers to these records. However, they may not perform address arithmetic, pointer type casts, or use variant records (unions in C terminology). Under these restrictions, any given program state (i. e., heap plus values of program variables) can be viewed a manysorted Σ-algebra A in the following way. (i) The C types are viewed as sorts. There are two classes of sorts: value sorts corresponding the C base types (int, float, etc.) and pointer sorts corresponding to C record types. (ii) The elements of the carrier T A of a value sort T are the values of the C type T. A interprets the standard functions (like addition) and relations (like order) on value sorts as intended. (iii) The elements of the carrier T A of a pointer sort T are the addresses of records of the C type T in the given heap, plus the special address NULLT , which represents NULL pointers of type T. (iv) A field f of type T’ in a record of type T corresponds to a unary function symbol f : T → T ′. Its interpretation f A maps addresses in T A to elements of T ′A (i. e., to values or addresses, depending on whether T ′ is a value or pointer sort). (v) To capture the values of program variables, we extend the signature Σ with constants, one per program variable. For example, the program variable x of type T is represented by the logical constant x of sort T ; the value of x is the interpretation xA of x in A. typedef double D; struct L_Node { struct L_Node* next; struct L_Node* prev;
D data; }; typedef struct L_Node* L; // lists // data values // list nodes // tree nodes struct T_Node { struct T_Node* left; struct T_Node* right; struct T_Node* parent; D val;
Pointer sorts: L, T
NULLL : L NULLT : T next, prev : L → L data : L → D left, right, parent : T → T val : T → D }; typedef struct T_Node* T; // binary trees
≤ ⊆ D × D Logic programs. Let Σ and Δ be signatures such that ΣΔ is a relational extension of Σ. A clause (over ΣΔ) is called Δ-Horn (resp. definite Δ-Horn) if it contains at most one (resp. exactly one) positive Δ-literal. A hΣ, Δi-LP is a finite set of Δ-Horn clauses over ΣΔ.
Given a Σ-algebra A, we call a (ΣΔ)-extension B of A an A-model of P if B |= P ; we call P A-satisfiable if it has an A-model. Note that for some A, P may not be A-satisfiable (because P may contain non-definite Δ-Horn clauses). However, a standard argument (Proposition 1) shows that if P is A-satisfiable then it has a least Amodel B0 (in the sense that RB0 ⊆ RB for all R ∈ ΔR and all A-models B of P ); we denote B0 by lm(P , A). Thus, P may be viewed as a transformer taking a Σ-algebra and computing its least (ΣΔ)-extension consistent with P (if it exists). Proposition 1. Let P be a hΣ, Δi-LP and A a Σ-algebra. If P is A-satisfiable then it has a least A-model.
Shape types. Informally, a shape type is a unary predicate on the heap, characterising the collection of heap cells that form a particular data structure (e. g., a sorted list). Its purpose is twofold: It serves to enforce integrity constraints (like sortedness) on the data structure, and it provides a handle to specify invariants (like separation of two lists). 3 This is very much what a programmer does, who is also not concerned about the contents of unreachable memory locations.
In the remainder of this section, we will define a number of shape types by hΣ, ΔiLPs P , where Σ is the signature of the heap (cf. Section 2.1), which ΣΔ extends with a unary predicate S. Given a heap A, the least model lm(P , A) may be viewed as an annotated heap, tagging heap cells (as belonging to the interpretation of S) which form the data structure specified by P . We note that the existence of least models will be guaranteed by Proposition 1 because the LPs will be evidently A-satisfiable in all intended heaps A (i. e., in all A where the data structure in question is not corrupt).
shape types of various list segments (singly- or doubly-linked, sorted or not). The programs are parameterised by input and output signatures Σ and Δ (the latter declaring only the single symbol S).
The simplest LP PList defines the shape type S of unsorted singly-linked list segments. The input signature comprises the sort of list cells L, the next-pointer function, the pointer p to the head, and the pointer q to the tail of the list beyond the segment. The clauses express (in order of appearance) that (i) the first cell of the tail (pointed to by q) does not belong to S, (ii) the head of the segment belongs to S unless p points to the tail, (iii) no cell in S points to the head, (iv) S is closed under following next-pointers up to q, and (v) each cell in S is pointed to by at most one cell in S (i. e., no sharing in S). Figure 3 (top) shows two models of PList. The first one is the intended least model, where the interpretation of S really is the set of cells forming the list segment from p to q, whereas in the second model the interpretation of S contains some junk, i. e., cells that are unreachable from the head.
The LP PDList defines the shape type S of doubly-linked list segments from head cell p to last cell r (where the cells ahead of p and behind r are s and q, respectively), see the picture in Figure 3 (middle). The program defines S as both, a next-linked list segment from p to q, and a prev-linked list segment from r to s. Moreover, it demands that p belongs to S iff r does, and that p and r are the only cells in S that may point to s and q, respectively. Finally, the last two clauses force the next-pointers inside S to be converses of the prev-pointers, and vice versa.
The LP PSList defines the shape type S of sorted, singly-linked list segments. Its parameter list extends that of PList by the data sort D, the total ordering ≤ on D, and the data field. It adds one more clause to PList, for comparing the data values of adjacent elements in the list segment.
Finally, the LP PSDList combines the LPs PDList and PSList, defining the shape type S of sorted, doubly-linked list segments.
Shape types of cyclic lists. The LP PCList in Figure 2 defines the shape type S of cyclic singly-linked lists. Its input signature comprises the sort of list cells L, the nextpointer function, and the pointer p into the cyclic list. The clauses express (in order of appearance) that: (i) NULL does not belong to S, (ii) the cell pointed to by p belongs to S unless p points to NULL, (iii) S is closed under following next-pointers, and (iv) each cell in S is pointed to by at most one cell in S (i. e., no sharing in S).
The LP PCDList defines the shape type S of doubly-linked cyclic lists by extending PCList with a clause forcing next and prev inside S to be converses. We remark that the LPs for LP for singly-linked list segments PList[L; next : L → L, p, q : L; S ⊆ L] = {¬ S(q),
S(p) ∨ p = q, ∀x:L . S(p) ∧ S(x) ⇒ next(x) 6= p, ∀x:L . S(x) ∧ next(x) 6= q ⇒ S(next(x)), ∀x, y, z:L . S(x) ∧ S(y) ∧ S(z) ∧ next(x) = z ∧ next(y) = z ⇒ x = y} LP for doubly-linked list segments PDList[L; next, prev : L → L, p, q, r, s : L; S ⊆ L] = PList[L; next, p, q; S] ∪ PList[L; prev, r, s; S] ∪ {S(r) ⇒ S(p), S(p) ⇒ S(r), ∀x:L . S(x) ∧ ¬ S(prev(x)) ⇒ x = p ∧ prev(x) = s, ∀x:L . S(x) ∧ ¬ S(next(x)) ⇒ x = r ∧ next(x) = q, ∀x:L . S(x) ∧ S(next(x)) ⇒ prev(next(x)) = x, ∀y:L . S(y) ∧ S(prev(y)) ⇒ next(prev(y)) = y} LP for singly-linked sorted list segments PSList[D, L; next : L → L, data : L → D, p, q : L, ≤ ⊆ D × D; S ⊆ L] = PList[L; next, p, q; S] ∪ {∀x:L . S(x) ∧ S(next(x)) ⇒ data(x) ≤ data(next(x))} LP for doubly-linked sorted list segments PSDList[D, L; next, prev : L → L, data : L → D, p, q, r, s : L, ≤ ⊆ D × D; S ⊆ L] = PDList[L; next, prev, p, q, r, s; S] ∪ PSList[D, L; next, data, p, q, ≤; S] LP for singly-linked cyclic lists PCList[L; next : L → L, p, NULLL : L; S ⊆ L] = {¬ S(NULLL),
S(p) ∨ p = NULLL, ∀x:L . S(x) ⇒ S(next(x)), ∀x, y, z:L . S(x) ∧ S(y) ∧ S(z) ∧ next(x) = z ∧ next(y) = z ⇒ x = y} LP for doubly-linked cyclic lists PCDList[L; next, prev : L → L, p, NULLL : L; S ⊆ L] = PCList[L; next, p, NULLL; S] ∪ {∀x:L . S(x) ⇒ prev(next(x)) = x ∧ next(prev(x)) = x} LP for arrays of singly-linked NULL-terminated lists PListArray[I, L; next : L → L, a : I → L, NULLL : L; S ⊆ I × L] = {∀i:I . ¬ S(i, NULLL), ∀i:I . S(i, a(i)) ∨ a(i) = NULLL, ∀i:I ∀x:L . S(i, a(i)) ∧ S(i, x) ⇒ next(x) 6= a(i), ∀i:I ∀x:L . S(i, x) ∧ next(x) 6= NULLL ⇒ S(i, next(x)), ∀i:I ∀x, y, z:L . S(i, x) ∧ S(i, y) ∧ S(i, z) ∧ next(x) = z ∧ next(y) = z ⇒ x = y, ∀i, j:I ∀x:L . S(i, x) ∧ S(j, x) ⇒ i = j} LP for arrays of singly-linked cyclic lists PCListArray[I, L; next : L → L, a : I → L, NULLL : L; S ⊆ I × L] = {∀i:I . ¬ S(i, NULLL), ∀i:I . S(i, a(i)) ∨ a(i) = NULLL, ∀i:I ∀x:L . S(i, x) ⇒ S(i, next(x)), ∀i:I ∀x, y, z:L . S(i, x) ∧ S(i, y) ∧ S(i, z) ∧ next(x) = z ∧ next(y) = z ⇒ x = y, ∀i, j:I ∀x:L . S(i, x) ∧ S(j, x) ⇒ i = j} LP for binary trees PTree[T ; left, right : T → T, r, NULLT : T ; S ⊆ T ] = {¬ S(NULLT ),
S(r) ∨ r = NULLT , ∀x:T . S(r) ∧ S(x) ⇒ (left(x) 6= r ∧ right(x) 6= r), ∀x:T . S(x) ∧ left(x) 6= NULLT ⇒ S(left(x)), ∀x:T . S(x) ∧ right(x) 6= NULLT ⇒ S(right(x)), ∀x, y, z:T . S(x) ∧ S(y) ∧ S(z) ∧ left(x) = z ∧ left(y) = z ⇒ x = y, ∀x, y, z:T . S(x) ∧ S(y) ∧ S(z) ∧ right(x) = z ∧ right(y) = z ⇒ x = y, ∀x, y, z:T . S(x) ∧ S(y) ∧ S(z) ∧ left(x) = z ∧ right(y) = z ⇒ x = y, ∀x, y, z:T . S(x) ∧ S(y) ∧ S(z) ∧ left(x) = y ∧ right(x) = z ⇒ y 6= z} LP for binary trees with parent pointers PPTree[T ; left, right, parent : T → T, r, s, NULLT : T ; S ⊆ T ] = PTree[T ; left, right, r, NULLT ; S] ∪ {s 6= NULLT ⇒ S(r),
S(r) ⇒ s = parent(r), ¬ S(s), ∀x:T . S(x) ∧ S(left(x)) ⇒ parent(left(x)) = x, ∀x:T . S(x) ∧ S(right(x)) ⇒ parent(right(x)) = x, ∀y:T . S(y) ∧ S(parent(y)) ⇒ (left(parent(y)) = y ∨ right(parent(y)) = y)} next prev p S next next p next next
S(i) next
next next next NULL S(j) empty next next
S(k) next next r q q next next q p l
r l l r r l
r NULL
S next prev next prev next prev next prev next cyclic lists are more elegant than the corresponding LPs for singly- and doubly-linked list segments.
Shape types of arrays of lists. The LP PCListArray in Figure 2 defines the shape type S of arrays of singly-linked cyclic lists, see Figure 3 (bottom left) for a graphical depiction. The input signature comprises the array index sort I , the list cell sort L, the next-pointer function, and the function a mapping array indices to pointers into the lists. The shape type S is a binary relation between array indices and list cells. Note that we model arrays as functions from index type to element type4, ignoring array bounds. In the light of this, the shape type S may be viewed as an array of sets of list cells rather than as a binary relation.
The first four clauses of PCListArray state that for each index i, the unary relation S(i, ·) — S with fixed first argument i — is the shape type of a cyclic singly-linked list pointed to by a(i); note how these four clauses correspond to the clauses of PCList. 4 Our model assumes that arrays do not live in the heap. The last clause states that the shape types S(i, ·) and S(j, ·) must be disjoint for distinct indices i and j.
The LP PListArray defines the shape type S of arrays of singly-linked NULL-terminated lists in a similar way. Its first five clauses force each shape type S(i, ·) to be a singlylinked list segment from a(i) to NULLL, and the last clause forces disjointness of distinct shape types S(i, ·) and S(j, ·).
Shape types of binary trees. The LP PTree defines the shape type S of plain binary trees, see the picture in Figure 3 (bottom right). The input signature comprises the sort of tree nodes T , the left- and right-pointer functions and the pointer r to the root. The clauses borrow heavily from the LP PList for singly-linked list segments (with q replaced by NULLT ) and express that: (1) NULL does not belong to S, (2) the root belongs to S unless r points to NULL, (3) no node in S points to the root, (4-5) S is closed under following left- and right-pointers up to NULL, and (6-9) there is no sharing in S because each node in S is pointed to by at most one node in S (clauses 6-8) and has distinct leftand right-successors (clause 9).
The LP PPTree defines the shape type S of binary trees with parent pointers by extending PTree. The additional clauses express that (1-2) s is the parent of the root r unless r is not in S, in which case s must be NULL, (3) s does not belong to S, and (4-6) the parent-pointers are converse to the union of the left- and right-pointers. 3
We aim to verify imperative programs that manipulate dynamic data structures on the heap. Given the code of a C function plus specifications of its input and output (and possibly of loop invariants), we want to verify that the program maintains certain shape invariants, e. g., that the sorted list being updated remains a list and sorted. Notation. Given a signature Σ, we define the signature Σ′ as a copy of Σ where all functions f (except the constants NULLT ) and relations R are replaced by primed functions f ′ resp. relations R′. Given a Σ-formula φ (resp. a hΣ, Δi-LP P ), we write φ′ (resp. P ′) for the Σ-formula (resp. hΣ′, Δ′i-LP) that arises from φ (resp. P ) by replacing all functions f (except NULLT ) and relations R by f ′ and R′, respectively. 3.1
We verify C functions by checking verification conditions. To do this, we convert the code of a function into a control flow graph (CFG) and find a set of cut locations, to which we attach shape invariants. Each path between cut locations gives rise to a verification condition (VC), which claims that the path establishes the invariant at its end location, given that the invariant at the start location was assumed.
We will not elaborate on the well-known techniques for translating C code to CFGs and identifying cut locations; the reader may consult Figure 4 for an example. The figure shows the code for inserting an element e into a non-empty sorted list pointed to by p. The CFG has three cut locations l0 (the entry location) to l2 (the exit location), with four paths σ1 to σ4 between them.
(t == NULL) e−>next = t; s−>next = e;
l2 s = p; l1 t = s−>next; (e−>data >= t−>data)
s = t; t = s−>next; path formula π (t != NULL) (e−>data < t−>data) void insert(L p, L e) {
L s = p; L t = s->next; while (t != NULL) { if (e->data >= t->data) { s = t; t = s->next; } } else break; } e->next = t; s->next = e;
path State signature. Associated with a C function is a state signature Σ, the signature of the Σ-algebras serving as logical models of program state, see Section 2.1. In the following, Σ always refers to a fixed state signature.
In the example of Figure 4, Σ declares the value sort D and the pointer sort L, the constants p, e, s, t, NULLL : L, the functions data : L → D and next : L → L and the order relation ≤ ⊆ D × D.
Path formulas. A path σ through the CFG is a sequence consisting of variable assignments x = e; array updates a[i] = e; heap updates x->f = e; and conditions (c) where e is an expression (an R-value in C terminology) and c is a conditional expression.5 The translation of such paths to first-order logic is well-known and will not be detailed here; the reader is referred to Figure 4 for examples. The path formula π resulting from translation of a path σ is a (ΣΣ′)-formula, where the signatures Σ and Σ′ belong to the state at the start and end locations of σ, respectively. Two things to note. First, part of each path formula is an explicit “frame condition” stating which variables and pointer fields do not change; note the use of second-order equalities like next′ = next as short-hands for more complex first-order expressions. Second, path formulae, like the ones for paths σ3 and σ4, may start with a string of second-order ∃quantifiers to project away intermediate state; these quantifiers will always be eliminable by Skolemisation.
Shape invariants. A Δ-shape invariant is a pair hP , φi, where P is a hΣ, Δi-LP and φ is a (ΣΔ)-formula. Its purpose is to constrain the program state by the relating shape types, which are defined by the LP P , with each other or with program variables.
Shape invariants are associated with cut locations in the CFG. Figure 4 presents the shape invariants for the insert function. These shape invariants involve two shape types S and E defined by the LP P = PSList[D, L; next, data, p, NULLL, ≤; S] ∪ PList[L; next, e, NULLL, ≤; E] ∪ {∀x:L . ¬ S(x) ∨ ¬ E(x)}. I. e., S is the shape type of NULL-terminated sorted lists pointed to by p, E of NULL-terminated lists pointed to by e, and both shape types are disjoint. Note that the LP P is common to all three invariants. The shape invariant at l0, for instance, stipulates that the lists S and E are disjoint and non-empty (because they contain their heads p and e), E is of length 1 (because the next-pointer of its head e is NULL), and the data at p is less than or equal to the data at e. Note the use of set-relational expressions like S ∩ E = ∅ as short-hand for more complex first-order expressions. The shape invariant at l2 stipulates that the list S is the sum of the start lists S0 and E06 and that the program variables p and e retain their start values p0 and e0, respectively. This, together with sortedness of S, which is enforced by the LP defining S, is a statement of functional correctness of insert. Verification condition. Given a path σ from ℓ to k, let π be the path formula for σ, hP , φi the Δ-shape invariant at ℓ, and hQ, ψi the Λ-shape invariant at k. To prove correctness of σ, we must show that every execution establishes the post shape invariant hQ, ψi at the end, provided that the pre shape invariant hP , φi held at the start. This translates to the following verification condition.
∀(ΣΣ′)-algebra A : lm(P , A) |= π ∧ φ =⇒ lm(Q′, A) |= ψ′ (VC) Note that the antecedent of (VC) tacitly depends on the existence of lm(P , A), and the succedent tacitly states that the existence of lm(Q′, A) follows from the antecedent. 5 To keep the presentation simple, we ignore dynamic memory allocation and function calls.
Both could be handled: memory allocation through tracking the set of allocated heap cells, function calls through extra cut locations before and after call sites. 6 The use of subscript 0 indicates values of program variables or shape types at the initial location l0. Strictly speaking, a shape invariant is not just constraining the program state at location ℓ, but the relation between the initial state and the state at location ℓ.
The trouble with (VC) is that it requires reasoning in least models, i. e., inductive reasoning. The next section presents our methodology to rephrase the inductive condition (VC) in first-order logic. 3.2
The obvious problem with using first-order provers for reasoning about shape types is their ignorance of least models. For instance, a VC on a path σ may be invalid in firstorder logic because there is a counter model which picks the least interpretation for shape type S at the start of σ but the greatest interpretation for S at the end.
To deal with this problem, we weaken the VC by speculatively assuming a shape effect relating shape types at the start and end of σ. Often, the weakened VC becomes provable in first-order logic. However, we still have to justify the assumed shape effect. We do so by proving two further first-order VCs, which together imply that the shape effect is an inductive consequence of the LPs defining the shape types. Shape effects. Given a path σ from ℓ to k, let π be the path formula for σ, hP , φi the Δ-shape invariant at ℓ, and hQ, ψi the Λ-shape invariant at k. A shape effect for σ is a (ΣΔΣ′Λ′)-formula ε which is back-and-forth total, that is, – ∀(ΣΔΣ′)-algebra A: A |= P ∪ {π} =⇒ ∃(ΣΔΣ′Λ′)-extension B: B |= ε, and – ∀(ΣΣ′Λ′)-algebra C: C |= Q′ ∪ {π} =⇒ ∃(ΣΔΣ′Λ′)-extension D: D |= ε. The purpose of a shape effect ε is to relate the shape types at the start of path σ with those at the end. A convenient way to specify simple shape effects is to write set-relational expressions like S′ = S ⊎ E (cf. Figure 4) as short-hands for more complex quantified expressions. This style also makes it easy to check the totality requirement. For example, back-and-forth totality of the shape effect S′ = S ⊎ E for σ3 holds because (1) every (ΣΔΣ′)-algebra which interprets S and E disjointly (which is enforced by the LP P ) has a (ΣΔΣ′Λ′)-extension which interprets S′ as the sum of S and E, and (2) every (ΣΣ′Λ′)-algebra (which interprets S′) has a (ΣΔΣ′Λ′)-extension which interprets S and E disjointly such that their sum is S′. Note that in this particular case, totality is independent of the path formula π.
Notation. Given a Σ-algebra A, one may need to compare one A-model of the hΣ, ΔiLP P to another one. Logically, this can be done by fusing the two models, which requires duplicating all symbols that are not shared, i. e., all relations in Δ.
We define the signature Δˆ as a copy of Δ where all relations R are replaced by capped relations Rˆ. Given a Δ-shape invariant hP , φi, we write hPˆ, φˆi for the Δˆ-shape invariant that arises from hP , φi by replacing all relations R in Δ with Rˆ. Given a shape effect ε (as defined above) for a path σ, we write εˆ for the (ΣΔˆΣ′Λˆ′)-formula ε that arises from ε by replacing all relations R in ΔΛ with R′; note that εˆ is also a shape effect for σ. Verification conditions. Given a path σ from ℓ to k, let π be the path formula for σ, hP , φi the Δ-shape invariant at ℓ, hQ, ψi the Λ-shape invariant at k, and ε the shape effect for σ. To prove the inductive condition (VC) it suffices to prove the following three first-order conditions.
P ∪ Q′ ∪ {π, ε, φ} |= ψ′
P ∪ {π, ε, φ} |= Q′ Q′ ∪ Qˆ′ ∪ {VS∈ΛR Sˆ′ ⊆ S′, WS∈ΛR Sˆ′ 6= S′, π, ε, εˆ} |=
P ∪ Pˆ ∪ {VS∈ΔR Sˆ ⊆ S, WS∈ΔR Sˆ 6= S} (VC1) (VC2) (VC3) (VC1) and (VC2) together state preservation of shape invariants, subject to the (yet unjustified) assumption of a shape effect ε. (VC2) can be read as a model transformation: Given any model of P that satisfies the path formula and the pre shape invariant, the shape effect ε will produce models of Q′. Finally, (VC3) implies that ε preserves minimal models. It can be seen as a reverse model transformation which preserves order: Given any two models of Q′ such that both satisfy the path formula and one is strictly contained in the other, the shape effects ε and εˆ will produce two models of P such that one is strictly contained in the other.
Soundness. The following theorem proves that the conditions (VC1) – (VC3) together imply that a shape effect is an inductive consequence (i. e., entailed in the least model) of the LPs defining the shape types. Soundness of the first-order verification conditions w. r. t. to the inductive condition (VC) is an easy corollary.
Theorem 2. Let σ be a path from ℓ to k. Let π be the path formula for σ, hP , φi the Δ-shape invariant at ℓ, hQ, ψi the Λ-shape invariant at k, and ε the shape effect for σ. Assume that (VC2) and (VC3) hold. For all (ΣΣ′)-algebras A, if lm(P , A) exists and lm(P , A) |= π ∧ φ then lm(P ∪ Q′, A) exists and lm(P ∪ Q′, A) |= ε. Proof. Towards a contradiction assume there is a (ΣΣ′)-algebra A such that lm(P , A) and lm(P ∪ Q′, A) exist and lm(P , A) |= π ∧ φ, but lm(P ∪ Q′, A) 6|= ε. As ε is total, the (ΣΔΣ′)-model lm(P , A) of π extends to a (ΣΔΣ′Λ′)-model B of ε. Thus, B |= P ∪ {π, ε, φ}, which by (VC2) implies B |= Q′. Note that B is not an extension of the (ΣΣ′Λ′)-model lm(Q′, A), for if it were then B = lm(P ∪ Q′, A) and hence lm(P ∪ Q′, A) |= ε, which would contradict our assumption. Thus B|ΣΣ′Λ′ is a nonleast, hence non-minimal, A-model of Q′, which implies that B has a (ΣΔΣ′Λ′Λˆ′)extension C such that C |= Q′ ∪ Qˆ′ ∪ {VS∈ΛR Sˆ′ ⊆ S′, WS∈ΛR Sˆ′ 6= S′}. As the shape effect εˆ is total, the (ΣΣ′Λˆ′)-model C|ΣΣ′Λˆ′ of π extends to a (ΣΔˆΣ′Λˆ′)model D of εˆ. Hence, the (ΣΔΔˆΣ′Λ′Λˆ′)-algebra E, which extends both C and D, is a model of Q′ ∪ Qˆ′ ∪ {VS∈ΛR Sˆ′ ⊆ S′, WS∈ΛR Sˆ′ 6= S′, π, ε, εˆ}. By (VC3), this implies E |= P ∪ Pˆ ∪ {VS∈ΔR Sˆ ⊆ S, WS∈ΔR Sˆ 6= S}, i. e., E is an extension of a non-minimal A-model of P , contradictory to E|ΣΔΣ′ = C|ΣΔΣ′ = B|ΣΔΣ′ = lm(P , A). ⊓⊔ Corollary 3. If (VC1) – (VC3) hold then (VC) holds. 3.3
We have used our methodology to successfully verify a number of simple heapmanipulating algorithms, including the sorted list insert function from Figure 4. Other examples include functions for inserting and deleting elements into binary trees, and functions for moving elements between ring buffers organised in an array. All functions were manually annotated with shape invariants and effects. Due to lack of space, we do not report on these experiments in detail.
We have run our experiments on the theorem provers SPASS and Yices. Both provers succeeded to prove all verification conditions. The typical run-time per VC was below 10 seconds for SPASS, below 1 second for Yices. More experiments are necessary to determine whether our methodology scales to more complex code.
We remark on the somewhat surprising fact that Yices succeeded on all VCs, despite its incomplete heuristics for quantifier instantiation (which we did not assist using the trigger mechanism). We suspect that a key reason for this is our choice of defining shape types by logic programs, which to a first-order theorem prover are just universally quantified clauses; avoiding existential quantifiers seems to suit Yices well. However, we did observe cases where Yices’ instantiation heuristic was sensitive to the formulation of particular clauses (especially the no-sharing clauses for binary trees). 4
Efficient theorem provers make first-order logic attractive framework for studying reachability in mutable linked data structures. However, transitive closure, essential for properties of pointer structures presents a challenge because first-order theorem provers cannot handle transitive closure.
Various approaches for program analysis that use first-order logic have been investigated. We next discuss the most prominent.
The logic of interpreted sets and bounded quantification is used for specifying
properties of heap manipulating programs [
The use of a decidable fragment of first-order logic augmented with arithmetic on
scalar field to specify properties of data structures is studied in [
In [
Alternative approach for symbolic shape analysis [
Syntactically defined logics for shape analysis, such as local shape logic LSL [
Approaches based on three valued logic, which use over-approximation, have been
studied in [
Prominent verification approaches for analysis of data structures use parameterised
abstract domains; these analyses include parametric shape analysis [
An algebraic approach towards analysis of pointer programs in the framework of
first-order logic is presented in [
Separation logic [
In [
Alternative languages for modelling and reasoning include modal μ-calculus [
In this paper we study imperative programs with destructive update of pointer fields. We model shape types, such as linked lists, cyclic lists, and binary trees as least models of logic programs. We approximate the inductive reasoning about least models by firstorder reasoning. We demonstrate that the method is effective for simple programs. Acknowledgements. This work was funded in part by the Sixth Framework programme of the European Community under the MOBIUS project FP6-015905. This paper reflects only the authors’ views and the European Community is not liable for any use that may be made of the information contained therein.