[spec] Execution: conventions, runtime, instructions #467
Conversation
https://webassembly.github.io/spec/ A related pull request: WebAssembly/spec#467
document/execution/runtime.rst
Outdated
| WebAssembly computations manipulate *values* of the four basic :ref:`value types <syntax-valtype>`: :ref:`integers <syntax-int>` and :ref:`floating-point data <syntax-float>` of 32 or 64 bit width each, respectively. | ||
|
|
||
| In most places of the semantics, values of different types can occur. | ||
| In order to avoid ambiguities, values are therefor represented with an abstract syntax that makes their type explicit. |
document/execution/numerics.rst
Outdated
| .. math:: | ||
| \begin{array}{lll@{\qquad}l} | ||
| \bytes_N(i) &=& \epsilon & (N = 0 \wedge i = 0) \\ | ||
| \bytes_N(i) &=& b~\bytes_{N-8}(j) & (N \geq 8 \wedge i = 8\cdot j + b) \\ |
There was a problem hiding this comment.
Should this be i = 2^8\cdot j + b?
document/execution/instructions.rst
Outdated
| (\mbox{if} & S.\FUNCS[a] = f \\ | ||
| \wedge & f.\CODE = \{ \TYPE~x, \LOCALS~t^\ast, \BODY~\instr^\ast~\END \} \\ | ||
| \wedge & f.\MODULE.\TYPES[x] = [t_1^n] \to [t_2^m] \\ | ||
| \wedge & F = \{ \MODULE~f.\MODULE, ~\LOCALS~\val^n~(t.\CONST~0)^\ast \}) |
There was a problem hiding this comment.
Seems a bit confusing to use * here since I normally assume they are all unrelated.
There was a problem hiding this comment.
Well, this pattern of implicit "mapping" over a sequence actually occurs in many places, not just this chapter. That is, when there is a sequence x*, then a sequence (...x...)* is meant to correlate. I added an explanation to the syntactic conventions section.
There was a problem hiding this comment.
Ah, I see. The mapping normally tracks for me, but t* -> (t.const 0)* didn't as much. In my mind using another symbol would make it clearer (e.g. t^k -> (t.const 0)^k), but I'm no formalist so I don't know if that makes any sense. :-)
|
|
||
| a. Trap. | ||
|
|
||
| 12. Let :math:`a` be the :ref:`function address <syntax-funcaddr>` :math:`\X{tab}.\ELEM[i]`. |
There was a problem hiding this comment.
a is redefined here (previously defined at step 3). Maybe worth using a new letter?
|
Really nice! lgtm with a few small nits/suggestions:
|
|
@lukewagner, thanks! Addressed comments, except the hyperlinking suggestion (put on my todo list of xref clean-ups/additions) and the bounds checking. I think the bounds check is correct as is -- note that it already includes the width of the data, and reading, say, 2 bytes at address 8 in a 10 byte address space should be fine. |
|
@rossberg-chromium D'oh, you're right; I missed the data width. Btw, have you considered any way to visually separate the end of the prose notation from the beginning of the formal rules? (e.g.) They sortof run together atm. |
|
@lukewagner, yeah, I don't like that running together either, and I already tried an hline (which is the only thing markdown offers) but it made the grouping really confusing visually (rules looked as if they belonged to the next section title). Tweaking vertical spacing might be better, but markdown makes it impossible to insert less than a full empty line + paragraph space (so similar effect). But I just realised that I could play with putting the space in the formulas themselves. Are you okay with making that a todo? |
|
FWIW in the HTML spec we use |
|
@domenic, whew, dirty. :) |
Oh of course; already lgtm, just a broader question. |
Changes to interpreter will come in a follow-up patch. Fixed WebAssembly#467.
First stab at of the execution semantics. Describes conventions, runtime structures, and the semantics of instructions. Still missing: the description of the numeric operations and the instantiation/linking of modules. Various other tweaks included.
Preview at https://webassembly.github.io/spec/