Manipulating flat memory

This guide gives an overview about manipulating flat memory data structure in ATS. The types of flat memory supported by ATS have the t@ype sort.

Flat type and size

The following built-in primitive types have the sort t@ype and are all flat: bool, char, double, int, uint, size_t and void. In addition, ATS supports flat data structure types for tuple, record, and array.

Every t@ype has an associated size information, but the size information is unknown to the ATS compiler. The static sizeof(t) function (where t is a t@ype or a viewt@ype) gives you the unique static variable of the int sort, assigned to represent the size of t. The dynamic "{t:viewt@ype} sizeof()" function (which is a template function parameterized by t@ype or viewt@ype t) gives you an integer indexed by the static variable associated with static sizeof(t). It is possible to write "sif sizeof(t) == 4 then ... else ..." or "assert {t} sizeof() == 4" to make assumption about the size of t, but in general the size of any t@ype is unknown to us.

View of memory region

Flat t@ype on its own isn't very useful. If anything, it describes just the layout of memory but doesn't tell you anything else. In particular, it doesn't tell you:

    • If we do own a piece of memory with that layout.
    • The address of the memory.
    • Whether the memory is well-aligned.
    • How the memory is allocated: from the garbage collector, malloc(), shmget()/shmat(), mmap(), or even on the stack.

In order to access flat memory, we need two pieces of information: a proof of the view "t @ l", which states that we have type t at memory location l, and a value of type "ptr l", which is a pointer pointing to memory location l.Typically, each heap allocator will also give you a linear proof of an abstract view of the sort "addr -> view" which testifies that location l:addr is allocated by that allocator. This way, the memory allocated from one heap cannot be freed to another heap.

To allocate flat data structure on stack, ATS introduces a new form of "var" binding.

Terminology

The dynamic world of ATS has three kind of terms.

    • A type (also t@ype, viewt@ype) characterizes an expression.
    • A view characterizes a linear proof term.
    • A prop characterizes a propositional proof term.

After compilation, all linear and propositional proof terms are erased, and the program is left with expressions to be evaluated at run-time when someone executes the program.

Flat array on stack is a bit different.

(TODO: unfinished)