search

Wasm-DSL / spectec

Wasm SpecTec specification tools
https://wasm-dsl.github.io/spectec/
Other
27 stars 9 forks source link

Obtaining more specific type from IL expression #120

Closed f52985 closed 3 months ago

f52985 commented 3 months ago

Here's what I want to do (for more robust handling of exception handling proposal):

When I have an IL case expression like LABEL_ (n, instr*, instr*), I want to know that the type of this expression is instr/admin, and when I have an IL case expression like NOP, I want to know that the type of this expression is not instr/admin (specifically, it is instr/parametric)

But it seems that I cannot tell whether it is a admin instruction or not.

If I access e.note, it just returns instr, without further information about if the instruction is from instr/admin or instr/parametric.

Would this be possible currently? If not, would it be possible to implement it?

rossberg commented 3 months ago

It's all one type. The only reason SpecTec allows defining it in fragments is so that we can splice fragments instead of one huge definition. But semantically, they just form one big type.

So there (intentionally) is no way to distinguish the fragments in the IL. If we wanted to distinguish admin instructions, then we'd need to make them a separate type. That's how it was before, but the problem is that it did not scale to some of the newer proposals, and already complicated the subtype relation.

Would that even be the right distinction for your problem? There are some admin instructions, like all the addrrefs, that are simply values, and I'd assume you'd need to treat them no different from t.const, for example? The threads proposal has other examples like wait'/notify' which may not fit your intentions. Can you give a few more details on what exactly you'd like to use the distinction for?

f52985 commented 3 months ago

Can you give a few more details on what exactly you'd like to use the distinction for?

To be more specific, what I want to achieve is to tell whether a given wasm instruction is a "context" or not, in more robust way.

Currently, what I have to do is, to look at the mixop of the CaseE, and if that is one of FRAME_, LABEL_ or HANDLER_, then consider that as a case,

..which might not work if a new hypothetical context is introduced.

rossberg commented 3 months ago

That makes sense. How about we introduce a hint on the respective constructors for that?

f52985 commented 3 months ago

Oh that makes much more sense. I'll try that, thanks!