Pass on instruciton syntax

[rossberg]

This PR does some tweaks to the instruction syntax.

I had to change the syntax of loadops from sz sx to sz _ sx, in order to make sure that the show hint actually applies. I adapted convert.ml accordingly, but unfortunately, the change still breaks the interpreter, which encounters some Let (n, sx) = loadop with a tuple on the lhs. I could not figure out where this let is coming from — it does not appear in the AL shown with --print-al, nor could I find a place in the backend code that introduces it. So I'm a bit puzzled.

@f52985, any help is appreciated.

[f52985]

So.. the main issue was that:
the loadop syntax for wasm 1.0 and wasm 2.0 was not modified,
which was fixed by the latest commit.

Regarding the error message:
i.e. ($LOAD: on expr `(n, sx)` invalid assignment: on rhs (_ 8 U) (interpreting Let (n, sx) = loadop__0 at :0.1-236.36))
Yeah... I have to admit that the error message is a bit hard to dechiper.
First of all, the function named $LOAD, actually refers to the execution prose for the wasm LOAD instruction, which is translated from the reduction rule for it, i.e.,

Step_read/load t_u1 loadop__u1? ao
1. Let z be the current state.
2. Assert: Due to validation, a value of value type I32 is on the top of the stack.
3. Pop the value (I32.CONST i) from the stack.
4. If loadop__u1? is defined, then:
  1) Let ?(loadop__0) be loadop__u1?.
  2) Let (n, sx) be loadop__0.   ;;<- HERE
  3) ...

and the (half of the) location information for this expression seems to be lost somewhere in the middle of translation (mainly due to anti-unification, I guess), displaying the weird location information, i.e. 0.1-236.36.

[rossberg]

Ah, of course! Thank you for looking into it! I sort of understood the error message (having experienced it many times before), but really couldn't understand where that LHS was coming from, since I only thought of the Wasm 3 spec.

Do you think there is a chance that we can fix the error location in this message?

[f52985]

since I only thought of the Wasm 3 spec.

Oh, I see. I guess this is also an unfortunate result of the broken location information.

Do you think there is a chance that we can fix the error location in this message?

Yes, we will try to fix it. :)

[702fbtngus]

The commit d8e33e6 fixed the issue where the error location was missing (originally noticed in commit 073be71).
With this fix applied retroactively, the location :0.1-236.36 is now correctly displayed as 8-reduction.watsup:0.1-236.36, including the file name.

Does this seem sufficient for now, or do you think the rule name (e.g., Step_read/load) should also be included in the error location?

[rossberg]

@702fbtngus, thanks! The location info is the essential information, any additional info just nice to have. We don't provide the name of the surrounding definition in other cases either, so I'd say that isn't necessary.