[K-Bug] LLVM Backend crash when comparing MInt
@dwightguth がすでに取り組んでいます。
2025年3月3日 から。
評価
この issue はまだ評価されていません。
説明
What component is the issue in?
llvm-backend
Which command
- kompile
- kast
- krun
- kprove
- kprovex
- ksearch
What K Version?
v7.1.217-0-gf236685fdd
Operating System
Linux
K Definitions (If Possible)
module A
imports BOOL
imports INT
imports K-EQUAL-SYNTAX
imports MINT
syntax MInt{8}
syntax KItem ::= "a" | b(MInt{8}, MInt{8}) | c(Bool)
rule a => b(Int2MInt(2), Int2MInt(2))
rule b(X, Y) => c(X ==K Y)
endmodule
Steps to Reproduce
kompile a.k
echo "a" >> a.in
krun a.in
This crashes with
.../lib/kframework/k-util.sh: line 114: 399174 Aborted (core dumped) "$@"
[Error] krun: ./a-kompiled/interpreter
GDB has this in the stack trace:
#4 0x00007ffff70287f3 in __GI_abort () at ./stdlib/abort.c:79
#5 0x0000555555683f4e in hook_KEQUAL_eq (arg1=0x7e00000001a8, arg2=0x7e00000001d0)
at /mnt/data/runtime-verification/k/llvm-backend/src/main/native/llvm-backend/runtime/collections/kelemle.cpp:161
#6 0x0000555555683eb9 in hook_KEQUAL_eq (arg1=0x7e00000001b8, arg2=0x7e00000001e0)
at /mnt/data/runtime-verification/k/llvm-backend/src/main/native/llvm-backend/runtime/collections/kelemle.cpp:112
#7 0x00005555555c5972 in k_step ()
This is the code that seems to be crashing:
https://github.com/runtimeverification/llvm-backend/blob/4203a45110504a6661ca086816e28dafa9e7ac54/runtime/collections/kelemle.cpp#L156-L166
Expected Results
Not crashing. The <k> cell should contain c(true).
- 主要言語
- 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 が 124 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン
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 ·