[K-Bug] The LLVM backend ignores rule priorities
まだ誰も着手していません。
評価
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 初心者へのやさしさ
- 35/100
- issue の種類
- バグ
- 明瞭さ
- おおむね明確
- 活発さ
- 停滞
- 技術スタック
- linux
- 領域
- compilers
調査の方向性
Start with the minimal definition in a.k and input in a.in, then run kompile followed by krun to reproduce the LLVM backend result. Compare the priority and requires cases described in the issue; done means both produce b rather than c and neither enters an infinite loop.
索引モデルが issue の本文から書いたものです。
説明
What component is the issue in?
llvm-backend
Which command
- kompile
- kast
- krun
- kprove
- kprovex
- ksearch
What K Version?
v7.1.164-0-g459fdd7b84
Operating System
Linux
K Definitions (If Possible)
a.k:
module A
imports K-EQUAL-SYNTAX
syntax Stuff ::= "a" | "b" | "c"
rule A:Stuff => b requires A ==K a [priority(10)]
rule a => c
endmodule
Steps to Reproduce
use this a.in file:
a
Then, kompile a.k && krun a.in produces
<k>
c ~> .K
</k>
This is wrong, it should have produced b instead of c.
A few more notes:
Commenting out rule a => c produces b as a result. Removing the requires clause from rule A:Stuff => b requires A ==K a makes the backend enter an infinite loop. Replacing the same rule with rule a => b, while keeping the priority produces the expected result.
Expected Results
The command above should have produced this (both in the main case described above and in the infinite loop one):
<k>
b ~> .K
</k>
- 主要言語
- Python
- スター
- 591
- フォーク
- 163
- PR マージ指標
- 30日以内にマージされた PR はありません
環境構築
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
runtimeverification/k のほかの issue
-
Introduce composable symbolic execution interface in pyx再び着手できるかも @Stevengre が 98 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン
runtimeverification/k#4939 · 担当者 1 名 ·
-
Concolic Explorerオープン
難易度 5/5 1週間以上 初心者へのやさしさ 32/100
runtimeverification/k#4937 ·
-
難易度 5/5 1週間以上 初心者へのやさしさ 30/100
runtimeverification/k#4936 ·
-
Accelerating all-path reachability proofs with one-path reachability proofs再び着手できるかも @Stevengre が 104 日前に担当しましたが、オープン中のプルリクエストはありません。 オープンtype:epic
runtimeverification/k#4934 · コメント 4 件 · 担当者 1 名 ·
-
Support progressive depth halving as a generic policy in `Prover.advance_proof`再び着手できるかも @Stevengre が 123 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン
runtimeverification/k#4924 · 担当者 1 名 ·
runtimeverification/k の issue をすべて見る
似ている issue
-
namespace operations
難易度 1/5 1時間未満 初心者へのやさしさ 82/100
EclipseFdn/open-vsx.org#13573 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
collective/icalendar#1854 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
rancher/rancher-ai-agent#412 ·
メンテナーはふだん 6 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 84/100
TUDelftGeodesy/DePSI#134 ·
-
難易度 2/5 1〜3時間 初心者へのやさしさ 88/100
HenriquesLab/rxiv-maker#335 ·