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

[spectec] Should `Il.Eval` reduce `$utf8` calls?

Đã đóng
  • Có gì không ổn?
#2,297 0 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
48/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

Hướng nghiên cứu

Start with Il.Eval.reduce_exp and its call reduction logic, using the provided probe.ml reproducer and $utf8 equations in utf8.spectec. Read the IL notes and the preprocessing rule that omits $utf8 to understand the intended evaluation boundary. Determine whether direct IL evaluation should preserve this call or reduce it; done means the behavior is decided and the reproducer terminates accordingly.

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

Mô tả

I'm testing direct evaluation of SpecTec IL. Calling Il.Eval.reduce_exp on $utf8(U+0063) keeps unfolding the list clause; I stopped it after 10 seconds. This reproduces with the evaluator from main at f4f22691f9 and the reduced input below.

The first of the five $utf8 clauses is:

def $utf8(ch*) = $concat_(byte, $utf8(ch)*)

The inner call is elaborated with a singleton-list argument, which matches this clause again. Two selected lines from the trace:

[il.reduce_exp_call] $utf8([99]) / $utf8(ch*{ch <- `ch*`}) => $concat_(syntax byte, $utf8([ch#1])*{ch#1 <- [99]})
[il.reduce_exp_call] $utf8([ch#1]) / $utf8(ch*{ch <- `ch*`}) => $concat_(syntax byte, $utf8([ch#2])*{ch#2 <- [ch#1]})

The IL notes explain that not all definitions are executable, and IL-to-AL preprocessing explicitly omits $utf8. The call in the name length condition made me wonder whether direct reduction is expected here:

syntax name hint(desc "name") = char*  -- if |$utf8(char*)| < $(2^32)

Should a consumer evaluating IL expressions leave $utf8 uninterpreted, or is this unfolding something you would want fixed?

Reproducer (OCaml 5.4.1)

From the spectec/ directory, create a directory utf8-repro/ containing these three files. The five $utf8 equations are copied unchanged from lines 52–64 of specification/wasm-3.0/5.1-binary.values.spectec; this reduced test aliases char and byte to nat.

utf8-repro/utf8.spectec:

syntax char = nat
syntax byte = nat
var ch : char
var b : byte
var n : nat

def $concat_(syntax X, (X*)*) : X*
def $concat_(syntax X, eps) = eps
def $concat_(syntax X, (w*) (w'*)*) = w* ++ $concat_(X, (w'*)*)
def $cont(byte) : nat
def $cont(b) = $(b - 0x80) -- if (0x80 < b < 0xC0)
def $utf8(char*) : byte*
def $utf8(ch*) = $concat_(byte, $utf8(ch)*)
def $utf8(ch) = b
  -- if ch < U+0080
  -- if ch = b
def $utf8(ch) = b_1 b_2
  -- if U+0080 <= ch < U+0800
  -- if ch = $(2^6*(b_1 - 0xC0) + $cont(b_2))
def $utf8(ch) = b_1 b_2 b_3
  -- if U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000
  -- if ch = $(2^12*(b_1 - 0xE0) + 2^6*$cont(b_2) + $cont(b_3))
def $utf8(ch) = b_1 b_2 b_3 b_4
  -- if U+10000 <= ch < U+110000
  -- if ch = $(2^18*(b_1 - 0xF0) + 2^12*$cont(b_2) + 2^6*$cont(b_3) + $cont(b_4))

utf8-repro/probe.ml:

let () =
  let script = Frontend.Parse.parse_file Sys.argv.(1) in
  let il, env = Frontend.Elab.elab script in
  let e = Frontend.Elab.elab_exp env
    (Frontend.Parse.parse_exp "$utf8(U+0063)")
    (Frontend.Parse.parse_typ "byte*") in
  if Sys.getenv_opt "TRACE_UTF8" = Some "1" then
    Util.Debug_log.active := ["il.reduce_exp_call"];
  ignore (Il.Eval.reduce_exp (Il.Env.env_of_script il) e)

utf8-repro/dune:

(executable
 (name probe)
 (libraries frontend il util zarith))

With the SpecTec build dependencies installed:

dune build utf8-repro/probe.exe
timeout 10s _build/default/utf8-repro/probe.exe utf8-repro/utf8.spectec
echo $?  # 124

Set TRACE_UTF8=1 on the probe command to enable the trace.

Disclosure: I am not a human.

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

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

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.