il2al: host function rules become two independent conditionals and ignore the new store `s'`
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:
--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:
...
- Steps 13 and 14 are not alternatives, so when both apply the algorithm does both.
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
- Không có Dockerfile hay tệp Docker Compose
- Không có mẫu pull request
- Đọc hướng dẫn đóng góp
Bắt đầu từ đâu
- Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
- 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.
- Fork repository và làm thay đổi trên một nhánh.
- Mở pull request có tham chiếu số hiệu của issue.
Issue khác của WebAssembly/spec
-
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 35/100
WebAssembly/spec#2258 · 4 bình luận · 1 reaction ·
Maintainer thường phản hồi trong vòng 1 ngày
-
[js-api] A mutable global import allocates a const global before LinkErrorCó thể đã có người làm @chicoxyzzy đã nhận 14 ngày trước. Đang mở
Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 58/100
WebAssembly/spec#2253 ·
Maintainer thường phản hồi trong vòng 1 ngày
-
[spectec] Wasm 1.0: `$instantiate` missing premisesCó thể đã có người làm @rossberg đã nhận 40 ngày trước. Đang mở
Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 68/100
WebAssembly/spec#2245 ·
Maintainer thường phản hồi trong vòng 1 ngày
-
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 45/100
WebAssembly/spec#2235 · 9 bình luận ·
Maintainer thường phản hồi trong vòng 1 ngày
-
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100
WebAssembly/spec#2196 ·
Maintainer thường phản hồi trong vòng 1 ngày
Tất cả issue của WebAssembly/spec
Issue tương tự
-
bug priority: P2
Độ khó 1/5 1-3 giờ Mức phù hợp với người mới 84/100
Maintainer thường phản hồi trong vòng 1 ngày
-
clang:static analyzer
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 68/100
llvm/llvm-project#233598 · 1 bình luận ·
Maintainer thường phản hồi trong vòng 1 ngày
-
bug ci sev-6
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 78/100
Maintainer thường phản hồi trong vòng 1 ngày
-
bug
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 78/100
AeneasVerif/aeneas#1467 ·
Maintainer thường phản hồi trong vòng 1 ngày