Stream: general

Topic: #56292


gnzlbg (Nov 28 2018 at 19:52, on Zulip):

@centril what isn't clear about https://github.com/rust-lang/rust/issues/56292#issuecomment-442561265 ?
WASM does not have signed or unsigned integers, it just has bag of bits that are integers

gnzlbg (Nov 28 2018 at 19:53, on Zulip):

@Dan Gohman explained here https://github.com/rust-lang/rust/issues/56292#issuecomment-442561265 that WASM checks for overflow using gt_u, which means that this check interprets the bits as an unsigned integer

RalfJ (Nov 28 2018 at 19:53, on Zulip):

it has signed and unsigned integer operations (for those where it makes a difference)

centril (Nov 28 2018 at 19:53, on Zulip):

@gnzlbg the operational semantics of WASM does not state whether delta < 0 is permitted or not

gnzlbg (Nov 28 2018 at 19:54, on Zulip):

If wasm interprets delta as unsigned, then it does not have to state that AFAICT because it always holds ?

centril (Nov 28 2018 at 19:55, on Zulip):

@gnzlbg to frame it in @RalfJ's terms, I didn't see that it states whether the concatenation is interpreted in terms of signed or unsigned integer operations or not

centril (Nov 28 2018 at 19:56, on Zulip):

I would expect that it is unsigned; but there's doubt here imo

gnzlbg (Nov 28 2018 at 19:56, on Zulip):

I think that's what @Dan Gohman was hinting at when they said gt_u is used.

centril (Nov 28 2018 at 19:56, on Zulip):

in particular the phrasing "grow" and "append" suggest >= but that's not a formal semantics :P

gnzlbg (Nov 28 2018 at 19:56, on Zulip):

gt_u is the "greater-than unsigned" operation

centril (Nov 28 2018 at 19:57, on Zulip):

@gnzlbg ye; sadly I didn't find the OCaml code well documented or readable

gnzlbg (Nov 28 2018 at 19:58, on Zulip):

FWIW the spec isn't readable either, it's the only spec I actually had to send multiple PRs to because I had no idea what it was trying to say

gnzlbg (Nov 28 2018 at 19:58, on Zulip):

There are multiple sources of truth that sometimes are contradictory, etc.

centril (Nov 28 2018 at 19:58, on Zulip):

@gnzlbg the notation wrt. operational semantics is somewhat nonstandard

RalfJ (Nov 28 2018 at 19:59, on Zulip):

I'm so happy they even have a normative operational semantics

centril (Nov 28 2018 at 19:59, on Zulip):

anyways; by keeping it usize, we at least can rule out some bugs even if WASM permits more

gnzlbg (Nov 28 2018 at 19:59, on Zulip):

Basically, the word of the implementors is worth a bit more than what's on the spec

centril (Nov 28 2018 at 19:59, on Zulip):

@RalfJ this is so true; it's much more than you can usually expect

gnzlbg (Nov 28 2018 at 19:59, on Zulip):

The problem is that, if the spec is ambiguous enough, people might decide to recycle these to allow for shrinking memory in the future

centril (Nov 28 2018 at 20:00, on Zulip):

would be nice to formalize this in Agda

centril (Nov 28 2018 at 20:00, on Zulip):

@gnzlbg we can add another function in such a case can we not?

gnzlbg (Nov 28 2018 at 20:00, on Zulip):

yeah, but honestly, if this is an issue, then we should just file a github issue with the wasm spec

centril (Nov 28 2018 at 20:01, on Zulip):

memory_grow_yolo

gnzlbg (Nov 28 2018 at 20:01, on Zulip):

they tend to clarify these things pretty quickly and amend the spec as necessary

centril (Nov 28 2018 at 20:01, on Zulip):

@gnzlbg this is why I suggested talking to the WASM folks on the issue

centril (Nov 28 2018 at 20:02, on Zulip):

but if I can just file a GitHub issue then ill do that

gnzlbg (Nov 28 2018 at 20:04, on Zulip):

Reading the semantics: they say "Either, try growing mem by n pages:"

gnzlbg (Nov 28 2018 at 20:05, on Zulip):

growing seems to imply that the number of pages before has to be less or equal to the number of pages afterwards

centril (Nov 28 2018 at 20:05, on Zulip):

@gnzlbg yes, however, "append" and "grow" are not defined terms

gnzlbg (Nov 28 2018 at 20:05, on Zulip):

in any case, if that fails, this returns -1

centril (Nov 28 2018 at 20:05, on Zulip):

@gnzlbg sure, I agree that it implies that; but implication is not certainty

gnzlbg (Nov 28 2018 at 20:06, on Zulip):

still, for Rust this doesn't help much, it still doesn't really tell us whether this has to be a signed or unsigned integer type

gnzlbg (Nov 28 2018 at 20:07, on Zulip):

https://webassembly.github.io/spec/core/exec/modules.html#grow-mem

gnzlbg (Nov 28 2018 at 20:07, on Zulip):

If len is larger than 2^16, then fail.

I guess that's where Dan meant that the ML implementation uses gt_u

gnzlbg (Nov 28 2018 at 20:08, on Zulip):

Let len be n added to the length of meminst.𝖽𝖺𝗍𝖺 divided by the page size 64Ki.

The question is, how is this len added, is it a signed or unsigned add ? I don't remember if there was a difference here. Add works for both signed and unsigned integers the same.

centril (Nov 28 2018 at 20:12, on Zulip):

https://github.com/WebAssembly/spec/issues/924

Last update: Nov 20 2019 at 12:10UTC