I joined the SPARK team during the big revamp leading to the SPARK 2014 version of the proof technology. Our aim was to include in SPARK all features of Ada 2012 that did not specifically cause problems for the formal verification process. Since that time, I have always noticed the same introduction to the SPARK 2014 language: a subset of Ada, excluding features not easily amenable to formal analysis. Following this sentence was a list of (more notable) excluded features. Over the years, this list of features has started to shrink, as (restricted) support for object oriented programming, tasking and others were added to the language. Up until now, the most notable feature that was still missing, to my sense, was pointer support (or support for access types as they are called in Ada). I always thought that this was a feature we were never going to include. Indeed, absence of aliasing is a key assumption of the SPARK analysis, and removing it would induce so much additional annotation burden for users, that it would make the tool hardly usable. This was what I believed, and this was what we kept explaining to users, who were regretting the absence of an often used feature of the language.

I think it was work on the ParaSail language, and the emergence of the Rust language, that first made us look again into supporting this feature. Pointer ownership models did not appear explicitly within Rust, but Rust made the restrictions associated with them look tractable, and maybe even desirable from a safety point of view. So what is pointer ownership? Basically, the idea is that an object designated by a pointer always has a single owner, which retains the right to either modify it, or (exclusive or) share it with others in a read-only way. Said otherwise, we always have either several copies of the pointer which allow only reading, or only a single copy of the pointer that allows modification. So we have pointers, but in a way that allows us to ignore potential aliases… What a perfect fit for SPARK! So we began to look into how ownership rules were enforced in Rust and ParaSail, and how we could adapt some of them for Ada without introducing too many special cases and new annotations. In this post, I will show you what we came up with. Don’t hesitate to comment and tell us what you like / don’t like about this feature.

The main idea used to enforce single ownership for pointers is the move semantics of assignments. When a pointer is copied through an assignment statement, the ownership of the pointer is transferred to the left hand side of the assignment. As a result, the right hand side loses the ownership of the object, and therefore loses the right to access it, both for writing and reading. On the example below, the assignment from X to Y causes X to lose ownership on the value it references. As a result, the last assertion, which reads the value of X, is illegal in SPARK, leading to an error message from GNATprove:

test.adb:9:20: insufficient permission on dereference from "X"
test.adb:9:20: object was moved at line 6

In this example, we can see the point of these ownership rules. To correctly reason about the semantics of a program, SPARK needs to know, when a change is made, what are the objects that are potentially impacted. Because it assumes that there can be no aliasing (at least no aliasing of mutable data), the tool can easily determine what are the parts of the environment that are updated by a statement, be it a simple assignment, or for example a procedure call. If we were to break this assumption, we would need to either assume the worst (that all references can be aliases of each other) or require the user to explicitly annotate subprograms to describe which references can be aliased and which cannot. In our example, SPARK can deduce that an assignment to Y cannot impact X. This is only correct because of ownership rules that prevent us from accessing the value of X after the update of Y.

Note that a variable which has been moved is not necessarily lost for the rest of the program. Indeed, it is possible to assign it again, restoring ownership. For example, here is a piece of code that swaps the pointers X and Y:

This code is accepted by the SPARK tool. Intuitively, we can see that writing at top-level into X after it has been moved is OK, since it will not modify the actual owner of the moved value (here Tmp). However, writing in X.all is forbidden, as it would affect Tmp (don’t hesitate to look at the SPARK Reference Manual if you are interested in the formal rules of the move semantics). For example, the following variant is rejected:

insufficient permission on dereference from "X"
object was moved at line 2

Moving is not the only way to transfer ownership. It is also possible to borrow the ownership of (a part of) an object for a period of time. When the borrower disappears, the borrowed object regains the ownership, and is accessible again. It is what happens for example for mutable parameters of a subprogram when the subprogram is called. The ownership of the actual parameter is transferred to the formal parameter for the duration of the call, and should be returned when the subprogram terminates. In particular, this disallows procedures that move some of their parameters away, as in the following example:

insufficient permission for "Y" when returning from "Move"
object was moved at line 3

Note that I used a record type for the type of the parameters. Indeed, SPARK RM has a special wording for in out parameters of an access type, stating that they are not borrowed but moved on entry and on exit of the subprogram. This allows us to move in out access parameters, which otherwise would be forbidden, as borrowed top-level access objects cannot be moved.

The SPARK RM also allows declaring local borrowers in a nested scope by using an anonymous access type:

But this is not supported yet by the proof tool, as it raises the complex issue of tracking modifications of X that were done through Y during its lifetime:

local borrower of an access object is not yet supported

It is also possible to share a single reference between several readers. This mechanism is called observing. When a variable is observed, both the observed object and the observer retain the right to read the object, but none can modify it. As for borrowing, when the observer disappears, the observed object regains the permissions it had before (read-write or read-only). Here is an example. We have a list L, defined as a recursive pointer-based data structure in the usual way.  We then observe its tail by introducing a local observer N using an anonymous access to constant type. We then do it again to observe the tail of N:

We can see that the three variables retain the right to read their content. But it is OK as none of them is allowed to update it. When no more observers exist, it is again possible to modify L.

In addition to single ownership, SPARK restricts the use of access types in several ways. The most notable one is that SPARK does not allow general access types. The reason is that we did not want to deal with accesses to variables defined on the stack and accessibility levels. Also, access types cannot be stored in subcomponents of tagged types, to avoid having access types hidden in record extensions.

To get convinced that the rules enforced by SPARK still allow common use cases, I think the best is to look at an example.

A common use case for pointers in Ada is to store indefinite types inside data-structures. Indefinite types are types whose subtype is not known statically. It is the case for example for unconstrained arrays. Since the size of an indefinite type is not known statically, it is not possible to store it inside a data-structure, such as another array, or a record. For example, as strings are arrays, it is not possible to create an array that can hold strings of arbitrary length in Ada. The usual work-around consists in adding an indirection via the use of pointers, storing pointers to indefinite elements inside the data structure. Here is an example of how this can now be done in SPARK, for a minimal implementation of a dictionary. A simple vision of a dictionary is an array of strings. Since strings are indefinite, I need to define an access type to be allowed to store them inside an array:

We can then search for a word in a dictionary. The function below is successfully verified in SPARK. In particular, SPARK is able to verify that no null pointer dereference may happen, due to Word being an access type with null exclusion:

Now imagine that I want to modify one of the words stored in my dictionary. The words may not have the same length, so I need to replace the pointer in the array. For example:

But this is not great, as now I have a memory leak. Indeed, the value previously stored in My_Dictionary is no longer accessible and it has not been deallocated. The SPARK tool does not currently complain about this problem, even though the SPARK definition says it should (it has not been implemented yet). But let’s try to correct our code nevertheless by storing the value previously in dictionary in a temporary and deallocating it afterward. First I need a deallocation function. In Ada, they can be obtained by instantiating the generic procedure Ada.Unchecked_Deallocation with the appropriate types (note that as access objects are set to null after deallocation, I had to introduce a base type for Word without the null exclusion constraint):

Then, I can try to do the replacement:

Unfortunately this does not work, the SPARK tool complains with:

test.adb:36:37: insufficient permission on dereference from "My_Dictionary"
test.adb:36:37: object was moved at line 3

Where line 31 is the line where Temp is defined and 36 is the assertion. So, what is happening? In fact, this is due to the way checking of single ownership is done in SPARK. As the analysis used for this verification is not value dependent, when a cell of an array is moved, the tool is never able to determine whether or not ownership to an array cell has been regained. As a result, if an element of an array is moved away, the array will never become readable again unless it is assigned as a whole. Better to avoid moving elements of an array in these conditions, right? So what can we do? If we cannot move, what about borrowing... Let us try with an auxiliary Swap procedure:

Now everything is fine. The ownership on My_Dictionary (1) is temporarily transferred to the X formal parameter of Swap for the duration of the call, and it is restored at the end. Now the SPARK tool can ensure that My_Dictionary indeed has the full ownership of its content after the call, and the read inside the assertion succeeds. This small example is also verified by the SPARK tool.

I hope this post gave you a taste of what it would be like to program using pointers in SPARK. If you now feel like using them, a preview is available in the community 2019 edition of GNAT+SPARK. Don’t hesitate to come back to us with your findings, either on GitHub or by email.