Constructor Block

ConstructorBlock ::= '(' ')' ':' '{' Assign* '}'
Assign           ::= ident '=' RHS ';'
RHS              ::= ident '.' MappingField
                   | <anything up to the terminating ';'>
MappingField     ::= 'vaddr' | 'paddr' | 'size'

The constructor block is the per-PD initialiser that runs before the PD’s first event. It binds globals declared in the imported .c / .rs file to either:

• a mapping field — mapping.vaddr, mapping.paddr, or .size — in which case the value is patched into the binary by the seL4 Microkit loader before the PD starts (via the setvar mechanism); or
• an opaque expression — anything up to the terminating ; — in which case the assignment runs at PD-init time inside the imported source’s init() function.

There is at most one constructor block per .fi file. Its leading (): borrows the empty-parameter-list shape; the parens are required even though there are no parameters yet.

Mapping-field RHS

The compiler classifies the RHS as a mapping field only when it is exactly mapping.field, with nothing between the field name and the terminating ; (whitespace excepted). The matched fields are:

Each matched assignment becomes one SDF setvar entry in the lowered output. The Microkit loader patches the named symbol in the PD’s ELF before launch.

(): {
    rbd = ring_buffer.vaddr;            // setvar "rbd" → vaddr
    tbd = ring_buffer.size;             // setvar "tbd" → size in bytes
    pa  = packet_buffer.paddr;          // setvar "pa"  → physical address
}

Opaque RHS

Any RHS that is not exactly mapping.field is recorded as an opaque blob and emitted into the PD’s runtime init code rather than as setvar. The parser consumes verbatim up to the next ;.

(): {
    tbd = ring_buffer.vaddr + (sizeof(struct rbd) * RBD_COUNT);  // opaque
    irq_ack_index = 0;                                            // opaque
}

This split exists because setvar only supports literal-substitution patching: it cannot evaluate arithmetic. Anything more elaborate than a direct field read is deferred to runtime initialisation in the imported source file.

🚧 Constructor block is being unified with the broader statement grammar and the expression grammar — see #128. Once that lands, the mapping-field / opaque distinction moves out of the AST and the constructor body becomes a plain sequence of statements.

Example

import "eth.c" as eth;

Low Mapping ring_buffer(ring_buffer_outer, "rw");
Low Mapping packet_buffer(packet_buffer_outer, "rw");

(): {
    ring_buffer_vaddr  = ring_buffer.vaddr;       // setvar
    packet_buffer_vaddr = packet_buffer.vaddr;    // setvar
    ring_buffer_paddr  = ring_buffer.paddr;       // setvar
    packet_buffer_paddr = packet_buffer.paddr;    // setvar

    rbd_count = RBD_COUNT;                         // opaque (runtime init)
}

Validation

• The mapping referenced on the left of .vaddr / .paddr / .size must exist in the same .fi file.
• .paddr is rejected if the underlying MemoryRegion was declared without an explicit physical address.
• Only one constructor block per .fi; a second (): block is a parse error.