Only validate memops when there is a memory section #107
Conversation
|
We should make this the default, as memory just causes so many problems. Haha, jk. I like this idea. On Fri, Oct 2, 2015 at 5:41 PM, Luke Wagner [email protected]
|
|
lgtm |
ml-proto/spec/eval.ml
Outdated
There was a problem hiding this comment.
Can we make this a proper runtime error instead of an assertion failure? As a rule of thumb, always assume that the evaluator can be fed unchecked code. In fact, we even do so for invoke arguments.
There was a problem hiding this comment.
As brought up in #109, I wonder if we can stop feeding the evaluator unchecked code. In that case, I think it'd be nice if our use of assert in eval specifically meant "checked earlier" and so we had a clear documented distinction between actual runtime errors and things that should never happen, assuming soundness. That is, if someone did a soundness proof, they'd prove we never hit an assert.
There was a problem hiding this comment.
... but I should probably leave that for a separate issue so it can be considered orthogonally; I'll put in the runtime error here for now.
There was a problem hiding this comment.
There was a problem hiding this comment.
That sounds good. So maybe a new Soundness exn type? Since this shouldn't ever happen, seems like it could be made more terse to raise and leave out position/string.
There was a problem hiding this comment.
There was a problem hiding this comment.
Not strong reason: just because the source info clutters a bit and while it's generally worth it because it helps us when developing, the Crashes should never happen, even when developing. That's why I liked assert. Since impl=spec (sortof), I do wonder if we need to discriminate bugs in impl and bugs in semantics.
There was a problem hiding this comment.
There was a problem hiding this comment.
I can see your point and I don't have a strong opinion on this.
lukewagner
force-pushed
the
only-allow-memops-with-mem-sec
branch
from
70ea369 to
638a543
Compare
lukewagner
force-pushed
the
only-allow-memops-with-mem-sec
branch
from
9acfe42 to
a492677
Compare
|
Merging with comments addressed. |
Only validate memops when there is a memory section
Add Python pseudocode to memory operations
Currently, the link to the instruction syntax document results in a 404. This commit updates the link to point to a instructions.rst that exists and hopefully is the correct one to link to.
Fix formatting in the spec binary section for table initializers
Sync with WebAssembly/spec branch `wasm-3.0`.
…mbly#107) This means that the memory64 proposal now only contains that tests that differe from its upstream branch which is wasm-3.0, instead of including basically all test files. See WebAssembly/wabt#2495
This PR makes it a validation error to use linear memory operations (load, store, page_size, resize_memory, memory_size) when there is no memory section declared in the module. Since it is possible to have a
(memory 0)section (which allows memory ops but doesn't require allocation), there is no loss of expressiveness for producers. Rather, this is a simple a priori way to capture the wasm producer's intent to never use linear memory that allows the impl to take advantage of this (to reduce footprint, avoid corner cases in codegen) without having to worry about a linear memory later appearing (via resize_memory or dynamic linking). This restriction could later be backwards-compatibly relaxed if necessary. The main expected use is apps using GC for all memory.