WebAssembly backend

[romac]

reclang IR

Defines a language, 'reclang', that functions as an intermediate language between stainless trees and wasm code.

The main feature of reclang is that its structured types are extensible record, which are meant to be easily translatable both to the current memory model of wasm (linear memory) and the planned future extension of reference types.
The class stainless.wasmgen.intermediate.Lowering is responsible for the lowering to this intermediate language.

We now give an informal overview of reclang.
In the following grammars, nonterminal symbols are given in single quotes('), and terminal symbols without quotes.

The types of reclang are defined as follows:

'type' ::= Boolean | Char | Int | Long | Unit | Double | String | Array | ('type'*) => 'type' | 'id'

where id refers to the name of a record sort defined in the program.
There is no type polymorphism, including arrays, which always contain boxed values.

A record sort is defined as follows:

'sort' ::= struct 'id' ('field'*) [extends 'id']?
'field' ::= 'id' : 'type'

There is a single sort, called "anyref", that does not have a parent:

struct anyref (typeTag: Int)

anyref has a single field which represents the type tag of a given runtime value.
anyref is the root of the record hierarchy. All other records have a parent.
There is no subtyping in reclang, but there are operators which can cast one record to another, provided they are connected with the ancestor (transitive reflexive closure of parent) relation.

At runtime, a record's representation contains a list of values corresponding to the fields it defines as well as all fields that its ancestors define.
The order of fields is from the further ancestor until the current field type.

The expressions of reclang are given below:

'e' ::= error | 'id' // variable, or pointer to a named function
      | val 'id' = 'e'; 'e' | println('e')
      | 'id'('e'*) // function invocation
      | 'e'; 'e' | if ('e') 'e' else 'e' | 'e' == 'e'
      | 'intconst' | 'doubleconst' | 'charconst' | 'stingliteral'
      | true | false | ()
      | 'id'({'e' {, 'e'}*}?) // record constructor
      | 'e'.'id' // record field selector
      | 'e'({'e' {, 'e'}*}?) // higher-order application
      | 'e'.asInstanceOf['id']

      | new Array['type']('e'{, 'e'}?) // length, optional initializer
      | 'e'('e') // array select
      | 'e'('e') = 'e' // array set
      | 'e'.length // array or string length
      | 'e'.substing('e', 'e') // string operations

      | 'e' 'binop' 'e'
      | ! 'e'

'binop' ::= + | - | * | / | mod | remainder
          | < | > | <= | >= | & | "|"
          | ^ | << | >> | >>>
          | (bitvector casts)
          | "||" | && | concat

The notable typing rules are for records: a record constructor takes as arguments expressions of the types of the fields of all the ancestors of the current type.
Also, a selector is allowed with the name of a field of an ancestor.
Casts have to be between compatible record types, i.e., that are related by the ancestor relation.
An upcast is always successful.
A downcast to an incompatible type fails the program.

The only values that can have a function type in reclang are function pointers.
Functions are represented by closures, i.e., records containing a function pointer and the environment captured by the function.

Polymorphism is implemented with type erasure and boxing.
There are boxed versions of the elementary types (which are regular record types).
Boxed types are records containing one additional field named "value" of the corresponding type.

The typetag field (which is defined in anyref, therefore is present in every record) defines the type of a record value at runtime as follows:

• 0 for boxed Unit,
• 1 for boxed Boolean,
• 2 for boxed Char,
• 3 for boxed Int,
• 4 for boxed Long,
• 5 for boxed Float,
• 6 for boxed Double,
• 7 for boxed Array,
• 8 for boxed String,
• 9 for closure,

and then as many tags as are needed for record sorts that are instantiated in the program.
We differentiate between records which correspond to abstract types (cannot be instantiated, do not possess a tag) and records which correspond to constructors (can be instantiated, possess a tag).
Two record values are equal if their type tags are equal and all fields defined by their tagged type are equal.
Arrays, functions and strings are compared by reference.
All other types are compared by value.

by @manoskouk

[CLAassistant]

Thank you for your submission! We really appreciate it. Like many open source projects, we ask that you sign our Contributor License Agreement before we can accept your contribution.
_{You have signed the CLA already but the status is still pending? Let us recheck it.}