Allocation in Stack Frames

ATS supports memory allocation in the stack frame of a calling function, and it is guaranteed by the type system of ATS that memory thus allocated cannot be accessed once the calling function returns.

Storing Arrays in Stack Frames

In the following contrived example, the implemented function name_of_month_1 allocates in its stack frame a string array of size 12 that is initialized with the names of 12 months, and then returns the name of the ith month.

fn name_of_month_1 {i:int | 1 <= i; i <= 12} (i: int i): string = let
  var !p_arr with pf_arr = @[string](
    "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"
  )
in
  p_arr->[i-1]
end // end of [name_of_month_1]

The following syntax indicates that the starting address of the allocated array is stored in p_arr while the view of the array is stored in pf_arr:

  var !p_arr with pf_arr = @[string](
    "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"
  )

This allocated array is initialized with the strings representing the names of the 12 months: "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec".

A variant of the function name_of_month_1 is implemeneted as follows:

fn name_of_month_2 {i:int | 1 <= i; i < 12} (i: int i): string = let
  var !p_arr with pf_arr = @[string][12]("")
  val () = p_arr->[0] := "Jan"
  val () = p_arr->[1] := "Feb"
  val () = p_arr->[2] := "Mar"
  val () = p_arr->[3] := "Apr"
  val () = p_arr->[4] := "May"
  val () = p_arr->[5] := "Jun"
  val () = p_arr->[6] := "Jul"
  val () = p_arr->[7] := "Aug"
  val () = p_arr->[8] := "Sep"
  val () = p_arr->[9] := "Oct"
  val () = p_arr->[10] := "Nov"
  val () = p_arr->[11] := "Dec"
in
  p_arr->[i-1]
end // end of [name_of_month_2]

The following syntax means that the function name_of_month_2 allocates a string array of size 12 in its stack frame and initializes the array with the empty string:

var !p_arr with pf_arr = @[string][12]("")

The starting address and the view of the allocated array are stored in p_arr and pf_arr, respectively. If the following syntax is used:

var !p_arr with pf_arr = @[string][12]()

then the allocated array is uninitialized, that is, the view of the proof pf_arr is [string?][12] @ p_arr (instead of [string][12] @ p_arr).

Storing Closures in Stack Frames

When higher-order functions are employed in systems programming, it is often desirable to form closures in the stack frame of the calling function so as to avoid the need for memory allocation on heap.

In the following example, the implemented function print_month_name forms a closure in its stack frame, which is then passed to a higher-order function iforeach_array_ptr_clo:

fn print_month_names () = let
  var !p_arr with pf_arr = @[string](
    "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"
  )
  var !p_clo with pf_clo = @lam // this closure is allocated in the stack frame
    (pf: !unit_v | i: sizeLt 12, x: &string): void =<clo1> (if i > 0 then print ", "; print x)
  // end of [var]
  prval pf = unit_v ()
  val () = iforeach_array_ptr_clo_tsz {string} {unit_v} (pf | !p_clo, !p_arr, 12, sizeof<string>)
  prval unit_v () = pf
  val () = print_newline ()
in
  // empty
end // end of [print_month_names]

Note that the keyword @lam (instead of lam) is used here to indicate that the closure is constructed in the stack frame of the function print_month_names.

The code used for illustration is available here.