As I explained in a blog post a couple of years ago, pointers are subjected to a strict ownership policy in SPARK. It prevents aliasing and allows for an efficient formal verification model. Of course, it comes at the cost of restrictions which might not be applicable to all usage. In particular, while ownership makes it possible to represent certain recursive data-structures, those involving cycles or sharing are de-facto forbidden. This is a choice, and not every proof tool did the same. For example, the WP plug-in of Frama-C supports pointers with arbitrary aliasing. If some information about the separation of memory cells is necessary to verify a program, then the user shall give the annotation explicitly. I have investigated modeling pointers with aliasing in SPARK as indices in a big memory array. I will present the results of my experiments in this blog post. We will see that, while such a representation is indeed possible modulo some hiding in SPARK, it can quickly become rather heavy in practice.

First of all, as pointers in SPARK are always subjected to ownership, we need to hide the access type from the analysis tool. For that, we can use a private type whose full view is annotated with SPARK_Mode => Off. Since we might want to declare pointers designating different types, I have declared this private type inside a generic package:

The functionalities are the same as basic pointers: they can be allocated, dereferenced, assigned, and deallocated. Deallocation takes a parameter of mode IN OUT, because it resets it to null, just like normal deallocation in Ada. Note that the Create subprogram, used for the allocation, is a procedure and not a function. Indeed, functions cannot have side-effects in SPARK, and we want allocations to have some global effect on the memory. To model the effects of these subprograms, I have declared a Memory object that I can use inside global contracts. I could have used an abstract state instead, but an actual object is more appropriate as it makes it possible to copy a previous value of the memory into a ghost constant to refer to it later if necessary:

Now let's consider some functional specifications. We represent the memory as a big map from addresses to objects: a pointer is valid if and only if its address, computed through an Address function, is associated with an object in the map, in which case it designates the object. This model can be used to annotate our primitives in a mostly straight-forward way. However, we can already get a taste at this stage of the annotation burden. For all procedures which update the memory, we must not only describe the effect on the modified cells, but also state that all the other cells are preserved. To make it easier, I have defined three helper functions, Writes, Allocates, and Deallocates. They take as a parameter a representation of the memory foot-print of the subprogram. For example, here is the contract of Assign. It states that no cells are either allocated or deallocated by Assign, and that all the previous mappings are preserved except for the address of P:

There is no magic behind the helper functions, they are simply defined using quantified formulas on the memory. The function Writes for example states that the mappings of all valid cells which are not in the memory foot-print are preserved. Foot-prints are represented here as a big array from addresses to a boolean value. An address is included in the foot-print if the array associates it with the value True:

Note that this representation of pointers has some draw-backs with respect to the use of normal (ownership-based) pointers, some of which can be alleviated. First, there is no way with these pointers to use SPARK to check the absence of memory leaks. As a work-around, it is probably possible to use some sort of ref-counting mechanism in the implementation of the library, but this mechanism will not be verified by SPARK. I have not tried it. Another disadvantage is the lack of a possible way to update a value in place (calling Deref and then Assign will copy the designated value twice). To alleviate this concern, I have introduced Constant_Reference and Reference functions which turn one of our pointers into an ownership pointer while observing or borrowing the whole memory. It still remains a bit more cumbersome to use than a direct update inside a visible pointer though. Finally, using a big memory object as a representation of the designated data might prevent SPARK from verifying that the program is thread safe. Indeed, if all pointers to a type are conceptually designating the same memory object, then all threads using these pointers are considered to access this object, potentially leading to a race condition. We would need some higher-level memory model to handle this case, maybe based on separation logic.

Now that we have defined a modelisation for our new pointer with aliasing, let's try to write and verify a few programs to assess their usability. We start with a very simple example, a Swap procedure. It is well known that it is not necessary to have two distinct pointers for swap to work as expected. Let's check it. First, we need to choose a type of objects and instantiate our generic to declare the pointer type. I have chosen a small record type with two fields. Swap can be defined straightforwardly from there:

We can see that I have annotated Swap with already a fair amount of specifications, especially considering its size and its complexity. The precondition states that X and Y are valid pointers in the memory. It is necessary since aliasing may result in the pointer referencing some deallocated data in one of the parameters. In the first line of the postcondition, I use Deref to state that the values designated by the pointers have indeed been swapped. The following 3 lines are here to express the frame condition of Swap: all other memory cells but the ones taken as parameters by Swap are preserved. These 3 lines would not have been needed if we were using ownership pointers, as the separation is handled in a built-in way by the tool. Still, this is not horrendous, and the SPARK analysis tool can check Swap without any issues. We can call it on the same memory cell for both parameters, which would not have been possible if we were using ownership pointers.

Let's try our modelisation on a (slightly) more complex example: a simply linked list. Linked lists can be defined using pointers with ownership too, but let's assume that we want to allow sharing between linked lists. The first issue we encounter is technical, we cannot instantiate our generic package with an incomplete type, so we cannot construct our recursive data-structure directly. This means that we need to use a class-wide type for our designated element, so we can declare a pointer before the actual designated object:

In addition, as our memory model uses the equality operator on the object type, we'd better know what it is. To this effect, we introduce a Valid_Memory predicate which states that all the objects in the memory are list cells, and not some other type derived from Object for which the "=" operator could behave unexpectedly:

As our memory could theoretically contain cycles, it seems safer to store the length of the list on the side. It makes it easy to define what it means for an address to designate a valid (acyclic) list of a given length as follows:

Now that we have defined our linked list objects, let's try to write a utility program for them. To keep it simple, I have chosen to consider an Append procedure which takes a list and inserts it at the end of another list. We don't consider the actual elements stored in the list and focus on the memory safety only. As an example, let's assume that we have three valid lists L1, L2, L3 and that we want to be able to prove that it is safe to use Append to concatenate L2 to both L1 and L3 so we get two valid lists which share a sublist:

Let's try to come up with a minimal contract for Append that would allow us to prove this kind of code. The first thing we need is to be able to say that two lists are disjoint (they do not share any memory cell). This is necessary as Append should only be called on disjoint lists if we do not want to create a cycle. To express it, we define a reachability predicate which returns True when there is a path from an address to another in the list structure. Using this predicate, we can say that two lists are disjoint if there is no cell reachable from both:

Using the above definitions, I have written the following specification for Append, which I have tried to make as simple as possible. In the precondition, I state that L1 and L2 are disjoint valid lists. In the postcondition, I need to express that L1 is still a valid list, the fact that other, disjoint lists are preserved is expressed through the frame condition: we only update memory cells reachable from L1 before the call. Finally, to be able to continue tracking the partitioning of memory after the call, I need to describe the cells which are reachable from L1 after the call. Note that I could have been more precise here, and constrain the list structure in a stronger way:

To prove the natural implementation of Append, I had to write 6 lemmas, all involving proofs by induction, which are currently out-of-reach of the automatic solvers at the backend of SPARK. Mostly, they state what happens to the validity of lists and reachability on preserved parts of the memory. Applications of the same lemmas were also necessary to prove the memory safety of the two consecutive applications of Append above. Here again, the complexity turned out to be tractable, even if definitely non-trivial. Note that an Append function on simply linked lists using regular SPARK pointers does not require any contract or ghost code to be proven correct, so the advantages of using regular pointers are obvious here. Whether they are coming from ownership or the fact that the pointers are supported in a built-in way by the tool is less clear. The need for a classwide type to construct the list would definitely disappear with built-in support, but the reachability predicate, the frame conditions, as well as some auxiliary lemmas would most probably remain, as can be seen on list examples in the Frama-C framework.

We have reached the end of this post. If you are still with me, I think that we have demonstrated that, while it is possible to define and use pointers with aliasing in SPARK, it definitely does not come for free. If you are interested, you can find the complete example in the spark testsuite.