Compilation optimization idea: allocate varargs-style trailing sequence argument on the stack

Writing down some thoughts as I push this idea out of scope for #2390, to come back to later.

So far I've been able to implement the seq<T> type in native Dafny code, including optimized concatenation and slicing, based on a native implementation of a single-dimensional NativeArray<T> trait. It is very tempting to use this same technique to implement multi-dimensional arrays on top of NativeArray<T> as well, something like the following:

module {:options "/functionSyntax:4"} Dafny {

  trait NativeArray<T> {
    function Length(): nat
    function Select(i: nat): (ret: T)
  }

  class MultiDimensionalArray<T> {

    const storage: NativeArray<T>
    const dims: NativeArray<int>

    constructor(storage: NativeArray<T>, dims: NativeArray<int>) {
      this.storage := storage;
      this.dims := dims;
    }

    method Read(indices: seq<nat>) returns (t: T)
      requires |indices| == dims.Length()
      requires forall i | 0 <= i < |indices| :: indices[i] < dims.Select(i)
    {
      var storageIndex: nat := 0;
      var size: nat := 1;
      for d := dims.Length() - 1 downto 0 {
        storageIndex := storageIndex + size * indices[d];
        size := size * dims.Select(d);
      }
      return storage.Select(storageIndex);
    }

    // ...
  }
}

This is appealing for the same reasons as implementing seq<T> in Dafny: the added assurance of verification, saving implementation effort per target language, and ensuring consistent runtime performance across backends. The last point is particularly applicable here: some backends allocate nested arrays instead of a single flat array, which is equally correct and simpler logic, but incurs a lot more allocations and memory traversals.

The reason we should NOT do this yet is that allocating the indices sequence value for every access will be relatively expensive with the current set of backends. The manual implementations of multi-dimensional arrays in Go avoids this by using varargs, so the equivalent Read method in DafnyRuntime.go accepts a ixs ...int parameter.

The best solution I can see is to find opportunities to compile a trailing sequence parameter to a varargs parameter where supported, and optimize calls to such methods that pass a sequence display literal. Another alternative is to generate multiple copies of such methods for low arities and unroll loops, which is essentially what the Java compiler does by generating multiple Array*<T> classes.

dafny-lang / dafny

Compilation optimization idea: allocate varargs-style trailing sequence argument on the stack #2749