Bluish Coder

The ATS programming language was designed to enable safe systems programming. This requires dealing with pointers safely. In this post I intend to go through the basics of pointer handling in ATS and how this safety is achieved.

Raw Pointers

ATS has a basic pointer type called ptr. This is a non-dependent type and is the equivalent to a void* in the C programming language. It also has a dependently typed pointer type that is indexed over an addr sort (sorts are the types of type indexes) that represents the address of the pointer. This allows the proof and type system to reason about pointer addresses. Pointer arithmetic can be done on values of these types but they can't be safely dereferenced. The following example shows some basic usage:

extern fun malloc (s: size_t): ptr = "mac#malloc"
extern fun free (p: ptr):void = "mac#free"

implement main() = let
  val a = malloc(42);
in
  print (a); print_newline();
  print (a + 1); print_newline ();
  free(a)
end

This program offers no compile time safety for dealing with the pointers. You can leave the free call out and it will compile, run and leak memory. You can use unsafe functions to dereference the pointer to retrieve and store data at that location:

staload "prelude/SATS/unsafe.sats"
staload _ = "prelude/DATS/unsafe.dats"

extern fun malloc (s: size_t): [l:addr | l > null] ptr l = "mac#malloc"
extern fun free {l:addr | l > null} (p: ptr l):void = "mac#free"

implement main() = let
  val a = malloc(sizeof<int> * 2)
in
  ptrset<int> (a, 10);
  ptrset<int> (a + sizeof<int>, 20);
  print (ptrget<int> (a)); print_newline();
  print (ptrget<int> (a + sizeof<int>)); print_newline ();
  free(a)
end

ptrset and ptrget are template functions in the unsafe module that allow storing and retrieving values using raw pointers. No safety guarantees are available and it is assumed that the pointers are valid and the pointer arithmetic is done correctly. One slight change to this example is it uses the dependently typed variant of ptr with the constraint that the index is greater than null. ptrset and ptrget are defined to take a pointer that is non null so malloc and free in this example had to be modified to use these dependent types to prove the pointer is non-null.

At Views

ATS has a concept called 'views' which is part of the proof system. Views are linear resources that exist at type checking time and are erased during compilation. They have no runtime overhead and can be used to prove aspects of a program. For pointer handling there exists a type of view commonly called an 'At View' or '@ view' because of their syntax. An at-view that represents that a type T is stored at a memory location L is written as T @ L.

An at-view is often returned when memory containing a value of a particular type is allocated. The functions to get and set this memory then take the at-view as a proof argument along with the raw pointer. This tells the type system that you have a proof that the raw pointer points to that particular type. An at-view is linear so must be destroyed. By requiring the deallocating function to consume the at-view as a proof argument it can prevent further access to that memory address. It no longer exists to be able to be passed to the get and set functions.

Using this approach will result in compile time errors if the pointer is used incorrectly. The following demonstrates the approach:

staload _ = "prelude/DATS/pointer.dats"

extern fun malloc (s: sizeof_t int): [l:agz] (int @ l | ptr l) = "mac#malloc"
extern fun free {l:agz} (pf: int @ l | p: ptr l): void = "mac#free"

implement main() = let
  val (pf | a) = malloc (sizeof<int>)          // 1
in
  ptr_set_t<int> (pf | a, 10);                 // 2
  print (ptr_get_t (pf | a)); print_newline(); // 3
  free (pf | a)                                // 4
end

In this example, malloc is changed to return a proof as well as the raw pointer. In ATS syntax proof arguments are to the left of the pipe, |, symbol while non-proof arguments are to the right. The proof here is an at-view indicating that the type int is stored at memory address l - the same memory address as the raw pointer returned. The free function is changed to take the at-view as a proof argument. It is consumed by the free call (the absence of a ! symbol as part of the argument type means it is consumed). The addresses in these definitions have been changed to be agz which is short for 'address greater than zero' and is equivalent to the [l:addr | l > null] form shown previously.

In line 1 malloc is called passing it the size of an integer. The at-view is stored in the pf variable and the raw pointer in a. In line 2 the standard prelude function ptr_set_t is used to set the value at the pointer address to 10. This requires the passing of the at-view to prove that we have an integer stored at that memory address. pf is of type int @ l where l is the same address as the index type of a. Line 3 obtains the value at that address using the prelude function ptr_get_t. Again we need the proof to get it. Line 4 calls free and consumes the proof.

This example is safer than the previous examples:

• We can't forget to call free as we would be left with the linear at-view alive and it would fail to compile.
• We can't pass any random pointer to ptr_get_t or ptr_set_t. These functions require an at-view that has the same address in it's type index as the raw pointers type index.
• We can't malloc memory less than the size of the data we are storing there. The definition of malloc declares that its initial argument is of type sizeof_t int which is an integer that is the actual value returned by sizeof int. Any other value passed would be a compile error.

Implicit at-view usage

The use of at-views, ptr_get_t and ptr_set_t tends to clutter code somewhat. ATS provides some syntax to dereference pointers that automatically look for valid at-view proofs in scope. The changes to the previous example to use this are:

implement main() = let
  val (pf | a) = malloc {int} (sizeof<int>)
in
  !a := 10;
  print (!a); print_newline();
  free (pf | a)
end

The ! operator is like the unary * operator in the C programming language. It dereferences a pointer. It requires an at-view to be in scope that has the same address as its indexed type as the pointer's indexed type. In this case the variable a uses address l which matches the int @ l type of the pf variable. := is assignment. As pf is in scope for both the assignment and the print call the code typechecks. If pf wasn't in scope the code would fail to compile.

Getting pointers to variables

The unary & operator can be used like in the C programming language to get a pointer to a variable. Given a variable containing an integer a, then &a is of type ptr. Note that this is a raw pointer which you can't derefence without an at-view in scope of type int @ l. To obtain an at-view from an existing variable on the stack you use the view@ function. The result of view@ on a variable of type T is an at-view of type T @ l where l is the memory address of the variable.

The following code has an add_one function that increments an integer by one given a pointer to it. The body of main has an integer, a, on the stack and view@ is used to obtain the at-view allowing dereferencing a pointer to it:

fn add_one {l:agz} (pf: !int @ l | p: ptr l): void = 
  ! p := !p + 1

implement main() = let
  var a: int = 0
in
  print (a); print_newline();
  add_one (view@ a | &a);
  print (a); print_newline();
end

Pairs

One of the earlier raw pointer examples in this post allocated a memory area containing two integers and used pointer arithmetic to access the second integer offset from the original pointer. So far the at-view usage examples here have only used single values stored at a memory address. To access consecutive memory locations we can use arrays. ATS doesn't have arrays built into the language, rather they are implemented using views, at-views and pointers.

To demonstrate how this is implemented we'll construct a simple example of rolling our own types to safely access memory containing two integers. Then I'll show how to use the standard prelude array handling for the same problem and hopefully that will give an idea of how things work under the covers.

If we have a memory area containing two integers that we need to access individually we will need at-views for both memory locations containing the integers. We could write a function that takes both at-views individually:

extern fun malloc (n: size_t (sizeof(int)*2)):
            [l:agz] (int @ l, int @ (l+sizeof(int)) | ptr l) = "mac#malloc"
extern fun free {l:agz} (pf1: int @ l, pf2: int @ (l+sizeof(int)) | p: ptr l):void = "mac#free"

fn set {l:agz} (pf1: !int @ l, pf2: !int @ (l+sizeof(int)) | p: ptr l): void = begin
  !p := 10;
  !(p+sizeof<int>) := 20
end

implement main() = let
  val (pf1, pf2 | a) = malloc(sizeof<int> * 2)
in
  set (pf1, pf2 | a);
  print (!a); print_newline();
  print (!(a+sizeof<int>)); print_newline ();
  free(pf1, pf2 | a)
end

In this example, malloc is defined to allocate a memory area containing two integers. It restricts the number of bytes it receives as an argument to match exactly that of the size of two integers. It returns a pointer and two at-views as proofs. The first being an int @ l and the second being an int @ (l+sizeof(int)). This provides a caller of malloc with at-views allowing access to the integers that can be stored in the returned memory.

The function set requires these two proofs so it can set the value of both integers in the memory area. The first is done via a simple dereference of the pointer, p. The second adds sizeof<int> to that pointer and dereferences it to set the value. This succeeds because there is a proof in scope (the pf2 at-view) that is for the correct type, int and the memory address of the value being set. A mistake in the pointer arithmetic would result in a compile error.

Passing multiple proofs around like this is a chore. To make it easier we can wrap them in a dataview. A dataview is like a datatype but creates a linear datastructure used in proofs. This is the same example with the at-views wrapped in a dataview:

dataview pair_v (l:addr) = PAIR (l) of (int @ l, int @ (l + sizeof(int)))

extern fun malloc (n: size_t (sizeof(int)*2)): [l:agz] (pair_v l | ptr l) = "mac#malloc"
extern fun free {l:agz} (pf: pair_v l | p: ptr l):void = "mac#free"

fn set {l:agz} (pf: !pair_v l | p: ptr l): void = let
  prval PAIR (pf1, pf2) = pf
in
  !p := 10;
  !(p+sizeof<int>) := 20;
  pf := PAIR (pf1, pf2)
end

fn show {l:agz} (pf: !pair_v l | p: ptr l): void = let
  prval PAIR (pf1, pf2) = pf
in
  print (!p); print_newline();
  print (!(p+sizeof<int>)); print_newline ();
  pf := PAIR (pf1, pf2)
end

implement main() = let
  val (pf | a) = malloc(sizeof<int> * 2)
in
  set (pf | a);
  show (pf | a);
  free(pf | a)
end

The pair_v dataview has a single constructor, PAIR, that takes two at-views as arguments, one for each integer held in the pair. malloc now returns a pair_v and free consumes it. For set to be able to dereference the pointer it needs to have the at-views in scope, not bundled in the pair_v instance. To get them in scope it uses pattern matching on the PAIR constructor to obtain the two proofs and have them in scope. As a dataview is a linear type this will consume the pair_v. This is why at the end of the scope the PAIR constructor is used to create the pair_v again and reassign it to the pf proof variable.

This proof unpacking and repacking is a common idiom for dealing with at-views and other proofs that need to be in scope. These are type level operations and are erased at compile time so contain no run time overhead.

The show function does the same to access the proofs to enable it to print the values at the memory address. It's also possible to use proof functions to further encapsulate access to the pointers.

A nice feature of the use of at-views is you can have an array of memory containing lots of values but when you pass pointers to functions requiring only portions of this array you can give it a specific at-view or proof for only the area it needs to manage. The function cannot access any other part of the array since it does not have a proof for it. For example:

dataview pair_v (l:addr) = PAIR (l) of (int @ l, int @ (l + sizeof(int)))

extern fun malloc (n: size_t (sizeof(int)*2)): [l:agz] (pair_v l | ptr l) = "mac#malloc"
extern fun free {l:agz} (pf: pair_v l | p: ptr l):void = "mac#free"

fn set1 {l:agz} (pf: !int @ l | p: ptr l): void = 
  !p := 10;

fn show1 {l:agz} (pf: !int @ l | p: ptr l): void = 
  (print (!p); print_newline())

implement main() = let
  val (pf | a) = malloc(sizeof<int> * 2)
  prval PAIR (pf1, pf2) = pf
in
  set1 (pf1 | a);
  show1 (pf1 | a);
  pf := PAIR (pf1, pf2);
  free(pf | a)
end

Although set1 and show1 here get a pointer to the memory address containing two integers they can only access the single integer at the pointer it is given. This is because the at-view it takes only is for int @ l. To access the integer following this it would need to somehow obtain the at-view for it and it cannot.

Arrays

The ATS prelude has an array_v view for dealing with arrays that are a memory area containing consecutive elements of the same type. The dataview definition looks like (it is actually not defined like this, but operates the same as if it was):

dataview array_v ( a:viewt@ype+, int, addr) =
  | {n:int | n >= 0} {l:addr}
    array_v_cons (a, n+1, l) of (a @ l, array_v (a, n, l+sizeof a))
  | {l:addr} array_v_nil (a, 0, l)

An array_v has three type indexes. They are the type of the item in the array, the number of items in the array, and the address of the first element. It has two constructors. array_v_nil is an empty array. array_v_cons has two arguments, the first being the at-view for the first item and the second being an array_v of the rest of the array. This is the previous pair example using array_v instead:

staload "prelude/SATS/array.sats"

extern fun malloc (n: size_t (sizeof(int)*2)): [l:agz] (array_v (int, 2, l) | ptr l) = "mac#malloc"
extern fun free {l:agz} (pf: array_v (int, 2, l) | p: ptr l):void = "mac#free"

fn set1 {l:agz} (pf: !int @ l | p: ptr l): void = 
  !p := 10;

fn show1 {l:agz} (pf: !int @ l | p: ptr l): void = 
  (print (!p); print_newline())

implement main() = let
  val (pf | a) = malloc(sizeof<int> * 2)
  prval (pf1, pf2) = array_v_uncons (pf)
in
  set1 (pf1 | a);
  show1 (pf1 | a);
  pf := array_v_cons (pf1, pf2);
  free(pf | a)
end

There are various other operations for dealing with packing and unpacking the at-views from the array_v view in prelude/SATS/array.sats. Due to the list like nature of the array_v definition it's easy to write recursive routines that walk through the array providing only access to the single item currently being operated on.

Initialized vs uninitialized memory

When using pointers you often have to deal with a pointer to memory that has not yet been initialized. This is common when first allocating the memory. ATS differentiates unitialized memory from initialized by appending a ? to the type. For example, an int? is a integer that has not been initialized. A int? @ l is an at-view for an uninitialized integer at memory address l. When the variable is initialized the type changes to drop the ?.

This is useful for defining functions that must have valid data. The following will fail to compile because the show1 function requires the memory to first have been set:

extern fun malloc (n: sizeof_t int): [l:agz] (int? @ l | ptr l) = "mac#malloc"
extern fun free {l:agz} (pf: int? @ l | p: ptr l):void = "mac#free"

fn set1 {l:agz} (pf: !int? @ l >> int @ l | p: ptr l): void = 
  !p := 10;

fn show1 {l:agz} (pf: !int @ l | p: ptr l): void = 
  (print (!p); print_newline())

implement main() = let
  val (pf | a) = malloc(sizeof<int>)
in
//  set1 (pf | a);
  show1 (pf | a);
  free(pf | a)
end

Uncommenting the set1 call enables it to compile. The set1 definition declares that it requires an at-view for an uninitialized int and after calling the at-view becomes one for an initialized int. The syntax T1 >> T2 means that on calling a T1 is required but after calling it becomes a T2.

Conclusion

ATS provides access to pointers at the level of the C programming language but provides a type system, combined with proofs, that enable using this memory safely. This comes with no runtime overhead. There are many other ways of structuring memory access using ATS, beyond the simple examples here. ATS allows memory allocation on the stack, which is reclaimed when the stack frame exits, and prevents access to the memory after it is reclaimed, optional garbage collection, and other features which I haven't gone through.

Some pointers to futher reading on this subject, and which helped with the writing of this post, are:

• Views for Memory Access through Pointers
• Linear Arrays
• Proof Functions for View Changes
• Sane Programming with Pointers through Stateful Views