A significant achievement of ATS lies in its support for safe and flexible use of pointers. This is done in a programming paradigm that is often referred to as programming with theorem proving.
Generally speaking, stateful views are linear propositions for describing memory layouts. For instance, given a type T and a memory location L, T@L is a primitive (stateful) view stating that a value of type T is stored at L. We can also form compound views in terms of primitive views. For instance, given types T_1 and T_2 and an address L, we can form a view (T_1@L, T_2@L+sizeof(T_1)) to mean that a value of type T_1 and another value of type T_2 are stored at addresses L and L+sizeof(T_1), respectively, where sizeof(T_1) is the size of a value of type T. Given a term of some view V, we often say that the term proves the view V and thus refer to the term as a proof (of V).
There are two built-in functions ptr_get_t and ptr_set_t that are given the following types:
fun{a:t@ype} ptr_get_t : {l:addr} (a @ l >> a @ l | ptr l) -<> a
fun{a:t@ype} ptr_set_t : {l:addr} (a? @ l >> a @ l | ptr l, a) -<> void
These two functions are used to read from and write to a given pointer.
Clearly, the type of
ptr_get_t indicates that ptr_get_t requires a proof of view
T@L for some type T when reading from a pointer
L. This requirement disallows reading from a dangling pointer as
such a proof cannot be found for any dangling pointers. Similarly, the type
of ptr_set_t means that writing to a dangling pointer is also
disallowed. When reading from a pointer L with a proof of view
T@L, ptr_get_t consumes the proof and then generates a proof
of the same view (and stores it in the same variable where the orginal
proof was stored). On the other hand, when writing a value of type
T to a pointer with a proof of view T?@L, where the type
T? is for possibly uninitialized values of type T,
ptr_set_t consumes the proof and then generates a proof of the view
T@L, which simply attests to the fact that a value of type T
is stored at L after the writing is done.
As an example, we implement a (template) function swap1 as follows that swaps the contents stored at two memory locations:
fn{a:viewt@ype} swap1 {l1,l2:addr}
(pf1: !a @ l1, pf2: !a @ l2 | p1: ptr l1, p2: ptr l2): void =
let
val tmp = ptr_get_vt<a> (pf1 | p1)
in
ptr_set_vt<a> (pf1 | p1, ptr_get_vt (pf2 | p2));
ptr_set_vt<a> (pf2 | p2, tmp)
end
Note that the (linear) proofs are manipulated explicitly in the
implementation of swap1. This can be burdensome in practice. In
ATS/Anairiats, (certain) proof manipulation can also be done implicitly by
the typechecker. For instance, the following code implements a (template)
function swap2 that is equivalent to swap1:
fn{a:viewt@ype} swap2 {l1,l2:addr}
(pf1: !a @ l1, pf2: !a @ l2 | p1: ptr l1, p2: ptr l2): void =
let
val tmp = !p1
in
!p1 := !p2; !p2 := tmp
end
There is no explicit manipulation of (linear) proofs in the implementation
of swap2.
The code used for illustration is available here.