WebAssembly / function-references

Proposal for Typed Function References
https://webassembly.github.io/function-references/
Other
101 stars 15 forks source link

Initialization of non-defaultable locals #117

Closed verbessern closed 2 months ago

verbessern commented 2 months ago

Greetings, in the current overview, I see the note "Extending block types with index sets to allow initialization status to last beyond a block's end is a possible extension."

Is it planned to address this note before the next phase, like to upgrade the validation algorithm to handle blocks? Is that at all possible, how it can be validated if, for an example, an exception occurs before the local.set instruction?

I would like to note that the validation algorithm (get_local, set_local), does require, all locals (including the defaultable) to be initialized, but the wording states that only the non-defaultable ones.

rossberg commented 2 months ago

This proposal has already moved to phase 4, so no further changes are intended.

The mentioned extension would be fairly straightforward as a future proposal. We simply have to check for every branch instruction that the initialisation status declared for the target label is subsumed by the status at the branch site.

For exceptions the only interesting case is try_table, since there is no other way to observe an exception. There, the initialisation status for each catch target label has to be subsumed by the status at the try_table's entry point already. Possible additional initialisations inside the try block are not taken into account, because an exception can be raised at any point inside the block.

As for your last comment, can you point to the exact place? But note that initialisation includes implicit initialisation for defaultable locals, so that shouldn't be a contradiction.

verbessern commented 2 months ago

Possible additional initialisations inside the try block are not taken into account, because an exception can be raised at any point inside the block

That is what I had imagined and it seems to have no workaround, I would assume that then it is a feature.

As for the implicit initialization, that I have missed. Thank you for the clarification.

rossberg commented 2 months ago

it seems to have no workaround

It would require a full-blown effect system.

verbessern commented 2 months ago

When I think again about it, it could be that the try_table and each catch must all set the local's value, so to be known as 'set' after the try_table, in basically the same way the if-else-end, with a conjunction.

rossberg commented 2 months ago

Try_table's catch clauses only consist of labels to jump to, so they cannot set any local.