Combining Deductive Verification with Shape Analysis

Frama-C  [6] is an integrated toolbox built around a kernel offering core services and plugins dedicated to specific analysis or verification tasks for C code, e.g. value analysis, runtime assertion checking and deductive verification. Acsl (ANSI C Specification Language) [6] is the common specification language of the plugins. The Wp plugin performs modular deductive verification: each function is verified independently. It generates verification conditions (VCs) from the C code with Acsl annotations and requests their proof by the QED simplifier or by external provers.

We illustrate the main Acsl features on the running example² of Fig. 1, 3, 4, 5, presented as we go, where Acsl notation (e.g. ) is pretty-printed (resp., as \(\forall , \mathbb {Z},\Rightarrow ,\le , \wedge \)). Lines 69–85 of Fig. 4 show a contract for function (detailed below) that adds a new value into a linked list (cf. Lines 1–2 of Fig. 1), allocating a new cell. The contract includes pre-conditions ( clauses) and post-conditions ( clauses). The clause is a special kind of post-condition that indicates the memory locations the function is allowed to modify. Acsl formulas are mostly multi-sorted first-order logic where types are either C types or logic types (such as , the type of mathematical integers). Acsl provides built-in constructs such as (the value returned by the function) and predicates such as (stating that pointer refers to an allocated memory location, so that can be safely read and written) and (stating that the memory locations referred to by given pointers do not intersect). Notice that the considered memory locations are here indicated by pointers. Users can define predicates such as those in Fig. 1, adapted here from a previous work [1] on verifying linked lists in Wp.

The main predicate is the inductively defined predicate (Lines 10–19) stating that a linked list (segment) of values (defined on Lines 1–2) from pointer to pointer (excluded) is a well-formed list represented by an Acsl logical list . In other words, contains the pointers to the cells of that list segment (or the whole list if is ). Acsl lists are similar to lists in functional programming. In the inductive case ( ) overlapping list cells (or cyclic lists) are avoided by requiring that the first cell is separated from all the other cells in the list including , so the list is well-formed. The predicates on Lines 4–9 use predefined functions: and that returns the \(n^\text {th}\) element of a logic list. Predicates can take one or several program points (C labels plus some Acsl labels: and ). The built-in specifies the value of an expression at a label . Using these features, states that a logic list does not change between two program points (Lines 20–24). Finally, Lines 25–36 define an axiomatic function that constructs a logic list from a C linked list. While it would be possible to write instead of Line 72 of Figure 4, the scope of the existential quantifier is just this line. Therefore, cannot be used in the post-conditions, hence the need for .

Let us now detail the contract of (its code is detailed below). The pre-conditions state that is a valid pointer to a list (Line 70), separated from every element in the list (Line 71), and refers to a linked list verifying the inductive predicate (Line 72). Line 73 specifies that the only locations the function is allowed to modify are , the head pointer of the list, and , the first element of the list at the exit point, i.e. the freshly allocated cell. We cannot reference the new list cell at the entry point because it is not allocated yet. In post-conditions, the returned value indicates whether or not the allocation is successful (Line 76). Regardless of the success, we expect the list invariants to hold (Lines 74–75). In case the allocation fails, we expect the pointer and the list contents to be unchanged (Lines 77–79). If it succeeds, we expect the list to be composed of the new cell followed by the old list (Lines 80–81), the old list being unchanged (Lines 82–83), and the fields of the new cell, and , resp., to point to the old list (Line 84) and to contain the expected value (Line 85).

The purpose of MemCAD  [10] is to automatically infer precise invariants about programs manipulating complex data structures. It is based on shape analysis [3], a static code analysis technique that discovers and verifies properties of recursive, dynamically allocated data structures. It relies on separation logic and abstract interpretation. Unlike in Wp, the analysis is global.

To use MemCAD on linked lists defined on Lines 1–2 of Fig. 1, the user first defines an inductive predicate expressing a structural invariant of a well-formed linked list, such as predicate on Lines a–h of Fig. 2. A list, i.e. a pointer to a list cell, satisfies the predicate in two cases. Each case defines a memory separation formula and additional constraints. In the first case, the pointer is null (Line d) and no specific memory separation is required (Line c). This case has no additional arguments (cf. on Line b). The second case has two (existentially quantified) arguments: an address and an integer (Line e), denoted, resp., by and in the rest of the case. The pointer is non null and refers to a valid memory block of 8 bytes (Line h), assuming a 32-bit system. Lines f–g define the values of the fields and (at offsets 0 and 4) as and , and require separation between those fields and the rest of the list. The separation is expressed by the separating conjunction “ ” [10]. Notice that “ ” on Line f specifies separation recursively, for all list cells reached by the predicate via the inductive case. The user can insert the instruction to assume that list respects predicate , or to check the same property in MemCAD.

Predicate on Lines n–t is very close to predicate except that it only defines one list cell without recursion. Predicate on Lines j–m expresses that a double pointer to a list cell (i.e. of type ) is valid, refers to a well-formed list and is separated from its cells. Predicate is explained below.

To prove complex memory-related annotations with Wp on real-life code [11], the user typically has to manually annotate the code with many additional carefully chosen assertions establishing structural invariants and separation properties at several intermediate program points, and to add numerous lemmas to facilitate reasoning about them (whose proof must usually be done manually in Coq, an interactive proof assistant). Our approach proposes to let MemCAD deal with the structural invariants of recursive data structures and separation properties, and to admit them in Wp at some key points.

In order to use both tools simultaneously in this way, we first need to show the equivalence between MemCAD and Wp inductive predicates. For MemCAD, predicate (Lines a–h of Fig. 2) specifies that each element of the list is a valid cell, is separated from every other cell of the list and the list is null-terminated. This is equivalent to the predicate for Wp (Lines 10–19 of Fig. 1) when we consider the whole list. Indeed, when is , this predicate also means that every list cell is valid and separated from any other list cell, and the list is null-terminated. Explicit separation conditions in the Acsl predicate for Wp are expressed by the separating conjunction in the MemCAD counterpart. (Notice that separation of with on Line 15 is trivial.) The sequence of list elements, expressed by a logic list in Acsl and used to prove functional properties about the contents of the list (cf. Lines 80–81) in Wp, does not need to be specified for MemCAD, which we only use to reason about structural properties.

To check if invariants hold in MemCAD, we define check functions shown in Fig. 3. These functions are specified to be side-effect-free (cf. Lines 40, 47) to prevent interference with the proof in Wp.

The first function, (Lines 41–43), checks that respects the predicate, i.e. is a valid pointer to a well-formed list from which it is separated (Line 42, see also Lines j–m of Fig. 2).

The goal of the second function, , is to check that refers to a list cell, respects the predicate, and the corresponding pointer and the list cells are separated from the cell referred to by . To do that in MemCAD, we introduce an ad-hoc structure with both pointers (Line 45). The function initializes a local structure (Lines 49–50) and takes its address (Line 51) in order to express the required check (Line 52). This check relies on the predicate (Lines v–z of Fig. 2) stating that the given pointer is non-null and refers to a structure with two pointers at offsets 0 and 4, denoted and , referring, resp., to a cell and to a double pointer to a well-formed list, which are separated (between them and from the list cells). Notice that “ ” on Line y specifies separation recursively, that is, from all locations considered in separation constraints reached via (and hence via ).

An important benefit of using MemCAD is its capacity to automatically handle dynamic memory allocation, which is not yet supported in Wp. Thus, we define a custom allocator that simulates the behavior of for list cells on Lines 59–67 of Fig. 4. Wp uses its contract, which is simple but currently unprovable by Wp since dynamic allocation is not supported (it should become provable when this support is added into Wp).

We illustrate our approach on function of Fig. 4. It tries to allocate a new cell (Lines 87–88), and, in case of success, puts it on top of the list with the given data (Lines 93, 95, 97, 103). Lines 92, 96 define ghost labels (that is, labels used only in annotations).

Lines 89–91 show how we use MemCAD to verify that the new cell (referred to by ) is separated both from the list cells and the pointer referred to by (Line 89), and introduce these properties as assumptions for Wp ( clauses on Lines 90–91). They help Wp to prove in an clause on Line 94 that the list remains unchanged since label (i.e. Line 92) despite writing into the new cell on Line 93, and a similar assertion for the old list on Lines 98–99 despite the assignment on Line 97.

Instead of reasoning about the modified list directly in Wp—which often presents another difficulty for deductive verification—we let MemCAD check the list invariants on Line 100 and admit them on Lines 101–102 for Wp to prove the post-conditions. Thanks to those assumptions, Wp successfully proves this function. Notice that the check instruction for MemCAD and the admit instructions for Wp are placed (for the moment, manually) at the same program location to ensure the soundness of the global verification.

In order to have a full proof, we also need to run MemCAD to verify all the checks in . For this purpose, we define a wrapper in Fig. 5 to analyze the call to on Line 108 with an arbitrary list respecting the given pre-conditions (which correspond in MemCAD, as we explained above, to assuming predicate for , cf. Lines 70–72, 107). MemCAD also succeeds in its analysis, hence, we can conclude that our function respects its Acsl contract.

While the annotation step is done manually in the current work, it can be better automated in the future. A coordinated generation of checks and assumptions for a given recursive data structure for both tools will facilitate the verification and the justification of soundness of the combined approach. An early idea consists in defining a domain-specific language for the description of the target recursive data structure that is then used for the generation of necessary predicates for MemCAD and for Wp as well as necessary assumptions and checks. The investigation of this research direction is left for future work.