Wasm-DSL / spectec

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

Remove $idx #122

Closed ShinWonho closed 3 weeks ago

ShinWonho commented 1 month ago

Hello, There had been a spec bug in ref.null, so ref.null algorithm was hardcoded in AL interpreter. Now the bug is fixed, I'm trying to remove the hardcoding. However, there is a problem.

rule Step_read/ref.null-idx:
  z; (REF.NULL $idx(x))  ~>  (REF.NULL $type(z, x))
Step_read/ref.null $idx(x)
1. Let z be the current state.
2. Push the value (REF.NULL $type(z, x)) to the stack.

This is current reduction rule and prose of ref.null. There is a function call $idx(x) in the LHS. The problem is, we cannot pattern match on a function call.

One possible solution is to use inverse function, and another is not to use function call in LHS.

  1. To use inverse function

    
    Step_read/ref.null typevar
  2. Let z be the current state.

  3. Let x be $idx^-1(typevar).

  4. Push the value (REF.NULL $type(z, x)) to the stack.

  5. Not to use function call in lhs

    rule Step_read/ref.null-idx:
    z; (REF.NULL (_IDX x))  ~>  (REF.NULL $type(z, x))
    
    Step_read/ref.null (_IDX x)
  6. Let z be the current state.

  7. Push the value (REF.NULL $type(z, x)) to the stack.

I think the prose of the second version looks better, but this version means that function call is not allowed in LHS of reduction rule. Do you think the constraint is reasonable, @rossberg?

rossberg commented 4 weeks ago

Yeah, this function is a hack, the only reason is exists is that it will otherwise render redundant parentheses around x, i.e., you'll see "(ref.null (x))" instead of "(ref.null x)".

Maybe a better way to solve this problem is to either special-case rendering of parens around hidden constructors, or introduce some form of hidden parentheses.

As a temporary solution to unblock you, I'm okay with removing this call site for now. But please add a TODO assigned to me to fix rendering. :)

ShinWonho commented 4 weeks ago
Screenshot 2024-09-04 at 7 29 54 PM

I just want a double-check. I built the document, but it seems that there are no redundant parentheses. Does the problem still exist?

rossberg commented 4 weeks ago

Oh. Looking back at the code, it turns I already implemented that special case in the renderer. :) So the $idx function is completely unnecessary now. Would you mind removing it everywhere?

ShinWonho commented 4 weeks ago

No! I'll remove all $idx :)