search

Wasm-DSL / spectec

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

Split sx for uniformity #112

Closed rossberg closed 3 months ago

rossberg commented 3 months ago

Hey folks, I'm afraid I need help again. This PR is supposed to be a tiny syntax refactor, but somehow it breaks the interpreter, and I have no clue why. I get this error, which seems quite unrelated to the change:

3-numerics.watsup:375.11-375.74: interpreter error: vbinop: fpmax: [0x40, 0x0, 0x0] (interpreting LetI (VarE (v128), CallE (invlanes_, [ InfixE (VarE (Fnn), X, VarE (N)), IterE (CallE (fpmax, [ CallE (size, [ VarE (Fnn) ]), VarE (lane_1), VarE (lane_2) ]), [lane_1, lane_2], *) ])))

Any help appreciated.

f52985 commented 3 months ago

Here's a probable scenario for what had happened:

vbinop (lanet_u1 X N) vbino_u0 v128_1 v128_2
1. If ...
...
5. If ((vbino_u0 is AVGR) and the type of lanet_u1 is Jnn), then:
  a. Let Jnn be lanet_u1.
  b. Let lane_1* be $lanes_((Jnn X N), v128_1).
  c. Let lane_2* be $lanes_((Jnn X N), v128_2).
  d. Let v128 be $invlanes_((Jnn X N), $iavgr_u($lsize(Jnn), lane_1, lane_2)*).
  e. Return [v128].
13. If ...
...
14. Assert: Due to validation, (vbino_u0 is PMAX).
15. Assert: Due to validation, the type of lanet_u1 is Fnn.
16. Let Fnn be lanet_u1.
17. Let lane_1* be $lanes_((Fnn X N), v128_1).
18. Let lane_2* be $lanes_((Fnn X N), v128_2).
19. Let v128 be $invlanes_((Fnn X N), $fpmax($size(Fnn), lane_1, lane_2)*).
20. Return [v128].

It seems that the name of binary operator vbino_u0 did not match the string "AVGR" on line 5 for some reason, and the execution fell through the 14th line, falsely asserting it was a "PMAX".

I'm not sure why the condition on line 5 became false though, and I'll try investigating it.

BTW, one entry of our TODO list is to actually check the assertions, and let the user know in case of the assertion failure. (So that it would be easier to know the actual problem in case like this)