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

[K-Improvement] Metadata attribute

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

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
5/5
Tempo stimato
Più di una settimana
Idoneità per principianti
35/100
Tipo di issue
Funzionalità
Chiarezza
Abbastanza chiara
Stato di attività
Ferma
Ambito
compilers

Direzione di ricerca

Start by locating the K grammar's existing attribute handling and the parser or example-file tests; no specific paths are named in the issue. The work is done when metadata is accepted in every attribute context, valid key-value pairs and escaped strings parse, duplicate keys are rejected, and metadata is passed through generated output as described.

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

Descrizione

Motivation

Sometimes, K files are consumed programmatically (e.g. via pyk), but currently, there are only limited ways to pass additional contextual information to such tools.

Here I propose that a new metadata attribute be added to the grammar which is accepted wherever attributes are allowed to appear.

Example K Code

I have several possible syntax variations we could consider. Each variation would parse a bit differently and would give the metadata attribute different structure.

Of the options below, my preference is that metadata would have an implicit key-value structure, since I don't think it would be significantly more difficult than the other options but it would much nicer if K-based tooling needed to store multiple bits of metadata about a single K syntactic item.

Basic String Syntax

In this variation, the value of a metadata attribute is a string.

module MODULE [meta("module metadata")]
  imports INT
  syntax Foo ::= Foo(Int)
               | foo(Int) [function, meta("production metadata")]
  rule foo(5) => Foo(5 -Int 2) [meta("rule metadata")]
endmodule
String Syntax with Repeats

In this variation, the value of a metadata attribute is a string set.

module MODULE [meta("module metadata"), meta("module metadata 2")]
  imports INT
  syntax Foo ::= Foo(Int)
               | foo(Int) [function, meta("production metadata"), meta("production metadata 2")]
  rule foo(5) => Foo(5 -Int 2) [meta("rule metadata"), meta("rule metadata 2")]
endmodule
String Syntax with Key-Value Structure

In this variation, the value of a metadata attribute is a string->string map.

There would also be additional requirements:

  1. it would be an error to map the same key for the same metadata attribute group twice to different values --- this also includes when a piece of syntax is redeclared with different metadata (if that is possible)
  2. keys would have a very limited syntactic structure to ease parsing (presumably no spaces, starts with letter, alphanumerics, maybe underscore/dash --- and that's it)
module MODULE [meta(key1="module metadata", key2="module metadata 2")]
  imports INT
  syntax Foo ::= Foo(Int)
               | foo(Int) [function, meta(key2="production metadata",)]
  rule foo(5) => Foo(5 -Int 2) [meta(key3="rule metadata")]
endmodule
Non-String Syntax

All of the above syntaxes could be changed to not use string syntax and to have some other delimiter mechanism. However, I think that strings are probably the most natural since they are already supported by the tokenizer.

Documentation

K supports metadata attributes in all context where attributes are allowed to appear. The purpose of these attributes is to annotate certain parts of a K specification so that other tools which programmatically consume K specifications may read --- K itself does not examine these attributes except to pass them through to generated output files during compilation.

An example metadata attribute is as follows:

rule foo => bar [meta(phase="runtime", type="local")]

In this case, the K compiler, when generating code for this rule, will note that it has two key-value pairs in its metadata as specified above.

The syntax for these key-value pairs is as follows:

  • keys: metadata attribute keys must start with a letter, followed by any number of ASCII letters, numbers, and underscores;
  • values: metadata attribute values must be string tokens with any nested double quotes or special characters properly escaped;
  • it is an error to specify the same key twice with separate values.

Potential Alternatives/Workarounds

Currently, the K grammar allows for symbol and group attributes to be set by the user --- these can be (ab)used to encode metadata --- but the process is somewhat hacky.

Testing Approach

Example files could be created with all possible metadata attribute styles in all possible contexts to ensure that they parse correctly.

Invalid metadata attribute examples could also be created to ensure that the parser can reject them.

Lingua principale
Python
Stelle
591
Fork
163
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.