address.wast testcase constants

[kripken]

That testcase has

    (func $bad1 (param $i i32) (i32.load offset=4294967296 (get_local $i)))

and it tests that that traps on loads of 0 and 1.

1. The offset seems odd - that isn't a 32-bit unsigned. Is it internally represented as a larger number?
2. If it's a 32-bit unsigned, shouldn't that first turn into a 0, and so there is no fault?

[binji]

https://github.com/WebAssembly/design/blob/master/AstSemantics.md#addressing mentions that the sum of address and offset is specified as being infinite precision.

[jcbeyler]

Interesting to have an infinite precision, is there a rationale behind that?

[kripken]

The sum is treated that way for offset bounds checking. But it seems silly, at least to me, to allow infinite precision integers for the offset :) e.g. would we actually ensure that the binary format can pack an i512 in there? ;) seems like it should just be a uint32 field for 32-bit pointers, uint64 for 64-bit.

[sunfishcode]

I agree. The sum is infinite precision because we don't want to worry about an offset causing an address computation to wrap around the address space and end up back in bounds. And the offset has the type of the address in the design repo so it looks like we just need to enforce that in the spec repo.

[titzer]

Technically the offset is (or should be) a 32-bit unsigned constant and the
index is a 32-bit unsigned integer, so 33 bit precision is enough :-)

Obviously, we only bounds check against (mem_size - offset), which can be
computed at compile time and no 33-bit arithmetic is done at runtime.

On Wed, Nov 4, 2015 at 7:47 PM, Dan Gohman notifications@github.com wrote:

I agree. The sum is infinite precision because we don't want to worry
about an offset causing an address computation to wrap around the address
space and end up back in bounds. And the offset has the type of the address in
the design repo
https://github.com/WebAssembly/design/blob/master/AstSemantics.md#addressing
so it looks like we just need to enforce that in the spec repo.

—
Reply to this email directly or view it on GitHub
#161 (comment).

[kripken]

Even if the VM can avoid 33-bit arithmetic at runtime, allowing 33-bit integers in the s-expression format is odd. Would we have actually have 33-bit offsets in the binary format?

[titzer]

On Sun, Nov 8, 2015 at 10:52 AM, Alon Zakai notifications@github.com
wrote:

Even if the VM can avoid 33-bit arithmetic at runtime, allowing 33-bit
integers in the s-expression format is odd. Would we have actually have
33-bit offsets in the binary format?

No, the offset is an unsigned 32-bit number as an immediate in the code
stream.

—
Reply to this email directly or view it on GitHub
#161 (comment).

[kripken]

Ok. I guess we just have a weird discrepancy between the binary and the s-expression format. I'm not sure how serious we are about the s-expression syntax and if it should match the binary or not. If not, I guess this doesn't matter.

[sunfishcode]

I think there's a misunderstanding here. The 33-bit type is only a theoretical consequence of being the minimal result type of adding two 32-bit values without overflow. It doesn't actually exist anywhere in either the text or binary formats. We just have 32-bit values. I believe the ml-proto parser is incorrectly accepting an offset constant which is outside the 32-bit unsigned range.

[lukewagner]

Agreed that the test case in the OP should be assert_invalid instead. Memory.offset is an int64 mostly just for simplicity (and lack of uint32). check.ml already rejects negative values; it'd be easy to reject values > UINT32_MAX.

[kripken]

Cool, submitted a fix and test update in #172.