[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.

[rossberg]

@f52985, did you have any chance to look into this?

[f52985]

Oh, I've been a bit busy lately and haven't had time to look into it yet. I'll take a look soon.

[f52985]

Sorry for the delay.

The issue with the AL interpreter was indeed the hardcoded injection of the ThrowI instruction. It was originally injected in the algorithm for throw_ref, and it now needs to be injected in the algorithm for throw_addr to stay in sync with the updated specification.

In the fixed version, the generated prose for this case looks like:

6. Else if the first non-value entry of the stack is not a HANDLER_, then:
   a. Throw the exception (THROW_ADDR a) as a result.
7. Else:
   ...

I wasn't entirely sure what the exact wording should be, so I used THROW_ADDR a directly as the execution result to match how the specification defines result. Extracting the immediate a and rendering only that should be straightforward (which is simply extracting the first argument of the CaseE) if that's the preferred presentation.

[rossberg]

Thanks @f52985. I think that specific wording is fine, but I agree that there still are some stylistic issues and unexpected changes in the prose:

• Step 3 is an artefact of the contextual rules. Like for return, it should better be suppressed for the prose.
• For some reason, the .rst output differs from the ASCII output: it breaks the "else if" chain at step 5 and produces the FRAME case as a nested step 5a.
• In the old rendering using throw_ref, the uncaught exception case (return throw as a result), came as the last step, which is a more natural progression. It appears in the middle now.

Can these perhaps be tweaked somehow?

[rossberg]

@f52985, just tagging you again to make sure that you saw my questions above. :)

[f52985]

Oh, somehow I missed the rest of questions. I'll take a look.

[rossberg]

Hi @f52985, did you ever get a chance to look into this?

[f52985]

Oops, my bad. It completely slipped my mind.

I've investigated each issue, and all of them are now fixed:

Step 3 is an artefact of the contextual rules. Like for return, it should better be suppressed for the prose.

Context rules are now excluded from the prose generation target. The filter depends on the naming convention of the rules, where they all end with -instrs, which might be a bit hacky, but I believe this should be sufficient.

For some reason, the .rst output differs from the ASCII output: it breaks the "else if" chain at step 5 and produces the FRAME case as a nested step 5a.

The rst renderer had an issue where it could not correctly render long if-else chains. This is now fixed, which also uncovered and fixed a similar issue in other rendered algorithms.

In the old rendering using throw_ref, the uncaught exception case (return throw as a result), came as the last step, which is a more natural progression. It appears in the middle now.

The translator now enforces that the single Throw appears in the latter position of an if-else block.