Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

Non-ASCII characters in symbol names

Aperta
  • Qualcosa non va?
#4,941 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
3/5
Tempo stimato
Mezza giornata
Idoneità per principianti
75/100
Tipo di issue
Bug
Chiarezza
Specificata chiaramente
Stato di attività
Attiva
Stack tecnologico
java, python, scala
Ambito
backend

Direzione di ricerca

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.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

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.
Lingua principale
Python
Stelle
596
Fork
164
Nessuna PR unita negli ultimi 30g

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di runtimeverification/k

Tutte le issue di runtimeverification/k

Issue simili

Altre issue su Python

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.