[spectec] wasm-2.0: $vextunop__/$vextbinop__ are defined only for Inn, so I8/I16-lane extadd_pairwise, extmul, and dot have no result

Aperta Adatta ai principianti
  • Qualcosa non va?
#2,321 2 commenti 0 reazioni 0 assegnatari Vedi su GitHub

I maintainer di solito rispondono entro 1 giorno

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
2/5
Tempo stimato
1-3 ore
Idoneità per principianti
75/100
Tipo di issue
Bug
Chiarezza
Specificata chiaramente
Stato di attività
Attiva
Stack tecnologico
wasm
Ambito
compilers

Direzione di ricerca

Leggi le clausole $vextunop__ e $vextbinop__ in specification/wasm-2.0/3-numerics.spectec, poi confronta le clausole corrispondenti in 3.2-numerics.vector.spectec di wasm-3.0 e controlla $vunop_ nel file wasm-2.0. Aggiorna le forme degli operandi per coprire i casi Jnn descritti nell’issue, quindi esegui i cinque file di test SIMD indicati tramite il flusso di convalida Spec2Maude; il lavoro è completato quando tutti e cinque passano.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

In specification/wasm-2.0/3-numerics.spectec (checked on main, e7a9df7c), the clauses of $vextunop__ and $vextbinop__ (lines 588, 595, 600) match only Inn shapes:

def $vextunop__(Inn_1 X M_1, Inn_2 X M_2, EXTADD_PAIRWISE sx, c_1) = c
def $vextbinop__(Inn_1 X M_1, Inn_2 X M_2, EXTMUL half sx, c_1, c_2) = c
def $vextbinop__(Inn_1 X M_1, Inn_2 X M_2, DOT S, c_1, c_2) = c

Inn is I32 | I64 (1-syntax.spectec:141), but the syntax admits Jnn shapes (syntax vextunop_(Jnn X M), 1-syntax.spectec:376-381), and the binary format produces them, e.g. (A-binary.spectec:623):

| 0xFD 124:Bu32 => VEXTUNOP (I16 X 8) (I8 X 16) (EXTADD_PAIRWISE S)

So no clause applies to i16x8.extadd_pairwise_i8x16_s/u, i32x4.extadd_pairwise_i16x8_s/u, i16x8.extmul_*_i8x16_*, i32x4.extmul_*_i16x8_*, and i32x4.dot_i16x8_s. The premise of Step_pure/vextunop / Step_pure/vextbinop has no solution, and execution gets stuck. Only i64x2.extmul_*_i32x4_* is covered. Example (test/core/simd/simd_i16x8_extadd_pairwise_i8x16.wast:13 in wg-2.0):

(assert_return (invoke "i16x8.extadd_pairwise_i8x16_s" (v128.const i8x16 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1))
                                                       (v128.const i16x8 2 2 2 2 2 2 2 2))

We found this with Spec2Maude, a tool that translates the SpecTec IL of the Wasm spec into Maude, a rewriting-logic framework, so that the spec semantics can be formally analyzed (e.g., model checking of Wasm programs). To validate the translation, we run the official test suite of each Wasm version (here, the wg-2.0 tag) on the translated semantics. Five files fail on the wasm-2.0 spec as is: simd_i16x8_extadd_pairwise_i8x16, simd_i32x4_extadd_pairwise_i16x8, simd_i16x8_extmul_i8x16, simd_i32x4_extmul_i16x8, and simd_i32x4_dot_i16x8.

Possible fix: use Jnn in these clauses, as wasm-3.0 does (3.2-numerics.vector.spectec:316-325) and as $vunop_ already does in the same wasm-2.0 file:

def $vextunop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTADD_PAIRWISE sx, c_1) = c
def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTMUL half sx, c_1, c_2) = c
def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, DOT S, c_1, c_2) = c

(with Inn_1/Inn_2 replaced by Jnn_1/Jnn_2 in the premises as well). With this change, all five files pass with the Maude translation.

Lingua principale
WebAssembly
Stelle
3.5k
Fork
543
Merge medio
1g 28m
PR unite (30g)
35

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di WebAssembly/spec

Tutte le issue di WebAssembly/spec

Issue simili

Altre issue su Compilers

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.