Non-determinism with division by zero

[axic]

Source: https://webassembly.github.io/spec/core/_download/WebAssembly.pdf

pp48: idiv_u𝑁 (𝑖1, 𝑖2) • If 𝑖2 is 0, then the result is undefined.

idiv_s𝑁 (𝑖1, 𝑖2) • If 𝑗2 is 0, then the result is undefined. • Else if 𝑗1 divided by 𝑗2 is 2𝑁−1, then the result is undefined.

irem_u𝑁 (𝑖1, 𝑖2) • If 𝑗2 is 0, then the result is undefined.

irem_s𝑁 (𝑖1, 𝑖2) • If 𝑖2 is 0, then the result is undefined.

pp61: trunc_u𝑀,𝑁 (𝑧) (Not a problem since this is floating point only.)

pp62: trunc_s𝑀,𝑁 (𝑧) (Not a problem since this is floating point only.)

(raised by @holiman)

[axic]

The case when the argument is zero, could be easily solved by embedding a call to a function check_for_zero, which traps if the argument is zero, at run time. If it is constant zero, the entire statement could be replaced with (unreachable) by the "deploy time verification process".

This still leaves "Else if 𝑗1 divided by 𝑗2 is 2𝑁−1, then the result is undefined." as a problem.

Potentially we could propose to introduce alternative versions of these instructions which do the is-zero check on the wasm engine side.

[pepyakin]

Isn’t this operations are partial, i.e not defined on the full input domain space? If so, these operators should trap instead of return non deterministic results?

[axic]

@pepyakin good catch, all these four are.

Perhaps the way forward is to specify a deterministic version of these four instructions, which are either: a) provided by the "ewasm vm" (and the instructions replaced with a call to them) or b) just injected (and thus copied in) by the verification process

[pepyakin]

yeah i mean that these operators are already act deterministically on all of their inputs.

So I’m not sure what you mean

[axic]

How are they deterministic with division by 0?

[pepyakin]

Sorry for terse answers, I was commuting.

1. Let's take idiv_un(i1, i2) for example.
2. It states, that if i2 is 0, then the result is undefined.
3. In context of numeric operations this means that operator is partial, i.e if i2 is 0 the return value is empty set.
4. then, let's look at definition of the numeric instructions: It specifically says that

Where the underlying operators are partial, the corresponding instruction will trap when the result is not defined

So, in other words: I expect that division by 0 in every execution will result in trap. Am I missing something?

[axic]

pp45:

Some operators are partial, because they are not defined on certain inputs. Technically, an empty set of results is returned for these inputs.

pp63:

Where the underlying operators are partial, the corresponding instruction will trap when the result is not defined. Where the underlying operators are non-deterministic, because they may return one of multiple possible NaN values, so are the corresponding instructions.

Lets see if there are appropriate test cases for this in the wasm spec.

[pepyakin]

Yeah, sure, for example take a look at this one

[ehildenb]

Hmmm, seems like a bug in the spec then (that it says is "undefined" instead of saying "trap").

[ehildenb]

@axic you want to do the honors of opening an issue on the wasm spec repo?

[pepyakin]

I think that's not a bug but just unfortunate wording issue: partial functions are "undefined" on some of their inputs, and the instructions are always traps when functions they invoking are "undefined".

So this "undefined" has nothing to do with "undefined" from "undefined behavior".

[ehildenb]

I think the spec is pretty clear in other places where there should be a Trap, so I think it should say Trap instead of "undefined". I think either way we should open an issue on the spec repo to bring it to their attention and clarify our understanding.

[axic]

I think the spec could be improved, because one needs to jump around to unfold the entire story.

I did found some missing test cases though which I'll try to add and/or report.