Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

Non-ASCII characters in symbol names

Abierto
  • ¿Algo no está bien?
#4,941 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
3/5
Tiempo estimado
Medio día
Aptitud para principiantes
75/100
Tipo de issue
Error
Claridad
Bien especificado
Estado de actividad
Activo
Stack tecnológico
java, python, scala
Área
backend

Línea de trabajo

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.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

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.
Lenguaje dominante
Python
Estrellas
596
Forks
164
Sin PR fusionados en 30 d

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de runtimeverification/k

Todos los issues de runtimeverification/k

Issues similares

Más issues de Python

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.