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

Non-ASCII characters in symbol names

Đang mở
  • Có gì không ổn?
#4,941 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

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

Đánh giá

Độ khó
3/5
Thời gian dự kiến
Nửa ngày
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ệ
java, python, scala
Lĩnh vực
backend

Hướng nghiên cứu

Start from pyk/src/pyk/konvert/_utils.py to fix munge to encode non-ASCII characters as 4-hex-digit UTF-16 chunks. Then update the decoders: KoreToK.mapCode in k-frontend/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala, decodeKoreString in k-frontend/src/main/java/org/kframework/utils/StringUtil.java, and decode_kore in llvm-backend/lib/ast/AST.cpp to recognize [0-9a-f]{4} chunks and convert them back to characters. Run the relevant test suites to verify the round-trip.

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

Mô tả

bug

ModuleToKORE encodes each non-ASCII UTF-16 code unit as a 4-hex-digit chunk inside the '...' block, so λ → Lbl'03bb' and 𐔷 (U+10537, a surrogate pair) → Lbl'd801dd37':

https://github.com/runtimeverification/k/blob/4a46d1231473b599c699160132fd6e76a5c46406/k-frontend/src/main/java/org/kframework/utils/StringUtil.java#L529-L559

Every chunk is exactly 4 characters (the overrides below make sure of that) and lowercase hex never collides with a mnemonic, so the encoding is unambiguous:

https://github.com/runtimeverification/k/blob/4a46d1231473b599c699160132fd6e76a5c46406/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java#L2154-L2165

Both backends accept these names, since ' is a legal identifier character:

Bug 1: pyk munge does not encode non-ASCII

Characters outside MUNGE_TABLE are copied verbatim, so munge('λ') == 'λ', which is not a valid KORE identifier and differs from what kompile emits:

https://github.com/runtimeverification/k/blob/4a46d1231473b599c699160132fd6e76a5c46406/pyk/src/pyk/konvert/_utils.py#L53-L66

Bug 2: no decoder converts hex chunks back to characters

Reachable today:

KoreToK.mapCode (used for symbol names) parses the hex and then discards it, returning the text \u03bb instead of the character:

https://github.com/runtimeverification/k/blob/4a46d1231473b599c699160132fd6e76a5c46406/k-frontend/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala#L59-L65

pyk unmunge raises ValueError('Unknown encoding "03bb"'):

https://github.com/runtimeverification/k/blob/4a46d1231473b599c699160132fd6e76a5c46406/pyk/src/pyk/konvert/_utils.py#L73-L118

Latent, because these two are only applied to variable names and #KVariable restricts those to ASCII [A-Za-z0-9'_] plus a !/?/@ prefix (the @ is split off before encoding):

https://github.com/runtimeverification/k/blob/4a46d1231473b599c699160132fd6e76a5c46406/k-distribution/include/kframework/builtin/kast.md#L206

StringUtil.decodeKoreString looks the slice up in the default map and appends the string "null" on a miss:

https://github.com/runtimeverification/k/blob/4a46d1231473b599c699160132fd6e76a5c46406/k-frontend/src/main/java/org/kframework/utils/StringUtil.java#L561-L579

llvm-backend decode_kore does codes[code] on a missing key and emits a NUL byte per chunk:

https://github.com/runtimeverification/llvm-backend/blob/7ca095a55430e587a444c4dbdbc96ab3ee9d4933/lib/ast/AST.cpp#L30-L85

The haskell-backend never decodes names and is unaffected.

Side issues

decodeKoreString uses the default table, so it would also miss the KORE overrides And-, -LT-, -GT-, -AT-, Xor- if ever applied to a symbol name:

https://github.com/runtimeverification/k/blob/4a46d1231473b599c699160132fd6e76a5c46406/k-frontend/src/main/java/org/kframework/utils/StringUtil.java#L569

llvm-backend maps SCln to 'l' instead of ';':

https://github.com/runtimeverification/llvm-backend/blob/7ca095a55430e587a444c4dbdbc96ab3ee9d4933/lib/ast/AST.cpp#L50

Expected

  • munge produces the same encoding as ModuleToKORE (per UTF-16 code unit, %04x).
  • Decoders recognise a [0-9a-f]{4} chunk and convert it back to a code unit, recombining surrogate pairs where the host string type is not UTF-16, or fail loudly instead of producing null/NUL.
Ngôn ngữ chính
Python
Star
600
Fork
164
Không có pull request nào được merge trong 30 ngày

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 runtimeverification/k

Tất cả issue của runtimeverification/k

Issue tương tự

Thêm issue về Python

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.