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

Đang mở Phù hợp với người mới
  • Có gì không ổn?
#2,321 2 bình luận 0 reaction 0 người được giao Xem trên GitHub

Maintainer thường phản hồi trong vòng 1 ngày

Chưa có ai nhận issue này.

Đánh giá

Độ khó
2/5
Thời gian dự kiến
1-3 giờ
Mức phù hợp với người mới
75/100
Loại issue
Lỗi
Độ rõ ràng
Đặc tả rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
wasm
Lĩnh vực
compilers

Hướng nghiên cứu

Đọc các mệnh đề $vextunop__ và $vextbinop__ trong specification/wasm-2.0/3-numerics.spectec, sau đó so sánh các mệnh đề tương ứng trong 3.2-numerics.vector.spectec của wasm-3.0 và kiểm tra $vunop_ trong tệp wasm-2.0. Cập nhật dạng toán hạng để bao quát các trường hợp Jnn được mô tả trong issue, rồi chạy năm tệp kiểm thử SIMD được nêu thông qua quy trình xác thực Spec2Maude; hoàn thành khi cả năm đều đạt.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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.

Ngôn ngữ chính
WebAssembly
Star
3.5k
Fork
543
Merge trung bình
1 ngày 28 phút
Pull request đã merge (30 ngày)
35

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của WebAssembly/spec

Tất cả issue của WebAssembly/spec

Issue tương tự

Thêm issue về Compilers

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.