Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[js-api] Fix up missing preconditions on allocations #1793

Merged
merged 2 commits into from
Oct 7, 2024
Merged

[js-api] Fix up missing preconditions on allocations #1793

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
74c1ab9
Fix up missing preconditions on allocations
bvisness Aug 27, 2024
5ddf187
Link limits, add note about infallible checks in table limits
bvisness Aug 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 12 additions & 5 deletions document/js-api/index.bs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df
url: valid/modules.html#valid-module
text: valid
text: WebAssembly module validation
text: valid limits; url: valid/types.html#valid-limits
text: valid memtype; url: valid/types.html#valid-memtype
text: valid tabletype; url: valid/types.html#valid-tabletype
text: module grammar; url: binary/modules.html#binary-module
text: custom section; url: binary/modules.html#custom-section
text: customsec; url: binary/modules.html#binary-customsec
Expand Down Expand Up @@ -98,9 +101,11 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df
text: global_write; url: appendix/embedding.html#embed-global-write
text: error; url: appendix/embedding.html#embed-error
text: store; url: exec/runtime.html#syntax-store
text: limits; url: syntax/types.html#syntax-limits
text: table type; url: syntax/types.html#syntax-tabletype
text: table address; url: exec/runtime.html#syntax-tableaddr
text: function address; url: exec/runtime.html#syntax-funcaddr
text: memory type; url: syntax/types.html#syntax-memtype
text: memory address; url: exec/runtime.html#syntax-memaddr
text: global address; url: exec/runtime.html#syntax-globaladdr
text: extern address; url: exec/runtime.html#syntax-externaddr
Expand Down Expand Up @@ -658,8 +663,8 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
The <dfn constructor for="Memory">Memory(|descriptor|)</dfn> constructor, when invoked, performs the following steps:
1. Let |initial| be |descriptor|["initial"].
1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be |descriptor|["maximum"]; otherwise, let |maximum| be empty.
1. If |maximum| is not empty and |maximum| &lt; |initial|, throw a {{RangeError}} exception.
1. Let |memtype| be { min |initial|, max |maximum| }.
1. Let |memtype| be the [=memory type=] { <b>[=limits|min=]</b> |initial|, <b>[=limits|max=]</b> |maximum| }.
1. If |memtype| is not [=valid memtype|valid=], throw a {{RangeError}} exception.
1. Let |store| be the [=surrounding agent=]'s [=associated store=].
1. Let (|store|, |memaddr|) be [=mem_alloc=](|store|, |memtype|). If allocation fails, throw a {{RangeError}} exception.
1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
Expand Down Expand Up @@ -819,14 +824,16 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address
1. [=Throw=] a {{TypeError}} exception.
1. Let |initial| be |descriptor|["initial"].
1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be |descriptor|["maximum"]; otherwise, let |maximum| be empty.
1. If |maximum| is not empty and |maximum| &lt; |initial|, throw a {{RangeError}} exception.
1. Let |type| be the [=table type=] { <b>[=limits|min=]</b> |initial|, <b>[=limits|max=]</b> |maximum| } |elementType|.
1. If |type| is not [=valid tabletype|valid=], throw a {{RangeError}} exception.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since IDL already enforces most of this, I would prefer keeping the existing check, and adding an "Assert: type is valid" line after it

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The IDL cannot enforce semantic well-formedness of Wasm types, which is what's needed here.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand your comment

Copy link
Member

@rossberg rossberg Aug 28, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not every syntactically expressible table/memory (or other) type is actually legal. Hence, the Wasm semantics has to validate types themselves, pretty much the same way it validates instructions. Where the JS API allows expressing types in JS, it must hence validate them according to Wasm rules before using them.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I quite understand which semantic issues @rossberg is referring to, but I guess to me it seems like it comes down to whether [EnforceRange] unsigned long is equivalent enough to wasm's u32. To me they do seem generally equivalent enough to not cause problems. After all, n <= k, n <= m, and m <= k should all evaluate exactly the same whether you operate semantically on EnforceRange'd JS numbers or on u32.

Still, to me it feels more natural to leverage the wasm spec's notion of validity here instead of duplicating the checks in the JS API. For one, wasm engines already have validation code around, and for another, calling out to the wasm spec is more "future-proof" in that updates to validation in the core spec will be implicitly reflected in the JS API spec. (This is especially on my mind as I work to finalize the spec for memory64.)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

More concretely, given the current state of the core spec, what possible way could there be for table type created from u32 values min and max, with min <= max, and reftype either funcref or externref, to fail to be valid?

I could understand an argument about the robustness to potential changes in the core spec (though the assertion I suggest would cover that fine). I just don't understand your suggestion that the current rules are impossible to verify from "the outside".

As an alternative, I'd at least add a note that the 0 <= n < 2 ** 32 checks cannot fail due to the conversion in the IDL layer.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While, for this moment, type validity still is relatively simple (here: proper ordering of limits, and checking the upper limit of memtypes is ≤2^16), that changes with function references or GC types, which are already included on the staging wasm-3.0 branch, and with whom it involves a recursive algorithm.

It's also a question of spec modularity and hygiene not to duplicate definitions that are "owned" by other parts of a spec if possible. That just risks incoherence and possible hick-ups. An assertion does not magically cover mistakes in such a case — rather, an assertion that doesn't actually hold is a spec bug in itself.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Alright, let's just stick with the note about the integer limits, then


Note: Because tables may have up to 2<sup>32</sup> - 1 elements in validation, the checks for [=limits|min=] ≤ 2<sup>32</sup> - 1 and [=limits|max=] ≤ 2<sup>32</sup> - 1 in [=valid limits|limits validation=] cannot fail.
1. If |value| is missing,
1. Let |ref| be [=DefaultValue=](|elementType|).
1. Otherwise,
1. Let |ref| be [=?=] [=ToWebAssemblyValue=](|value|, |elementType|).
1. Let |type| be the [=table type=] {[=table type|min=] |initial|, [=table type|max=] |maximum|} |elementType|.
1. Let |store| be the [=surrounding agent=]'s [=associated store=].
1. Let (|store|, |tableaddr|) be [=table_alloc=](|store|, |type|, |ref|). <!-- TODO(littledan): Report allocation failure https://github.com/WebAssembly/spec/issues/584 -->
1. Let (|store|, |tableaddr|) be [=table_alloc=](|store|, |type|, |ref|). If allocation fails, throw a {{RangeError}} exception.
1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
1. [=initialize a table object|Initialize=] **this** from |tableaddr|.
</div>
Expand Down
Loading