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

[K-Improvement] Metadata attribute

Đang mở
  • Có gì không ổn?
#4,568 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ó
5/5
Thời gian dự kiến
Hơn một tuần
Mức phù hợp với người mới
35/100
Loại issue
Tính năng
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Đình trệ
Lĩnh vực
compilers

Hướng nghiên cứu

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.

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

Mô tả

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.

Ngôn ngữ chính
Python
Star
591
Fork
163
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.