Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

il2al: host function rules become two independent conditionals and ignore the new store `s'`

Đang mở
#2,279 6 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ó
4/5
Thời gian dự kiến
3-5 ngày
Mức phù hợp với người mới
25/100
Loại issue
Lỗi
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
ocaml, wasm
Lĩnh vực
compilers

Hướng nghiên cứu

The two host-function rules are in spectec/specification/wasm-3.0/4.3-execution.instructions.spectec around lines 184-198. The translation that emits Either only for condition-free rules is in spectec/src/il2al/translate.ml near line 1155, so start there and compare with how memory.grow is handled. Done means the RES and BOT cases become mutually exclusive alternatives, and the store s' from the RES case is applied, as checked by the --prose output.

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

Mô tả

I came across this while looking at how il2al uses Either for nondeterminism.

The rules Step/call_ref-hostfunc-res and -div (added in #2210) can both apply:

https://github.com/WebAssembly/spec/blob/8d6a3afa965a28e145110445101338bed947991b/specification/wasm-3.0/4.3-execution.instructions.spectec#L184-L198

--prose gives:

13. If an element of $hostcall((_HOSTFUNC hf), s, val^n) is some RES, then:
  a. Let (RES s' result) be an element of $hostcall((_HOSTFUNC hf), s, val^n).
  b. Execute the sequence $lift_result(result).
14. If BOT is contained in $hostcall((_HOSTFUNC hf), s, val^n), then:
  ...
  1. Steps 13 and 14 are not alternatives, so when both apply the algorithm does both.
  2. s' is never used, so the store is not updated.

I would expect something like this, as for memory.grow (not sure how AL should update the whole store):

13. Either:
  a. Let (RES s' result) be an element of $hostcall((_HOSTFUNC hf), s, val^n).
  b. Update the store s to s'.
  c. Execute the sequence $lift_result(result).
14. Or:
  ...

It seems il2al produces Either only for rules without conditions (translate.ml#L1155).

Note: This might be low priority since neither the document nor the reference interpreter uses this algorithm.

Ngôn ngữ chính
WebAssembly
Star
3.5k
Fork
540
Merge trung bình
1 ngày 6 giờ
Pull request đã merge (30 ngày)
20

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.