[spec] Add call_addr and throw_addr as admin instructions

[rossberg]

@raoxiaojia, this makes the change suggested in #2188 and replaces the use of call_ref as a semi-administrative instruction with a dedicated call_addr. Analogously, do the same change for throw_ref/throw_addr. This allowed to remove all occurrences of typeuse from the instruction syntax. PTAL.

@f52985, the change to throw_ref breaks AL translation. There appears to be some special handling of throw rules, but I couldn't figure out exactly what it does and why the tweak I did wasn't enough how to get the immediate of the throw_addr instruction instead of the stack top. Can you please take a look?

[raoxiaojia]

Same for the ref null dt here

[raoxiaojia]

t^* here looks to be droppable as well (same as the above 2)

[raoxiaojia]

Hmm, I thought we would be able to drop the additional REF NULL dt here given that call_addr is now the dedicated invoke admin instruction (so it only resolves the lookup and invoke the function frame).

[raoxiaojia]

That's a nice and helpful cleanup! Most of the changes look correct, although there are some instr_ok2 typing rules that look a bit suspicious.

The AL breakage might be due to Step_read/throw_ref-addr carrying a suspicious sidecondition requiring val^* and instr^* to not be empty at the same time. I thought programs like e.g. [frame ... [ref.exn_addr a; throw_ref]] would now be stuck, but maybe there was a reason to add that premise for something I've overlooked? iirc originally that premise is for framing a evaluation context with [...; throw_ref; ...] down to only the throw_ref (and the reference before it).

Upd: Oh I might have seen the point -- without the guard it seems to introduce nondet reduction paths. But I think the program above is genuinely stuck, as the reference cannot be resolved to a throw_addr.

Given that we now have throw_addr, I think a more principled design might be to make ref.exn_addr a; throw_ref -> throw_addr a, and then let throw_addr handle the framing of val and instr stacks (instead of trying to handle it at the throw_ref layer. i.e. something like this probably, so that throw_ref's obligation is to resolve ref.exn_addr into throw_addr, and throw_addr handles the stack reduction duty (which sounds correctly like an admin job).

rule Step_read/throw_ref-addr:
  z; (REF.EXN_ADDR a) THROW_REF ~>  (THROW_ADDR a)

rule Step_read/throw_addr-instrs:
  z; val* (THROW_ADDR a) instr*  ~>  (THROW_ADDR a)
  ----
  -- if val* =/= eps \/ instr* =/= eps

[rossberg]

Ah, too many copy&paste errors, thanks!

As for the the AL problem, that already occurs during translation, so isn't a stuck rule. Fixing the throw_ref rule didn't change it. I suspect that I need to change where the ThrowI arg is coming from in the translate.ml, but I'm not sure how to get (and transform) the immediate.

[raoxiaojia]

I see. iirc the AL had some hard coded implementations for evaluation context instructions, and throw_ref needed to handle a lot of cases there (before this change) indeed..

On a side note, I'd only wish if a similar clean restriction could apply to the reference instructions like br_on_cast(_fail)/ref_test/ref_cast to rule out the REC/deftype cases of reftype -- basically, ruling out the typeuse/sem family that shouldn't appear in the AST. But those arguments cannot be similarly restricted to just an IDX, because they can be absheaptype as well.

In my work I've made typeuse/syn + absheaptype a subset type of the general heaptype and plug that in there, as otherwise I'll need to handle some spurious reasoning of inlined deftype conversion there which isn't helpful for anything.